This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Programming and Verifying Real-Time Systems by Means of the Synchronous Data-Flow Language LUSTRE
September 1992 (vol. 18 no. 9)
pp. 785-793

The benefits of using a synchronous data-flow language for programming critical real-time systems are investigated. These benefits concern ergonomy (since the dataflow approach meets traditional description tools used in this domain) and ability to support formal design and verification methods. It is shown, using a simple example, how the language LUSTRE and its associated verification tool LESAR, can be used to design a program, to specify its critical properties, and to verify these properties. As the language LUSTRE and its uses have already been discussed in several papers, emphasis is put on program verification.

[1] R. Alur, C. Courcoubetis, and D. Dill, "Model-checking for real-time systems," inProc. 5th Annual IEEE Symp. Logic in Computer Science, pp. 414-425, 1990.
[2] E. A. Ashcroft and W. W. Wadge,Lucid, the data-flow programming language. New York: Academic Press, 1985.
[3] A. Benveniste and G. Berry, "The synchronous approach to reactive and real-time systems,"Proc. IEEE, vol. 79, pp. 1270-1282, Sept. 1991.
[4] G. Berry, "Real time programming: Special purpose or general purpose languages," inIFIP World Computer Congress, 1989.
[5] G. Berry,et al., "Synchronous programming of reactive systems, an introduction to Esterel," in K. Fuchi and M. Nivat, Eds.,Programming of Future Generation Computers. North Holland: Elsevier, 1988, pp. 35-55.
[6] G. Berry and G. Gonthier, "The synchronous programming language Esterel, design, semantics, implementation,"Tech. Rep. 842, INRIA, 1988, (to appear in Science of Computer Programming).
[7] A. Bouajjani, J. C. Fernandez, and N. Halbwachs, "On the verification of safety properties,"Tech. Rep., SPECTRE L12, IMAG, Grenoble, Mar. 1990.
[8] F. Boussinot and R. de Simone, "The Esterel language,"Proceedings IEEE, vol. 79, pp. 1293-1304, Sept. 1991.
[9] R. E. Bryant, "Graph-based algorithms for Boolean function manipulation,"IEEE Trans. Comput., vol. C-35, no. 8, pp. 677-691, Aug. 1986.
[10] J. R. Burchet al., "Symbolic model checking: 1020states and beyond," technical report, Carnegie Mellon University, 1989.
[11] P. Caspi, D. Pilaud, N. Halbwachs, and J. Plaice, LUSTRE: A declarative language for programming synchronous systems," in14th ACM Symposium on Principles of Programming Languages, Jan. 1987.
[12] E. M. Clarke, E. A. Emerson, and A. P. Sistla, "Automatic verification of finite-state concurrent systems using temporal logic,"ACM Trans. Program. Lang. Syst., vol. 8, no. 2, pp. 244-263, Apr. 1986.
[13] E. M. Clarke, D. E. Long, and K. L. McMillan, "A language for compositional specification and verification of finite state hardware controllers,"Proc. IEEE, vol. 79, pp. 1283-1292, Sept. 1991.
[14] O. Coudert, C. Berthet, and J. C. Madre, "Verification of synchronous sequential machines based on symbolic execution," inInternational Workshop on Automatic Verification Methods for Finite State Systems, LNCS 407. New York: Springer Verlag, 1989.
[15] O. Coudert, J. C. Madre, and C. Berthet, "Verifying temporal properties of sequential machines without building their state diagrams." inInt. Workshop on Computer-Aided Verification, June 1990.
[16] D. L. Dill, "Timing assumptions and verification of finite state concurrent systems," inWorkshop on Automatic Verification Methods for Finite State Systems, LNCS 407. New York: Springer Verlag, June 1989.
[17] A. C. Glory, "Vérification de propriétés de programmes flots de données synchrones," dissertation, UniversitéJoseph Fourier, Grenoble, Dec. 1989.
[18] N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, "The synchronous dataflow programming language LUSTRE,"Proc. IEEE, vol. 79, pp. 1305-1320, Sept. 1991.
[19] N. Halbwachs and F. Lagnier, "An experience in proving regular networks of processes by modular model checking,"Tech. Rep. SPECTREL13 (to appear in Acta Informatica), IMAG, Grenoble, Mar. 1990.
[20] N. Halbwachs, P. Raymond, and C. Ratel, "Generating efficient code from data-flow programs, " inThird Int. Symp. Programming Language Implementation and Logic Programming, Passau, Aug. 1991.
[21] D. Harel, "Statecharts: A visual formalism for complex systems,"Sci. Comput. Program., vol. 8, pp. 231-274, 1987.
[22] G. J. Holzmann, "On limits and possibilities of automated protocols analysis," inIFIP WC-6.1 7th Int. Conf. Protocol Specification, Testing and Verification. North Holland, 1987.
[23] G. Kahn, "The semantics of a simple language for parallel programming," inIFIP 74. North Holland, 1974.
[24] P. LeGuernic, T. Gautier, M. LeBorgne, and C. LeMaire, "Programming real time applications with Signal,"Proc. IEEE, vol. 79, pp. 1321-1336, Sept. 1991.
[25] O. Lichtenstein, A. Pnueli, and L. Zuck, "The glory of the past," inConf. Logics of Programs, LNCS 194. Springer Verlag, 1985.
[26] J. S. Ostroff, "Automated verification of timed transition systems," inWorkshop on Automatic Verification Methods for Finite State Systems, LNCS 407. Springer Verlag, June 1989.
[27] J. P. Queille and J. Sifakis, "Specification and verification of concurrent systems in Cesar," inInt. Symp. Programming, LNCS 137. Springer Verlag, Apr. 1982.
[28] C. Ratel, N. Halbwachs, and P. Raymond, "Programming and verifying critical systems by means of the synchronous data-flow programming language lustre," inACM-SIGSOFT'91 Conf. Software for Critical Systems, Dec. 1991.
[29] J. L. Richier, C. Rodriguez, J. Sifakis, and J. Voiron, "Verification in xesar of the sliding window protocol, " inIFIP WG-6.1 7th Int. Conf. Protocol Specification, Testing and Verification. North Holland, 1987.

Index Terms:
data-flow language LUSTRE; synchronous data-flow language; critical real-time systems; ergonomy; dataflow approach; traditional description tools; formal design; verification methods; verification tool LESAR; critical properties; program verification; parallel languages; parallel programming; program verification; real-time systems
Citation:
N. Halbwachs, F. Lagnier, C. Ratel, "Programming and Verifying Real-Time Systems by Means of the Synchronous Data-Flow Language LUSTRE," IEEE Transactions on Software Engineering, vol. 18, no. 9, pp. 785-793, Sept. 1992, doi:10.1109/32.159839
Usage of this product signifies your acceptance of the Terms of Use.