CEGAR based bounded model checking of discrete time hybrid systems

被引：0

作者：

Mari, Federico ^{[1
]}

Tronci, Enrico ^{[1
]}

机构：

[1] Univ Roma La Sapienza, Dipartimento Informat, Via Salaria 113, I-00198 Rome, Italy

来源：

HYBRID SYSTEMS: COMPUTATION AND CONTROL, PROCEEDINGS | 2007年 / 4416卷

关键词：

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

Many hybrid systems can be conveniently modeled as Piecewise Affine Discrete Time Hybrid Systems PA-DTHS. As well known Bounded Model Checking (BMC) for such systems comes down to solve a Mixed Integer Linear Programming (MILP) feasibility problem. We present a SAT based BMC algorithm for automatic verification of PA-DTHSs. Using Counterexample Guided Abstraction Refinement (CECAR) our algorithm gradually transforms a PA-DTHS verification problem into larger and larger SAT problems. Our experimental results show that our approach can handle PADTHSs that are more then 50 times larger than those that can be handled using a MILP solver.

引用

页码：399 / +

页数：3

共 21 条

[1] Automatic symbolic verification of embedded systems [J].

Alur, R ;

Henzinger, TA ;

Ho, PH .

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1996, 22 (03) :181-201

[2]

AUDERMAND G, 2004, P 2 INT WORKSH BOUND

[3]

BEMPORAD A, 1999, LNCS, V1569

[4]

BIERE A, 1999, LNCS, V1579

[5]

Bozzano M., 2005, LNCS, V3576

[6]

Carter M. W., 2001, OPERATIONS RES PRACT

[7] Bounded model checking using satisfiability solving [J].

Clarke, E ;

Biere, A ;

Raimi, R ;

Zhu, Y .

FORMAL METHODS IN SYSTEM DESIGN, 2001, 19 (01) :7-34

[8]

CLARKE E, 2003, P ASP DAC

[9]

CLARKE EM, 2000, LNCS

[10]

DELLAPENNA G, 2004, INT J SOFTWARE TOOLS, V6

← 1 2 3 →