Verifying behavioural specifications in CafeOBJ environment

被引：0
|
作者：
Mori, A [1 ]
Futatsugi, K [1 ]
机构：
[1] Japan Adv Inst Sci & Technol, Hokuri Ku, Tatsunokuchi Nomi, Ishikawa 9231292, Japan
来源：
FM'99-FORMAL METHODS, VOL II | 1999年 / 1709卷
关键词：
D O I：
暂无
中图分类号：
TP39 [计算机的应用];
学科分类号：
081203 ; 0835 ;
摘要：
In this paper, we present techniques for automated verification of behavioural specifications using hidden algebra. Two non-trivial examples, the Alternating Bit Protocol and a snooping cache coherence protocol, are presented with complete specification code and proof scores for CafeOBJ verification system. The refinement proof based on behavioural coinduction is given for the first example, and the coherence proof based on invariance is given for the second.
引用
收藏
页码：1625 / 1643
页数：19
相关论文
共 50 条
  • [21] On the complexity of verifying consistency of XML specifications
    Arenas, Marcelo
    Fan, Wenfei
    Libkin, Leonid
    SIAM JOURNAL ON COMPUTING, 2008, 38 (03) : 841 - 880
  • [22] Behavioural and abstractor specifications
    Bidoit, M
    Hennicker, R
    Wirsing, M
    SCIENCE OF COMPUTER PROGRAMMING, 1995, 25 (2-3) : 149 - 186
  • [23] Formally verifying decompositions of stochastic specifications
    Anton Hampus
    Mattias Nyberg
    International Journal on Software Tools for Technology Transfer, 2024, 26 : 207 - 228
  • [24] Verifying communication constraints in RSML specifications
    Heimdahl, MPE
    1997 HIGH-ASSURANCE ENGINEERING WORKSHOP - PROCEEDINGS, 1997, : 56 - 61
  • [25] A Spiral Process of Modeling and Verifying the Scheduling Mechanism of OSEK/VDX in OTS/CafeOBJ Method
    Zhang, Min
    Aoki, Toshiaki
    2015 2ND INTERNATIONAL SYMPOSIUM ON DEPENDABLE COMPUTING AND INTERNET OF THINGS (DCIT), 2015, : 11 - 20
  • [26] Automated test case generation from OTS/CafeOBJ specifications by specification translation
    Mori, Ryusei
    Nakamura, Masaki
    10TH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION WORKSHOPS - ICSTW 2017, 2017, : 403 - 404
  • [27] VERIFYING AND VALIDATING SOFTWARE REQUIREMENTS AND DESIGN SPECIFICATIONS
    BOEHM, BW
    IEEE SOFTWARE, 1984, 1 (01) : 75 - 88
  • [28] Verifying consistency and validity of formal specifications by testing
    Liu, SY
    FM'99-FORMAL METHODS, 1999, 1708 : 896 - 914
  • [29] CHARMY: A Framework for Designing and Verifying Architectural Specifications
    Pelliccione, Patrizio
    Inverardi, Paola
    Muccini, Henry
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2009, 35 (03) : 325 - 346
  • [30] Verifying temporal specifications of Java']Java programs
    Spegni, Francesco
    Spalazzi, Luca
    Liva, Giovanni
    Pinzger, Martin
    Bollin, Andreas
    SOFTWARE QUALITY JOURNAL, 2020, 28 (02) : 695 - 744
12345