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 条
  • [31] A model checking approach for verifying COWS specifications
    Fantechi, Alessandro
    Gnesi, Stefania
    Lapadula, Alessandro
    Mazzanti, Franco
    Pugliese, Rosario
    Tiezzi, Francesco
    FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS, 2008, 4961 : 230 - +
  • [32] Verifying scenario-based aspect specifications
    Katz, E
    Katz, S
    FM 2005: FORMAL METHODS, PROCEEDINGS, 2005, 3582 : 432 - 447
  • [33] Verifying Concurrent Programs against Sequential Specifications
    Bouajjani, Ahmed
    Emmi, Michael
    Enea, Constantin
    Hamza, Jad
    PROGRAMMING LANGUAGES AND SYSTEMS, 2013, 7792 : 290 - 309
  • [34] Verifying specifications in hybrid automata models of systems
    Kotini, Isabella
    Hassapis, George
    Mavridis, Ioannis
    Computational Methods in Circuits and Systems Applications, 2003, : 146 - 151
  • [35] Towards Verifying Declarative Specifications of Reactive Systems
    Kameda, Tae
    Arai, Osamu
    Gorlatch, Sergei
    Fujita, Hamido
    NEW TRENDS IN SOFTWARE METHODOLOGIES, TOOLS AND TECHNIQUES, 2008, 182 : 389 - 400
  • [36] Verifying model oriented specifications through animation
    Kazmierczak, E
    Winikoff, M
    Dart, P
    1998 ASIA PACIFIC SOFTWARE ENGINEERING CONFERENCE, PROCEEDINGS, 1998, : 254 - 261
  • [37] Revani: Revising and Verifying Normative Specifications for Privacy
    Kafali, Ozgur
    Ajmeri, Nirav
    Singh, Munindar P.
    IEEE INTELLIGENT SYSTEMS, 2016, 31 (05) : 8 - 15
  • [38] Behavioural specifications in type theory
    Mylonakis, N
    RECENT TRENDS IN DATA TYPE SPECIFICATION, 1996, 1130 : 394 - 408
  • [39] Behavioural specifications in type theory
    Lect Notes Comput Sci, (394):
  • [40] Foundations for structuring behavioural specifications
    Diaconescu, Razvan
    Tutu, Ionut
    JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2014, 83 (3-4) : 319 - 338
12345