Please wait a minute...
Shopping Cart Email List Chinese
Advanced Search Fig/Tab
Frontiers of Computer Science

ISSN 2095-2228

ISSN 2095-2236(Online)

CN 10-1014/TP

Postal Subscription Code 80-970

2018 Impact Factor: 1.129

Featured Articles  |  Most Downloaded  |  Most Reading
Online Submission Subscribe to Our RSS Content Feed
Front Comput Sci    2013, Vol. 7 Issue (5) : 673-693    https://doi.org/10.1007/s11704-013-3908-2
REVIEW ARTICLE
A comparative study of two formal semantics of the SIGNAL language
Zhibin YANG1,2(), Jean-Paul BODEVEIX2(), Mamoun FILALI2()
1. School of Computer Science and Engineering, Beihang University, Beijing 100191, China; 2. IRIT-CNRS, Université de Toulouse, Toulouse 31062, France
 Download: PDF(602 KB)   HTML
 Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks
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     
Corresponding Author(s): YANG Zhibin,Email:Zhibin.Yang@irit.fr; BODEVEIX Jean-Paul,Email:bodeveix@irit.fr; FILALI Mamoun,Email:filali@irit.fr   
Issue Date: 01 October 2013
 Cite this article:   
Zhibin YANG,Jean-Paul BODEVEIX,Mamoun FILALI. A comparative study of two formal semantics of the SIGNAL language[J]. Front Comput Sci, 2013, 7(5): 673-693.
 URL:  
https://academic.hep.com.cn/fcs/EN/10.1007/s11704-013-3908-2
https://academic.hep.com.cn/fcs/EN/Y2013/V7/I5/673
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
doi: 10.1109/5.97299
4 Halbwachs N, Caspi P, Raymond P, Pilaud D. The synchronous dataflow programming language lustre. Proceedings of the IEEE , 1991, 79(9): 1305-1320
doi: 10.1109/5.97300
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
doi: 10.1016/0167-6423(91)90001-E
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
doi: 10.1109/MDT.2007.151
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
doi: 10.1007/978-1-4419-0941-1
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
doi: 10.1142/S0218126603000763
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
doi: 10.1007/BFb0055148
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
doi: 10.1007/3-540-44659-1_22
16 Bertot Y, Casteran P. Interactive theorem proving and program development: Coq art: the calculus of inductive constructions. Springer , 2004
doi: 10.1007/978-3-662-07964-5
17 The polychrony toolset. http://www.irisa.fr/espresso/Polychrony
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
doi: 10.1016/0890-5401(92)90030-J
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
doi: 10.1109/43.736561
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
doi: 10.1145/1376804.1376811
23 Benveniste A, Caillaud B, Le Guernic P. Compositionality in dataflow synchronous languages: specification distributed code generation. Information and Computation , 2000, 125-171
doi: 10.1006/inco.2000.9999
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
doi: 10.1007/s10703-006-7844-8
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
[1] Hao LIN, Guannan LIU, Fengzhi LI, Yuan ZUO. Where to go? Predicting next location in IoT environment[J]. Front. Comput. Sci., 2021, 15(1): 151306-.
[2] Zhibin YANG, Jean-Paul BODEVEIX, Mamoun FILALI. Towards a simple and safe Objective Caml compiling framework for the synchronous language SIGNAL[J]. Front. Comput. Sci., 2019, 13(4): 715-734.
[3] Maoguo GONG, Xiangming JIANG, Hao LI. Optimization methods for regularization-based ill-posed problems: a survey and a multi-objective framework[J]. Front. Comput. Sci., 2017, 11(3): 362-391.
[4] Zhibin YANG,Jean-Paul BODEVEIX,Mamoun FILALI,Kai HU,Yongwang ZHAO,Dianfu MA. Towards a verified compiler prototype for the synchronous language SIGNAL[J]. Front. Comput. Sci., 2016, 10(1): 37-53.
[5] Huafeng YU, Yue MA, Thierry GAUTIER, Lo?c BESNARD, Jean-Pierre TALPIN, Paul Le GUERNIC, Yves SOREL. Exploring system architectures in AADL via Polychrony and SynDEx[J]. Front Comput Sci, 2013, 7(5): 627-649.
[6] Kai HU, Teng ZHANG, Zhibin YANG. Multi-threaded code generation from Signal program to OpenMP[J]. Front Comput Sci, 2013, 7(5): 617-626.
[7] Yongjian ZHAO, Hong HE, Jianxun Mi. Noisy component extraction with reference[J]. Front Comput Sci, 2013, 7(1): 135-144.
[8] Tim SCHLüTER, Stefan CONRAD. An approach for automatic sleep stage scoring and apnea-hypopnea detection[J]. Front Comput Sci, 2012, 6(2): 230-241.
[9] Yongjian ZHAO, Boqiang LIU, Sen WANG. A robust extraction algorithm for biomedical signals from noisy mixtures[J]. Front Comput Sci Chin, 2011, 5(4): 387-394.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed