Formal Software Verification: How Close Are We?

Abstract : Spin and its immediate predecessors were originally designed for the verification of data communication protocols. It didn't take long, though, for us to realize that a data communications protocol is just a special case of a general distributed process system, with asynchronously executing and interacting concurrent processes. This covers both multi-threaded software systems with shared memory, and physically distributed systems, interacting via network channels. The tool tries to provide a generic capability to prove (or as the case may be, to disprove) the correctness of interactions in complex software systems. This means a reliable and easy-to-use method to discover the types of things that are virtually impossible to detect reliably with traditional software test methods, such as race conditions and deadlocks. As initially primarily a research tool, Spin has been remarkably successful, with well over one million downloads since it was first made available by Bell Labs in 1989. But our goal is the development of a tool that is not only grounded in foundational theory, but also usable by all developers of multi-threaded software, not requiring specialized knowledge of formal methods. In this talk we try to answer the question how close we have come to reach these goals, and where especially we are still lacking. We will see that our understanding has changed of what a verification tool can do - and what it should do.
Type de document :
Communication dans un congrès
John Hatcliff; Elena Zucca. Joint 12th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 30th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2010, Amsterdam, Netherlands. Springer, Lecture Notes in Computer Science, LNCS-6117, pp.1, 2010, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-13464-7_1〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01055211
Contributeur : Hal Ifip <>
Soumis le : lundi 11 août 2014 - 17:12:09
Dernière modification le : vendredi 11 août 2017 - 16:16:23
Document(s) archivé(s) le : mercredi 26 novembre 2014 - 22:31:39

Fichier

61170001.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Gerard Holzmann. Formal Software Verification: How Close Are We?. John Hatcliff; Elena Zucca. Joint 12th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 30th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2010, Amsterdam, Netherlands. Springer, Lecture Notes in Computer Science, LNCS-6117, pp.1, 2010, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-13464-7_1〉. 〈hal-01055211〉

Partager

Métriques

Consultations de la notice

123

Téléchargements de fichiers

49