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 条
  • [1] Formal semantics and verification for feature modeling
    Sun, J
    Zhang, HY
    Li, YF
    Wang, H
    [J]. ICECCS 2005: 10TH IEEE INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS, PROCEEDINGS, 2005, : 303 - 312
  • [2] AADL execution semantics transformation for formal verification
    Abdoul, Thomas
    Champeau, Joel
    Dhaussy, Philippe
    Pillain, Pierre-Yves
    Roger, Jean-Charles
    [J]. ICECCS 2008: THIRTEENTH IEEE INTERNATIONAL CONFERENCE ON THE ENGINEERING OF COMPLEX COMPUTER SYSTEMS, PROCEEDINGS, 2008, : 263 - 268
  • [3] Hyperhierarchy of Semantics - A Formal Framework for Hyperproperties Verification
    Mastroeni, Isabella
    Pasqua, Michele
    [J]. STATIC ANALYSIS (SAS 2017), 2017, 10422 : 232 - 252
  • [4] Simulator Semantics for System Level Formal Verification
    Mancini, Toni
    Mari, Federico
    Massini, Annalisa
    Melatti, Igor
    Tronci, Enrico
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2015, (193): : 86 - 99
  • [5] Formal Semantics and Verification of BPMN Transaction and Compensation
    Takemura, Tsukasa
    [J]. 2008 IEEE ASIA-PACIFIC SERVICES COMPUTING CONFERENCE, VOLS 1-3, PROCEEDINGS, 2008, : 284 - 290
  • [6] A Formal CHERI-C Semantics for Verification
    Park, Seung Hoon
    Pai, Rekha
    Melham, Tom
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT I, TACAS 2023, 2023, 13993 : 549 - 568
  • [7] Research on Microkernel Integrity Semantics Model and Formal Verification
    Qian Zhenjiang
    Liu Wei
    Huang Hao
    [J]. CHINESE JOURNAL OF ELECTRONICS, 2014, 23 (01) : 43 - 48
  • [8] Formal Semantics of Runtime Monitoring, Verification, Enforcement and Control
    Chen, Zhe
    Wei, Ou
    Huang, Zhiqiu
    Xi, Hongwei
    [J]. PROCEEDINGS 2015 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, 2015, : 63 - 70
  • [9] Research on Microkernel Integrity Semantics Model and Formal Verification
    QIAN Zhenjiang
    LIU Wei
    HUANG Hao
    [J]. Chinese Journal of Electronics, 2014, 23 (01) : 43 - 48
  • [10] Verification of PLC Properties Based on Formal Semantics in Coq
    Blech, Jan Olaf
    Biha, Sidi Ould
    [J]. SOFTWARE ENGINEERING AND FORMAL METHODS, 2011, 7041 : 58 - +
12345