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] USE OF A FORMAL NOTATION FOR STATIC SEMANTICS IN COMPILER DESIGN
    WILLIAMS, MH
    BULMER, AR
    [J]. SOFTWARE-PRACTICE & EXPERIENCE, 1978, 8 (05): : 579 - 584
  • [32] What is formal in formal semantics?
    Wolenski, J
    [J]. DIALECTICA, 2004, 58 (03) : 427 - 436
  • [33] VERIFICATION OF ISO ACSE PROTOCOL SPECIFIED IN ESTELLE
    LAI, R
    JIRACHIEFPATTANA, A
    [J]. COMPUTER COMMUNICATIONS, 1994, 17 (03) : 172 - 188
  • [34] Games for formal design and verification of reactive systems
    Alur, Rajeev
    [J]. Fourth ACM & IEEE International Conference on Formal Methods and Models for Co-Design, Proceedings, 2006, : 3 - 3
  • [35] EVEN: A software environment for Estelle specification verification
    Jirachiefpattana, A
    Lai, R
    [J]. JOURNAL OF SYSTEMS AND SOFTWARE, 1997, 39 (02) : 119 - 143
  • [36] A Formal Method for Early Spacecraft Design Verification
    Fischer, Philipp M.
    Luedtke, Daniel
    Schaus, Volker
    Gerndt, Andreas
    [J]. 2013 IEEE AEROSPACE CONFERENCE, 2013,
  • [37] INCREMENTAL DESIGN AND FORMAL VERIFICATION OF MICROCODED MICROPROCESSORS
    HERBERT, JMJ
    [J]. IFIP TRANSACTIONS A-COMPUTER SCIENCE AND TECHNOLOGY, 1992, 10 : 157 - 174
  • [38] Heterogeneous formal specification based on Object-Z and statecharts: semantics and verification
    Gruer, JP
    Hilaire, V
    Koukam, A
    Rovarini, P
    [J]. JOURNAL OF SYSTEMS AND SOFTWARE, 2004, 70 (1-2) : 95 - 105
  • [39] A design phase directed formal verification process
    Keane, JA
    Hussak, W
    [J]. SOFTWARE QUALITY JOURNAL, 1999, 8 (04) : 255 - 269
  • [40] Formal Design and Verification of an Asynchronous SRAM Controller
    Khomenko, Victor
    Mokhov, Andrey
    Sokolov, Danil
    Yakovlev, Alex
    [J]. 2017 17TH INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN (ACSD), 2017, : 59 - 67
12345