Model Based System Development/Research Themes/Embedded and Distributed Systems

Embedded Systems

In order to validate the effectiveness of our basic technologies and to get inspiration for further research, we apply them to challenging industrial applications. Embedded systems constitute a natural application area for the technologies developed within our group, in particular for computer-aided verification and analysis. Crucial for our work in this area is the collaboration with the Embedded Systems Institute (ESI), a research organization founded in 2002 by the three Dutch technological universities and a number of companies. Two members of our group, Jozef Hooman and Jan Tretmans work four days per week as research fellow at ESI and one day per week at our institute. ESI acts as coordinator of research projects in embedded systems in which industry and universities collaborate following an industry-as-laboratory approach.

The industry-as-laboratory approach.

Our group particpates (or has participated) in three of these projects (Boderc, Octopus and Tangram). Another rich source of case studies are some European projects (VHS, OMEGA, AMETIST, QUASIMODO) in which our group is (or has been) involved. Within these projects the industrial partners provided challenging problems for us to work on. Finally, we have informal contacts and ad-hoc research collaborations with a large number of companies, for instance through Master's Thesis projects.

Co-simulation

Our research in this area took place within the ESI Boderc project. Within this project, Océ was the leading industrial partner. The projects's objective was to develop multi-disciplinary, model based techniques and methods for early design exploration of high-tech systems. We extended an existing formal semantic framework for discrete event models to allow for consistent co-simulation of continuous time models from within this framework. It enables integrated models that can be checked by simulation in addition to the verification and validation techniques already offered by each discipline individually. The level of confidence in the design can now be raised in the very early stages of the system design life-cycle instead of postponing system-level design issues until the integration and test phase is reached. We demonstrate the extended semantic framework by co-simulation of VDM++ and bond-graph models on two case studies:

• Embedded control of a printer paper path (2007-2009)
• Level control of a water tank (2007)

Océ expressed great satisfaction with the results of the Boderc project: it brought them both useful, specific results and promising general directions. For example, Orbons states that the "Happy flow" modeling approach from Boderc has enabled Océ to skip a complete physical machine-build iteration cycle, saving many man-years of effort [Boderc]. Verhoef states that Chess has explicitly implemented the innovative processes from Boderc in their business model [Verhoef].

Performance Evaluation of Embedded Architectures

Another contribution to the Boderc project has been the development of techniques to model and evaluate the performance of embedded system architectures. In joint work with the group of prof. Lothar Thiele at ETH Zurich, a number of state-of-the-art performance evaluation methods and tools were put to test on a simple case study that has been inspired by industrial practice:

• Architecture evaluation for a distributed in-car radio navigation system of Siemens VDO (2006)

This was the first time that such a quantitative comparison was performed on a single case study at this scale. As the only tool, Uppaal was able to compute the exact best and worst case execution times, with as a price that Uppaal does not scale so well. Our work on comparing performance models was continued with a significantly larger scope involving more case studies and additional tools by subsequent work at ETH Zurich.

Combining Formal Methods and UML

To connect formal approaches to industrial practice, the combination of formal methods and UML has been studied in EU-IST project Omega (Correct Development of Real-Time Embedded systems in UML). A formal semantics of a UML kernel has been defined in PVS and the verification of UML models by means of PVS has been studied. A part of the MARS system (Medium Altitude Reconnaissance System) from the NLR (National Aerospace Laboratory) has been selected as a common real-time embedded application within the OMEGA project. This industrial case study has been used to illustrate interactive verification supported by the PVS theorem prover. In addition, a comparison has been made with other techniques applied that have been applied to the MARS case study, such as Live Sequence Charts, the UVE tool for model checking of functional properties, and the IFx tool for timed model checking. [HoomanEtAl2008].

Analysis and Synthesis of Controllers

Within our group we have done a limited number of case studies on analysis and synthesis of controllers. Although we obtained some nice results, this is not a primary topic of research for us at the moment.

• Deadlock avoidance and throughput optimization for a wafer scanner from ASML (2004)
  We use the SMV model checker to synthesize a deadlock avoidance policy for a new EUV wafer scanner from ASML, and Uppaal to optimize the throughput of this machine. Our results are referred to in patent application ASML ref. P-1784.010.
• Analysis of a car periphery supervision (CPS) system from Bosch (2004)
  We present a formal model of the real-time service allocation unit for the Car Periphery Supervision (CPS) system - a case study proposed by Robert Bosch GmbH. The CPS system is a hybrid system but by overapproximating this behavior, we manage to verify some safety properties using Uppaal.
• Control of a Lego car (2003)
  We model and analyze the behavior of a simple Lego car with caterpillar treads using the hybrid I/O automata framework.
