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.
Verfasser*innenangaben: | Jan Bredereke, Reinhard Gotzhein, F. H. Vogt |
---|---|
URN: | urn:nbn:de:hbz:386-kluedo-2769 |
Dokumentart: | Preprint |
Sprache der Veröffentlichung: | Englisch |
Jahr der Fertigstellung: | 1999 |
Jahr der Erstveröffentlichung: | 1999 |
Veröffentlichende Institution: | Technische Universität Kaiserslautern |
Datum der Publikation (Server): | 03.04.2000 |
Freies Schlagwort / Tag: | Requirements/Specifications; Semantics of Programming Languages |
Fachbereiche / Organisatorische Einheiten: | Kaiserslautern - Fachbereich Informatik |
CCS-Klassifikation (Informatik): | 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-Sachgruppen: | 0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik |
Lizenz (Deutsch): | Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011 |