Scalable shared memory LTL model checking

被引：13

作者：

Barnat J. ^{[1
]}

Brim L. ^{[1
]}

Ročkai P. ^{[1
]}

机构：

[1] Faculty of Informatics, Masaryk University, Brno

来源：

International Journal on Software Tools for Technology Transfer | 2010年 / 12卷 / 02期

关键词：

Formal verification; LTL model checking; Parallel; Shared memory;

D O I：

10.1007/s10009-010-0136-z

中图分类号：

学科分类号：

摘要：

Recent development in computer hardware has brought more widespread emergence of shared memory, multi-core systems. These architectures offer opportunities to speed up various tasks-model checking and reachability analysis among others. In this paper, we present a design for a parallel shared memory LTL model checker that is based on a distributed memory algorithm. To improve the scalability of our tool, we have devised a number of implementation techniques which we present in this paper. We also report on a number of experiments we conducted to analyse the behaviour of our tool under different conditions using various models. We demonstrate that our tool exhibits significant speedup in comparison with sequential tools, which improves the workflow of verification in general. © Springer-Verlag 2010.

引用

页码：139 / 153

页数：14

共 41 条

[1]

Barnat J., Brim L., Chaloupka J., Parallel breadth-first search LTL model-checking, IEEE International Conference On Automated Software Engineering (ASE'03), pp. 106-115, (2003)

[2]

Barnat J., Brim L., Rockai P., Scalable multi-core LTL model-checkin, Model Checking Software (SPIN'07), Volume 4595 of LNCS, pp. 187-203, (2007)

[3]

Barnat J., Brim L., Rockai P., DiVinE multi-core-a parallel LTL model-checker, Automated Technology For Verification and Analysis (ATVA'08), Volume 5311 of LNCS, pp. 234-239, (2008)

[4]

Barnat J., Brim L., Stribrna J., Distributed LTL model-checking in SPIN, Model Checking Software (SPIN'01), Volume 2057 of LNCS, pp. 200-216, (2001)

[5]

Barnat J., Brim L., Cerna I., Property driven distribution of nested DFS, International Workshop On Verification and Computational Logic (VCL'02), pp. 1-10, (2002)

[6]

Barnat J., Brim L., Cerna I., Cluster-based LTL model checking of large systems, Formal Methods For Components and Objects (FMCO'05), Number 4111 In LNCS, pp. 259-279, (2006)

[7]

Barnat J., Brim L., Cerna I., Moravec P., Rockai P., Simecek P., DiVinE-a tool for distributed verification (Tool Paper), In: Computer Aided Verification (CAV'06), Volume 4144 of LNCS, pp. 278-281, (2006)

[8]

Barnat J., Rockai P., Shared hash tables in parallel model checking, Parallel and Distributed Methods In Verification (PDMC'07), pp. 81-95, (2007)

[9]

Behrmann G., Hune T.S., Vaandrager F.W., Distributed timed model checking-How the search order matters, Computer Aided Verification (CAV'00), Volume 1855 of LNCS, pp. 216-231, (2000)

[10]

Bell A., Haverkort B.R., Sequential and distributed model checking of Petri Net specifications, Int. J. Softw. Tools Technol. Transfer, 7, 1, pp. 43-60, (2005)

← 1 2 3 4 5 →