<Emphasis Type="SmallCaps">ProB</Emphasis>: an automated analysis toolset for the B method |
| |
Authors: | Michael Leuschel Michael Butler |
| |
Affiliation: | 1.School of Electronics and Computer Science,University of Southampton,Southampton,UK;2.Institut für Informatik,Heinrich-Heine Universit?t Düsseldorf,Düsseldorf,Germany |
| |
Abstract: | We present ProB, a validation toolset for the B method. ProB’s automated animation facilities allow users to gain confidence in their specifications. ProB also contains a model checker and a refinement checker, both of which can be used to detect various errors in B specifications.
We describe the underlying methodology of ProB, and present the important aspects of the implementation. We also present empirical evaluations as well as several case
studies, highlighting that ProB enables users to uncover errors that are not easily discovered by existing tools.
This research was carried out as part of the EU research project IST 511599 RODIN (Rigorous Open Development Environment for
Complex Systems). |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|