EVA STAR Trefferanzeige

Volltext Volltext.pdf1.pdf (229 KB)
URN (für Zitat) http://nbn-resolving.org/urn:nbn:de:swb:90-AAA306957
Titel A case study on different modelling approaches based on model checking - verifying numerous versions of the alternating bit protocol with SMV.
Autor Biere, Armin
Kick, Alexander
Institution Fakultät für Informatik (INFORMATIK)
Informatik für Ingenieure und Naturwissenschaftler (Inf. für Ing. u. Naturwiss.)
Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Dokumenttyp Buch
Jahr 1995
Erscheinungsvermerk Karlsruhe 1995. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1995,5.)
Abstract
Recently, outstanding results have been achieved in the formal
verification of concurrent systems by model checking techniques. In
this paper we report our experience with SMV, a symbolic model
verifier, applied to a communication protocol, the alternating bit
protocol. We investigated different approaches of modeling the
alternating bit protocol in SMV. We describe the problems
encountered because of the restrictions of SMV. As a consequence, we
call for a more general language for model checking, which both
overcomes these disadvantages of SMV and enhances the possibility of
optimizations, and more specific input languages on top of it,
easing the application of model checking for the end user.