Parameterized verification of monotone information systems

Raphael Chane-Yack-Fa (1) , Marc Frappier (1) , Amel Mammar (2, 3, 4) , Alain Finkel (5)

1 UdeS - Département d'informatique [Sherbrooke]
2 METHODES-SAMOVAR - Méthodes et modèles pour les réseaux
3 TSP - INF - Département Informatique
4 CNRS - Centre National de la Recherche Scientifique
5 LSV - Laboratoire Spécification et Vérification [Cachan]

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

Mots clés: Information systems; Well-structured transition systems; Parameterized verification; Process algebra; Model checking; Well-quasi-ordering; Coverability

Domaines: Génie logiciel [cs.SE]

Raphael Chane-Yack-Fa, Marc Frappier, Amel Mammar, Alain Finkel. Parameterized verification of monotone information systems. Formal Aspects of Computing, 2018, 30 (3-4), pp.463 - 489. ⟨10.1007/s00165-018-0460-8⟩. ⟨hal-01847131⟩