• Control synthesis for a smart card personalization system from Cybernetix (2003)
  Using the Cadence SMV model checker we synthesize, under certain error assumptions, a scheduler for the smart card personalization system, a case study that has been proposed by Cybernetix. The controller that we synthesize automatically, and of which we prove optimality, has been previously patented by Cybernetix.
• Design of a PLC control program for a chemical batch plant (2002)
• The Advanced Automatic Train Control (AATC) system for the Bay Area Rapid Transit (BART) system (2001)
• A light control system (2000)

Scheduling Related Problems

Scheduling and resource allocation problems occur in many different domains, for instance (1) scheduling of production lines in factories to optimize costs and delays, (2) scheduling of computer programs in (real-time) operating systems to meet deadline constraints, (3) scheduling of micro instructions inside a processor with a bounded number of registers and processing units, (4) scheduling of trains (or airplanes) over limited quantities of railway tracks and crossroads, and (5) mission planning for autonomous robots on spacecrafts. Typically, in each of these domain problems are solved using different approaches and mathematical tools. The EU IST AMETIST project, that we coordinated, has provided the foundations for a unifying framework for time-dependent behavior and dynamic resource allocation that crosses the boundaries of application domains.

In the AMETIST approach, components of a system are modeled as dynamical systems with a state space and a well-defined dynamics. All that can happen in a system is expressed in terms of behaviors that can be generated by the dynamical systems; these constitute the semantics of the problem. Verification, optimization, synthesis and other design activities explore and modify system structure so that the resulting behaviors are correct, optimal, etc. Preferably, the limitations of currently known computational solutions should not influence modeling too much: only after the semantics of a problem is properly understood, abstractions and specialization due to computational considerations can intervene. In such situations, the soundness of abstractions should ideally also be proved, either via deductive verification or model checking. AMETIST has shown that this approach, which underlies the successful domain of formal verification, can be extended to resource allocation, scheduling and other time-related problems.

• Within the Octopus project we study the design of the datapath of printers/copiers at Oce. The datapath encompasses the complete trajectory of the image data from source (for example the network) to target (the imaging unit). Runtime changes in the environment (such as the observed image quality) may require the use of different algorithms in the datapath, deadlines for completion of computations may change, new jobs may suddenly arrive, and resource availability may change. To realize this type of behavior in a predictable way is a major challenge. We apply Uppaal to derive schedules for multiple concurrent jobs in the presence of limited resources [FORMATS08].
• Scheduling lacquer production by reachability analysis -- a case study for Axxom (2005)
  For this specific case study, our model checking technology outperformed the tools of Axxom Software AG, a company that specializes in value chain management.
• Scheduling of a steel plant for Sidmar (1999)
  This case study by our PhD student Ansgar Fehnker solved a problem posed by Sidmar and was the starting point for developing the Uppaal Cora tool within the context of AMETIST.

Model Based Testing

 Tangram.

Distributed Algorithms and Protocols

We use (extensions of) model-checkers and interactive theorem provers for the verification of complex real-time and fault-tolerant distributed algorithms and protocols. Part of our research in this area is supported by the NWO project FRAAI and the FP7 project Quasimodo. Case studies are provided by industrial partners in projects, organizations such as NLnetsLabs, or just taken from the literature. Our goal is to push forward the range of applicability of formal methods. As a tangible result of our analysis efforts, we discovered many errors and ambiguities in industrial communication protocols, and thus helped to improve the quality of these protocols. Tool support is mainly obtained by the use of interactive theorem provers (such as PVS, Isabelle/HOL and ACL2), and model checkers (such as Uppaal, Murphi, NuSMV, Spin and PRISM). We take a pragmatic approach and use whichever tools that are most suited to do the analysis. Frequently, we benefit from using combinations of theorem provers and model checkers. Using state-of-the-art model checking and theorem proving technology, we regularly manage to analyze protocols which, just a few years before, would have been far too complex for formal analysis. Several case studies that were carried out by our team have become standard benchmarks in the verification literature.

Case studies that we have carried out during recent years include:

• Zeroconf, a protocol for self configuration of IPv4 network interfaces (2003-2009)
  In our initial work [IPDS03] we answered a question posed by Philips Research concerning the tradefoff between configuration time and error probability. Subsequent modeling and analysis with Uppaal revealed several errors (or at least ambiguities) in this protocol, which has been standardised in RFC 3927 of the IETF.
• The impact of GSM-R on railway capacity (2008)
  ERTMS (EuropeanRail Traffic Management System) is a project launched by the European Union in order to increase the interoperability of the national railway systems in Europe. One of the two main components of ERTMS is GSMR, a wireless communication standard based on GSM.In this case study, we focus on the stochastic nature of GSM-R communication failures and their possible impact on railway capacity.
