The dependability of high-volume embedded systems, such a consumer electronic devices, is threatened by a combination of quickly increasing complexity, decreasing\ntime-to-market, and strong cost constraints. This poses challenging research questions that are investigated in the Trader project, following the industry-as-lab approach. We\npresent the main vision of this project, which is based on a model-based control paradigm, and the current status of the project results.

Mobile health systems can extend the enterprise computing system of the healthcare provider by bringing services to the patient any time and anywhere. We propose a model-driven design and development methodology for the development of the m-health components in such extended enterprise computing systems. The methodology applies a model-driven design and development approach augmented with formal validation and verification to address quality and correctness and to support model transformation. Work on modelling applications from the healthcare domain is reported. One objective of this work is to explore and elaborate the proposed methodology. At the University of Twente we are developing m-health systems based on body area networks (BANs). One specialization of the generic BAN is the health BAN, which incorporates a set of devices and associated software components to provide some set of health-related services. A patient has a personalized instance of the health BAN customized to their current set of needs. A health professional interacts with their patients' BANs via a BAN professional system. The set of deployed BANs are supported by a server. We refer to this distributed system as the BAN System. The BAN system extends the enterprise computing system of the healthcare provider. Development of such systems requires a sound software engineering approach and this is what we explore with the new methodology. The methodology is illustrated with reference to modelling activities targeted at real implementations. In the context of the awareness project BAN implementations are tested in a number of clinical settings including epilepsy management and management of chronic pain.

Object-based distributed computing is now a well established technique for constructing large, heterogeneous computing and telecommunications systems. Indeed, standards bodies and consortia such as, ITU, ISO, OMG, TINA-C, etc., have all defined distributed object-based frameworks as a foundation for open distributed computing.

This paper presents a process algebra for specifying soft real-time constraints in a compositional way. For these soft constraints we take a stochastic point of view and allow arbitrary probability distributions to express delays of activities. The semantics of this process algebra is given in terms of stochastic automata, a variant of timed automata where clocks are initialised randomly and run backwards. To analyse quantitative properties, an algorithm is presented for the on-the-fly generation of a discrete-event simulation model from a process algebra specification. On the qualitative side, a symbolic technique for classical reachability analysis of stochastic automata is presented. As a result a unifying framework for the specification and analysis of quantitative and qualitative properties is obtained. We discuss an implementation of both analytic methods and specify and analyse a fault-tolerant multi-processor system.

This paper discusses stochastic extensions of a simple process algebra in a causality-based setting. Atomic actions are supposed to happen after a delay that is determined by a stochastic variable with a certain distribution. A simple stochastic type of event structures is discussed, restricting the distribution functions to be exponential. A corresponding operational semantics of this model is given and compared to existing (interleaved) approaches. Secondly, a stochastic variant of event structures is discussed where distributions are of a much more general nature, viz. of phase-type. This includes exponential, Erlang, Coxian and mixtures of exponential distributions.