A comparative study of two formal semantics of the SIGNAL language

Abstract

SIGNAL is a part of the synchronous languages family, which are broadly used in the design of safety-critical real-time systems such as avionics, space systems, and nuclear power plants. There exist several semantics for SIGNAL, such as denotational semantics based on traces (called trace semantics), denotational semantics based on tags (called tagged model semantics), operational semantics presented by structural style through an inductive definition of the set of possible transitions, operational semantics defined by synchronous transition systems (STS), etc. However, there is little research about the equivalence between these semantics.

In this work, we would like to prove the equivalence between the trace semantics and the tagged model semantics, to get a determined and precise semantics of the SIGNAL language. These two semantics have several different definitions respectively, we select appropriate ones and mechanize them in the Coq platform, the Coq expressions of the abstract syntax of SIGNAL and the two semantics domains, i.e., the trace model and the tagged model, are also given. The distance between these two semantics discourages a direct proof of equivalence. Instead, we transformthem to an intermediate model, which mixes the features of both the trace semantics and the tagged model semantics. Finally, we get a determined and precise semantics of SIGNAL.

Keywords

synchronous language / SIGNAL / trace semantics / tagged model semantics / semantics equivalence / Coq

References

[1] Harel D, Pnueli A. On the development of reactive systems. Logics and Models of Concurrent Systems, 1989, F(13): 477-498

[2] Potop-Butucaru D, De Simone R, Talpin J P. The synchronous hypothesis and synchronous languages. The Embedded Systems Handbook, 2005, 1-21

[3] Boussinot F, De Simone R. The esterel language. Proceedings of the IEEE, 1991, 79(9): 1293-1304

[4] Halbwachs N, Caspi P, Raymond P, Pilaud D. The synchronous dataflow programming language lustre. Proceedings of the IEEE, 1991, 79(9): 1305-1320

[5] Benveniste A, Le Guernic P, Jacquemot C. Synchronous programming with events and relations: the signal language and its semantics. Science of Computer Programming, 1991, 16: 103-149

[6] Schneider K. The synchronous programming language quartz. Internal Report, Department of Computer Science, University of Kaiserslautern, Germany, 2010

[7] Teehan P, Greenstreet M, Lemieux G. A survey and taxonomy of gals design styles. IEEE Design and Test of Computers, 2007, 24: 418-428

[8] Benveniste A, Caillaud B, Le Guernic P. From synchrony to asynchrony. In: Proceedings of CONCUR 99. 1999, 162-177

[9] Besnard L, Gautier T, Le Guernic P. SIGNAL V4 Reference Manual, 2010

[10] Gamatié A. Designing Embedded Systems With the SIGNAL Programming Language. Springer, 2010

[11] Le Guernic P, Gautier T. Data-flow to von neumann: the signal approach. Advanced Topics in Data-Flow Computing, 1991, 413-438

[12] Le Guernic P, Talpin J P, Le Lann J C. Polychrony for system design. Journal of Circuits Systems and Computers, 2002, 12: 261-304

[13] Pnueli A, Siegel M, Singerman F. Tanslation validation. In: Proceedings of TACAS’98. 1998, 151-166

[14] Nowak D, Beauvais J R, Talpin J P. Co-inductive axiomatization of a synchronous language. In: Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics. 1998, 387-399

[15] Kerboeuf M, Nowak D, Talpin J P. Specification and verification of a stream-boiler with signal-coq. In: Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics. 2000, 356-371

[16] Bertot Y, Casteran P. Interactive theorem proving and program development: Coq art: the calculus of inductive constructions. Springer, 2004

[17] The polychrony toolset.

[18] Benveniste A, Le Guernic P, Sorel Y, Sorine M. A denotational theory of synchronous reactive systems. Information and Computation, 1992, 99(2): 192-230

[19] Lee E A, Sangiovanni-Vincentelli A. A framework for comparing models of computation. IEEE Transactions on Computer-aided Design of Integrated Circuits and Systems, 1998, 17(12): 1217-1229

[20] Cormen T, Leiserson C, Rivest R, Stein C. Introduction to Algorithms. MIT Press, 2009

[21] Houssais B. The synchronous programming language signal-a tutorial. 2004

[22] Benveniste A, Caillaud B, Carloni L P, Caspi P, . Sangiovanni- Vincentelli A L. Composing heterogeneous reactive systems. ACM Transactions on Embedded Computing Systems, 2008, 7(4): 1-36

[23] Benveniste A, Caillaud B, Le Guernic P. Compositionality in dataflow synchronous languages: specification distributed code generation. Information and Computation, 2000, 125-171

[24] Boulmé S, Hamon G. Certifying synchrony for free. In: Proceedings of the Artificial Intelligent on Logic for Progamming (LPAR). 2001, 495-506

[25] Schneider K. Proving the equivalence of microstep and macrostep semantics. LNCS2410, 2002, 314-331

[26] Kerboeuf M, Nowak D, Talpin J P. Formal proof of a polychromous protocol for loosely time-triggerd architectures. In: Proceedings of the 5th International Conference on Formal Engineering Methods, ICFEM 03. 2003, 359-374

[27] Potop-Butucaru D, Caillaud B, Benveniste A. Concurrency in synchronous systems. Formal Methods in System Design, 2006, 111-130

[28] . B. A. J. Formal model driven software synthesis for embedded systems. PhD thesis, Virginia Polytechnic Institute and State Univeristy, 2011

[29] Papailiopoulou V, Potop-Butucaru D, Sorel Y, Simone d R, Besnard L, Talpin J P. From design-time concurrency to effective implementation parallelism: the multi-clock reactive case. In: Proceedings of Electronic System Level Synthesis Conference, 2011, 1-6

RIGHTS & PERMISSIONS

Higher Education Press and Springer-Verlag Berlin Heidelberg