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 条
  • [21] Verification of parameterized systems using logic program transformations
    Roychoudhury, A
    Kumar, KN
    Ramakrishnan, CR
    Ramakrishnan, IV
    Smolka, SA
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2000, 1785 : 172 - 187
  • [22] A Framework for the Verification of Parameterized Infinite-state Systems
    Alberti, Francesco
    Ghilardi, Silvio
    Sharygina, Natasha
    FUNDAMENTA INFORMATICAE, 2017, 150 (01) : 1 - 24
  • [23] Parameterized Verification of Asynchronous Shared-Memory Systems
    Esparza, Javier
    Ganty, Pierre
    Majumdar, Rupak
    JOURNAL OF THE ACM, 2016, 63 (01)
  • [24] Stability verification for monotone systems using homotopy algorithms
    Rueffer, Bjoern S.
    Wirth, Fabian R.
    NUMERICAL ALGORITHMS, 2011, 58 (04) : 529 - 543
  • [25] Stability verification for monotone systems using homotopy algorithms
    Björn S. Rüffer
    Fabian R. Wirth
    Numerical Algorithms, 2011, 58 : 529 - 543
  • [26] Parameterized Verification of Leader/Follower Systems via Arithmetic Constraints
    Kourtis, Georgios
    Dixon, Clare
    Fisher, Michael
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2024, 50 (09) : 2458 - 2471
  • [27] Parameterized verification of graph transformation systems withwhole neighbourhood operations
    Universit`a di Genova, Italy
    不详
    Lect. Notes Comput. Sci., (72-84):
  • [28] Microprocessor Hazard Analysis Via Formal Verification of Parameterized Systems
    Charvat, Lukas
    Smrcka, Ales
    Vojnar, Tomas
    COMPUTER AIDED SYSTEMS THEORY - EUROCAST 2015, 2015, 9520 : 605 - 614
  • [29] Parameterized verification of systems with component identities, using view abstraction
    Lowe, Gavin
    INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2022, 24 (02) : 287 - 324
  • [30] Parameterized verification of systems with component identities, using view abstraction
    Gavin Lowe
    International Journal on Software Tools for Technology Transfer, 2022, 24 : 287 - 324
12345