Dr. Michael Leining, DB Netz AG

Prof. Dr. Werner Damm, SafeTRANS

Rüdiger Kaffenberger, softwareinmotion GmbH

• Abstractkeyboard_arrow_down

  Als James Martin 1982 in seinem Buch „Application Development Without Programmers” den Begriff “4th Generation Language” geprägt hat, kämpfte die Industrie bereits fast 15 Jahre mit der “Software Crisis”. Nun 30 Jahre später stellen wir fest, 4GL ist noch immer ein Thema, aber offensichtlich auch alle Programmierphilosophien, die es davor schon gab und die am Entstehen der „Software-Crisis“ mitgewirkt haben – und ein paar neue sind auch noch nachgefolgt. 4GL – ein gescheitertes Konzept? Besser, als aus der Sichtweise des Software-Entwicklers, kann vielleicht aus der Sichtweise des Systems-Engineer erklärt werden, warum wir auch heute noch nicht in der Lage sind, uns jede Software-Applikation und erst recht kein System am Computer „zusammenzuklicken“. Bei dieser Betrachtung erkennt man, dass die Programmiersprachen der 4. Generation in speziellen Teilbereichen der Systementwicklung durchaus präsent sind und auch weiterentwickelt werden. Man erkennt aber auch, dass sie ein schweres „psychologisches“ Problem mit sich herumschleppen, ein Problem, das sie mit anderen wichtigen Techniken der Systementwicklung teilen: „Front Loading“. 4GL sind domänenspezifisch, das bedeutet, bevor mir eine solche Sprache– und der „Compiler“ der sie in eine der konkreteren Sprachen für die Realisierung übersetzt – zur Verfügung steht, muss eine umfangreiche Analyse und Modellierung des Entwicklungsgegenstands durchgeführt werden, insbesondere dann, wenn Sicherheit und Zuverlässigkeit ein bestimmender Faktor sind. Die dazu notwendige Zeit wird in der Systementwicklung meist nicht zugestanden. Mit Blick auf industrielle Ansätze zum Systementwurf, wie beispielsweise AUTOSAR, stellt sich die Frage, ob es nicht doch den Aufwand wert wäre, einen umfassenderen Einsatz von 4GL zu untersuchen – gerade im Hinblick auf Sicherheit und Zuverlässigkeit .

Vortragsfolien (passwortgeschützt)

Heiko Richter, DB Netz AG

Vortragsfolien (passwortgeschützt)

Dr. Wolfgang Kremer, Dornier Consulting Engineering & Service GmbH

• Abstractkeyboard_arrow_down

  In dem Vortrag wird zunächst erläutert, wie UML als „4th Generation Language“ genutzt werden kann, um Testspezifikationen bzw. Testabläufe und -logiken zu formalisieren als Vorstufe zur Testautomatisierung. Diese Vorgehensweise wir im allgemeinen MBT (Model Based Testing) genannt. Durch die Einführung eine Modellierungssprache werden Testspezifikationen zum einen formalisiert, und damit für den Computer „lesbar“, und zum anderen auf einer höheren Abstraktionsebene gehoben. Die Formalisierung führt nun dazu, dass diese grafisch spezifizierten Testabläufe und –logiken mehr oder weniger automatisiert in letztendlich ausführbare Testfälle transformiert werden können. Die bei der Modellierung mögliche höhere Abstraktion von Testspezifikationen erlauben es grundsätzliche Testlogiken und –szenarien verständlicher zu definieren, Komplexitäten in Systemen, z.B. getrieben durch Produktvarianten, besser zu kontrollieren, aber auch mit den geeigneten MBT-Tools gezielt ganze Testkampagnen zu generieren. Dabei gibt es grundsätzlich zwei Ansätze, die in der Industrie verfolgt werden. Zum einen die Modellierung von Testmodellen, die nicht direkt aus anderen Modellen, z.B. Systemmodellen, hergeleitet werden sondern von einem Testdesigner entwickelt wird, basierend auf seinem Verständnis und Sicht auf die Spezifikationen aus der Entwicklungsphase. Der andere Modellierungsansatz verfolgt die Idee, falls vorhanden, aus Systemmodellen geeignete Testmodelle direkt abzuleiten, zu generieren. Beide Ansätze werden in der Präsentation diskutiert. Die Dornier Consulting ist nun schon seit vielen Jahren im Bereich MBT tätig und konnte im Rahmen von Kundenprojekten entsprechende Erfahrungen insb. aus der Automobilindustrie sammeln. Über die Jahre entstand u.a. das Testframework do.ATOMS, an Hand dessen gezeigt wird, wie zum einen UML Modelle in Testmodelle überführt werden können aber auch direkt Testlogiken modelliert werden können in Form von sog. Workflows. Die erste industrielle Umsetzung dieser Methode waren zwei Test Roboter, mit denen vernetzte Infotainmentsysteme für die Autoindustrie aus User-Sicht getestet werden können und nun seit ca. 4 Jahren bei einem OEM im Einsatz sind. Darüber wird noch das ITEA Forschungsprojekt DIAMONDS vorgestellt, in dem wir, zusammen mit dem Fraunhofer FOKUS und anderen Partnern, an Modell basierte Testmethoden für Security arbeiten. In diesem Projekt wurde eine grundlegende Vorgehensweise entwickelt und von uns an Hand einer „Case Study“ aus dem Automotive Bereich in einer ersten Implementierung umgesetzt. Die Vorgehensweise besteht im Wesentlichen aus den Schritten Risikoanalyse – Testmodellierung – Testgenerierung – Ausführung – Ergebnisanalyse, und soll in dem Vortrag näher beschrieben werden. In einem finalen Ausblick werden nochmal die Möglichkeiten und das Potential von MBT erläutert und unsere bisherigen Erfahrungen mit MBT zusammenfassend dargestellt.

