KIT | KIT-Bibliothek | Impressum | Datenschutz

A verification concept for SDL systems and its application to the Abracadabra protocol

Rinderspacher, Markus


SDL is a specification language to specify distributed systems.
Especially it is suitable for communication protocols. In some
cases however it is not enough to describe just the behaviour of a
protocol, but there are formulated some additional properties as
requirements of the SDL system. A formalism convenient to describe

them is for example first order logic. Our approach is to prove
such properties with methods of automated reasoning after
transforming the SDL specification into a first order logic
specification. The proofs are done with the program verification
system Tatzelwurm, especially with its prover. Practical
experience shows that it is convenient to do a proof in two steps.
In the first step the behaviour of the system is calculated out of
the behaviour of the agents. The proofs of this step is
independent of the property to prove. In this report we give a
proof methods containing instructions how the arguments are
applied during these proofs. It is shown how reachability analysis
is done during a formal proof and how fairness arguments are
applied. The report contains two papers, where the first one
describes the formal basis of the method and shows the proof
... mehr

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