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 条
  • [21] FORMAL DESIGN VERIFICATION OF DIGITAL CIRCUITRY
    BUTLER, RW
    SJOGREN, JA
    RELIABILITY ENGINEERING & SYSTEM SAFETY, 1991, 32 (1-2) : 67 - 93
  • [22] Formal System Design and Verification: A Perspective
    Rajamani, Sriram
    ISOFT: PROCEEDINGS OF THE 13TH INNOVATIONS IN SOFTWARE ENGINEERING CONFERENCE, 2020,
  • [23] Getting formal verification into design flow
    Arvind, S.
    Dave, Nirav
    Katelman, Michael
    FM 2008: FORMAL METHODS, PROCEEDINGS, 2008, 5014 : 12 - +
  • [24] Practical formal verification in microprocessor design
    Jones, RB
    O'Leary, JW
    Seger, CJH
    Aagaard, MD
    Melham, TF
    IEEE DESIGN & TEST OF COMPUTERS, 2001, 18 (04): : 16 - 25
  • [25] Formal verification in intel CPU design
    O'Leary, J
    Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, Proceedings, 2004, : 152 - 152
  • [26] Assured VLSI design with formal verification
    Kim, JD
    Chin, SK
    COMPASS '97 - ARE WE MAKING PROGRESS TOWARDS COMPUTER ASSURANCE?, 1997, : 13 - 22
  • [27] Formal verification and hardware design with statecharts
    Philipps, J
    Scholz, P
    PROSPECTS FOR HARDWARE FOUNDATIONS: ESPRIT WORKING GROUP 8533 NADA - NEW HARDWARE DESIGN METHODS SURVEY CHAPTERS, 1998, 1546 : 356 - 389
  • [28] Formal Semantics for PSL Modeling Layer and Application to the Verification of Transactional Models
    Ferro, Luca
    Pierre, Laurence
    2010 DESIGN, AUTOMATION & TEST IN EUROPE (DATE 2010), 2010, : 1207 - 1212
  • [29] Formal Verification of Automotive Design in Compliance With ISO 26262 Design Verification Guidelines
    Bahig, Ghada
    El-Kadi, Amr
    IEEE ACCESS, 2017, 5 : 4505 - 4516
  • [30] EDA formal verification - Expanding static verification with model checking and formal design rule checks
    Czeck, E
    Sandler, S
    ELECTRONIC ENGINEERING, 1999, 71 (869): : 35 - +
12345