Vortragsfolien (passwortgeschützt)

Bernd Holzmüller und Dr. Martin Sulzmann, ICS AG

• Abstractkeyboard_arrow_down

  Software Cost Reduction (SCR) is an established textual tabular notation for specifying complex embedded control systems. Tools supporting the SCR method are either not publicly available or are tied to a specific proprietary model-based tool such as for example Simulink. A further problem is that different projects often require slight adaptations of the SCR method. We propose the usage of domain-specific languages (DSLs) to support the SCR method. Specifically, we consider two SCR DSLs which evolved out of two Aerospace & Defence projects. (1) One of the DSLs uses a visual representatation based on a UML profile, where the dynamic semantics of the SCR UML profile is described by means of a systematic translation scheme to SCADE. (2) The other DSL is an internal DSL embedded in the functional language Haskell. We rely here on our own code generator to C. Thanks to the functional and strongly-typed nature of Haskell, we can quickly and easily integrate new project-specific SCR-style extensions. We report on the techniques and methods involved in implementing and evolving the DSLs, their practical application in safety-critical projects following safety norms such as IEC 61508 and DO-178B and the experiences and feedback we gained from customers.

Vortragsfolien (passwortgeschützt)

Dr. Christian Ferdinand, AbsInt GmbH

• Abstractkeyboard_arrow_down

  Sicherheitskritische Software wird zunehmend modellbasiert entwickelt. Hierbei erstellen Entwickler ein Modell der Anwendung in einer graphischen Notation, wie z.B. SCADE, Statecharts/Statemate, oder Matlab/Simulink. Aus dem Modell wird die Implementierung durch Einsatz eines Codegenerators automatisch erzeugt, in der Regel in Form von C-Code. Dieses Verfahren bietet viele Vorteile, von erhöhter Entwicklungseffizienz, niedrigerer Fehleranfälligkeit bis hin zur Automatisierung von Testen und Verifikation. Durch Kopplung modellbasierter Verifikation mit codebasierter Verifikation kann die Korrespondenz zwischen der Modellebene und der Implementierungsebene automatisch sichergestellt werden. Eine wichtige Rolle spielt die automatische Verifikationsunterstützung im Bereich der nicht-funktionalen Programmeigenschaften, insbesondere bezüglich Timing, Speicherverbrauch, und Laufzeitfehlern wie arithmetischen Überläufen, Division durch Null, usw. Alle gängigen Sicherheitsstandards (DO-178B, DO-178C, ISO-26262, EN-50128, IEC-61508) fordern den Nachweis der Abwesenheit solcher Fehler für sicherheitskritische Anwendungen. Der höhere Abstraktionsgrad der Softwareentwicklung auf Modellebene führt dazu, dass die Laufzeit- bzw. Speicheranforderungen der entwickelten Applikation, sowie das Auftreten von Laufzeitfehlern für die Entwickler schwerer zu beurteilen sind, als bei Entwicklung auf C-Ebene. Durch statische Programmanalysen können sichere obere Schranken der längstmöglichen Ausführungszeit von Anwendungstasks (Worst-Case Execution Time, WCET) und des maximalen Stackverbrauchs bestimmt werden, sowie die Abwesenheit von Laufzeitfehlern bewiesen werden. Die Analyse der längstmöglichen Ausführungszeit und des maximalen Stackverbrauchs muss hierbei auf Binärebene, also auf ausführbarem Maschinencode durchgeführt werden, die Laufzeitfehleranalyse auf Ebene des generierten C-Codes. In der Regel erfordern statische Analyseverfahren Benutzerinteraktionen, da die benötigten Informationen oft nicht vollständig statisch ermittelt werden können. Beispiele sind die manuelle Eingabe von Schleifeniterationsgrenzen im Fall der WCET- oder Stack-Analyse, oder die manuelle Eingabe von Präzisionssteuerungsdirektiven im Fall der Laufzeitfehleranalyse. Durch eine Kopplung statischer Analysewerkzeuge mit modellbasierten Codeerzeugern kann diese manuelle Interaktion für automatisch generierten Code eliminiert werden. Die vom statischen Analysator benötigten Informationen sind in der Regel auf Modellebene bekannt, stehen dem Codeerzeuger zur Verfügung und können auch dem statischen Analysator über geeignete Schnittstellen übergeben werden. Desweiteren können die Ergebnisse der statischen Analyse automatisch auf die Modellebene übertragen werden. Der Laufzeit- oder Stackbedarf des generierten Codes, sowie potentiell auftretende Laufzeitfehler können somit in den Modellierungswerkzeugen selbst dargestellt werden. Dadurch erhalten Entwickler direktes Feedback über Timing, Stackverbrauch und Laufzeitfehler während der Modellentwicklung, und können nicht-funktionale Probleme frühzeitig identifizieren und beheben. Im Vortrag werden die Grundlagen der Kopplung statischer Analysewerkzeugen mit modellbasierten Entwicklungs- und Testwerkzeugen erläutert und die erforderlichen Prozesse und Schnittstellen definiert. Praktische Erfahrungen werden anhand existierender Toolkopplungen zwischen den statischen Analysatoren aiT WCET Analyzer, StackAnalyzer und Astrée und den modellbasierten Entwicklungswerkzeugen SCADE und Matlab/Simulink/TargetLink vorgestellt.

