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 条
  • [1] Verifying specifications with proof scores in CafeOBJ
    Futatsugi, Kokichi
    ASE 2006: 21ST IEEE INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS, 2006, : 3 - 10
  • [2] An integrated tool set for verifying CafeOBJ specifications
    Riesco, Adrian
    Ogata, Kazuhiro
    JOURNAL OF SYSTEMS AND SOFTWARE, 2022, 189
  • [3] A Maude environment for CafeOBJ
    Riesco, Adrian
    Ogata, Kazuhiro
    Futatsugi, Kokichi
    FORMAL ASPECTS OF COMPUTING, 2017, 29 (02) : 309 - 334
  • [4] Verifying Safe Memory Reclamation in Concurrent Programs with CafeOBJ
    Duong Dinh Tran
    Ogata, Kazuhiro
    REWRITING LOGIC AND ITS APPLICATIONS, WRLA 2024, 2024, 14953 : 45 - 61
  • [5] Verifying the design of dynamic software updating in the OTS/CafeOBJ method
    Zhang, Min
    Ogata, Kazuhiro
    Futatsugi, Kokichi
    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2014, 8373 : 560 - 577
  • [6] Verifying architectural specifications
    Hoffman, P
    RECENT TRENDS IN ALGEBRAIC DEVELOPMENT TECHNIQUES, 2001, 2267 : 152 - 175
  • [7] Verifying SOS specifications
    Bloom, B
    Cheng, A
    Dsouza, A
    COMPASS '96 - PROCEEDINGS OF THE ELEVENTH ANNUAL CONFERENCE ON COMPUTER ASSURANCE: SYSTEMS INTEGRITY, SOFTWARE SAFETY, PROCESS SECURITY, 1996, : 117 - 127
  • [8] Writing concurrent Java']Java programs based on CafeOBJ specifications
    Ha, Xuan-Linh
    Ogata, Kazuhiro
    2017 24TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2017), 2017, : 618 - 623
  • [9] An object-oriented modeling method for algebraic specifications in CafeOBJ
    Nakajima, S
    Futatsugi, K
    PROCEEDINGS OF THE 1997 INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, 1997, : 34 - 44
  • [10] A Preliminary Study of Test Case Generation by CafeOBJ Rewrite Specifications
    Nakamura, Masaki
    2016 IEEE 5TH GLOBAL CONFERENCE ON CONSUMER ELECTRONICS, 2016,
12345