Lacramioara Astefanoaei ; Souha Ben Rayana ; Saddek Bensalem ; Marius Bozga ; Jacques Combaz - Compositional Verification for Timed Systems Based on Automatic Invariant Generation

lmcs:1591 - Logical Methods in Computer Science, September 17, 2015, Volume 11, Issue 3 - https://doi.org/10.2168/LMCS-11(3:15)2015
Compositional Verification for Timed Systems Based on Automatic Invariant GenerationArticle

Authors: Lacramioara Astefanoaei ; Souha Ben Rayana ; Saddek Bensalem ; Marius Bozga ; Jacques Combaz

    We propose a method for compositional verification to address the state space explosion problem inherent to model-checking timed systems with a large number of components. The main challenge is to obtain pertinent global timing constraints from the timings in the components alone. To this end, we make use of auxiliary clocks to automatically generate new invariants which capture the constraints induced by the synchronisations between components. The method has been implemented in the RTD-Finder tool and successfully experimented on several benchmarks.

    https://doi.org/10.2168/LMCS-11(3:15)2015
    Source: arXiv.org:1506.04879
    Volume: Volume 11, Issue 3
    Published on: September 17, 2015
    Submitted on: October 28, 2014
    Keywords: Computer Science - Logic in Computer Science
    Licence: arXiv.org - Non-exclusive license to distribute
    Funding:
      Source : OpenAIRE Graph
    • Autonomic Service-Component Ensembles; Funder: European Commission; Code: 257414
    • CErtification of Real Time Applications desIgNed for mixed criticaliTY; Funder: European Commission; Code: 288175

    5 Documents citing this article

    Share and export

    Consultation statistics

    This page has been seen 1752 times.
    This article's PDF has been downloaded 628 times.