More Web Proxy on the site http://driver.im/

research-article

Open access

Discovery of invariants through automated theory formation

Authors:

Maria Teresa Llano,

Andrew Ireland,

Alison PeaseAuthors Info & Claims

Formal Aspects of Computing, Volume 26, Issue 2

Pages 203 - 249

https://doi.org/10.1007/s00165-012-0264-1

Published: 01 March 2014 Publication History

Abstract

Refinement is a powerful mechanism for mastering the complexities that arise when formally modelling systems. Refinement also brings with it additional proof obligations—requiring a developer to discover properties relating to their design decisions. With the goal of reducing this burden, we have investigated how a general purpose automated theory formation tool, HR, can be used to automate the discovery of such properties within the context of the Event-B formal modelling framework. This gave rise to an integrated approach to automated invariant discovery. In addition to formal modelling and automated theory formation, our approach relies upon the simulation of system models as a key input to the invariant discovery process. Moreover we have developed a set of heuristics which, when coupled with automated proof-failure analysis, have enabled us to effectively tailor HR to the needs of Event-B developments. Drawing in part upon case study material from the literature, we have achieved some promising experimental results. While our focus has been on Event-B, we believe that our approach could be applied more widely to formal modelling frameworks which support simulation.

References

References

[1]

Abrial J-R, Butler M, Hallerstede S, Hoang T, Mehta F, and Voisin L Rodin: an open toolset for modelling and reasoning in Event-B STTT 2010 12 6 447-466

[2]

Abrial J-R Modeling in Event-B—system and software engineering 2010 Cambridge Cambridge University Press

[3]

Baars B A cognitive theory of consciousness 1988 Cambridge Cambridge University Press

[4]

Baars B In the theater of consciousness: the workspace of the mind 1997 New York Oxford University Press

[5]

Bruner J, Goodnow JJ, and Austin GA A study of thinking 1967 New York Science Editions

[6]

Bolton C Using the Alloy analyzer to verify data refinement Z Electron Notes Theoret Comput Sci 2005 137 2 23-44

Digital Library

[7]

Banach R and Schellhorn G Atomic actions, and their refinements to isolated protocols Formal Aspects Comput 2010 22 1 33-61

Digital Library

[8]

Buchanan B (1975) Applications of artificial intelligence to scientific reasoning. In: Second USA–Japan computer conference, Tokyo, AFIPS and IPS I, pp 189–194

[9]

Butler M and Yadav D An incremental development of the Mondex system in Event-B Formal Aspects Comput 2008 20 1 61-77

Digital Library

[10]

Colton S, Bundy A, Walsh T (1999) Automatic concept formation in pure mathematics. In: Proceedings of the 16th international joint conference on artificial intelligence, pp 786–793

[11]

Colton S, Bundy A, Walsh T (2000) Automatic identification of mathematical concepts. In: Proceedings of the 17th international conference on machine learning. Morgan Kaufmann, San Francisco, pp 183–190

[12]

Colton S, Bundy A, Walsh T (2000) Automatic invention of integer sequences. In: Proceedings of the 17th national conference on artificial intelligence, pp 558–563

[13]

Colton S, Bundy A, and Walsh T On the notion of interestingness in automated mathematical discovery Int J Human Comput Stud 2000 53 3 351-375

Digital Library

[14]

Charnley J, Colton S (2008) A global workspace framework for combining reasoning systems. In: Proceedings of the symposium on the integration of symbolic computation and mechanised reasoning, pp 261–265

[15]

Charnley J, Colton S, Miguel I (2006) Automatic generation of implied constraints. In: Proceedings of the 17th European conference on AI, pp 73–77

[16]

Charnley J (2010) A global workspace framework for combined reasoning. PhD thesis, Imperial College, London

[17]

Colton S, Miguel I (2001) Constraint generation via automated theory formation. In: 7th international conference on the principles and practice of constraint programming, pp 575–579

[18]

Colton S and Muggleton S Mathematical applications of inductive logic programming Mach Learn 2006 64 25-64

Digital Library

[19]

Colton S (1999) Refactorable numbers—a machine invention. J Integer Sequen 2

[20]

Colton S Automated theory formation in pure mathematics 2002 Berlin Springer

[21]

Colton S (2002) The HR program for theorem generation. In: CADE’18. Lecture notes in computer science, vol 2392. Springer, Berlin, pp 37–61

[22]

Colton S, Pease A (2004) The TM system for repairing non-theorems. In Workshop on Disproving, Proceedings of IJCAR’04, pages 13–26

[23]

Colton S, Pease A (2005) The TM system for repairing non-theorems. In: Selected papers from IJCAR’04 disproving workshop. Electron Notes Theoret Comput Sci vol 125(3):87–101

