Abstract
The activities of formal modelling and reasoning are closely related. But while the rigour of building formal models brings significant benefits, formal reasoning remains a major barrier to the wider acceptance of formalism within design. Here we propose reasoned modelling critics – a technique which aims to abstract away from the complexities of low-level proof obligations, and provide high-level modelling guidance to designers when proofs fail. Inspired by proof planning critics, the technique combines proof-failure analysis with modelling heuristics. Here, we present the details of our proposal and outline future plans.
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, Cambridge (2009) (To be published)
Abrial, J.-R., Butler, M., Hallerstede, S., Voisin, L.: An Open Extensible Tool Environment for Event-B. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 588–605. Springer, Heidelberg (2006)
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)
Brown, W., Malveau, R., McCormick, H.W.S., Mowbray, T.: AntiPatterns: Refactoring Software, Architectures, and Projects in Crisis. John Wiley & Sons, Chichester (1998)
Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-level Guidance for Mathematical Reasoning. Cambridge University Press, Cambridge (2005)
Bundy, A.: The Use of Explicit Plans to Guide Inductive Proofs. In: Lusk, R., Overbeek, R. (eds.) CADE 2009, pp. 111–120. Springer, Heidelberg (1988)
Bundy, A., Chan, M.: Towards ontology evolution in physics. In: Hodges, W., de Queiroz, R. (eds.) Logic, Language, Information and Computation. LNCS (LNAI), vol. 5110, pp. 98–110. Springer, Heidelberg (2008)
Butler, M., Yadav, D.: An Incremental Development of the Mondex System in Event-B. Formal Aspects of Computing 20(1), 61–77 (2008)
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading (1995)
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., Stark, J.: Proof Planning for Strategy Development. Annals of Mathematics and Artificial Intelligence 29(1-4), 65–97 (2001)
Monroy, R., Bundy, A., Ireland, A.: Proof Plans for the Correction of False Conjectures. In: Pfenning, F. (ed.) LPAR 1994. LNCS (LNAI), vol. 822, Springer, Heidelberg (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ireland, A., Grov, G., Butler, M. (2010). Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidance. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds) Abstract State Machines, Alloy, B and Z. ABZ 2010. Lecture Notes in Computer Science, vol 5977. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11811-1_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-11811-1_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11810-4
Online ISBN: 978-3-642-11811-1
eBook Packages: Computer ScienceComputer Science (R0)