Multi-Object Checking Counterexamples

Abstract : Model checking has become the most widely used technique for the verification of state based systems. In addition to its automation in checking whether a system model satisfies a specification, model checking provides a counterexample trace if the checking condition does not hold. Such a sequence of states illustrates how the model falsifies the specification. Multi-object checking utilizes model checking as the underlying verification technique for each object so that the verification of a system is only limited by the state space of the largest object. Our contribution proposes an enhancement to multi-object checking -- the automated generation of a global system trace, if a specification in multi-object logic does not hold.
Type de document :
Communication dans un congrès
Stephan Merz and Tobias Nipkow. Automatic Verification of Critical Systems, Sep 2006, Nancy/France, pp.163-167, 2006, Automatic Verification of Critical Systems (AVoCS 2006)
Liste complète des métadonnées

Littérature citée [7 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00091663
Contributeur : Stephan Merz <>
Soumis le : mercredi 6 septembre 2006 - 19:19:10
Dernière modification le : mercredi 6 septembre 2006 - 20:47:35
Document(s) archivé(s) le : lundi 5 avril 2010 - 23:02:29

Fichier

Identifiants

  • HAL Id : inria-00091663, version 1

Collections

Citation

Maik Kollmann, Yuen Man Hon. Multi-Object Checking Counterexamples. Stephan Merz and Tobias Nipkow. Automatic Verification of Critical Systems, Sep 2006, Nancy/France, pp.163-167, 2006, Automatic Verification of Critical Systems (AVoCS 2006). 〈inria-00091663〉

Partager

Métriques

Consultations de la notice

72

Téléchargements de fichiers

188