×

Unifying theories in Isabelle/HOL. (English) Zbl 1309.68045

Qin, Shengchao (ed.), Unifying theories of programming. Third international symposium, UTP 2010, Shanghai, China, November 15–16, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-16689-1/pbk). Lecture Notes in Computer Science 6445, 188-206 (2010).
Summary: In this paper, we present various extensions of Isabelle/HOL by theories that are essential for several formal methods. First, we explain how we have developed an Isabelle/HOL theory for a part of the Unifying Theories of Programming (UTP). It contains the theories of alphabetized relations and designs. Then we explain how we have encoded first the theory of reactive processes and then the UTP theory for CSP. Our work takes advantage of the rich existing logical core of HOL.
Our extension contains the proofs for most of the lemmas and theorems presented in the UTP book. Our goal is to propose a framework that will allow us to deal with formal methods that are semantically based, partly or totally, on UTP, for instance CSP and Circus. The theories presented here will allow us to make proofs about such specifications and to apply verified transformations on them, with the objective of assisting refinement and test generation.
For the entire collection see [Zbl 1200.68018].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI