OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

An Automatic Technique for Checking the Simulation of Timed Systems

Fares, Elie and Bodeveix, Jean-Paul and Filali, Mamoun and Garnacho, Manuel An Automatic Technique for Checking the Simulation of Timed Systems. (2013) In: 11th International Symposium Automated Technology for Verification and Analysis (ATVA 2013), 15 October 2013 - 18 October 2013 (Hanoï, Viet Nam).

(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/978-3-319-02444-8_7


In this paper, we suggest an automatic technique for checking the timed weak simulation between timed transition systems. The technique is an observation-based method in which two timed transition systems are composed with a timed observer. A μ-calculus property that captures the timed weak simulation is then verified on the result of the composition. An interesting feature of the suggested technique is that it only relies on an untimed μ-calculus model-checker without any specific algorithm needed to analyze the result of the composition. We also show that our simulation relation supports interesting results concerning the trace inclusion and the preservation of linear properties. Finally, the technique is validated using the FIACRE/TINA toolset.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to Springer editor. This papers appears in Volume 8172 Lecture Notes in Computer Science ISSN : 0302-9743. ISBN: 978-3-319-02443-1. The original PDF is available at : http://link.springer.com/chapter/10.1007%2F978-3-319-02444-8_7
HAL Id:hal-01226470
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
Deposited On:13 Oct 2015 09:37

Repository Staff Only: item control page