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.

Download full text files

Export metadata

Additional Services

Search Google Scholar
Metadaten
Author:Jan Bredereke, Reinhard Gotzhein, F. H. Vogt
URN:urn:nbn:de:hbz:386-kluedo-2769
Document Type:Preprint
Language of publication:English
Year of Completion:1999
Year of first Publication:1999
Publishing Institution:Technische Universität Kaiserslautern
Date of the Publication (Server):2000/04/03
Tag:Requirements/Specifications; Semantics of Programming Languages
Faculties / Organisational entities:Kaiserslautern - Fachbereich Informatik
CCS-Classification (computer science):C. Computer Systems Organization / C.2 COMPUTER-COMMUNICATION NETWORKS / C.2.4 Distributed Systems
D. Software / D.2 SOFTWARE ENGINEERING (K.6.3) / D.2.1 Requirements/Specifications (D.3.1)
F. Theory of Computation / F.3 LOGICS AND MEANINGS OF PROGRAMS / F.3.2 Semantics of Programming Languages (D.3.1)
DDC-Cassification:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Licence (German):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011