Compositional Verification for Timed Systems Based on Automatic Invariant Generation
| Autor: | Marius Bozga, Souha Ben Rayana, Jacques Combaz, Lacramioara Astefanoaei, Saddek Bensalem |
|---|---|
| Přispěvatelé: | VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF) |
| Jazyk: | angličtina |
| Rok vydání: | 2015 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science General Computer Science Computer science 0102 computer and information sciences 02 engineering and technology 01 natural sciences Logic in Computer Science (cs.LO) Theoretical Computer Science 010201 computation theory & mathematics 0202 electrical engineering electronic engineering information engineering [INFO.INFO-ES]Computer Science [cs]/Embedded Systems 020201 artificial intelligence & image processing Invariant (mathematics) Algorithm |
| Zdroj: | Logical Methods in Computer Science Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2015, 11 (3), ⟨10.2168/LMCS-11(3:15)2015⟩ |
| ISSN: | 1860-5974 |
| DOI: | 10.2168/LMCS-11(3:15)2015⟩ |
| Popis: | International audience; 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 synchroni-sations between components. The method has been implemented in the RTD-Finder tool and successfully experimented on several benchmarks. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|