Compositional verification for timed systems based on automatic invariant generation

DOI10.2168/LMCS-11(3:15)2015zbMATH Open1448.68216arXiv1506.04879OpenAlexW3106343240MaRDI QIDQ3196346FDOQ3196346

Authors: Lăcrămioara Aştefănoaei, Souha Ben Rayana, Saddek Bensalem, Marius Bozga, Jacques Combaz 

Publication date: 29 October 2015

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Abstract: 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.

Full work available at URL: https://arxiv.org/abs/1506.04879

Recommendations

• scientific article; zbMATH DE number 1696495
• An alternative definition for timed automata composition
• A compositional approach to the verification of hybrid systems
• Automatic verification of concurrent systems using a formula-based compositional approach
• scientific article; zbMATH DE number 2080038

zbMATH Keywords

interactionsinvariantscompositional verificationtimed automatacomponent invariantsinteraction invariants

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Distributed systems (68M14)

Cited In (8)

• Constraint-based algorithm for computing temporal invariants
• “ReLIC: Reduced Logic Inference for Composition” for Quantifier Elimination based Compositional Reasoning
• Safe decomposition of startup requirements: verification and synthesis
• Title not available (Why is that?)
• Title not available (Why is that?)
• An alternative definition for timed automata composition
• Title not available (Why is that?)
• Learning assumptions for compositional verification of timed automata

Uses Software

• MOCHA

This page was built for publication: Compositional verification for timed systems based on automatic invariant generation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3196346)