Research Projects

Our research focuses on:

• network protocols: specification, verification, and efficient implementation,
• distributed applications:
• computer-assisted quality-assured development,
• configuration and management of distributed applications,
• integrated network and system management:
• policy- and model-based automation of technical management tasks,
• security of networks and distributed systems:
• tool-assisted security-analysis,
• trust-adapted security policy enforcement,
• automated security management.

Recent developments enclose the modular formal specification technique cTLA, a technique translating state-machine-models to efficient implementations of network protocols, control wrappers interacting with trust information services in order to secure component-structured applications, the approach of object-oriented security analysis, the automated management approach model-based management (MBM), and the Web Services server implementation Java Multi Edition DPWS Stack (JMEDS).

The MBM approach is an extension of the so-called policy-based technical network, system and application management. MBM provides the refinement of abstract high-level policy definitions into configuration descriptions and executable management rules. Its application is supported by the tool MoBaSeC (model-based service configuration) and a run-time management system. The tool performs the interactive graphical modelling of management policies and system structures. Moreover, it translates representations of abstract policies into low-level policies which are automatically enforced by the management system at runtime. The MBM approach has successfully been applied for the configuration of security services and protection mechanisms of networked systems as well as for the technical management of distributed service systems including general configuration, fault, performance, security and account management.

The JMEDS DPWS server implementation supports the light-weight implementation of service systems by means of resource-restricted devices and embedded systems. The implementation is Java-based and suitable for the Micro Java Edition. It is compliant with the OASIS standard Devices Profile for Web Services (DPWS).

MBM and JMEDS have been developed in close cooperation together with the industrial partner MATERNA, Dortmund. Both approaches will be applied in the project OSAMI, where JMEDS will be adapted to OSGi environments and support the interactions between distributed devices. MBM will form the basis of policy-controlled self-management functions which will support the adaptation of device-based service systems to changing conditions, user needs and environments.

Project Medolution

Innovative approach „Big Dependable Systems (BDS)“ und Application at the Monitoring and Control of Left Ventricular Devices (LVDs)

The current European medical system is lagging behind the emerging changes in society. An increasing portion of the population suffers from chronical diseases; people are getting older, need more medical care and consequently the healthcare costs are increasing rapidly. People wish to stay autonomous and mobile. Therefore, our society has to deal with societal and economic challenges in the medical care sector, especially in European countries.

An increase the efficiency of both reactive and proactive care and services will effectively support healthcare professionals. Therefore a large amount and variety of enriched and accurate information and tools for effective interpretation are needed. These should be based upon relevant healthcare information, extracted from data originating from diverse sources. In addition of image data and sensor data – both from medical and consumer devices – historical data from the individual person, latest medical evidence sources or existing databases containing medical study data will be sources or relevant information.

Our focus in the project is on BDS. Here, device based systems particularly perform critical medical functions and therefore have to provide dependability in a certifiable way. This has to be ensured already during design and development by two complementary approaches: On the one hand the development process has to be correspondingly aligned, on the other hand, the architecture of the system has to be suitably arranged.

In particular the device based systems have to support an high level of dependability and the interoperation with less reliable sensor networks. We develop an architecture model for device-based systems, a suite of utility functions and implementation modules as well as a suite of infrastructure services and interface definitions. The architecture shall follow the paradigm of service-orientation. Particularly it shall be accompanied by architecture design patterns supplying security, functional safety, reliability and fault-tolerance mechanisms for distributed service systems.

The project is funded by the German Federal Minister of Education and Research (BMBF).

Project BaaS

OSAMI-Commons targets open source common foundations for a dynamic service-oriented platform which is able to personalise itself in large diversity of co-operating Software Intensive Systems (SISs).
The platform makes easy what is difficult now, it facilitates seamlessly:

• Service retrieval from external centralised or distributed repositories
• Devices to connect and exchange information and services
• The connection between various vertical markets in order to allow for new business solutions

OSAMI-Commons targets open source common foundations for a reference platform building-up from the embedded system domain. Based on dynamic service-oriented programming principles it will be able to personalise itself in large diversity of co-operating Software Intensive Systems (SISs). This is achieved through technologies allowing virtualisation of SISs with a high level of abstraction (e.g OSGi and Web Services).

OSAMI-Commons will demonstrate derived benefits in the services domain and will extend service oriented solutions in vertical domains, such as healthcare..
The common architectural approach will support not only the reuse of assets across different domains but also (in run time) a cooperation framework of embedded devices for providing added value services. Deployed applications will allow seamless access to services across devices in the context of interaction domains (e.g., personal, family, social network, equipment & service provider, industrial systems ….).

Project SIRENA

The SIRENA project is an European research and advanced development project with the objective to develop a Service Infrastructure for Real time Embedded Networked Applications. SIRENA is part of the ITEA programme, itself a "cluster" organisation within the Eureka framework.

