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

共 50 条

[31] Automatic symbolic compositional verification by learning assumptions
Nam, Wonhong
Madhusudan, P.
Alur, Rajeev
FORMAL METHODS IN SYSTEM DESIGN, 2008, 32 (03) : 207 - 234
[32] Business process automatic verification with a compositional approach
Mendoza Morales, Luis E.
Capel Tunon, Manuel I.
Perez, Maria A.
REVISTA TECNICA DE LA FACULTAD DE INGENIERIA UNIVERSIDAD DEL ZULIA, 2013, 36 (01): : 70 - 79
[33] Specification and verification of timed lazy systems
Corradini, F
Pistore, M
MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 1996, 1996, 1113 : 279 - 290
[34] Modular verification of timed circuits using automatic abstraction
Zheng, H
Mercer, E
Myers, C
IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2003, 22 (09) : 1138 - 1153
[35] Verification of timed systems using POSETs
Belluomini, W
Myers, CJ
COMPUTER AIDED VERIFICATION, 1998, 1427 : 403 - 415
[36] Automatic generation of fast timed simulation models for operating systems in SoC design
Yoo, S
Nicolescu, G
Gauthier, L
Jerraya, AA
DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION, 2002 PROCEEDINGS, 2002, : 620 - 627
[37] Business Process Verification using a Formal Compositional Approach and Timed Automata
Mendoza Morales, Luis E.
PROCEEDINGS OF THE 2013 XXXIX LATIN AMERICAN COMPUTING CONFERENCE (CLEI), 2013,
[38] Learning-Based Compositional Verification for Synchronous Probabilistic Systems
Feng, Lu
Han, Tingting
Kwiatkowska, Marta
Parker, David
AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, 2011, 6996 : 511 - 521
[39] Automatic Testbench Generation for Simulation-based Verification of Safety-critical Systems in UML
Weissnegger, Ralph
Schuss, Markus
Kreiner, Christian
Pistauer, Markus
Roemer, Kay
Steger, Christian
PECCS: PROCEEDINGS OF THE 6TH INTERNATIONAL JOINT CONFERENCE ON PERVASIVE AND EMBEDDED COMPUTING AND COMMUNICATION SYSTEMS, 2016, : 70 - 75
[40] Automatic synthesis of schedulers in timed systems
Krishnan, Padmanabhan
Electronic Notes in Theoretical Computer Science, 2000, 31 : 118 - 131

← 1 2 3 4 5 →