OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

A comparative study of two formal semantics of the SIGNAL language

Yang, Zhibin and Bodeveix, Jean-Paul and Filali, Mamoun A comparative study of two formal semantics of the SIGNAL language. (2013) Frontiers of Computer Science, vol. 7 (n° 5). pp. 673-693. ISSN 2095-2228

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: http://dx.doi.org/10.1007/s11704-013-3908-2


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.

Item Type:Article
Additional Information:Thanks to Springer editor. The definitive version is available at http://link.springer.com The original PDF of the article can be found at Frontiers of Computer Science website : http://link.springer.com/article/10.1007%2Fs11704-013-3908-2
HAL Id:hal-01154264
Audience (journal):International peer-reviewed journal
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut National Polytechnique de Toulouse - INPT (FRANCE)
French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Université Paul Sabatier-Toulouse III - UPS (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université de Toulouse I-Sciences Sociales - UT1 (FRANCE)
Laboratory name:
Deposited By: IRIT IRIT
Deposited On:16 Mar 2015 08:32

Repository Staff Only: item control page