Skip to Main content Skip to Navigation
Conference papers

A contribution to the validation of complex real-time systems

Mohamed Khalgui 1 Xavier Rebeuf 1 Françoise Simonot-Lion 1
1 TRIO - Real time and interoperability
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper deals with the verification of temporal properties on a complex real-time system. We use a sub class of timed automata formalism called Timed Input Output State machine (TIOSM) to model system and properties. In order to verify one property on a system, we applied formerly a method that is based on the synchronous product of the two state machines. If the system and the property are designed thanks to state machines containing cycles, the complexity of the analysis increased. We propose then to transform each strongly connected component of each automata into simple cycles. We show that it is possible to identify matching cycles of the two automata and present a validation algorithm based on the matching cycles.
Keywords : temps réel model-checking real time timed automata timed input output state machines tiosm automates synchronisés modèle vérification
Document type :
Conference papers
Complete list of metadata
https://hal.inria.fr/inria-00108083
Contributor : Publications Loria <>
Submitted on : Thursday, October 19, 2006 - 3:40:50 PM
Last modification on : Friday, February 26, 2021 - 3:28:07 PM

Identifiers

  • HAL Id : inria-00108083, version 1

Collections

CNRS | INRIA | LORIA | UNIV-LORRAINE

Citation

Mohamed Khalgui, Xavier Rebeuf, Françoise Simonot-Lion. A contribution to the validation of complex real-time systems. 2nd International Conference : Sciences of Electronic,Technologies of Information and Telecommunications - SETIT 2004, 2004, Sousse/Tunisie, 8 p. ⟨inria-00108083⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

114

 

Contact                    Legal Notice                    Personal Data