Powered by OpenAIRE graph
Found an issue? Give us feedback
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/ International Journa...arrow_drop_down
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
DBLP
Article . 2011
Data sources: DBLP
versions View all 2 versions
addClaim

Incremental verification of component-based timed systems

Authors: Julliand, Jacques; Mountassir, Hassan; Oudot, Emilie;

Incremental verification of component-based timed systems

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.

Country
France
Keywords

[INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], 004

  • BIP!
    Impact byBIP!
    selected citations
    These citations are derived from selected sources.
    This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    0
    popularity
    This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
    Average
    influence
    This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    Average
    impulse
    This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
    Average
Powered by OpenAIRE graph
Found an issue? Give us feedback
selected citations
These citations are derived from selected sources.
This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Citations provided by BIP!
popularity
This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
BIP!Popularity provided by BIP!
influence
This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Influence provided by BIP!
impulse
This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
BIP!Impulse provided by BIP!
0
Average
Average
Average
Green
bronze
Related to Research communities
STARS EU