Output details
11 - Computer Science and Informatics
University of Southampton
Article title
An incremental development of the Mondex system in Event-B
Type
D - Journal article
Title of journal
Formal Aspects of Computing
Article number
-
Volume number
20
Issue number
1
First page of article
61
ISSN of journal
0934-5043
Year of publication
2008
Number of additional authors
1
Additional information
Significance of output:
<07>This work was part of a mini-grand challenge on formal verification of Mondex. It is different to the other attempts in that it makes very strong use of multi-level verification. We were able to show that this leads to a high degree of automatic verification and is robust to changes in the design.
The work has encouraged other researchers to use multi-level refinement more (Augsberg, Manchester, Heriot-Watt) and has influenced further development of the Event-B method and Rodin toolset in particular support for event extension and differential proving.
Interdisciplinary
-
Cross-referral requested
-
Research group
None
Citation count
22
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
