Comparison of Model Checking Tools for Information Systems

被引：0

作者：

Frappier, Marc ^{[1
]}

Fraikin, Benoit ^{[1
]}

Chossart, Romain ^{[1
]}

Chane-Yack-Fa, Raphael ^{[1
]}

Ouenzar, Mohammed ^{[1
]}

机构：

[1] Univ Sherbrooke, GRIL, Quebec City, PQ, Canada

来源：

FORMAL METHODS AND SOFTWARE ENGINEERING | 2010年 / 6447卷

关键词：

VERIFICATION;

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

This paper compares six model checkers (ALLOY, CADP, FDR2, NUSMV, PROB, SPIN) for the validation of information system specifications. The same case study (a library system) is specified using each model checker. Fifteen properties of various types are checked using temporal logics (CTL and LTL), first-order logic and failure-divergence (FDP2). Three characteristics are evaluated: ease of specifying information system i) behavior, ii) properties, and iii) the number of IS entity instances that can be checked. The paper then identifies the most suitable features required to validate information systems using a model checker.

引用

页码：581 / 596

页数：16

共 50 条

[1] Model Checking Information Flow in Reactive Systems
Dimitrova, Rayna
Finkbeiner, Bernd
Kovacs, Mate
Rabe, Markus N.
Seidl, Helmut
[J]. VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, 2012, 7148 : 169 - +
[2] Abstract interpretation and model checking for checking secure information flow in concurrent systems
De Francesco, N
Santone, A
Tesei, L
[J]. FUNDAMENTA INFORMATICAE, 2003, 54 (2-3) : 195 - 211
[3] Role updating in information systems using model checking
Hu, Jinwei
Khan, Khaled M.
Zhang, Yan
Bai, Yun
Li, Ruixuan
[J]. KNOWLEDGE AND INFORMATION SYSTEMS, 2017, 51 (01) : 187 - 234
[4] Role updating in information systems using model checking
Jinwei Hu
Khaled M. Khan
Yan Zhang
Yun Bai
Ruixuan Li
[J]. Knowledge and Information Systems, 2017, 51 : 187 - 234
[5] Comparison of Model Checking Tools Using Timed Automata - PRISM and UPPAAL
Naeem, Aaamir
Azam, Farooque
Amjad, Anam
Anwar, Muhammad Waseem
[J]. 2018 IEEE INTERNATIONAL CONFERENCE ON COMPUTER AND COMMUNICATION ENGINEERING TECHNOLOGY (CCET), 2018, : 248 - 253
[6] Formal analysis of production line systems by probabilistic model checking tools
Ballarini, Paolo
Horvath, Andras
[J]. 2021 26TH IEEE INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION (ETFA), 2021,
[7] Model checking: From tools to theory
Alur, Rajeev
[J]. 25 YEARS OF MODEL CHECKING: HISTORY, ACHIEVEMENTS, PERSPECTIVES, 2008, 5000 : 89 - 106
[8] The Impact of Strategies and Information in Model Checking for Multi-Agent Systems
Malvone, Vadim
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2023, 391 : 63 - 70
[9] Model Checking the Information Flow Security of Real-Time Systems
Gerking, Christopher
Schubert, David
Bodden, Eric
[J]. ENGINEERING SECURE SOFTWARE AND SYSTEMS, ESSOS 2018, 2018, 10953 : 27 - 43
[10] Comparative Analysis of Statistical Model Checking Tools
Bakir, Mehmet Emin
Gheorghe, Marian
Konur, Savas
Stannett, Mike
[J]. MEMBRANE COMPUTING (CMC 2016), 2017, 10105 : 119 - 135

← 1 2 3 4 5 →