Pardinus: A Temporal Relational Model Finder

被引：6
|
作者：
Macedo, Nuno [1 ,2 ]
Brunel, Julien [3 ,4 ]
Chemouil, David [3 ,4 ]
Cunha, Alcino [5 ,6 ]
机构：
[1] INESC TEC, Porto, Portugal
[2] Univ Porto, Fac Engn, Porto, Portugal
[3] ONERA DTIS, Toulouse, France
[4] Univ Fed Toulouse, Toulouse, France
[5] INESC TEC, Braga, Portugal
[6] Univ Minho, Braga, Portugal
来源：
JOURNAL OF AUTOMATED REASONING | 2022年 / 66卷 / 04期
关键词：
Model checking; Model finding; Relational logic; Temporal logic; CHECKING; ALLOY; LOGIC;
D O I：
10.1007/s10817-022-09642-2
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
This article presents Pardinus, an extension of the popular Kodkod relational model finder with linear temporal logic (including past operators), to simplify the analysis of dynamic systems. Pardinus includes a SAT-based bounded-model checking engine and an SMV-based complete model checking engine, both allowing iteration through the different instances (or counter-examples) of a specification. It also supports a decomposed parallel analysis strategy that improves the efficiency of both analysis engines on commodity multi-core machines.
引用
收藏
页码：861 / 904
页数：44
相关论文
共 50 条
  • [1] Pardinus: A Temporal Relational Model Finder
    Nuno Macedo
    Julien Brunel
    David Chemouil
    Alcino Cunha
    [J]. Journal of Automated Reasoning, 2022, 66 : 861 - 904
  • [2] Verifying Temporal Relational Models with Pardinus
    Macedo, Nuno
    Brunel, Julien
    Chemouil, David
    Cunha, Alcino
    [J]. RIGOROUS STATE-BASED METHODS, ABZ 2023, 2023, 14010 : 254 - 261
  • [3] Kodkod: A relational model finder
    Tortak, Emina
    Jackson, Daniel
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2007, 4424 : 632 - +
  • [4] Staged Evaluation of Partial Instances in a Relational Model Finder
    Montaghami, Vajih
    Rayside, Derek
    [J]. ABSTRACT STATE MACHINES, ALLOY, B, TLA, VDM, AND Z, ABZ 2014, 2014, 8477 : 318 - 323
  • [5] Temporal relational data model
    Tansel, AU
    [J]. IEEE TRANSACTIONS ON KNOWLEDGE AND DATA ENGINEERING, 1997, 9 (03) : 464 - 479
  • [6] A TEMPORAL RELATIONAL MODEL AND A QUERY LANGUAGE
    NAVATHE, SB
    AHMED, R
    [J]. INFORMATION SCIENCES, 1989, 49 (1-3) : 147 - 175
  • [7] Temporal relational and object relational application development using the TORM model
    Pornphol, P
    Chittayasothorn, S
    [J]. 8TH WORLD MULTI-CONFERENCE ON SYSTEMICS, CYBERNETICS AND INFORMATICS, VOL I, PROCEEDINGS: INFORMATION SYSTEMS, TECHNOLOGIES AND APPLICATIONS, 2004, : 20 - 25
  • [8] THE REPRESENTATION OF A TEMPORAL DATA MODEL IN THE RELATIONAL ENVIRONMENT
    SEGEV, A
    SHOSHANI, A
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1989, 339 : 39 - 61
  • [9] CME: A temporal relational model for efficient coalescing
    Al-Kateb, M
    Mansour, E
    El-Sharkawi, ME
    [J]. 12th International Symposium on Temporal Representation and Reasoning, Proceedings, 2005, : 83 - 90
  • [10] Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
    Blanchette, Jasmin Christian
    Nipkow, Tobias
    [J]. INTERACTIVE THEOREM PROVING, PROCEEDINGS, 2010, 6172 : 131 - 146
12345