Design of a Formal Estelle Semantics for Verification

  • AbstractOne main purpose for the use of formal description techniques (FDTs) is formal reasoningand verification. This requires a formal calculus and a suitable formal semantics of theFDT. In this paper, we discuss the basic verification requirements for Estelle, and howthey can be supported by existing calculi. This leads us to the redefinition of the stanADdard Estelle semantics using Lamport's temporal logic of actions and Dijkstra's predicatetransformers.

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Jan Bredereke, Reinhard Gotzhein, F. H. Vogt
URN (permanent link):urn:nbn:de:hbz:386-kluedo-2769
Document Type:Preprint
Language of publication:English
Year of Completion:1999
Year of Publication:1999
Publishing Institute:Technische Universität Kaiserslautern
Tag:Requirements/Specifications; Semantics of Programming Languages
Faculties / Organisational entities:Fachbereich Informatik
CCS-Classification (computer science):C.2.4 Distributed Systems
D.2.1 Requirements/Specifications (D.3.1)
F.3.2 Semantics of Programming Languages (D.3.1)
DDC-Cassification:004 Datenverarbeitung; Informatik

$Rev: 12793 $