Many future Driver-Assistance-Systems (DAS) will use components not permanently mounted to the vehicle. Unlike state-of-the-art DAS with static configurations, the system and software architecture changes at runtime. To handle configuration changes, Service Oriented Architecture (SOA) and automatic orchestration is a promising approach. Whenever systems are set up automatically, they have to be validated. This paper presents an approach based on formal methods. Existing component models are annotated with Quality-of-Service parameters and transformed automatically to Hybrid Automata. These automata are then composed to an overall system model and model checking is used to check safety properties. The complete transformation-orchestration-validation process is executed without user interaction and thus can be performed at runtime.

Dieser Artikel behandelt das Parametersynthese-Problem für hybride Systeme. Für ein parametrisiertes Modell und eine Sicherheitsbedingung wird eine sichere Teilmenge einer potentiell unsicheren Parametermenge gesucht. Im Gegensatz zu bestehenden symbolischen Ansätzen, werden dabei statistische Methoden eingesetzt. Dadurch können Unsicherheiten im Modell probabilistisch dargestellt werden und Systeme mit beliebiger Dynamik analysiert werden. Die vorgeschlagene Methode wurde prototypisch implementiert und anhand einer Echtzeitanwendung evaluiert.

Many real-time systems operate in safety-critical environments. Testing of these systems is hard in principle and can never guarantee full coverage. So a method for formally proving correctness is desirable. Another problem in real-time system design is the determination of deadlines and periods of time-critical processes as a prerequisite of the scheduler design. We want to use Hybrid Automata (HA) to tackle both problems. HA are a formal language that is equipped with semantics and thus accessible to formal analysis. We introduce the syntax and semantics of a new class of HA called Parameterized Linear Hybrid Automata and demonstrate its advantages by modelling a typical real-time control system using an extended version of the tool HieroMate.

We present a tool environment with a constraint logic programming core, that allows us to specify multi-agent systems graphically and verify them automatically. This combines the advantages of graphical notations from software engineering and formal methods. We demonstrate this on a Robocup rescue scenario.

In Anbetracht der fortschreitenden Automatisierung im Güterverkehr ist auch der Einsatz von Serienfahrzeugen erstrebenswert. Aus wissenschaftlicher Sicht besteht diesbezüglich ein Bedarf an präzisen und echtzeitfähigen Regelungsverfahren, die auch für Fahrzeuge mit einachsigem Anhänger ein exaktes Abfahren vorgegebener Pfade insbesondere bei rückwärtsgerichteten Fahrmanövern gewährleisten. In diesem Beitrag wird ein zweistufiges Regelungsverfahren vorgestellt, das diese Kriterien erfüllt und sich generisch auf verschiedene Fahrzeuge des gleichen Gespanntyps übertragen lässt. Darüber hinaus kann das vorgestellte Verfahren als Grundlage für das autonome oder assistierte Fahren fungieren.

In previous works, Hierarchical Hybrid Automata (HHA) have been proposed as a combination of UML state machine diagrams and hybrid automata to model complex and in particular multi-agent systems. This approach enables formal system specification on different levels of abstraction and expresses real-time system behavior. A prototype was implemented using constraint logic programming (CLP) as a framework to specify and verify these HHA. However, it still requires the user to write a CLP program in order to specify the HHA, which is a tedious and error-prone work. Therefore, this paper aims at simplifying the verification process by introducing a tool environment where a HHA model together with requirements are entered graphically and the process of verification is achieved automatically.