Compositional verification for timed systems based on automatic invariant generation

DOI10.2168/LMCS-11(3:15)2015MaRDI QIDQ3196346zbMATH OpenOpenAlexFDO

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)

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

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)

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.

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

Cited in

(8)

• An alternative definition for timed automata composition
• scientific article; zbMATH DE number 1796133 (Why is no real title available?)
• Safe decomposition of startup requirements: verification and synthesis
• scientific article; zbMATH DE number 2080038 (Why is no real title available?)
• scientific article; zbMATH DE number 1444724 (Why is no real title available?)
• Learning assumptions for compositional verification of timed automata
• “ReLIC: Reduced Logic Inference for Composition” for Quantifier Elimination based Compositional Reasoning
• Constraint-based algorithm for computing temporal invariants

Describes a project that uses

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)