DERty UML

Print

Model Driven Development (MDD) of embedded systems is a challenging topic currently in the focus of academia and industry. Based on principles of the Model Driven Architecture (MDA), MDD supports design reuse by employing high-level modeling and specification languages. These languages allow the description of the main aspects of embedded systems at higher levels of abstraction and, at the same time, realize a decoupling of system properties from the implementation platform. One such language is the Unified Modeling Language (UML).

A challenging topic in the context of MDD of embedded systems is the domain-specific application of UML towards the modeling, analysis, and synthesis of System-on-Chip (SoC) solutions. To investigate UML in this context, in 2004 we started the UML for SoC Design workshop at the Design Automation Conference in cooperation with Cadence Berkeley Labs. The workshop was conducted for the third time in 2006. Meanwhile, it is recognized as the international forum to discuss and present new developments in the application of UML to C/C++-based modeling for electronic and embedded systems. From this, an area of research has emerged, aiming at industrial application of domain-specific UML refinement, like, e.g., the SoC profile and the SysML (System Modeling Language). Further activities in this area are performed in cooperation with 16 leading European semiconductor companies, e.g., ARM, Infineon, NXP, and ST Microelectronics, through the EU funded project SPRINT (Open SoC Design Platform for Reuse and Integration of IPs). The focus of the project is on the realization of a common view on IP management through UML based on IEEE SystemC and SPIRIT IP-XACT.

Further technical activities in this area are in cooperation with the working group of Prof. Engels (Department of Computer Science) and mainly investigate executable UML 2.0 specifications. For executable UML, we have defined a UML subset with a well-defined semantics applying a specific set of diagrams and an action language. Here, our main interest is also on the domain of embedded and electronic systems with their specific properties like their real-time behavior. For their specification, we apply class diagrams as structural means and a combination of activity, sequence, and state machine diagrams for behavioral descriptions. For our application domain, we also extend state machines by additional basic concepts, like interrupts and timeouts. In this context, we currently investigate the application of activity diagrams for description of fine-grained parallelism based on a platform independent execution on a UML Virtual Machine (UVM).


Detailed Information

Validation and Verification

Another very challenging topic in the context of MDD of embedded systems is the development of efficient validation and verification techniques, which are capable of supporting the verification of models of an embedded system at different levels of abstraction. Our research in this field mainly focuses on the systematic application of various formal techniques for system specification, modeling, and verification. One of our goals is the integration of such techniques into the model driven development process of complex distributed real-time embedded systems. In particular, we consider executable specifications, UML formalization, semantic integration of heterogeneous specification techniques and languages, and application of methods to support functional verification of distributed systems under real-time and safety-constraints. These topics are investigated in the scope of the BMBF funded IMMOS project and Sonderforschungsbereich (SFB) 614, focusing on automotive systems and on self-optimizing mechatronic multi-agent systems, respectively.

Systematic Testing

In cooperation with DaimlerChrysler and dSPACE a uniform test-exchange format based on XML (TestML) was developed for model-based testing, which supports, e.g., time-based signal descriptions, matching signal patterns in automotive electronics. The TestML greatly supports the interoperability between diverse testing tools for testbench generation in the context of software-in-the-loop, as well as, hardware-in-the-loop testing methods. Further research focused on extension of the classification tree method for embedded systems (CTM/ES), by additional facilities for the description of waveform properties and of events, as well as an extension for the specification of functional coverage. The research was conducted within the IMMOS project and continued in SFB 614 subproject B3.

Online-Verification

By integrating formal specification and formal verification into the design phase of a system development process, the correctness of a system can be guaranteed to a great extent, but this approach may not be efficient for every kind of system. A mechatronic system, e.g., an automotive system, can be extended towards a self-optimizing system that needs to dynamically exchange its components in a safe and consistent manner. The SFB 614 project is dealing with an approach to develop such self-reflecting, self-adapting, and self-optimizing complex mechatronic systems, which represent a special class of complex cross-domain electronic and mechanic systems. In SFB 614 subproject C2, we focus on self-optimizing real-time applications with highly dynamic software components, which are optimized and even replaced at runtime. Safety and predictability is of paramount importance, as failures of these technical systems usually have severe consequences.

This puts new demands on verification of such complex and highly dependable systems. Therefore, in the second phase of SFB 614 C2, we develop a novel technique for on-line model checking context-specific parts of components at runtime and thus offer this verification as a service of the underlying Real-Time Operating System (RTOS). The real-time constraints make it necessary to perform the on-line model checking at the level of (UML) models, where any non context specific internals of components have been verified off-line at design phase.

The verification is performed at the level of models (RT-UML) developed according to the design technique presented in the first phase of the SFB 614 project B1. The properties to be checked are expressed by RT-OCL terms where the underlying temporal logic is restricted to the time-annotated ACTL/LTL formulae. The applied technique is based on improved bounded model checking. The on-line model checking runs interleaved with the execution of the component to be checked in a pipelined manner via the RTOS as intermediary. As a result, potential faults caused by a run-time reconfiguration of the system can be predicted ahead of time and thus enable the system to recover within minimum time to a safe mode.