Name
Abstract | ||
|---|---|---|
A development of the Mondex system was undertaken using Event-B and its associated proof tools. An incremental approach was used whereby the refinement between the abstract specification of the system and its detailed design was verified through a series of refinements. The consequence of this incremental approach was that we achieved a very high degree of automatic proof. The essential features of our development are outlined. We also present some modelling and proof guidelines that we found helped us gain a deep understanding of the system and achieve the high degree of automatic proof. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/s00165-007-0061-4 | Formal Asp. Comput. |
Keywords | Field | DocType |
high degree,detailed design,refinement,abstract specification,methodological guidelines,automatic proof,system design,mondex system,event-b,essential feature,proof guideline,associated proof tool,incremental development,incremental approach,deep understanding,mechanical proof | Programming language,Iterative and incremental development,Computer science,Systems design,Algorithm,Theoretical computer science | Journal |
Volume | Issue | ISSN |
20 | 1 | 1433-299X |
Citations | PageRank | References |
29 | 1.29 | 6 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Michael Butler | 1 | 1768 | 104.74 |
| Divakar Yadav | 2 | 54 | 5.47 |