Specification and Analysis of Embedded Systems

Leader of the group Specification and Analysis of Embedded Systems (SEN2): Paul Klint

The goal of this theme is to develop techniques that allow to increase the quality of software by employing a whole range of analysis techniques. Typically we study the development and use of proof methodologies, proof checkers and generators, test and visualisation techniques to effectively establish correctness of distributed, embedded and real-time systems. We use the language µCRL (micro Common Representation Language) as a testbed to carry out experiments, and implement many of our experiences in the µCRL toolset , which is publicly available. Other tools that we use are the model checker SPIN, the timed model checkers UPPAAL and KRONOS, the proof checker PVS, and the test tool TorX.

The TT-Medal project in which SEN2 took part won the ITEA Achievement Award 2005.

Members

Drs. J.R. Calame, T. Chen, Dr. F. Dechesne, Prof.dr. W.J. Fokkink, Prof.dr.ir. J.F. Groote,
Drs. B. Lisser, Dr. Y.S. Usenko, Drs. Y. Wang

Key publications

J.F. Groote and M.A. Reniers. Algebraic Process Verification.In Bergstra, Ponse and Smolka, editors, Handbook of Process Algebra. Elsevier, 2000.
J.F. Groote and J.C. van de Pol.State space reduction using partial tau-confluence.In M. Nielsen and B. Rovan, eds, Proceedings 25th Symposium on Mathematical Foundations of Computer Science (MFCS'2000), Bratislava, Slovakia, LNCS 1893, pp. 383-393. Springer-Verlag, 2000.
W.J. Fokkink. Introduction to Process Algebra.Texts in Theoretical Computer Science (an EATCS Series). Springer-Verlag, 2000.

Group publications

Publications in CWI repository