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/