• A method for automatic renewal of trust anchors (RFC 5011) (2008)
  Case study illustrating that we have reached the point where MSc students can succesfully apply the Uppaal model checker to complex protocols in the context of small research projects.
• A generic model for formally verifying network on chip communication architectures (2007)
  A generic formal model for NoC's has been developed and implemented in the ACL2 theorem prover. As an application, the HERMES network has been formalized in this model, and we show that both formal proofs and simulation experiments can be performed in ACL2.
• Asynchronous transmission at the gate level in the FlexRay protocol (2007)
  This is the first verification effort tackling asynchronous transmissions at the gate-level. Analog considerations are formalized in the logic of the Isabelle/HOL theorem prover. Digital arguments are discharged using the NuSMV model checker.
• The intrusion-tolerant group communication protocol Enclaves (2007)
  We use the model checker Murphi to prove the correctness of authentication, and the interactive theorem prover PVS to formally specify and verify Byzantine agreement, termination of agreement, and integrity.
• SHIM6, an internet protocol supporting host-based multihoming (2007)
  This Uppaal case study revealed several errors in the SHIM6 protocol that were not spotted before and that were difficult to derive from the protocol specification. These errors have been corrected in the new version of the internet draft.
• A Biphase Mark Protocol implementation from Intel (2006)
  Based on the derived parameter constraints we propose instances of BMP that are correct (at least in our model) but have a faster bit rate than the instances that are commonly implemented in hardware by companies such as Intel.
• Bluetooth inquiry phase (2006)
  We used Uppaal to verify for a variety of situations that indeed eventually two devices will find each other. Furthermore we used the modeling process as a way to find some incorrect statements in the Bluetooth specification.
• Aethereal guaranteed-throughput router for networks on chip (2005)
  We present a formal specification using PVS of the Aethereal protocol from Philips/NXP for networks on chip. Using PVS, we prove absence of deadlock for an abstract version of our model.
• Distributed agreement protocol of Attiya, Dwork, Lynch and Stockmeyer (2005)
  This algorithm belongs to the class of partially synchronous distributed systems, which is considered very difficult to analyze using model checkers. We show that the algorithm can easily be modeled with the Uppaal model checker and that it is possible to analyze some interesting and non-trivial instances with reasonable computational resources. This is the first mechanical verification of (instances of) this algorithm.
• A randomized wait-free consensus protocol (2005)
  Algorithm designed by Ling Cheung as part of her PhD work. Instances of the protocol are model checked using PRISM.
• Sliding window protocol (2003)
  A signifcant case study in which we apply PVS for the modeling and verification of a well-known protocol. Our modelling is very general and includes such important features of the protocol as sending and receiving windows of arbitrary size, bounded sequence numbers and channels that may lose, reorder and duplicate messages.
• Distributed real-time arbitration protocol of the IEEE 896 Future bus specification (2003)
  A small case study in applying PVS to protocol verification.
• Non-blocking atomic commitment protocol of Babaoglu and Toueg (2000)
  All safety and liveness properties, including a new improved termination property, have been proved with the interactive proof checker of PVS. We also show that the original termination protocol of Babaoglu and Toueg has an error.
• IEEE 1394 ("Firewire") tree identify protocol (2000)
  Also this PVS case study has become a standard benchmark in the area of protocol verification.
• IEEE 1394 ("Firewire") root contention protocol (1999).
  This case study has become a standard benchmark in the area of probabilistic model checking.
• HAVi leader election protocol (1999).
  Another significant consumer electronics protocol, used by Philips. Analysed by Judi Romijn as part of her PhD work using the model checkers Spin and Caesar/Aldebaran. It turns out that the protocol does not meet some safety properties and there are situations in which the protocol may never converge to designate a leader.
• Enhanced Easylink audio control protocol with bus collisions (1996,2002)
  A consumer electronics protocol developed by Philips. One of the first significant case studies with the Uppaal tool, carried out by David Griffioen as part of his PhD work, in collaboration with the Uppaal team. In their 1996 ACM Computing Survey paper, Clarke and Wing write about this work "In 1996, Bengtsson and his colleagues model checked the entire protocol, thus completing the quest of fully automating a human proof that as little as two years ago was considered far out of reach for algorithmic methods".
• Philips Audio Control Protocol (1994).
  For this case study, which we carried out for Philips Electronics, we received the FTRTFT'94 best paper award. It has become a benchmark for timed and hybrid automata model checkers.
• Bounded Retransmission Protocol (1994).
  Our paper presents the first formal model and verification (using the proof assistent Coq) of this protocol from Philips Electronics, which has become a benchmark for computer-aided verification (both model checking and theorem proving).