|
Courses
|
|
|
All presentation slides can be downloaded as a
gzipped archive
|
|
|
Refinement in Object-oriented
Development
|
|
Lecturer:
|
Augusto
Sampaio
|
|
|
Formal Methods Laboratory,
Centro de Informática,
Universidade Federal de
Pernambuco, Brazil
|
|
[Abstract]
[Slides 1]
[Slides 2]
[Slides 3]
|
|
|
Real-time and Fault-tolerant Systems
|
|
Lecturer:
|
Zhiming
Liu
|
|
|
IIST,
United Nations University,
Macao SAR China
|
|
[Abstract]
[Course Slides]
[Component
Based Programming Slides]
|
|
|
Concurrency: CSP and FDR
|
|
Lecturer:
|
Jim
Davies
|
|
|
Computing Laboratory,
University of Oxford,
UK
|
|
[Abstract]
[Slides 1]
[Slides 2]
[Slides 3]
[Slides 3 example]
[Slides 4]
[Slides 5]
[Exam]
|
|
|
Unifying Theories of Programming
|
|
Lecturers:
|
Jim
Woodcock
and
Ana
Cavalcanti
|
|
|
Department of Computer Science,
The University of York,
UK
|
|
[Abstract]
[Slides 1]
[Slides 2]
[Slides 3]
[Slides 4]
|
|
|
Refinement Tools:
Focus on Industrial Experience.
|
|
Lecturer:
|
Colin
O'Halloran
|
|
|
QinetiQ,
UK
|
|
[Abstract]
[Slides 1]
[Slides 2]
[Slides 3 - coming soon]
|
|
|
Refinement in Object-oriented
Development
|
|
Augusto
Sampaio
|
|
We describe refinement in the object-oriented setting, illustrating
the ideas using sequential Java, although the work is of general
applicability. The approach is algebraic: we give laws for reasoning
about and refining object-oriented programs. We discuss soundness
with respect to predicate transformer semantics, and demonstrate
completeness by showing that the set of laws is comprehensive enough
to be able to reduce any program to a normal form. Finally, they show
how their laws can be used to refactor programs, in order to adapt
their structure whilst preserving their semantics.
|
|
|
Real-time and Fault-tolerant Systems
|
|
Zhiming
Liu
|
|
We deal with refinement in real-time and fault-tolerant systems, using
transition systems as the computational model and Lamport's Temporal
Logic of Actions (TLA) as a specification language in reasoning about
functional correctness, timing properties, fault-tolerance, and
schedulability. The work is explained through an example of the
interface between a processor and a memory device.
|
|
|
Concurrency: CSP and FDR
|
|
Jim
Davies
|
|
We describe refinement of concurrent and distributed systems using the
notations of CSP. We starts by introducing CSP as a process algebra,
with a set of operators and a rich collection of laws for reasoning
about the behaviour of processes. The denotational semantics of the
language is used to give a simple notion of refinement between
processes: every behaviour of an implementation must be a specified
behaviour. These ideas are explored through an example involving
protocols and their service specifications.
|
|
|
Unifying Theories of Programming
|
|
Jim
Woodcock
and
Ana
Cavalcanti
|
|
We introduce Unifying Theories of Programming as a uniform foundation
for all these paradigms. We give a tutorial introduction to an
alphabetised version of Tarksi's relational calculus. We show how
this leads to a simple denotational semantics of a language of
terminating programs, and show that they form a complete lattice. We
extend this work to Hoare-He designs, a relational model of pre- and
postcondition specifications, exploring the space of designs as a
subtheory of relations characterised by certain healthiness
conditions. Then we turn our attention to another relational
subtheory (reactive processes) once again characterised by healthiness
conditions. Finally, we show that the reactive image of the design
lattice gives a suitable semantic model for CSP. We end by comparing
this semantics with the model given by Davies in his lectures.
|
|
|
Refinement Tools:
Focus on Industrial Experience
|
|
Colin
O'Halloran
|
|
We describe the practice of refinement in industry. They have
designed the Compliance Notation for demonstrating the refinement
relation between software and its specification. We have built a tool
to support this demonstration, an essential item for industrial-scale
application of refinement. We describe an extended example of a
correctness argument for programs written in the Spark Ada subset. We
present an application involving the correct implementation of control
laws that govern control systems.
|
|