Refinement, Decomposition, and Instantiation of Discrete Models: Application to Event-B

• Autorzy: Abrial J-R. , Hallerstede S.
• Języki publikacji: EN

Abstrakty

EN

We argue that formal modeling should be the starting point for any serious development of computer systems. This claim poses a challenge for modeling: at first it must cope with the constraints and scale of serious developments. Only then it is a suitable starting point. We present three techniques, refinement, decomposition, and instantiation, that we consider indispensable for modeling large and complex systems. The vehicle of our presentation is Event-B, but the techniques themselves do not depend on it.

Słowa kluczowe

EN

refinement; decomposition; generic instantiation; event-B

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 77, nr 1,2
• Strony: 1--28
• Opis fizyczny: bibliogr. 26 poz., wykr.

Twórcy

autor

Abrial J-R.

autor

Hallerstede S.

• ETH Zurich, Switzerland,

Bibliografia

• [1] J.-R. Abrial. The B Book - Assigning Programs to Meanings. Cambridge University Press, 1996.
• [2] J.-R. Abrial and L. Mussat. Introducing dynamic constraints in B. In D. Bert, editor, B'98 :Recent Advances in the Development and Use of the B Method, volume 1393 of Lecture Notes in Computer Science. Springer Verlag, 1998.
• [3] Jean-Raymond Abrial. Event-B: Mathematical Model. Internal Report, April 2005.
• [4] Jean-Raymond Abrial and Dominique Cansell. Click'n'prove : Interactive proofs within set theory. In David Basin et Burkhart Wolff, editor, 16th International Conference on Theorem Proving in Higher Order Logics - TPHOLs'2003, Rome, Italy, volume 2758 of Lecture notes in Computer Science, pages 1-24. Springer, Sep 2003.
• [5] Jean-Raymond Abrial, Dominique Cansell, and Dominique Méry. Refinement and Reachability in Event-B. In H. Treharne et al., editor, ZB 2005: Formal Specification and Development in Z and B, volume 3544 of LNCS, pages 222-241, 2005.
• [6] R. J. R. Back. Refinement calculus, part II: Parallel and reactive programs. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems, volume 430 of Lecture Notes in Computer Science, pages 67-93. Springer-Verlag, 1990.
• [7] R. J. R. Back and J. von Wright. Refinement calculus, part I: Sequential nondeterministic programs. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems, volume 430 of Lecture Notes in Computer Science, pages 42-66. Springer-Verlag, 1990.
• [8] Ralph-Johan Back and Joakim von Wright. Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer Verlag, 1998.
• [9] Frédéric Badeau and Arnaud Amelot. Using B as a High Level Programming Language in an Industrial Project: Roissy VAL. In H. Treharne et al., editor, ZB 2005: Formal Specification and Development in Z and B, volume 3544 of LNCS, pages 334-354, 2005.
• [10] Egon Börger. The ASM refinement method. Formal Aspects of Computing, 15(2-3):237-257, 2003.
• [11] Egon Börger and Robert Stärk. Abstract State Machines: A Method for High-Level System Design and Analysis. Springer-Verlag, 2003.
• [12] J. Gosling, B. Joy, G. Steele, and G. Bracha. The Java Language Specification. Addison-Wesley, 3rd edition, 2005.
• [13] Mary Jean Harrold. Testing: a roadmap. In ICSE '00: Proceedings of the Conference on The Future of Software Engineering, pages 61-72, New York, NY, USA, 2000. ACM Press.
• [14] Eric C. R. Hehner. A Practical Theory of Programming. Texts and Monographs in Computer Science. Springer-Verlag, 1993.
• [15] C. B. Jones, K. D. Jones, P. A. Lindsay, and R. Moore. Mural: A Formal Development Support System. Springer-Verlag, 1991.
• [16] Cliff B. Jones. Systematic Software Development Using VDM. Prentice Hall, 2nd edition, 1990.
• [17] Leslie Lamport. Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002.
• [18] Carroll Morgan. Programming from Specifications. Prentice Hall, 1990.
• [19] Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer Verlag, 1994.
• [20] W. Reif and G. Schellhorn. Theorem Proving in Large Theories. In W. Bibel and P. Schmitt, editors, Automated Deduction-A Basis for Applications, volume III, 2. Kluwer Academic Publishers, Dordrecht, 1998.
• [21] RODIN project homepage. http://rodin.cs.ncl.ac.uk/.
• [22] W. P. de Roever and K. Engelhardt. Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge Tracts in Theoretical Computer Science 47. Cambridge University Press, 1998.
• [23] Gerhard Schellhorn. ASM refinement and generalizations of forward simulation in data refinement: a comparison. Theoretical Compututer Science, 336(2-3):403-435, 2005.
• [24] Niklaus Wirth. Program development by stepwise refinement. CACM: Communications of the ACM, 14, 1971.
• [25] Niklaus Wirth. MODULA : A language for modular multiprogramming. Software Practice and Experience, 7:3-35, 1977.
• [26] J. Woodcock and J. Davies. Using Z. Specification, Refinement, and Proof. Prentice-Hall, 1996.