Incremental verification of component-based timed systems
by J. Julliand; H. Mountassir; E. Oudot
International Journal of Computer Applications in Technology (IJCAT), Vol. 42, No. 2/3, 2011

Abstract: We are interested in the incremental development, by integration of components, of component-based timed systems, and in particular, in the preservation of their properties during such a development process. We model timed components with timed automata. Their composition is achieved with the classic parallel composition operator for timed automata. The specifications of these timed systems are expressed with the timed linear logic Metric Interval Temporal Logic (MITL). To guarantee the preservation of properties during an incremental development process, we propose to use τ-simulation relations, adapted for timed systems. First, we extend the classic notion of τ-simulation with timed aspects. As in the untimed case, this relation, called timed τ-simulation, preserves safety properties. To preserve more properties, in particular liveness ones, we present another relation, called divergence-sensitive and stability-respecting (DS) timed τ-simulation. This last relation preserves all MITL properties (and thus liveness ones), but also strong non-zenoness and deadlock-freedom. Moreover, as we put ourselves in a component-based framework, we study if the relations are appropriate to the use of the composition operator that we consider. For this purpose, we study if the relations are compatible with this operator, and if composability and compositionality hold. These three properties are a way to reduce the cost of the verification of the preservation, or even to get it for free. It results that the timed τ-simulation is appropriate with the classic operator since the properties hold without any assumption. However, this is not the case for the DS timed τ-simulation. We implemented the algorithmic verification of the simulations in a tool called Verification of Simulation for Timed Automata (VeSTA). The structure of the tool was inspired from the one of the OPEN-KRONOS tool. This allows, as additional feature, to connect the models considered in VeSTA to the modules of the verification platform OPEN-CAESAR. We show the interest of our method by applying it on a case study, concerning a production cell example.

Online publication date: Sat, 11-Feb-2012

The full text of this article is only available to individual subscribers or to users at subscribing institutions.

 
Existing subscribers:
Go to Inderscience Online Journals to access the Full Text of this article.

Pay per view:
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.

Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of Computer Applications in Technology (IJCAT):
Login with your Inderscience username and password:

Username:        Password:          Forgotten your password?

Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.

If you still need assistance, please email subs@inderscience.com