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 条
  • [31] Unfold/fold transformations for automated verification of parameterized concurrent systems
    Roychoudhury, A
    Ramakrishnan, CR
    PROGRAM DEVELOPMENT IN COMPUTATIONAL LOGIC: A DECADE OF RESEARCH ADVANCES IN LOGIC-BASED PROGRAM DEVELOPMENT, 2004, 3049 : 261 - 290
  • [32] Beyond parameterized verification
    Bozzano, M
    Delzanno, G
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANAYLSIS OF SYSTEMS, PROCEEDINGS, 2002, 2280 : 221 - 235
  • [33] Decidability of parameterized verification
    Bloem, Roderick
    Khalimov, Ayrat
    Jacobs, Swen
    Konnov, Igor
    Veith, Helmut
    Widder, Josef
    Rubin, Sasha
    Synthesis Lectures on Distributed Computing Theory, 2015, 6 (01): : 1 - 170
  • [34] Verification of parameterized protocols
    Baukus, K
    Lakhnech, Y
    Stahl, K
    JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 2001, 7 (02): : 141 - 158
  • [35] Regular model checking without transducers (On efficient verification of parameterized systems)
    Abdulla, Parosh Aziz
    Delzanno, Giorgio
    Ben Henda, Noomene
    Rezine, Ahmed
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2007, 4424 : 721 - +
  • [36] HADES: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems
    Charvat, Lukas
    Smrcka, Ales
    Vojnar, Tomas
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2016, (233): : 87 - 93
  • [37] QUICKSILVER: Modeling and Parameterized Verification for Distributed Agreement-Based Systems
    Jaber, Nouraldin
    Wagner, Christopher
    Jacobs, Swen
    Kulkarni, Milind
    Samanta, Roopsha
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2021, 5 (OOPSLA):
  • [38] Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors
    Charvat, Lukas
    Smrcka, Ales
    Vojnar, Tomas
    2014 15TH INTERNATIONAL MICROPROCESSOR TEST AND VERIFICATION WORKSHOP (MTV 2014), 2015, : 83 - 89
  • [39] Behavioral Automata Composition for Automatic Topology Independent Verification of Parameterized Systems
    Hanna, Youssef
    Basu, Samik
    Rajan, Hridesh
    7TH JOINT MEETING OF THE EUROPEAN SOFTWARE ENGINEERING CONFERENCE AND THE ACM SIGSOFT SYMPOSIUM ON THE FOUNDATIONS OF SOFTWARE ENGINEERING, 2009, : 325 - 334
  • [40] Parameterized Verification of Systems with Precise (0,1)-Counter Abstraction
    Eichler, Paul
    Jacobs, Swen
    Weil-Kennedy, Chana
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2025, PT I, 2025, 15529 : 101 - 124
12345