Combining CSP and B for specification and property verification

被引：0
|
作者：
Butler, M
Leuschel, M
机构：
[1] Univ Southampton, Sch Elect & Comp Sci, Southampton SO17 1BJ, Hants, England
[2] Univ Dusseldorf, Inst Informat, D-40225 Dusseldorf, Germany
来源：
FM 2005: FORMAL METHODS, PROCEEDINGS | 2005年 / 3582卷
关键词：
B-method; tool support; model checking; animation; logic programming; constraints;
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
PROB is a model checking tool for the B Method. In this paper we present an extension of PRoB that supports checking of specifications written in a combination of CSP and B. We explain how the notations are combined semantically and give an overview of the implementation of the combination. We illustrate the benefit that appropriate use of CSP, in conjunction with our tool, gives to B developments both for specification and for verification purposes.
引用
收藏
页码：221 / 236
页数：16
相关论文
共 50 条
  • [41] Formalization and verification of dubbo using CSP
    Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China
    Proc. Int. Conf. Softw. Eng. Knowl. Eng., SEKE, 2325, (154-159):
  • [42] Verification of redesign models - A CSP approach
    Arana, I
    Ahriz, H
    DESIGN METHODS FOR PERFORMANCE AND SUSTAINABILITY, 2001, : 283 - 290
  • [43] Operators with the specification property
    Bartoll, Salud
    Martinez-Gimenez, Felix
    Peris, Alfredo
    JOURNAL OF MATHEMATICAL ANALYSIS AND APPLICATIONS, 2016, 436 (01) : 478 - 488
  • [44] Properties as processes: Their specification and verification
    Kelso, J
    Milne, G
    FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2005, 2005, 3731 : 503 - 517
  • [45] Specification and Verification of Pharmacokinetic Models
    Kwon, YoungMin
    Kim, Eunhee
    ADVANCES IN COMPUTATIONAL BIOLOGY, 2010, 680 : 465 - 472
  • [46] SPECIFICATION AND VERIFICATION OF VLSI SYSTEMS
    WILK, A
    PNUELI, A
    1989 IEEE INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN: DIGEST OF TECHNICAL PAPERS, 1989, : 460 - 463
  • [47] OCCAM IN THE SPECIFICATION AND VERIFICATION OF MICROPROCESSORS
    ROSCOE, AW
    PHILOSOPHICAL TRANSACTIONS OF THE ROYAL SOCIETY OF LONDON SERIES A-MATHEMATICAL PHYSICAL AND ENGINEERING SCIENCES, 1992, 339 (1652): : 137 - 151
  • [48] SPECIFICATION AND VERIFICATION OF DATABASE DYNAMICS
    FIADEIRO, J
    SERNADAS, A
    ACTA INFORMATICA, 1988, 25 (06) : 625 - 661
  • [49] Specification and verification of GPGPU programs
    Blom, Stefan
    Huisman, Marieke
    Mihelcic, Matej
    SCIENCE OF COMPUTER PROGRAMMING, 2014, 95 : 376 - 388
  • [50] PROTOCOL SPECIFICATION, TESTING AND VERIFICATION
    不详
    COMPUTER NETWORKS AND ISDN SYSTEMS, 1984, 8 (01): : 57 - 65
12345