Modeling and Validating Distributed Embedded Real-Time Control Systems

• promotor: prof. dr. Frits Vaandrager
• co-promotor and thesis supervisor: dr. Jozef Hooman
• hora est: 21 january 2009

Abstract

The development of complex embedded control systems can be improved significantly by applying formal techniques from control engineering and software engineering. It is shown how these approaches can be combined to improve the design and analysis of high-tech systems, both in theory and practice. The semantics of the integration of two established rigorous techniques has been defined formally in this work. The strength of this integrated semantics is demonstrated by means of application to a significant industrial case study: the embedded control of a printer paper path, whereby the full development life-cycle from model to realization is covered. The resulting model-driven design approach fits the current engineering practice in industry and is both flexible and effective.

Download the manuscript and related publications

Download the camera ready version of my dissertation and the propositions (or stellingen, in Dutch). If you would like to receive a printed copy of my thesis, please send me an e-mail .

Have a look at the not-quite-10-minute summary. Some pictures of the defence ceremony can be found here. Also check-out the article which appeared in Bits & Chips magazine on 23 January 2009 (in Dutch). Are you interested in (embedded) systems architecture related research? Please have a look at the Gaudi System Architecting web-site.

The models and tools described in the dissertation

• The MPA models of the in-car radio navigation system presented in Chapter 2, can be found on the RTC toolkit home page. More information on MPA models can be found here.
• UPPAAL models of the in-car radio navigation system presented in Chapter 2.
• MSc thesis of Menno de Hoon, describing the POOSL models of the in-car radio navigation case study presented in Chapter 2. The models can be found here.
• The Timed VDM++ (VICE) model of the in-car radio navigation system as presented in Chapter 2.
• PVS models of the extended VDM++ operational semantics presented in Chapter 3.
• The 20-sim watertank model and the VDM++ controller model from Chapter 5.
• The VDM++ paper path model from Chapter 6.
• The 20-sim paper path SIL model from Chapter 6.

• UPPAAL can be found here.
• SHESim / POOSL can be found here.
• PVS can be found here.
• VDMTools can be found here.
• 20-sim can be found here.

Note: none of these models are actively maintained. Check-out the Overture project, which aims at developing open-source plugins for Eclipse to support VDM++.

Academic review

The manuscript committee was formed by:

• prof. dr. Bart Jacobs (chair)
• prof. dr. Lothar Thiele (ETH Zurich, Switzerland)
• prof. dr. ir. Peter Gorm Larsen (Engineering College of Aarhus, Denmark)
• dr. ir. Jan Broenink (University of Twente)
• dr. ir. Jeroen Voeten (ESI)

The opposition during the public defence was formed by:

• prof. dr. ir. Peter Gorm Larsen (Engineering College of Aarhus, Denmark)
• dr. John Fitzgerald (University of Newcastle, United Kingdom)
• prof. dr. Gerrit Muller (ESI and Buskerud University College, Norway)
• dr. ir. Jan Broenink (University of Twente)
• dr. ir. Jeroen Voeten (ESI)
• prof. dr. Frank de Boer (University of Leiden)
• prof. dr. Bart Jacobs (Radboud University)

Cover design by Silvian de Jager