Authors: Florent Peres, Pierre-Emmanue Hladik, Francois Vernadat
Addresses: Universite de Lille Nord de France, F59000 Lille, IFSTTAR, ESTAS, F59650 Villeneuve d'Ascq, France. ' CNRS, LAAS, 7 avenue du colonel Roche, F-31077 Toulouse, France; Universite de Toulouse, UPS, INSA, INP, INSAE, LAAS, F-31077 Toulouse, France. ' CNRS, LAAS, 7 avenue du colonel Roche, F-31077 Toulouse, France; Universite de Toulouse, UPS, INSA, INP, INSAE, LAAS, F-31077 Toulouse, France
Abstract: Real-time systems are becoming more and more complex, making it hard for the industrial community to actually use experimental tools which are able to resolve some of the specification and verification issues of such systems. This work presents a tool which automatically transforms a domain specific language for the specification of real-time systems into its corresponding time Petri net semantics together with some related logical formulas. Consequently, the validity of the generated formulas are automatically checked with regard to the generated model using the TINA model checking toolbox. Using this automatic tool chain, the users can check the validity of real-time systems without any prerequisite knowledge of how it actually was accomplished.
Keywords: domain specific language; DSL; model checking; real time systems; specification; verification; time Petri nets; semantics.
International Journal of Critical Computer-Based Systems, 2011 Vol.2 No.3/4, pp.332 - 351
Available online: 04 Sep 2011Full-text access for editors Access for subscribers Purchase this article Comment on this article