Vortragsfolien (passwortgeschützt)

Dr. Udo Brockmeyer, BTC Embedded Systems AG

• Abstractkeyboard_arrow_down

  The requirement specification stands at the beginning of any development process. It builds the basis for the further development of embedded control devices. Their quality is of great importance for the progress and success of each project. Especially in the area of safety critical development and the fulfillment of industrial standards like IEC61508 and ISO26262 in respect to functional safety, formal requirement specification plays a major role. These are not very popular in the area of embedded software development, in comparison to model-based specification. Declarative methods, like formal requirement specifications, are considered to be too mathematical and too difficult to learn in general; it is observed as a method only for experts. Operational methods, like modeling, are widely accepted as typical activities of engineers. Formal specifications have various advantages in supporting a computer-aided fully automated requirement-based test process, due to its machinereadability, unambiguousness and traceability capabilities. This method presented here allows engineers, an intuitive and constructive specification of formal requirements, without having in-depth expertise in theory of Formal Methods. Starting point of the formalization process is the informal textual requirement, which is structured step-by-step by the user, in order to get a more and more unambiguous, machine-readable description. In the beginning, no concrete architecture, model, code or even implementation is mandatory. At later stages of the development process, the concrete architectures can be bound by the users to the former developed “virtual” formal requirement specification. This binding process always is accompanied by the wizard mechanism and allows a convenient and efficient handling. This automatically creates a linkage between the various artifacts of the development process. The specification environment enables automatic structuring and management of the corresponding links, which allows complete traceability throughout the entire development process. An important part of the described specification environment is the synthesis unit which automatically translates the formal specification into so called C-Observers. These C-Code-Functions are representing the particular requirements, which are executable as monitors/observers during the verification- and test process in the specific test environment. This allows a complete automated, requirement-based test approach, both at model level as well as at code and implementation levels.

Vortragsfolien (passwortgeschützt)

Dr. Jens Gerlach, Fraunhofer FIRST

• Abstractkeyboard_arrow_down

  Frama-C ist eine von CEA LIST (Frankreich) maßgeblich entwickelte quelloffene Werkzeugplattform zur statischen Analyse von C-Programmen. Im Device-Soft Projekt haben Fraunhofer FIRST und CEA LIST Frama-C für die formale Verifikation sicherheitskritischer Bahnsoftware eingesetzt. Im Vortrag geben wir einen Überblick über die wichtigsten Analyse-Plug-Ins von Frama-C und berichten über unsere Erfahrungen bei der formalen Verifikation von C-Software und gehen auch auf zukünftige Forschungsvorhaben ein.

Vortragsfolien (passwortgeschützt)