Abstract
Refinement is a powerful technique for tackling the complexities that arise when formally modelling systems. Here we focus on a posit-and-prove style of refinement, and specifically where a user requires guidance in order to overcome a failed refinement step. We take an integrated approach – combining the complementary strengths of top-down planning and bottom-up theory formation. In this paper we focus mainly on the planning perspective. Specifically, we propose a new technique called refinement plans which combines both modelling and reasoning perspectives. When a refinement step fails, refinement plans provide a basis for automatically generating modelling guidance by abstracting away from the details of low-level proof failures. The refinement plans described here are currently being implemented for the Event-B modelling formalism, and have been assessed on paper using case studies drawn from the literature. Longer-term, our aim is to identify refinement plans that are applicable to a range of modelling formalisms.
An earlier version of this paper appears in the informal proceedings of AFM’10 [23].
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.-R.: Modelling in Event-B: System and Software Engineering. Cambridge University Press (2010)
Abrial, J.-R., Hoang, T.S.: Using Design Patterns in Formal Methods: An Event-B Approach. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 1–2. Springer, Heidelberg (2008)
Bendisposto, J., Leuschel, M.: Automatic Flow Analysis for Event-B. In: Giannakopoulou, D., Orejas, F. (eds.) FASE 2011. LNCS, vol. 6603, pp. 50–64. Springer, Heidelberg (2011)
Bundy, A.: A science of reasoning. In: Computational Logic: Essays in Honor of Alan Robinson. MIT Press (1991)
Butler, M.: Decomposition Structures for Event-B. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 20–38. Springer, Heidelberg (2009)
Butler, M., Yadav, D.: An incremental development of the mondex system in Event-B. Formal Aspects of Computing 20(1) (2008)
Cavalcanti, A., Woodcock, J.: ZRC - A Refinement Calculus for Z. Formal Aspects of Computing 10(3) (1998)
Colton, S.: Automated Theory Formation in Pure Mathematics. Springer (2002)
Damchoom, K.: An Incremental Refinement Approach to a Development of a Flash-Based File System in Event-B. PhD thesis, University of Southampton (2010)
Salehi Fathabadi, A., Butler, M.: Applying Event-B Atomicity Decomposition to a Multi Media Protocol. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 89–104. Springer, Heidelberg (2010)
Salehi Fathabadi, A., Rezazadeh, A., Butler, M.: Applying Atomicity and Model Decomposition to a Space Craft System in Event-B. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 328–342. Springer, Heidelberg (2011)
Fürst, A.: Design Patterns in Event-B and Their Tool Support. Master’s thesis, ETH Zürich (2009)
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley (1995)
Hallerstede, S.: Structured Event-B Models and Proofs. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 273–286. Springer, Heidelberg (2010)
Hoang, T.S., Basin, D., Kuruma, H., Abrial, J.-R.: Development of a network topology discovery algorithm. DEPLOY project Repository, http://deploy-eprints.ecs.soton.ac.uk/82/
Iliasov, A.: Refinement Patterns for Rapid Development of Dependable Systems. In: EFTS. ACM Press (2007)
Iliasov, A.: Design Components. PhD thesis, University of Newcastle (2008)
Ireland, A.: The Use of Planning Critics in Mechanizing Inductive Proofs. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 178–189. Springer, Heidelberg (1992)
Ireland, A., Grov, G., Butler, M.: Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidance. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 189–202. Springer, Heidelberg (2010)
Ireland, A., Grov, G., Llano, M., Butler, M.: Reasoned modelling critics: turning failed proofs into modelling guidance. In: Science of Computer Programming. Elsevier (2011) (in Press)
Jones, C.B.: Systematic Software Development using VDM. Prentice Hall (1990)
Leuschel, M., Butler, M.: ProB: A Model Checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003)
Llano, M., Grov, G., Ireland, A.: Automatic guidance for refinement based formal methods. In: AFM Workshop (2010)
Llano, M.T., Ireland, A., Pease, A.: Discovery of invariants through automated theory formation. In: Refine Workshop. EPTCS, vol. 55 (2011)
Morgan, C.: Programming from Specifications. Prentice–Hall (1990)
Requet, A.: BART: A Tool for Automatic Refinement. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 345–345. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Grov, G., Ireland, A., Llano, M.T. (2012). Refinement Plans for Informed Formal Design. In: Derrick, J., et al. Abstract State Machines, Alloy, B, VDM, and Z. ABZ 2012. Lecture Notes in Computer Science, vol 7316. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30885-7_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-30885-7_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-30884-0
Online ISBN: 978-3-642-30885-7
eBook Packages: Computer ScienceComputer Science (R0)