This research is on integration of models for design of dependable, software-intensive embedded systems, trying to bring together existing modeling methods from the formal methods domain and the mechatronics / robotics domain. It is not to be expected that there is one single unifying semantic formalism for all different models, either because it may not exist, or because it is too complex. One alternative way of integration is co-simulation. The work focusses on semantic integration, algorithmic support, i.e. transformations to integrate model parts, and methods in the form of a way of working. Work done together with the CS-groups FMT and SE.

Results 2013

Separation of concerns, namely platform-independent control versus platform-dependent implementation issues have been studied. This separation is an essential assumption of model-based control software design, as models are developed independent from the execution platform, and the implementation is obtained via automated code generation. Each concern requires domain-specific techniques: control engineering domain-specific modeling and analysis versus computer engineering focused implementation techniques where reliability an real-time constraints are key issues. The contract-oriented description for embedded systems is being used as a way to structure descriptions.

Results 2012

Timing aspects of embedded control software has been studied. A framework has been formulated to analyse schedulability of CSP-based designs for non-preemptive fixed-priority multiprocessor scheduling. The framework is based on the PAT model checker and the analysis is done with dense-time model checking on timed CSP models. We also provide a schedulability analysis workflow to construct and analyse, using the proposed framework, a timed CSP model with scheduling from an initial untimed CSP model without scheduling. It is demonstrated using a case study of control software design for a mobile robot.

Results 2011

Timing aspects of the little line-following robot have been studied. Analysis of timing is being formulated in timed CSP using the analysis tool PAT.

Results 2010

Both bond graphs and hybrid state machines have been studied. A pilot study (little line-following robot) has been conducted using 20sim and Uppaal. Currently, the models are not yet combined, i.e. each model describes different but relevant aspects of the pilot study.

Project lead

no picture available Jan Broenink