Mechanised Theory Engineering in Isabelle

Simon David Foster; Jim Woodcock

doi:10.3233/978-1-61499-495-4-246

Mechanised Theory Engineering in Isabelle

Simon David Foster, Jim Woodcock

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Chapter

Abstract

This is an introduction to mechanised theory engineering in Isabelle, an LCF-style interactive theorem prover. We introduce an embedding of Hoare & He's Unifying Theories of Programming (UTP) in Isabelle (named Isabelle/UTP) and show how to mechanise two key theories: relations and designs. These theories are sufficient to give an account of the partial and total correctness of nondeterministic sequential programs and of networks of reactive processes. A tutorial introduction to each theory is interspersed with its formalisation and with mechanised proofs of relevant properties and theorems. The work described here underpins specification languages such as Circus, which combines state-rich imperative operations, communication and concurrency, object orientation, references and pointers, real time, and process mobility, all with denotational, axiomatic, algebraic, and operational semantics.

Original language	English
Title of host publication	Dependable Software Systems Engineering
Editors	Maximilian Irlbeck, Doron Peled, Alexander Pretschner
Publisher	IOS Press
Pages	246-287
Volume	40
ISBN (Print)	978-1-61499-494-7
DOIs	https://doi.org/10.3233/978-1-61499-495-4-246
Publication status	Published - 2015
Event	Marktoberdorf Summer School - Marktoberdorf, Germany Duration: 29 Jul 2014 → 10 Aug 2014

Publication series

Name	NATO Science for Peace and Security Series, D: Information and Communication Security
Publisher	IOS Press
Volume	40

Conference

Conference	Marktoberdorf Summer School
Country/Territory	Germany
City	Marktoberdorf
Period	29/07/14 → 10/08/14

Access to Document

10.3233/978-1-61499-495-4-246

Cite this

@inbook{b3936b70d4514b4e8f85fd9717f361c9,

title = "Mechanised Theory Engineering in Isabelle",

abstract = "This is an introduction to mechanised theory engineering in Isabelle, an LCF-style interactive theorem prover. We introduce an embedding of Hoare & He's Unifying Theories of Programming (UTP) in Isabelle (named Isabelle/UTP) and show how to mechanise two key theories: relations and designs. These theories are sufficient to give an account of the partial and total correctness of nondeterministic sequential programs and of networks of reactive processes. A tutorial introduction to each theory is interspersed with its formalisation and with mechanised proofs of relevant properties and theorems. The work described here underpins specification languages such as Circus, which combines state-rich imperative operations, communication and concurrency, object orientation, references and pointers, real time, and process mobility, all with denotational, axiomatic, algebraic, and operational semantics.",

author = "Foster, {Simon David} and Jim Woodcock",

year = "2015",

doi = "10.3233/978-1-61499-495-4-246",

language = "English",

isbn = "978-1-61499-494-7",

volume = "40",

series = "NATO Science for Peace and Security Series, D: Information and Communication Security",

publisher = "IOS Press",

pages = "246--287",

editor = "Maximilian Irlbeck and Doron Peled and Alexander Pretschner",

booktitle = "Dependable Software Systems Engineering",

address = "Netherlands",

note = "Marktoberdorf Summer School ; Conference date: 29-07-2014 Through 10-08-2014",

}

Foster, SD & Woodcock, J 2015, Mechanised Theory Engineering in Isabelle. in M Irlbeck, D Peled & A Pretschner (eds), Dependable Software Systems Engineering. vol. 40, NATO Science for Peace and Security Series, D: Information and Communication Security, vol. 40, IOS Press, pp. 246-287, Marktoberdorf Summer School, Marktoberdorf, Germany, 29/07/14. https://doi.org/10.3233/978-1-61499-495-4-246

Mechanised Theory Engineering in Isabelle. / Foster, Simon David ; Woodcock, Jim.
Dependable Software Systems Engineering. ed. / Maximilian Irlbeck; Doron Peled; Alexander Pretschner. Vol. 40 IOS Press, 2015. p. 246-287 (NATO Science for Peace and Security Series, D: Information and Communication Security; Vol. 40).

Research output: Chapter in Book/Report/Conference proceeding › Chapter

TY - CHAP

T1 - Mechanised Theory Engineering in Isabelle

AU - Foster, Simon David

AU - Woodcock, Jim

PY - 2015

Y1 - 2015

N2 - This is an introduction to mechanised theory engineering in Isabelle, an LCF-style interactive theorem prover. We introduce an embedding of Hoare & He's Unifying Theories of Programming (UTP) in Isabelle (named Isabelle/UTP) and show how to mechanise two key theories: relations and designs. These theories are sufficient to give an account of the partial and total correctness of nondeterministic sequential programs and of networks of reactive processes. A tutorial introduction to each theory is interspersed with its formalisation and with mechanised proofs of relevant properties and theorems. The work described here underpins specification languages such as Circus, which combines state-rich imperative operations, communication and concurrency, object orientation, references and pointers, real time, and process mobility, all with denotational, axiomatic, algebraic, and operational semantics.

AB - This is an introduction to mechanised theory engineering in Isabelle, an LCF-style interactive theorem prover. We introduce an embedding of Hoare & He's Unifying Theories of Programming (UTP) in Isabelle (named Isabelle/UTP) and show how to mechanise two key theories: relations and designs. These theories are sufficient to give an account of the partial and total correctness of nondeterministic sequential programs and of networks of reactive processes. A tutorial introduction to each theory is interspersed with its formalisation and with mechanised proofs of relevant properties and theorems. The work described here underpins specification languages such as Circus, which combines state-rich imperative operations, communication and concurrency, object orientation, references and pointers, real time, and process mobility, all with denotational, axiomatic, algebraic, and operational semantics.

U2 - 10.3233/978-1-61499-495-4-246

DO - 10.3233/978-1-61499-495-4-246

M3 - Chapter

SN - 978-1-61499-494-7

VL - 40

T3 - NATO Science for Peace and Security Series, D: Information and Communication Security

SP - 246

EP - 287

BT - Dependable Software Systems Engineering

A2 - Irlbeck, Maximilian

A2 - Peled, Doron

A2 - Pretschner, Alexander

PB - IOS Press

T2 - Marktoberdorf Summer School

Y2 - 29 July 2014 through 10 August 2014

ER -