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 条

[1] Specification and (property) inheritance in CSP-OZ
Olderog, ER
Wehrheim, H
[J]. SCIENCE OF COMPUTER PROGRAMMING, 2005, 55 (1-3) : 227 - 257
[2] Enhanced Property Specification and Verification in BLAST
Sery, Ondrej
[J]. FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS, 2009, 5503 : 456 - 469
[3] Using timed CSP for specification verification and simulation of multimedia synchronization
Ates, AF
Bilgic, M
Saito, S
Sarikaya, B
[J]. IEEE JOURNAL ON SELECTED AREAS IN COMMUNICATIONS, 1996, 14 (01) : 126 - 137
[4] csp2B: A practical approach to combining CSP and B
[J]. 2000, Springer-Verlag London Ltd (12)
[5] csp2B: A practical approach to combining CSP and B
Butler, M
[J]. FM'99-FORMAL METHODS, 1999, 1708 : 490 - 508
[6] Chunks:: Component verification in CSP||B
Schneider, S
Treharne, H
Evans, N
[J]. INTEGRATED FORMAL METHODS, PROCEEDINGS, 2005, 3771 : 89 - 108
[7] Property specification and static verification of UML models
Siveroni, Igor
Zisman, Andrea
Spanoudakis, George
[J]. ARES 2008: PROCEEDINGS OF THE THIRD INTERNATIONAL CONFERENCE ON AVAILABILITY, SECURITY AND RELIABILITY, 2008, : 96 - +
[8] CSP Specification and Verification of a Relay-Based Railway Interlocking System
Bezerra, P. E. R.
Oliveira, M. V. M.
Lecomte, Thierry
de Almeida Pereira, D. I.
[J]. FORMAL METHODS: FOUNDATIONS AND APPLICATIONS, SBMF 2023, 2024, 14414 : 36 - 54
[9] CSP Specification and Verification of Relay-based Railway Interlocking Systems
Pereira, D. I. de Almeida
Oliveira, M. V. M.
Bezerra, P. E. R.
Bon, P.
Collart-Dutilleul, S.
[J]. 37TH ANNUAL ACM SYMPOSIUM ON APPLIED COMPUTING, 2022, : 97 - 106
[10] Verification of Scheme Plans Using CSP∥B
James, Philip
Moller, Faron
Nguyen, Hoang Nga
Roggenbach, Markus
Schneider, Steve
Treharne, Helen
Trumble, Matthew
Williams, David
[J]. SOFTWARE ENGINEERING AND FORMAL METHODS, 2014, 8368 : 189 - 204

← 1 2 3 4 5 →