Our work focusses on security services and automated configuration management. We analyse the security and management needs of service systems and aim to technical and scientific contributions implementing scalable security services and automated administration functions. In more detail, a family of security services, components, and mechanisms shall be integrated into the middleware platform supporting the adaptation of an application's security properties to its special requirements. Moreover, since an application's security and reliability properties depend on its adequate administration, functions for the comfortable and highly automated management of applications and security services shall be developed and be implemented by means of framework components and administration tools.

Formal analysis of security properties

A method shall be developed which achieves the formal modeling of computer networks, their security mechanisms and services as well as behaviors of attackers and administration processes performing activities of technical network, system, and application management. Networks, mechanisms, services and processes are modeled as State Transition Systems. Verification and analysis apply Leslie Lamport’s Temporal Logic of Actions (TLA). The specification technique cTLA and a cTLA-based specification framework are used in order to support the modular description of systems and their structured verification. Moreover the cTLA-specifications used can be translated into Gerard Holzmann’s Protocol Specification Language PROMELA and analyzed by means of his efficient tool SPIN. Based on the method, we aim to the study of security properties of networked IT-infrastructures. In particular, we want to investigate effects of attacks and erroneous administration activities as well as undesired interferences of attack and administration processes.

Trust and Security Aspects of Distributed Component-Structured Software

Component-structured software is composed from components which are independently created, combined, and deployed. The high number of principals is a reason for more subtle security risks than in monolithic programs and special protection mechanisms are needed, which, however, introduce overhead and influence the application performance. Therefore a trust management system is applied which keeps track of the current risks, experiences, and trust levels of components and principals. The protection mechanisms employed in the applications are equipped with adaptation functions which adjust the monitoring efforts to the current trust levels and requirements.

Security Aspects of Distributed Component-Structured Software

Component-structured software is composed from components which are independently created, combined, and deployed. The high number of principals is a reason for more subtle security risks than in monolithic programs. In order to solve this problem we develop a formal security model for component-structured software. Moreover, we are developing methods and tools for securing components and applications against hostile attacks.

Model-based security management

The approach of model-based management supports the derivation of management applications. It concentrates on a hierarchically layered model representing the abstract nominal behaviour of the managed system, the working points and functions of the management application, and the internal structure and dependencies of the system. An object-oriented graphical modelling tool and predefined class libraries support the comfortable development of models. We apply model-based management to security management of enterprise IT systems supporting the integrated management of the various security services and mechanisms (e.g., firewalls, VPN-elements, authentication, authorization). In particular, we support that the detailed configuration settings and management rules of the different services and mechanisms can be derived from abstract policies.

Modular TKA-based specification of hybrid systems

The approach concentrates on the formal development of real-life hybrid technical systems based on TLA. A specification technique for the formal design, analysis, and verification of continuous-discrete models is developed which, particularly, facilitates the modular development of distributed process control software. To facilitate the formal specification of hybrid technical systems and a hazard analysis by formal verification, a Framework was developed. The project is supported by the DFG within the programme KONDISK.

Specification and Verification of distributed object-oriented real-time systems

The approach is based on UML and cTLA. We develop a method which supports the correctness-proved design of real-time process control software. The project is supported by the DFG within the postgraduate research programme Modelling and Model-Based Design of Complex Technological Systems.

Implementation of Communication Systems

Extended Finite State Machine (EFSM) models not only are used for the description of the protocols but also for the modelling of the software implementation on two levels: the logical implementation model is oriented at the abstract protocol stack and the instances of protocol entities, the software architecture model is oriented at the runtime objects of the final implementation. Thus, the important design decisions concern the refinement of the logical model into the software model and their correctness can be checked formally. The approach successfully has been applied to the development of an efficient integrated activity thread/server implementation of a 3-layer communication protocol stack.

Open Distributed Applications

The software of open distributed applications has to implement the productive functionality under special constraints: due to the distribution of the components distributed algorithms have to be applied, due to the openness required, standardized communication services / subsystems have to be used to realize component interactions. The code of components will reflect all of the three aspects in an integrated way. The interrelationships between productive functionality, distributed cooperation, and standardized communication are investigated by means of fundamental mechanism templates and combination principles resulting in construction guidelines and suitable strategies for analysis and verification.

Transfer Protocol Framework

A framework supporting the development and verification of high-speed communication protocols was designed. It consists of design patterns and theorems. The design patterns which model protocol mechanisms resp. service constraints can be composed to protocol and service specifications. Protocol proofs can be reduced into a sequence of proof steps which are verified by the theorems of the framework.

Tools for TLA

The development of tool-support for the temporal logic TLA (Temporal Logic of Actions) was the goal of this project. We designed several tools for the construction (composition, interpretation, and animation) and verification (theorem prover frontend, reachability analysis, and model checker) of TLA specifications. The project was supported by Digital Equipment Corporation (DEC) - Systems Research Center (SRC).

Visualization of distributed algorithms and communication protocols from formal specifications

During initial formalization of design ideas tools and concepts are necessary, to validate the formal specification against the ideas of the designer. Beside of formal proofs, animation with textual, graphical and audial means serve as important method for validation. First studies in the visualization domain of distributed systems have been conducted by the ZADA group.