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 条
  • [41] Behavioural and abstractor specifications revisited
    Hennicker, Rolf
    Madeira, Alexandre
    Wirsing, Martin
    THEORETICAL COMPUTER SCIENCE, 2018, 741 : 32 - 43
  • [42] An overview of CAFE specification environment - an algebraic approach for creating, verifying, and maintaining formal specifications over networks
    Futatsugi, K
    Nakagawa, A
    FIRST IEEE INTERNATIONAL CONFERENCE ON FORMAL ENGINEERING METHODS, PROCEEDINGS, 1997, : 170 - 181
  • [43] BehaVerify: Verifying Temporal Logic Specifications for Behavior Trees
    Serbinowski, Bernard
    Johnson, Taylor T.
    SOFTWARE ENGINEERING AND FORMAL METHODS, SEFM 2022, 2022, 13550 : 307 - 323
  • [44] Verifying Modal Workflow Specifications Using Constraint Solving
    Bride, Hadrien
    Kouchnarenko, Olga
    Peureux, Fabien
    INTEGRATED FORMAL METHODS, IFM 2014, 2014, 8739 : 171 - 186
  • [45] Verifying Linear Real-Time Logic specifications
    Andrei, Stefan
    Cheng, Albert M. K.
    RTSS 2007: 28TH IEEE INTERNATIONAL REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS, 2007, : 333 - +
  • [46] A Framework for Verifying the Conformance of Design to Its Formal Specifications
    Dieu-Huong Vu
    Chiba, Yuki
    Yatake, Kenro
    Aoki, Toshiaki
    IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 2015, E98D (06): : 1137 - 1149
  • [47] Verifying specifications with associated attributes in graph transformation systems
    Yu Zhou
    Yankai Huang
    Ou Wei
    Zhiqiu Huang
    Frontiers of Computer Science, 2015, 9 : 364 - 374
  • [48] Verifying Action Semantics Specifications in UML Behavioral Models
    Planas, Elena
    Cabot, Jordi
    Gomez, Cristina
    ADVANCED INFORMATION SYSTEMS ENGINEERING, PROCEEDINGS, 2009, 5565 : 125 - 140
  • [49] METHODS OF VERIFYING ADHERENCE TO THE NTSC COLOR SIGNAL SPECIFICATIONS
    LUTHER, AC
    PROCEEDINGS OF THE INSTITUTE OF RADIO ENGINEERS, 1954, 42 (01): : 235 - 240
  • [50] Verifying specifications with associated attributes in graph transformation systems
    Zhou, Yu
    Huang, Yankai
    Wei, Ou
    Huang, Zhiqiu
    FRONTIERS OF COMPUTER SCIENCE, 2015, 9 (03) : 364 - 374
12345