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 条

[1] Parameterized verification of π-calculus systems
Yang, Ping
Basu, Samik
Ramakrishnan, C. R.
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2006, 3920 : 42 - 57
[2] Verification of parameterized timed systems
Abdulla, PA
FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, 2005, 3829 : 95 - 97
[3] Compositional analysis for verification of parameterized systems
Basu, S
Ramakrishnan, CR
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2003, 2619 : 315 - 330
[4] Compositional analysis for verification of parameterized systems
Basu, S
Ramakrishnan, CR
THEORETICAL COMPUTER SCIENCE, 2006, 354 (02) : 211 - 229
[5] Automatic abstraction for verification of parameterized systems
Zhang, Long
Qu, Wanxia
Guo, Yang
Li, Sikun
Jisuanji Fuzhu Sheji Yu Tuxingxue Xuebao/Journal of Computer-Aided Design and Computer Graphics, 2014, 26 (06): : 991 - 998
[6] Parameterized Verification of Systems with Global Synchronization and Guards
Jaber, Nouraldin
Jacobs, Swen
Wagner, Christopher
Kulkarni, Milind
Samanta, Roopsha
COMPUTER AIDED VERIFICATION (CAV 2020), PT I, 2020, 12224 : 299 - 323
[7] Universal properties verification of parameterized parallel systems
Nugraheni, CE
COMPUTATIONAL SCIENCE AND ITS APPLICATIONS - ICCSA 2005, PT 3, 2005, 3482 : 453 - 462
[8] Incremental Inductive Verification of Parameterized Timed Systems
Isenberg, Tobias
2015 15TH INTERNATIONAL CONFERENCE ON APPLICATIONS OF CONCURRENCY TO SYSTEM DESIGN (ACSD), 2015, : 1 - 9
[9] An approach to the verification of symmetric parameterized distributed systems
Konnov, IV
Zakharov, VA
PROGRAMMING AND COMPUTER SOFTWARE, 2005, 31 (05) : 225 - 236
[10] Incremental Inductive Verification of Parameterized Timed Systems
Isenberg, Tobias
ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2017, 16 (02)

← 1 2 3 4 5 →