Advertisement

Refining reactive systems in HOL using action systems

  • Thomas Långbacka
  • Joakim von Wright
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1275)

Abstract

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.

Keywords

Action System Parallel Composition Data Refinement Predicate Transformer Abstraction Statement 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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. 2.
    R. Back Correctness Preserving Program Refinements: Proof Theory and Applications, volume 131 of Mathematical Center Tracts. Mathematical Centre, Amsterdam, 1980.Google Scholar
  3. 3.
    R. Back. A calculus of refinements for program derivations. Acta Informatica, 25:593–624, 1988.Google Scholar
  4. 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. 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. 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. 7.
    A. Camillieri. Mechanizing CSP trace theory in Higher Order Logic. IEEE Transactions on Software Engineering, 16(9):993–1004, 1990.Google Scholar
  8. 8.
    E. Dijkstra. A Discipline of Programming. Prentice-Hall International, 1976.Google Scholar
  9. 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. 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. 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. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Thomas Långbacka
    • 1
    • 3
  • Joakim von Wright
    • 2
  1. 1.Department of Computer ScienceUniversity of HelsinkiHelsinki
  2. 2.Department of Computer ScienceÅbo Akademi UniversityFinland
  3. 3.Turku Centre for Computer ScienceFinland

Personalised recommendations