KIT | KIT-Bibliothek | Impressum | Datenschutz

A case study on different modelling approaches based on model checking - verifying numerous versions of the alternating bit protocol with SMV

Biere, Armin; Kick, Alexander


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.

Volltext §
DOI: 10.5445/IR/30695
Cover der Publikation
Zugehörige Institution(en) am KIT Fakultät für Informatik – Informatik für Ingenieure und Naturwissenschaftler (Inf. für Ing. u. Naturwiss.)
Fakultät für Informatik – Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Publikationstyp Buch
Publikationsjahr 1995
Sprache Englisch
Identifikator urn:nbn:de:swb:90-AAA306957
KITopen-ID: 30695
Erscheinungsvermerk Karlsruhe 1995. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1995,5.)
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page