Specification and Analysis of Embedded Systems
by Henk Nieland
In order to increase the quality of software components that are
typically found in telecommunication and embedded systems, CWI studies
specification techniques for the unambiguous description of these systems,
and analysis techniques to establish that their implementations exhibit
the expected functionality. Viability assessment is made through experiments
with fundamental distributed algorithms and concrete industrial application.
The research contains a healthy mix of theoretical study and practical
application.
Ever more computers are embedded within real-world technical applications,
for example in avionics, process control, robotics, telecommunications
and consumer products. The quality of the installed software is crucial
for their proper functioning. Several of these applications require the
software to operate in real-time and in a distributed environment. Given
the ever increasing size and complexity of such systems, high demands are
made upon the correctness of the embedded software.
The road to correct software starts with a specification of the problem,
which provides criteria for the program to be designed. The program is
called 'correct' if these criteria are satisfied. The criteria are formulated
in a specification language which is kept preferably on a high abstraction
level and, for example, need not be executable. In algebraic specifications
axioms provide rules for simplification of expressions and fix the semantics
of the algebraic constructions. Such formal methods are increasingly used
in the specification of complex systems. They have the advantage that all
assumptions are made explicit in an early design phase, thus avoiding
errors that can be extremely costly to detect and repair at later stages
of product development.
The advent of distributed computer systems and parallel computation
created a need for new specification techniques in order to deal with,
eg, synchronization problems. A promising approach is the use of process
algebra in which concurrent processes can be formally described. CWI made
important contributions to the development of process algebra and of the
specification language mCRL (micro Common Representation Language) based
on it.
Current theoretical research at CWI is directed at a real-time extension
of mCRL. Its expressivity is studied in applications. In particular the
effectiveness of using formal methods is demonstrated and assessed by the
validation of (critical parts of) the software for selected applications
from within Philips, including the future generation of IC's. In addition,
CWI participates in a project at Philips, in which the system compliance
is studied of the DVB (Digital Video Broadcast) source decoder (still under
development). CWI's part consists of the development and execution of the
conformance tests by means of logical models and extended finite-state
models, to be derived from the relevant standards and system documentation.
Furthermore, there is an ongoing involvement in the European COST 247 programme,
which focuses on the formal specification and verification, validation
and testing of software in realistic problems in contemporary distributed
communication architectures.
A second branch of activity at CWI concerns proof searching and proof
checking. The first aim is to increase the efficiency of current symbolic
techniques to verify requirements on processes by a fundamental understanding
of proof search in simple logical systems (in casu propositional logic).
Secondly, proof checking methods are developed in order to establish the
correctness of programmed systems "beyond any reasonable doubt".
A recent application is the propositional logic tool Heerhugo. Heerhugowaard
is the largest train station in The Netherlands operating with a VPI (Vital
Process Interlocking) system, which is a kind of programmable controller.
The system has to comply with several safety requirements, for example:
"trains should not derail", or: "if a signal is green, the
next one should not be red". All these requirements can be formulated
as statements in propositional logic. The check on all requirements being
satisfied is an NP-complete problem. For this particular case CWI succeeded
to construct a workable prover, Heerhugo. It turned out that, contrary
to several other cases, Dutch Rail safety systems are of very high quality.
This prover was also successfully applied to consistency checks on two
merged databases of automobile components (NedCar and Volvo).
Future research will include the study of modal logic, the development
of tools and algorithms, and a better understanding of structural properties
of distributed systems.
Please contact:
Jan Friso Groote - CWI
Tel: +31 20 592 4232
E-mail: JanFriso.Groote@cwi.nl
http://www.cwi.nl/~jfg/
