|
|
|
|
|
Current projects:
The group welcomes any inquiries about the research we do. Click here for information about the various projects in the group.
Click here for contact information.
A statement of the groups research interests can be found as part on the On-line Heriot Watt Postgraduate Prospectus.
Dependable Systems Research Group
The dependability of computer systems may be analysed according
to many properties, such as reliability, predictability,
safety and security. Dependable systems research, by its very nature,
is a multi-disciplinary activity. Within the Dependable Systems
Group at Heriot-Watt our activities build upon a number of
complementary areas of research, as summarised below:
- Functional prototyping is the basis for our investigations
of functional environments, tools and methodologies for parallel and
distributed programming using both strict and lazy languages.
A pure, strongly typed, functional program is more likely to be correct
because it is clear, concise, and amenable to both proof and
transformation. The properties make functional languages
ideal for constructing prototypes. In addition to the
conventional benefits of prototypes, functional prototypes
typically greatly simplify the design of the final product. Specific areas
where we apply these techniques are in computer vision, for example for
matching 2D images to 3D models, and data-intensive applications, for
example to analyse traffic data for accident black spots.
- Formal verification builds upon methods of mathematical logic
and complements the traditional approaches to system verification,
such as prototyping and testing. We are interested in the development
of systems which automatically prove mathematical theorems. Such systems
represent an enabling technology for formal verification. Our goal is
to develop theorem provers which are aligned to the needs of system
designers. To achieve this goal we are focusing on techniques which
increase the scope of automation while at the same time facilitate
high-level interaction. We build upon proof plans, a technique
which provides a structured and transparent basis for building theorem
provers. A principal theme of our work is the automatic use of failure
during formal verification. Failure analysis plays a crucial role
in any creative process, such as system design. It is the nature
of the proof plans technique which enables us to achieve this kind
of automation.
- Practical techniques for estimating the performance of computer and
communication systems form a major strand of interest in our work. We
believe that it is naive to expect a system to behave correctly in
purely functional terms and, therefore, that quantitative
understanding is also essential.
The techniques we use include, measurement of systems, simulation at a
detailed level and a variety of analytic and numerical techniques. The
latter include queueing networks, stochastic Petri nets and stochastic
process algebras. These are all different forms of stochastic model,
where probability distributions are used to represent
non-deterministic and data dependent aspects of systems. Our view is
that tools and techniques must be adapted to suit the needs and
understanding of designers.
We have recently begun to examine how some of these modelling
techniques might be exploited in Computer Aided Software Engineering
tools, based around the emerging industry standard object oriented
design language, UML.
The demand for highly dependable computer systems is ever increasing,
in particular within the avionics and semiconductor (System-On-Chip)
industries. Tools which enhance our ability to understand and predict
the behaviour of complex computer systems are therefore essential in
order to meet this demand.
|
|
