Refining reactive systems in HOL using action systems
Work on embedding reasoning about programs in a mechanised logic has mostly focused on meta-theoretic reasoning about programming logics or notations. This paper describes an attempt to formalise a theory of actions systems in HOL, in such a way that a tool for developing and reasoning about distributed and reactive systems can be built on top of the theory. By reducing action system refinement proofs to proofs of data refinement between sequential statements, we are able to reuse existing theories and tools for sequential programs.
KeywordsAction System Parallel Composition Data Refinement Predicate Transformer Abstraction Statement
Unable to display preview. Download preview PDF.
- 1.F. Andersen, K.D. Petersen, and J.S. Petterson. A Graphical Tool for Proving UNITY Progress. In T.F. Melham and J. Camilleri, editors, Higher Order Logic Theorem Proving and Its Applications-7th International Workshop. Valletta, Malta, September 1994, volume 859 of Lecture Notes in Computer Science. Springer Verlag, 1994.Google Scholar
- 2.R. Back Correctness Preserving Program Refinements: Proof Theory and Applications, volume 131 of Mathematical Center Tracts. Mathematical Centre, Amsterdam, 1980.Google Scholar
- 3.R. Back. A calculus of refinements for program derivations. Acta Informatica, 25:593–624, 1988.Google Scholar
- 4.R. Back and J. von Wright. Refinement concepts formalized in higher order logic. Formal Aspects of Computing, 2:247–272, 1990.Google Scholar
- 5.R. Back and J. von Wright. Trace refinement of action systems. Reports on computer science and mathematics 153, Åbo Akademi, 1994.Google Scholar
- 6.M. Butler and T. Långbacka. Program derivation using the refinement calculator. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference, volume 1125 of Lecture Notes in Computer Science, pages 93–108. Springer Verlag, August 1996.Google Scholar
- 7.A. Camillieri. Mechanizing CSP trace theory in Higher Order Logic. IEEE Transactions on Software Engineering, 16(9):993–1004, 1990.Google Scholar
- 8.E. Dijkstra. A Discipline of Programming. Prentice-Hall International, 1976.Google Scholar
- 9.J. Grundy. Window inference in the HOL system. In M. Archer, J.J. Joyce, K.N. Levitt, and P.J. Windley, editors, Proceedings of the International Tutorial and Workshop on the HOL Theorem Proving System and its Applications, pages 177–189, University of California at Davis, August 1991. ACM-SIGDA, IEEE Computer Society Press.Google Scholar
- 10.R. Ruksenas and J. von Wright. A tool for data refinement. To appear as a TUGS Technical Report, Turku Centre for Computer Science, Lemminkäisenkatu 14A, 20520 Turku, Finland, 1997.Google Scholar
- 11.J. von Wright. Program refinement by theorem prover. In BCS FACS Sixth Refinement Workshop — Theory and Practise of Formal Software Development. 5th 7th January, City University, London, UK., 1994.Google Scholar
- 12.J. von Wright and T. Långbacka. Using a theorem prover for reasoning about concurrent algorithms. In G. von Bochmann and D.K. Probst, editors, Computer Aided Verification — Fourth International Workshop. CAV '92. Montreal. Canada. June 29–July 1. 1992, volume 663 of Lecture Notes in Computer Science. Springer Verlag, 1993.Google Scholar