Paper Info
Title
On fitting a formal method into practice
Abstract
The development of the Event-B formal method and the supporting tools Rodin and ProB was guided by practical experiences with the B-Method, the Z specification notation, VDM and similar practical formal methods. The case study discussed in this article -- a cruise control system -- is a serious test of industrial use. We report on where Event-B and its tools have succeeded, where they have not. We also report on advances that were inspired by the case study. Interestingly, the case study was not a pure formal methods problem. In addition to Event-B, it used Problem Frames for capturing requirements. The interaction between the two proved to be crucial for the success of the case study. The heart of the problem was tracing informal requirements from Problem Frames descriptions to formal Event-B models. To a large degree, this issue dictated the approach that had to be used for formal modelling. A dedicated record theory and dedicated tool support were required. The size of the formal models rather than complex individual formulas was the main challenge for tool support.
Year
DOI
Venue
2011
10.1007/978-3-642-24559-6_15
ICFEM
Keywords
Field
DocType
problem frames,pure formal methods problem,similar practical formal method,formal modelling,problem frames description,formal event-b model,event-b formal method,dedicated record theory,formal model,case study
Formal system,Notation,Software engineering,Computer science,Cruise control,Algorithm,Theoretical computer science,Formal specification,Formal methods,Proof obligation,Tracing,Formal verification
Conference
Volume
ISSN
Citations 
6991
0302-9743
10
PageRank 
References 
Authors
0.72
10
6
Name
Order
Citations
PageRank
Rainer Gmehlich1101.74
Katrin Grau2101.06
Stefan Hallerstede365444.88
Michael Leuschel42156135.89
Felix Lösch5111.08
Daniel Plagge61337.78