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

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