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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Harel D, Pnueli A. On the development of reactive systems. Logics and Models of Concurrent Systems, 1989, F(13): 477–498
Potop-Butucaru D, De Simone R, Talpin J P. The synchronous hypothesis and synchronous languages. The Embedded Systems Handbook, 2005, 1–21
Boussinot F, De Simone R. The esterel language. Proceedings of the IEEE, 1991, 79(9): 1293–1304
Halbwachs N, Caspi P, Raymond P, Pilaud D. The synchronous data-flow programming language lustre. Proceedings of the IEEE, 1991, 79(9): 1305–1320
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
Schneider K. The synchronous programming language quartz. Internal Report, Department of Computer Science, University of Kaiserslautern, Germany, 2010
Teehan P, Greenstreet M, Lemieux G. A survey and taxonomy of gals design styles. IEEE Design and Test of Computers, 2007, 24: 418–428
Benveniste A, Caillaud B, Le Guernic P. From synchrony to asynchrony. In: Proceedings of CONCUR 99. 1999, 162–177
Besnard L, Gautier T, Le Guernic P. SIGNAL V4 Reference Manual, 2010
Gamatié A. Designing Embedded Systems With the SIGNAL Programming Language. Springer, 2010
Le Guernic P, Gautier T. Data-flow to von neumann: the signal approach. Advanced Topics in Data-Flow Computing, 1991, 413–438
Le Guernic P, Talpin J P, Le Lann J C. Polychrony for system design. Journal of Circuits Systems and Computers, 2002, 12: 261–304
Pnueli A, Siegel M, Singerman F. Tanslation validation. In: Proceedings of TACAS’98. 1998, 151–166
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
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
Bertot Y, Casteran P. Interactive theorem proving and program development: Coq art: the calculus of inductive constructions. Springer, 2004
The polychrony toolset. http://www.irisa.fr/espresso/Polychrony
Benveniste A, Le Guernic P, Sorel Y, Sorine M. A denotational theory of synchronous reactive systems. Information and Computation, 1992, 99(2): 192–230
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
Cormen T, Leiserson C, Rivest R, Stein C. Introduction to Algorithms. MIT Press, 2009
Houssais B. The synchronous programming language signal-a tutorial. 2004
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
Benveniste A, Caillaud B, Le Guernic P. Compositionality in dataflow synchronous languages: specification distributed code generation. Information and Computation, 2000, 125–171
Boulmé S, Hamon G. Certifying synchrony for free. In: Proceedings of the Artificial Intelligent on Logic for Progamming (LPAR). 2001, 495–506
Schneider K. Proving the equivalence of microstep and macrostep semantics. LNCS2410, 2002, 314–331
Kerboeuf M, Nowak D, Talpin J P. Formal proof of a polychronous protocol for loosely time-triggerd architectures. In: Proceedings of the 5th International Conference on Formal Engineering Methods, ICFEM 03. 2003, 359–374
Potop-Butucaru D, Caillaud B, Benveniste A. Concurrency in synchronous systems. Formal Methods in System Design, 2006, 111–130
B.A. J. Formal model driven software synthesis for embedded systems. PhD thesis, Virginia Polytechnic Institute and State Univeristy, 2011
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
Author information
Authors and Affiliations
Additional information
Dr. Zhibin Yang received his PhD in Computer Science from Beihang University, China in February 2012. Since April 2012, he has been a Postdoc in IRIT of University of Toulouse, France. His research interests include safetycritical real-time system, formal verification, AADL, synchronous languages.
Dr. Jean-Paul Bodeveix received his PhD of Computer Science from the University of Paris-Sud 11 in 1989. He has been an assistant professor at University of Toulouse III since 1989 and is now a professor of computer science since 2003. His main research interests concern formal specifications, automated and assisted verification of protocols as well as of proof environments. He has participated in European and national projects related to these domains. His current activities are linked to real time modeling and verification either via model checking techniques or at the semantics level.
Dr. Mamoun Filali is a full time researcher at CNRS (Centre National de la Recherche Scientifique). His main research interests concern the certified development of embedded systems. He is concerned by formal methods, model checking, and theorem proving. During the last years, he has been mainly involved in the French Nationwide TOPCASED Project where he was concerned by the verification topic. He has also participated to the proposal of the AADL behavioral annex which has been been adopted as part of the AADL SAE standard.
Rights and permissions
About this article
Cite this article
Yang, Z., Bodeveix, JP. & Filali, M. A comparative study of two formal semantics of the SIGNAL language. Front. Comput. Sci. 7, 673–693 (2013). https://doi.org/10.1007/s11704-013-3908-2
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11704-013-3908-2