Array Iterators in Lustre: From a Language Extension to Its Exploitation in Validation
- PDF / 714,486 Bytes
- 16 Pages / 600.032 x 792 pts Page_size
- 95 Downloads / 186 Views
Research Article Array Iterators in Lustre: From a Language Extension to Its Exploitation in Validation Lionel Morel IRISA-INRIA, Campus Universitaire de Beaulieu, 35042 Rennes Cedex, France Received 29 June 2006; Revised 27 November 2006; Accepted 18 December 2006 Recommended by Jean-Pierre Talpin The design of safety critical embedded systems has become a complex task, which requires both appropriate language features and efficient validation techniques. In this work, we propose the introduction of array iterators to the synchronous dataflow language Lustre as a mean to alleviate this complexity. We propose these new operators to provide Lustre programmers with a new mean for designing regular reactive systems. We study a compilation scheme that allows us to generate efficient loop imperative code from these iterators. This language aspect of our work has been fruitful since the iterators are being introduced in the industrial version of Lustre. Finally, we propose to take these regular structures into account during the validation process. This approach has already shown its applicability on different real-life case studies. The work we relate here is thus complete in the sense that our propositions at the language level are taken into account both at the compilation and the validation levels. Copyright © 2007 Lionel Morel. This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
1.
INTRODUCTION
1.1. Reactive systems and the synchronous approach Reactive systems, as defined in [1], are characterized by the interaction with their environment being the prominent aspect of their behavior. Software embedded in aircraft, nuclear plants, and similar physical environments, is a typical example. Moreover, they interact with a noncollaborative environment, which may impose its own rhythm: it does not wait, nor reissue events. Synchronous languages [2] represent an important contribution to the programming of reactive systems. They are all based on the perfect synchrony hypothesis that establishes that communications between different components of a system are instantaneous and, more importantly, that computations performed by components are seen as instantaneous from their environment’s point of view. Among these languages, the most significant ones are Esterel [3], Lustre [4], and Signal [5]. These languages offer a strong formal semantics and associated validation tools. They are now commonly used in highly critical industry for the design of control systems in avionics, nuclear power plants, and so forth.
1.2.
Lustre: the language and associated verification tools
The language In this work, we are more particularly interested in the language Lustre. It is dataflow in the sense that every variable X represents an infinite flow of values (X1 , X2 , . . . , Xi , . . .), Xi being the value taken by X at the ith instant of the execution of the program. Classical opera
Data Loading...
