2011 IEEE 13th International Symposium on High-Assurance Systems Engineering (2011)
Boca Raton, Florida USA
Nov. 10, 2011 to Nov. 12, 2011
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/HASE.2011.47
In this paper, we explore the possibility to use Event-B as a formal domain modeling tool. We identify the areas where domain modelers can struggle and present some guidelines to avoid these pitfalls. We mainly address three questions about domain modeling: what to specify, how to refine, and how to verify. We discuss the strategy to express domain assumptions, protocols, time, and temporal properties. We also analyze the refinement and proof system of Event-B in this realm. We advocate small incremental steps and alternative refinement mechanisms, such as "observation levels. " We find animation a very helpful activity to complement the verification process.
Formal methods, Domain modeling, Event-B
J. Jacquot and A. Mashkoor, "Guidelines for Formal Domain Modeling in Event-B," 2011 IEEE 13th International Symposium on High-Assurance Systems Engineering(HASE), Boca Raton, Florida USA, 2011, pp. 138-145.