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.
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 |