Parameterized verification of monotone information systems

Raphaël Chane-Yack-Fa; Marc Frappier; Amel Mammar; Alain Finkel

doi:10.1007/s00165-018-0460-8

Parameterized verification of monotone information systems

Raphaël Chane-Yack-Fa
, Marc Frappier
, Amel Mammar
, Alain Finkel

Research output: Contribution to journal › Article › peer-review

Abstract

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.

Original language	English
Pages (from-to)	463-489
Number of pages	27
Journal	Formal Aspects of Computing
Volume	30
Issue number	3-4
DOIs	https://doi.org/10.1007/s00165-018-0460-8
Publication status	Published - 1 Aug 2018

Keywords

Coverability
Information systems
Model checking
Parameterized verification
Process algebra
Well-quasi-ordering
Well-structured transition systems

Access to Document

10.1007/s00165-018-0460-8

Cite this

@article{452d6b17fc1f45378ec6df0f0db95c02,

title = "Parameterized verification of monotone information systems",

abstract = "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.",

keywords = "Coverability, Information systems, Model checking, Parameterized verification, Process algebra, Well-quasi-ordering, Well-structured transition systems",

author = "Rapha{\"e}l Chane-Yack-Fa and Marc Frappier and Amel Mammar and Alain Finkel",

note = "Publisher Copyright: {\textcopyright} 2018, British Computer Society.",

year = "2018",

month = aug,

day = "1",

doi = "10.1007/s00165-018-0460-8",

language = "English",

volume = "30",

pages = "463--489",

journal = "Formal Aspects of Computing",

issn = "0934-5043",

number = "3-4",

}

TY - JOUR

T1 - Parameterized verification of monotone information systems

AU - Chane-Yack-Fa, Raphaël

AU - Frappier, Marc

AU - Mammar, Amel

AU - Finkel, Alain

PY - 2018/8/1

Y1 - 2018/8/1

N2 - 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.

AB - 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.

KW - Coverability

KW - Information systems

KW - Model checking

KW - Parameterized verification

KW - Process algebra

KW - Well-quasi-ordering

KW - Well-structured transition systems

U2 - 10.1007/s00165-018-0460-8

DO - 10.1007/s00165-018-0460-8

M3 - Article

AN - SCOPUS:85050233788

SN - 0934-5043

VL - 30

SP - 463

EP - 489

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

IS - 3-4

ER -

Parameterized verification of monotone information systems

Abstract

Keywords

Access to Document

Fingerprint

Cite this