Title: Specification and verification of real-time systems using POLA

 

Author: 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

 

Journal: Int. J. of Critical Computer-Based Systems, 2011 Vol.2, No.3/4, pp.332 - 351

 

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.

 

DOI: http://dx.doi.org/10.1504/IJCCBS.2011.042332

 

Available online 04 Sep 2011

 

 

Editors Full Text AccessAccess for SubscribersPurchase this articleComment on this article