Bounded Model Checking of Graph Transformation Systems via SMT Solving

Abstract : Bounded model checking (BMC) complements classical model checking by an efficient technique for checking error-freedom of bounded system paths. Usually, BMC approaches reduce the verification problem to propositional satisfiability. With the recent advances in SAT solving, this has proven to be a fast analysis.In this paper we develop a bounded model checking technique for graph transformation systems. Graph transformation systems (GTSs) provide an intuitive, visual way of specifying system models and their structural changes. An analysis of such models – however – remains difficult since GTSs often give rise to infinite state spaces. In our BMC technique we use first-order instead of propositional logic for encoding complex graph structures and rules. Today’s off-the-shelf SMT solvers can then readily be employed for satisfiability solving. The encoding heavily employs the concept of uninterpreted function symbols for representing edge labels. We have proven soundness of the encoding and report on experiments with different case studies.
Type de document :
Communication dans un congrès
Dirk Beyer; Michele Boreale. 15th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOOODS) / 33th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2013, Florence, Italy. Springer, Lecture Notes in Computer Science, LNCS-7892, pp.178-192, 2013, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-38592-6_13〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01515236
Contributeur : Hal Ifip <>
Soumis le : jeudi 27 avril 2017 - 10:46:43
Dernière modification le : jeudi 26 juillet 2018 - 15:20:05
Document(s) archivé(s) le : vendredi 28 juillet 2017 - 12:47:30

Fichier

978-3-642-38592-6_13_Chapter.p...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Tobias Isenberg, Dominik Steenken, Heike Wehrheim. Bounded Model Checking of Graph Transformation Systems via SMT Solving. Dirk Beyer; Michele Boreale. 15th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOOODS) / 33th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2013, Florence, Italy. Springer, Lecture Notes in Computer Science, LNCS-7892, pp.178-192, 2013, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-38592-6_13〉. 〈hal-01515236〉

Partager

Métriques

Consultations de la notice

62

Téléchargements de fichiers

40