DESIGN OF A FORMAL ESTELLE SEMANTICS FOR VERIFICATION

被引：0

作者：

BREDEREKE, J ^{[1
]}

GOTZHEIN, R ^{[1
]}

VOGT, FH ^{[1
]}

机构：

[1] UNIV HAMBURG,W-2000 HAMBURG 54,GERMANY

来源：

IFIP TRANSACTIONS C-COMMUNICATION SYSTEMS | 1993年 / 10卷

关键词：

SEMANTICS OF PROGRAMMING LANGUAGES; REQUIREMENTS SPECIFICATIONS; DISTRIBUTED SYSTEMS;

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

One main purpose for the use of formal description techniques (FDTs) is formal reasoning and verification. This requires a formal calculus and a suitable formal semantics of the FDT. In this paper, we discuss the basic verification requirements for Estelle, and how they can be supported by existing calculi. This leads us to the redefinition of the standard Estelle semantics using Lamport's temporal logic of actions and Dijkstra's predicate transformers.

引用

页码：153 / 168

页数：16

共 50 条

[31] ESTELLE FORMAL SPECIFICATION OF ISO VIRTUAL TERMINAL
AMER, PD
CECELI, F
COMPUTER STANDARDS & INTERFACES, 1989, 9 (02) : 87 - 104
[32] A formal approach to product semantics with an application to sustainable design
Feijs, L
Meinel, F
DESIGN ISSUES, 2005, 21 (03) : 67 - 81
[33] USE OF A FORMAL NOTATION FOR STATIC SEMANTICS IN COMPILER DESIGN
WILLIAMS, MH
BULMER, AR
SOFTWARE-PRACTICE & EXPERIENCE, 1978, 8 (05): : 579 - 584
[34] What is formal in formal semantics?
Wolenski, J
DIALECTICA, 2004, 58 (03) : 427 - 436
[35] EVEN: A software environment for Estelle specification verification
Jirachiefpattana, A
Lai, R
JOURNAL OF SYSTEMS AND SOFTWARE, 1997, 39 (02) : 119 - 143
[36] Heterogeneous formal specification based on Object-Z and statecharts: semantics and verification
Gruer, JP
Hilaire, V
Koukam, A
Rovarini, P
JOURNAL OF SYSTEMS AND SOFTWARE, 2004, 70 (1-2) : 95 - 105
[37] VERIFICATION OF ISO ACSE PROTOCOL SPECIFIED IN ESTELLE
LAI, R
JIRACHIEFPATTANA, A
COMPUTER COMMUNICATIONS, 1994, 17 (03) : 172 - 188
[38] Formal semantics, modular specification, and symbolic verification of product-line behaviour
Classen, Andreas
Cordy, Maxime
Heymans, Patrick
Legay, Axel
Schobbens, Pierre-Yves
SCIENCE OF COMPUTER PROGRAMMING, 2014, 80 : 416 - 439
[39] Games for formal design and verification of reactive systems
Alur, Rajeev
Fourth ACM & IEEE International Conference on Formal Methods and Models for Co-Design, Proceedings, 2006, : 3 - 3
[40] INCREMENTAL DESIGN AND FORMAL VERIFICATION OF MICROCODED MICROPROCESSORS
HERBERT, JMJ
IFIP TRANSACTIONS A-COMPUTER SCIENCE AND TECHNOLOGY, 1992, 10 : 157 - 174

← 1 2 3 4 5 →