[24]

Colton S, Sutcliffe G (2002) Automatic generation of benchmark problems for automated theorem proving systems. In: Proceedings of the 7th AI and maths symposium

[25]

Damchoom K (2010) An incremental refinement approach to a development of a flash-based file system in Event-B. PhD thesis, University of Southampton

[26]

Ernst M, Perkins J, Guo P, McCamant S, Pacheco C, Tschantz M, and Xiao C The Daikon system for dynamic detection of likely invariants Sci Comput Program 2007 69 1–3 35-45

Digital Library

[27]

Grov G, Ireland A, Llano MT (2012) Refinement plans for informed formal design. In: ABZ. Lecture notes in computer science. Springer, Berlin, pp 208–222

[28]

Holzmann GJ, Joshi R, Groce A (2008) 25 years of model checking. In: New challenges in model checking. Springer, Berlin, pp 65–76

[29]

Ireland A, Ellis BJ, Cook A, Chapman R, and Barnes J An integrated approach to high integrity software verification J Autom Reason (special issue on Empirically Successful Automated Reasoning) 2006 36 4 379-410

Digital Library

[30]

Johansson M, Dixon L, Bundy A (2010) Case-analysis for rippling and inductive proof. In: 1st international conference on interactive theorem proving. LNCS, vol 6127. Springer, Berlin, pp 291–306

[31]

Lakatos I Proofs and refutations 1976 Cambridge Cambridge University Press

[32]

Leuschel M, Butler M (2003) ProB: a model checker for B. In: International symposium of formal methods Europe. LNCS, vol 2805. Springer, Berlin, pp 855–874

[33]

Lenat D (1977) Automated theory formation in mathematics. In: Proceedings of the 5th international joint conference on artificial intelligence. Morgan Kaufmann, San Francisco, pp 833–842

[34]

Llano MT, Ireland A, Pease A (2011) Discovery of invariants through automated theory formation. In: Proceedings of the 15th international refinement workshop. In: Electronic proceedings in theoretical computer science, vol 55. Open Publishing Association, pp 1–19

[35]

McCasland R, Bundy A, Autexier S (2007) Automated discovery of inductive theorems. In: From insight to proof: festschrift in honour of Andrzej Trybulec. Studies in logic, grammar and rhetoric, vol 10(23). University of Białystok, pp 135–149

[36]

McCune W (1994) A Davis–Putnam program and its application to finite first-order model search. Technical Report ANL/MCS-TM-194, Argonne National Laboratories

[37]

McCune WW (1994) Otter 3.0 Reference Manual and Guide. Technical report ANL-94/6, Argonne National Laboratory, Argonne, USA

[38]

McCune W (2003) Otter 3.3 reference manual. CoRR, cs.SC/0310056

[39]

McCune W.: Prover9 and MACE4. http://www.cs.unm.edu/~mccune/prover9/, 2005–2010.

[40]

Maclean E, Ireland A, Dixon L, Atkey R (2009) Refinement and term synthesis in loop invariant generation. In: 2nd international workshop on invariant generation (WING’09), a satellite workshop of ETAPS’09

[41]

Maclean E, Ireland A, Grov G (2011) The CORE system: Animation and functional correctness of pointer programs. In: Proceedings of the 16th IEEE conference on automated software engineering (ASE 2011): Tool demonstration paper. Lawrence, Kansas, pp 588–591

[42]

Montano-Rivas O, McCasland R, Dixon L, and Bundy A Scheme-based theorem discovery and concept invention Expert Syst Appl 2011 39 1637-1646

Digital Library

[43]

Meier A, Sorge V, Colton S (2002) Employing theory formation to guide proof planning. In: AISC/Calculemus’02. LNAI, vol 2385. Springer, Berlin, pp 275–289

[44]

Pease A, Colton S, Charnley J (2012) Automated theory formation: the next generation. IFCoLog lectures in computational logic, (Forthcoming)

[45]

Pease A (2007) A computational model of Lakatos-style reasoning. PhD thesis, School of Informatics, University of Edinburgh, Online http://hdl.handle.net/1842/2113

[46]

Plagge D, Leuschel M (2007) Validating Z specifications using the ProB animator and model checker. In: Integrated formal methods. Lecture notes in computer science, vol 4591. Springer, Berlin, pp 480–500

[47]

Pease A, Smaill A, Colton S, Ireland A, Llano M, Ramezani R, Grov G, Guhe M (2010) Applying Lakatos-style reasoning to AI problems. In: Thinking machines and the philosophy of computer science: concepts and principles. IGI Global, pp 149–174

[48]

Ritchie G, Hanna F (1990) AM a case study in methodology. In: The foundations of AI: a sourcebook. Cambridge University Press, Cambridge, pp 247–265

