The Electrum Analyzer: Model Checking Relational First-Order Temporal Specifications

被引：24

作者：

Brunel, Julien ^{[1
,2
]}

Chemouil, David ^{[1
,2
]}

Cunha, Alcino ^{[3
,4
]}

Macedo, Nuno ^{[3
,4
]}

机构：

[1] Off Natl Etud & Rech Aerosp, DTIS, Palaiseau, France

[2] Univ Fed Toulouse, Toulouse, France

[3] INESC TEC, Porto, Portugal

[4] Univ Minho, Braga, Portugal

来源：

PROCEEDINGS OF THE 2018 33RD IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMTED SOFTWARE ENGINEERING (ASE' 18) | 2018年

关键词：

Formal specification language; model checking; model validation;

D O I：

10.1145/3238147.3240475

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

This paper presents the Electrum Analyzer, a free-software tool to validate and perform model checking of Electrum specifications. Electrum is an extension of Alloy that enriches its relational logic with LTL operators, thus simplifying the specification of dynamic systems. The Analyzer supports both automatic bounded model checking, with an encoding into SAT, and unbounded model checking, with an encoding into SMV. Instance, or counter-example, traces are presented back to the user in a unified visualizer. Features to speed up model checking are offered, including a decomposed parallel solving strategy and the extraction of symbolic bounds.

引用

页码：884 / 887

页数：4

共 11 条

[1]

[Anonymous], 1993, Symbolic Model Checking

[2]

Brunel Julien, 2018, Abstract State Machines, Alloy, B, TLA, VDM, and Z. 6th International Conference, ABZ 2018. Proceedings: LNCS 10817, P397, DOI 10.1007/978-3-319-91271-4_30

[3]

Cavada R, 2014, LECT NOTES COMPUT SC, V8559, P334, DOI 10.1007/978-3-319-08867-9_22

[4]

Cunha Alcino, 2018, Abstract State Machines, Alloy, B, TLA, VDM, and Z. 6th International Conference, ABZ 2018. Proceedings: LNCS 10817, P307, DOI 10.1007/978-3-319-91271-4_21

[5]

Cunha A, 2014, LECT NOTES COMPUT SC, V8411, P17

[6]

Jackson D, 2012, SOFTWARE ABSTRACTIONS: LOGIC, LANGUAGE, AND ANALYSIS, P1

[7]

Lamport L., 2002, SPECIFYING SYSTEMS T

[8] Exploiting Partial Knowledge for Efficient Model Analysis [J].

Macedo, Nuno ;

Cunha, Alcino ;

Pessoa, Eduardo .

AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS (ATVA 2017), 2017, 10482 :344-362

[9] Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations [J].

Macedo, Nuno ;

Brunel, Julien ;

Chemouil, David ;

Cunha, Alcino ;

Kuperberg, Denis .

FSE'16: PROCEEDINGS OF THE 2016 24TH ACM SIGSOFT INTERNATIONAL SYMPOSIUM ON FOUNDATIONS OF SOFTWARE ENGINEERING, 2016, :373-383

[10] Exploring Scenario Exploration [J].

Macedo, Nuno ;

Cunha, Alcino ;

Guimaraes, Tiago .

FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, FASE 2015, 2015, 9033 :301-315

← 1 2 →