Article: Incremental verification of component-based timed systems Journal: International Journal of Computer Applications in Technology (IJCAT) 2011 Vol.42 No.2/3 pp.159 - 176 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. Inderscience Publishers - linking academia, business and industry through research

Title: Incremental verification of component-based timed systems

Authors: J. Julliand; H. Mountassir; E. Oudot

Addresses: LIFC – Laboratoire d'Informatique de l'Université de Franche-Comté, 16, route de Gray, 25030 Besançon Cedex, France. ' LIFC – Laboratoire d'Informatique de l'Université de Franche-Comté, 16, route de Gray, 25030 Besançon Cedex, France. ' LIFC – Laboratoire d'Informatique de l'Université de Franche-Comté, 16, route de Gray, 25030 Besançon Cedex, France

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.

Keywords: timed tau-simulation; component-based timed systems; incremental development; property preservation; MITL; metic interval temporal logic; incremental verification; modelling; simulation; manufacturing cells.

DOI: 10.1504/IJCAT.2011.045404

International Journal of Computer Applications in Technology, 2011 Vol.42 No.2/3, pp.159 - 176

Published online: 11 Feb 2012 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article

Title: Incremental verification of component-based timed systems

Keep up-to-date