Effective Infinite-State Model Checking by Input Equivalence Class Partitioning - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2017

Effective Infinite-State Model Checking by Input Equivalence Class Partitioning

Niklas Krafczyk
  • Fonction : Auteur
  • PersonId : 1026230
Jan Peleska
  • Fonction : Auteur
  • PersonId : 1026233

Résumé

In this paper, it is shown how a complete input equivalence class testing strategy developed by the second author can be effectively used for infinite-state model checking of system models with infinite input domains but finitely many internal state values and finite output domains. This class of systems occurs frequently in the safety-critical domain, where controllers may input conceptually infinite analogue data, but make a finite number of control decisions based on inputs and current internal state. A variant of Kripke Structures is well-suited to provide a behavioural model for this system class. It is shown how the known construction of specific input equivalence classes can be used to abstract the infinite input domain of the reference model into finitely many classes. Then quick checks can be made on the implementation model showing that the implementation is not I/O-equivalent to the reference model if its abstraction to observable minimal finite state machines has a different number of states or a different input partitioning as the reference model. Only if these properties are consistent with the reference model, a detailed equivalence check between the abstracted models needs to be performed. The complete test suites obtained as a by-product of the checking procedure can be used to establish counter examples showing the non-conformity between implementation model and reference model. Using various sample models, it is shown that this approach outperforms model checkers that do not possess this equivalence class generation capability.
Fichier principal
Vignette du fichier
449632_1_En_3_Chapter.pdf (589.08 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-01678956 , version 1 (09-01-2018)

Licence

Paternité

Identifiants

Citer

Niklas Krafczyk, Jan Peleska. Effective Infinite-State Model Checking by Input Equivalence Class Partitioning. 29th IFIP International Conference on Testing Software and Systems (ICTSS), Oct 2017, St. Petersburg, Russia. pp.38-53, ⟨10.1007/978-3-319-67549-7_3⟩. ⟨hal-01678956⟩
167 Consultations
110 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More