[49]

Snook C and Butler M UML-B: Formal modeling and design aided by UML ACM Trans Softw Eng Methodol 2006 15 1 92-122

Digital Library

[50]

Sorge V, Colton S, McCasland R, and Meier A Classification results in quasigroup and loop theory via a combination of automated reasoning tools Comment Math Univ Carolin 2008 49 2 319-339

[51]

Sorge V, Meier A, McCasland R, and Colton S Automatic construction and verification of isotopy invariants J Autom Reason 2008 40 2–3 221-243

Digital Library

[52]

Woodcock J and Davies J Using Z: specification, refinement and proof 1996 New Jersey Prentice-Hall

[53]

Winston P (1970) Learning structural descriptions from examples. Technical Report TR-231, MIT

[54]

Zimmer J, Franke A, Colton S, Sutcliffe G (2002) Integrating HR and tptp2X into MathWeb to compare automated theorem provers. In: Proceedings of the CADE’02 workshop on problems and problem sets

Cited By

Grov GIreland ALlano M(2021)Reasoned Modelling: Harnessing the Synergies Between Reasoning and ModellingMathematical Reasoning: The History and Impact of the DReaM Group10.1007/978-3-030-77879-8_6(105-127)Online publication date: 24-May-2021
https://doi.org/10.1007/978-3-030-77879-8_6
Bundy A(2021)The History of the DReaM GroupMathematical Reasoning: The History and Impact of the DReaM Group10.1007/978-3-030-77879-8_1(1-35)Online publication date: 24-May-2021
https://doi.org/10.1007/978-3-030-77879-8_1
Ireland ALlano MColton S(2018)The Use of Automated Theory Formation in Support of Hazard AnalysisNASA Formal Methods10.1007/978-3-319-77935-5_17(237-243)Online publication date: 11-Mar-2018
https://doi.org/10.1007/978-3-319-77935-5_17
Show More Cited By

Index Terms

Discovery of invariants through automated theory formation

Index terms have been assigned to the content through auto-classification.

Recommendations

Towards the Composition of Specifications in Event-B

The development of a system can start with the creation of a specification. Following this viewpoint, we claim that often a specification can be constructed from the combination of specifications which can be seen as composition. Event-B is a formal ...
A method of refinement in UML-B

UML-B is a `UML-like' graphical front-end for Event-B that provides support for object-oriented and state machine modelling concepts, which are not available in Event-B. In particular, UML-B includes class diagram and state machine diagram editors with ...
Semantics Formalisation – From Event-B Contexts to Theories
Rigorous State-Based Methods
Abstract
The Event-B modelling language has been used to formalise the semantics of other modelling languages such as Time Mobility (TiMo) or State Chart XML (SCXML). Typically, the syntactical elements of the languages are captured as Event-B contexts ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Aspects of Computing

Formal Aspects of Computing Volume 26, Issue 2

Mar 2014

232 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

© British Computer Society 2012.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 March 2014

Accepted: 05 September 2012

Received: 07 November 2011

Published in FAC Volume 26, Issue 2

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
60
Total Downloads

Downloads (Last 12 months)35
Downloads (Last 6 weeks)9

Reflects downloads up to 19 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Grov GIreland ALlano M(2021)Reasoned Modelling: Harnessing the Synergies Between Reasoning and ModellingMathematical Reasoning: The History and Impact of the DReaM Group10.1007/978-3-030-77879-8_6(105-127)Online publication date: 24-May-2021
https://doi.org/10.1007/978-3-030-77879-8_6
Bundy A(2021)The History of the DReaM GroupMathematical Reasoning: The History and Impact of the DReaM Group10.1007/978-3-030-77879-8_1(1-35)Online publication date: 24-May-2021
https://doi.org/10.1007/978-3-030-77879-8_1
Ireland ALlano MColton S(2018)The Use of Automated Theory Formation in Support of Hazard AnalysisNASA Formal Methods10.1007/978-3-319-77935-5_17(237-243)Online publication date: 11-Mar-2018
https://doi.org/10.1007/978-3-319-77935-5_17
Grov GIreland ALlano MKovacs PColton SGow J(2016)Semi-Automated Design Space Exploration for Formal ModellingProceedings of the 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z - Volume 967510.1007/978-3-319-33600-8_22(282-289)Online publication date: 23-May-2016
https://dl.acm.org/doi/10.1007/978-3-319-33600-8_22
Zhang JChen JHao DXiong YXie BZhang LMei HCrnkovic IChechik MGrünbacher P(2014)Search-based inference of polynomial metamorphic relationsProceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering10.1145/2642937.2642994(701-712)Online publication date: 15-Sep-2014
https://dl.acm.org/doi/10.1145/2642937.2642994

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents