Parameterized verification of monotone information systems

被引：0
|
作者：
Chane-Yack-Fa, Raphael [1 ]
Frappier, Marc [1 ]
Mammar, Amel [2 ]
Finkel, Alain [3 ,4 ]
机构：
[1] Univ Sherbrooke, Fac Sci, Dept Informat, GRIL, Sherbrooke, PQ, Canada
[2] SAMOVAR CNRS, Telecom SudParis, Evry, France
[3] Univ Paris Saclay, CNRS, LSV, Paris, France
[4] Univ Paris Saclay, ENS Paris Saclay, Paris, France
来源：
FORMAL ASPECTS OF COMPUTING | 2018年 / 30卷 / 3-4期
基金：
加拿大自然科学与工程研究理事会;
关键词：
Model checking; Parameterized verification; Process algebra; Well-structured transition systems; Well-quasi-ordering; Coverability; Information systems; INFINITE-STATE SYSTEMS; MODEL CHECKING; PROCESS ALGEBRA; DECIDABILITY; STATECHARTS; CUTOFF;
D O I：
10.1007/s00165-018-0460-8
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
In this paper, we study the information system verification problem as a parameterized verification one. Informations systems are modeled as multi-parameterized systems in a formal language based on the Algebraic State-Transition Diagrams (ASTD) notation. Then, we use the Well Structured Transition Systems (WSTS) theory to solve the coverability problem for an unbounded ASTD state space. Moreover, we define a new framework to prove the effective pred-basis condition of WSTSs, i.e. the computability of a base of predecessors for every states.
引用
收藏
页码：463 / 489
页数：27
相关论文
共 50 条
  • [11] Verification of Parameterized Systems with Combinations of Abstract Domains
    Ghafari, Naghmeh
    Gurfinkel, Arie
    Trefler, Richard
    FORMAL TECHNIQUES FOR DISTRIBUTED SYSTEMS, PROCEEDINGS, 2009, 5522 : 57 - +
  • [12] MONOTONIC ABSTRACTION (ON EFFICIENT VERIFICATION OF PARAMETERIZED SYSTEMS)
    Abdulla, Parosh Aziz
    Delzanno, Giorgio
    Ben Henda, Noomene
    Rezine, Ahmed
    INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, 2009, 20 (05) : 779 - 801
  • [13] An Approach to the Verification of Symmetric Parameterized Distributed Systems
    I. V. Konnov
    V. A. Zakharov
    Programming and Computer Software, 2005, 31 : 225 - 236
  • [14] SMT-Based Verification of Parameterized Systems
    Gurfinkel, Arie
    Shoham, Sharon
    Meshman, Yuri
    FSE'16: PROCEEDINGS OF THE 2016 24TH ACM SIGSOFT INTERNATIONAL SYMPOSIUM ON FOUNDATIONS OF SOFTWARE ENGINEERING, 2016, : 338 - 348
  • [15] On Slicewise Monotone Parameterized Problems and Optimal Proof Systems for TAUT
    Chen, Yijia
    Flurn, Joerg
    COMPUTER SCIENCE LOGIC, 2010, 6247 : 200 - +
  • [16] Efficient Verification for Stochastic Mixed Monotone Systems
    Dutreix, Maxence
    Coogan, Samuel
    2018 9TH ACM/IEEE INTERNATIONAL CONFERENCE ON CYBER-PHYSICAL SYSTEMS (ICCPS 2018), 2018, : 150 - 161
  • [17] Parameterized verification
    Parosh A. Abdulla
    Giorgio Delzanno
    International Journal on Software Tools for Technology Transfer, 2016, 18 : 469 - 473
  • [18] Parameterized verification
    Abdulla, Parosh A.
    Delzanno, Giorgio
    INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2016, 18 (05) : 469 - 473
  • [19] Deductive Verification of Parameterized Embedded Systems Modeled in SystemC
    Tasche, Philip
    Monti, Raul E.
    Drerup, Stefanie Eva
    Blohm, Pauline
    Herber, Paula
    Huisman, Marieke
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2024, PT II, 2024, 14500 : 187 - 209
  • [20] Heuristic symbolic verification of safety properties for parameterized systems
    Yang, Qiu-Song
    Li, Ming-Shu
    Ruan Jian Xue Bao/Journal of Software, 2009, 20 (06): : 1444 - 1456
12345