| |
Concurrent and distributed
systems have increasingly
become an active area of research and development. This is an
inevitable consequence of the realisation that many problem areas, such
as the design of VLSI systems, telecommunications systems, and
real-time control systems, are inherently concurrent in nature.
Similarly, on the applications side, many enterprises and organisations
are cooperative in nature, eg. offices, companies, universities, etc.,
requiring the exchange and sharing of information and resources over a
geographically distributed and loosely coupled system. Distributed
computer systems better match the requirements of such organisations
than conventional centralised computer systems. However, distributed
computer systems are extremely complex artefacts and hence the use of
formal design and analysis techniques is common. This course will
introduce these techniques.
Course Coverage
The aim of the course is to
introduce the concepts,
theory, formal notations and programming languages which are necessary
to understand, analyse, design and build concurrent and distributed
systems. Firstly, the model checking approach is introduced. Here, you
build an automaton model of the system and specify some property in
temporal logic to be checked. Secondly, the formal theory of
Communicating Sequential Processes (CSP) is presented and used as a
descriptive and reasoning tool. Concepts, such as behaviour, complete
and partial specifications, design, design refinement, safety and
liveness properties, as well as proof of correctness are then defined
in a rigorous manner.
Several case studies, such
as communication protocols,
message passing networks, and distributed databases, will be used to
illustrate the concepts covered in the course. A set of simulation,
analysis, and formal verification tools, the CSP based tools ARC and
FDR are introduced and applied in practice. These tools are widely used
in the concurrent, safety critical, protocol system, and
telecommunications domains.
This course introduces
students to high-integrity software engineering, with a focus on the
development of safety-critical software. Lectures will cover
hazard analysis, risk analysis, safety-critical software, formal
methods, safety cases and safety management. Students are introduced to
a number of practical techniques, which are applied to a variety of
realistic examples.
The course starts by introducing a number of hazard and risk analysis
techniques, including: fault tree analysis; event tree analysis; hazard
and operability studies; and failure modes and effects analysis.
The course then introduces the notion of formal specification, using
the Z specification language.
Then the SPARK Ada language is introduced. Here we cover the general
notion of a safe subset of a programming language. Static analysis
techniques are introduced, as well as formal verification.
|
