COMPOSITIONAL VERIFICATION FOR TIMED SYSTEMS BASED ON AUTOMATIC INVARIANT GENERATION

被引：3

作者：

Ben Rayana, Souha ^{[1
]}

Astefanoaei, Lacramioara ^{[1
]}

Bensalem, Saddek ^{[1
,2
]}

Bozga, Marius ^{[1
,2
]}

Combaz, Jacques

机构：

[1] Univ Grenoble Alpes, VERIMAG, F-38000 Grenoble, France

[2] CNRS, VERIMAG, F-38000 Grenoble, France

来源：

LOGICAL METHODS IN COMPUTER SCIENCE | 2015年 / 11卷 / 03期

关键词：

compositional verification; timed automata; invariants; component invariants; interaction invariants; interactions;

D O I：

10.2168/LMCS-11(3:15)2015

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页数：27