Der Fachausschuss Q3.4 Software Engineering der DGLR veranstaltete am 4. Oktober 2011 einen eintägigen Workshop zum Thema

"Verifikation in der modellbasierten Software-Entwicklung"

Ort: Institut für Luft- und Raumfahrt, TU München, Garching bei München

Call for Paper

Software-Entwicklungsprojekte unterliegen einem stetig wachsenden Kosten- und Zeitdruck. Eine Möglichkeit, diesem Druck zu begegnen, ist die Erhöhung des Automatisierungsgrades durch modellbasierte Software-Entwicklung. Sie verspricht Effizienzsteigerung und damit einhergehende Reduzierung von Entwicklungszeiten und -kosten. Ihre Vorteile liegen in der konsistenten Code und Dokumentengenerierung sowie der Möglichkeit toolgestützter Analyse und Simulation des Modells.

Die modellbasierte Entwicklung war schon einmal Thema der DGLR Workshops in den Jahren 2004, 2005 und 2006. Bereits der Workshop im Jahre 2006 beschäftigte sich mit der Zulassung von generierter Software. In den vergangenen fünf Jahren hat sich die Technologie und mit ihr auch die Entwicklungsstandards weiterentwickelt. Während beispielsweise der DO-178B keine speziellen Richtlinien zur modellbasierten Entwicklung beinhaltet, wird sein Nachfolger, der DO-178C, ein eigenes Technisches Supplement zu diesem Thema erhalten.

Bei zulassungspflichtigen Projekten muss der Einsatz modellbasierter Techniken schon in der Planung berücksichtigt und mit den zulassenden Behörden abgestimmt werden. Jedes Projekt, das den Einsatz modellbasierter Techniken erwägt, muss die Frage klären, wie es die Vorgaben der anwendbaren Safety-Standards wie beispielsweise der DO-178B erfüllt.

Bei Luft- und Raumfahrtprojekten beanspruchen Design und Codierung einen geringeren Teil des Entwicklungsaufwands als die Verifikation. Der DO-178B verlangt beispielsweise, dass auch die Verifikation selbst verifiziert wird. Die modellbasierte Entwicklung entfaltet ihre Vorteile daher nur dann, wenn auch die Verifikationsprozesse entsprechend automatisiert, reduziert oder eliminiert werden, z.B. durch modellgetriebene Testfallentwicklung oder gar -Generierung, durch Simulation oder durch qualifizierbare Code Generatoren. Diese Verfahren müssen aber zur Zulassung der entwickelten Software anerkannt werden. Dazu müssen aber unter anderem die folgenden Fragen geklärt werden:

• Was bedeutet Testüberdeckung bei Modellen? Gibt es alternative Gütekriterien für die Vollständigkeit der Verifikation von Modellen?
• Was ist das Äquivalent von Dead Code oder De-activated Code in Modellen?
• Wie weit ist eine Modellsimulation repräsentativ für das endgültige Produkt?
• Wie weit und unter welchen Bedingungen kann Modell Simulation das aufwändige Testen in der Zielumgebung ersetzen?
• Wie weist man die Übereinstimmung (Compliance) von Source Code zu Modell nach?
• Wie sind Testfälle aus den Modellen zu erzeugen, damit sie den Testanforderungen genügen?

 Für den Workshop suchen wir Vorträge aus der industriellen Praxis oder der industrienahen Forschung. Jeder Vortrag sollte ca. 30 Minuten dauern, anschließend sind 15 Minuten Diskussion vorgesehen.  Zwecks Vorbereitung des Workshops wird um die Zusendung einer Kurzfassung des Vortrags bis spätestens 29. Juli 2011 gebeten.

Für weitere Informationen und zur Vortragsanmeldung stehen Ihnen der Leiter des Fachausschusses Q3.4 und sein Stellvertreter zur Verfügung:

Termine

Vortragsanmeldung: 29. Juli 2011

Programm und Benachrichtigung der Vortragenden: 12. August 2011

Anmeldung: bis 30. September 2011

Workshop: 4. Oktober 2011

Programm und Download der Vorträge

Bei Bedarf können die Dokumente zu den jeweiligen Vorträgen bei den Obleuten des Fachausschuss angefordert werden.

Bericht

Am 4. Oktober fand der jährliche Workshop des Fachausschusses Q3.4 Software Engineering zum Thema "Verifikation in der modellbasierten Software-Entwicklung" am Institut für Luft- und Raumfahrt der Technischen Universität München in Garching statt.

Als Gastgeber begrüßte Prof. Dr. Holzapfel vom Lehrstuhl für Flugsystemdynamik die mehr als 60 Workshopteilnehmer aus Forschung, Industrie, und von der Bundeswehr.

 Zu Beginn zeigte Dr. Björn Pötter von Cassidian den Trend zu immer umfangreicheren und komplexeren Systemen in der Luftfahrt auf. Eine der möglichen Antworten auf diesen Trend ist die modellbasierte Systementwicklung. In seiner Keynote beleuchtete Dr. Pötter die Vor- und Nachteile der modellbasierten Entwicklung sowie mögliche Fallstricke.

Dewi Daniels von Verocel referierte über das Model-Based Design and Verification Supplement der neuen Ausgaben der Richtlinien DO-178C und DO-254A, die für März 2012 geplant sind. Er betonte, dass Modelle immer aus Anforderungen entwickelt werden müssen, dass ein Modell entweder nur Spezifikations- oder nur Designmodell sein kann, und dass Modellsimulation partiell als Nachweis im Rahmen einer Zulassung anerkannt wird.

Christian Schrader von Esterel Technologies stellte den SCADE Combined Testing Process vor, der aus einer Mischung von Modellsimulation und traditionellem Testen besteht und den Anforderungen des DO-178C entspricht. Der Combined Testing Process stützt sich wesentlich auf die Qualifikation der SCADE Toolsuite.

Dr. Marc Segelken von Mathworks fragte in seinem Vortrag, ob die üblichen Testüberdeckungsmetriken wie MC/DC bei Modellen ausreichend sind und stellte Fehlersituationen vor, die durch diese Metriken nicht erfasst werden. Er schlug ergänzende Maßnahmen wie Defect Injection und Input Output Impact Coverage vor. Im Gegensatz zu Esterel stützt sich Mathworks auf qualifizierbare Verifikationswerkzeuge wie den neuen Simulink Code Inspector.

Dr. Ralf Gerlich von der BSSE stellte die Verifikation von Code Generatoren deren Zertifizierung gegenüber. Die Überprüfung bestimmter Eigenschaften des generierten Codes während der Ausführung auf dem Zielrechner könnte durch ein Orakel erfolgen, welches durch automatische Transformation aus dem Modell erzeugt wird.

Während die bisherigen Vorträge die Verifikation von Modellen und den daraus generierten Code zum Ziel hatten, beschrieb Frank Westerbuhr von Cassidian einen Ansatz zum modellbasierten Testen. Die vorgestellten Ergebnisse beruhen auf einem Pilotprojekt von Cassidian. Die in dem Pilotprojekt verwendete geschlossene Toolkette erlaubt es, durch Analysewerkzeuge aus einem in UML formulierten Testmodell vollständige Testpläne, Testspezifikationen und Testskripts zu generieren.

Markus Hornauer von der TU München berichtete über den Einsatz modellbasierter Verfahren für die Entwicklung von Flugregelungssystemen. Die Verifikation dieser Systeme vollzieht sich in mehreren Schritten von der Verifikation des Streckenmodells über die Verifikation von Design- und Code-Modellen bis zum Nachweis in der Zielumgebung.

 Peter Hermle von Silver Atena erläuterte die modellbasierte Entwicklung bei Silver Atena. Im Gegensatz zu den vorangegangenen Vorträgen verzichtet man dort auf die Qualifikation des Code Generators. Generierter Code wird wie handgeschriebener Code durch manuelle Code Reviews verifiziert. Diese Reviews werden durch Analysewerkzeuge unterstützt.

Im letzten Vortrag beschrieben Stefan Miller und Dr. Ralf Bogusch von Cassidian den Einsatz von modellbasierten Tests auf Luftfahrtzeug- und Systemebene im Projekt A400M Military Mission Management System. Wie im Vortrag von Frank Westerbuhr werden auch hier aus einem UML Modell Testfälle automatisch generiert.

Richard Seitz von Fachausschuss Q3.4 der DGLR schloss die Veranstaltung.

Die Vorträge wurden von umfangreichen Fragen und engagierten Diskussionen begleitet, die in den beiden Kaffeepausen und während des Mittagessens fortgesetzt wurden. Die Teilnehmer nutzten auch intensiv die Gelegenheit zu einem allgemeinen Informations- und Gedankenaustausch, welches ja ebenfalls eines der Ziele des Fachausschusses ist. Viele Teilnehmer haben überdies dasAngebot von Prof. Dr. Holzapfel wahrgenommen, während der Mittagspause die Einrichtungen und Simulatoren des Lehrstuhls für Flugsystemdynamik zu besichtigen und mit den Mitarbeitern des Lehrstuhls zu sprechen.

Ein herzliches Dankeschön geht an die Vortragenden für ihre hervorragenden Präsentationen. Ein ganz besonderer Dank geht an die Mitarbeiter des Lehrstuhls für Flugsystemdynamik von Prof. Dr. Holzapfel für ihre tatkräftige und sehr engagierte Unterstützung bei der Vorbereitung und Durchführung des Workshops. Wir möchten uns auch bei den Firmen Cassidian und ESG für die Übernahme der Kosten für die Verpflegung in den Pausen bedanken sowie bei der Technischen Universität München für die Überlassung des Hörsaals. Schließlich möchten wir uns bei allen Teilnehmern des Workshops bedanken, die durch ihre  rege Beteiligung die Veranstaltung erst zu einem Workshop gemacht haben.

Allgemeine Informationen

Kurzfassung der Vorträge

Dewi Daniels: The Model-Based Design and Verification Supplement for DO-178C/ED-12C

This presentation will describe the Model-Based Design and Verification Supplement for DO-178C/ED-12C, which is due to be published in the first quarter of 2012. The Supplement will address such questions as:

• How do you satisfy the DO-178C/ED-12C objectives when using model-based design and verification?
• When is a model a system model and when is it a software model? Why does it matter?
• Does a model express requirements or design?
• Can credit be taken for model simulation instead of testing?
• What credit can be taken for the use of a qualified auto code generator?

Eur Ing Dewi Daniels is Managing Director of Verocel Limited, and a member of SC-205/WG-71, the joint RTCA special committee and EUROCAE working preparing DO-178C/ED-12C. Dewi attended the most recent meeting of the Model-Based Design and Verification Sub-Group (SG-4) in Stockholm in April 2011, and is therefore familiar with the latest changes to the draft supplement.

Christian Schrader: SCADE Combined Testing Process im Kontext von DO178B und C

Der Vortrag skizziert die Verifikationsaktivitäten im DO178B praxisbewährten Combined Testing Process. Die Verifikationsaktivitäten lassen sich dabei in drei Bereiche aufteilen: die Verifikation auf SCADE-Modellebene inklusive Testabdeckungsanalyse, die qualifizierte Codegenerierung, welche die Verifikation des generierten Codes eliminiert, und schließlich die Objectcode-Verifikation des generieren Codes. Das neutrale Format der Testdaten für die Modellverifikation eröffnet dabei die Möglichkeit, diese auch für Integrationstests auf der Zielhardware wieder zu verwenden.
 

Dr. Rainer Gerlich, Dr. Ralf Gerlich: MDE – Mehr als modellieren und Code generieren

Diskutiert werden die Erfahrungen einer mehr als 10-jährigen Tätigkeit im Bereich Model Driven Engineering (MDE) mit domänenspezifischen Modellierungssprachen für verteilte Echtzeitsysteme, Datenverarbeitungsketten von der Erfassung bis zur Telemetrie und Telecommanding. Bei der Modellierung werden funktionale und nicht-funktionale Eigenschaften unterstützt bzw. vom Modellierungsansatz explizit gefordert. Die zugehörige Toolumgebung integriert Code- und Testgenerierung und ermöglicht einen vollautomatischen Ablauf zwischen Ablieferung eines Modells bis zur Erstellung eines Berichtes über die in der jeweiligen (Ziel-)Umgebung beobachteten Eigenschaften des umgesetzten Modells.

Angesprochen werden Aspekte der Verifikation, Repräsentativität der Modellierung, Testgenerierung und – abdeckung, Dead-code, Standardisierung und Compliance Modell-Code. Folgende Schlüsse werden abgeleitet:

Die Erhaltung der auf Modellebene verifizierten Eigenschaften kann auf Implementierungsebene nicht vorausgesetzt werden, da zu viele – nicht auf Modellebene bekannte und beherrschbare – Einflussfaktoren einwirken. Dies gilt besonders für die nicht-funktionalen Eigenschaften. Eine Überprüfung der auf dem Zielsystem beobachteten Eigenschaften ist daher notwendig.

Durch Integration der Erzeugung von Teststimuli in den Transformationsprozess kann diese Überprüfung automatisch und damit effizient erfolgen. Ein Automat kann dann das Modell mit dem Ergebnis für jede ausgeführte Transformation eines Modells vergleichen, Dies ist eine effiziente – weil schnelle und kostengünstige – Alternative zur Zertifizierung eines Codegenerators.

Dead-code kann auf Modellebene statisch nur schwer nachweisbar sein. Durch dynamische und komplexe Abläufe in verschiedenen Prozessen können Teile eines Modells nicht erreichbar sein, bspw. weil in einem Prozess eine Bedingung gesetzt wird, die die Ausführung eines Teils eines anderen Prozesses immer verhindert. Da eine prozessübergreifende Analyse notwendig ist, ist die Nichterreichbarkeit nur schwer zu identifizieren. Durch Stimulation und Messung der Modellabdeckung ist sie erkennbar.

Die Stimulation eines Modells impliziert nicht nur die Erzeugung von Stimuli, sondern auch deren Unterdrückung, bspw. im Falle von Datenverlust, und die Fehlereinspeisung. Zur vollständigen Abdeckung der Fehlerbehandlungsteile eines Modells ist Fehlereinspeisung unbedingt notwendig. Dabei ist durch entsprechende Vorgehensweise sicherzustellen, dass das Verhältnis von nominaler zu nicht-nominaler Stimulation nicht entartet.

Der gegenwärtige Prozess für die Überarbeitung von Standards läuft zu langsam ab und behindert dadurch technischen Fortschritt. Eine Analyse zeigt, dass die gegenwärtigen Standards nicht immer technologieneutral sind, obwohl sie meistens nicht sehr konkret einen Prozess definieren, sondern nur einen Korridor vorgeben. Eine Fokussierung auf die Produktqualität statt auf Prozessqualität würde schnelleren technischen Fortschritt ermöglichen.
 

Frank Westerbuhr: Modellbasiertes Testen für Avionik Systeme

Modellbasiertes Testen verspricht eine verbesserte Verständlichkeit von Testfällen durch deren Visualisierung und eine erhöhte Testabdeckung bei geringeren Aufwänden für die Testerstellung. Um diese Aussagen zu überprüfen und generell die Verwendung von MBT im Avioniktest zu erproben, wurde ein Pilotprojekt durchgeführt. Hier war es die Aufgabe, die korrekte Realisierung von Anforderungen für einen elektrooptischen Sensor zu testen. Der Vortrag schildert die Vorgehensweise und die Ergebnisse.
 

Peter Hermle: Wiederverwendung von Testfällen bei der modellbasierten SW-Entwicklung

Die Firma SILVER ATENA setzt seit Jahren modellbasierte Softwareentwicklung produktiv zur Entwicklung von sicherheitskritischen Systemen ein. Die dazu verwendete Toolkette (Software-Development Environment - SDE) basiert auf Matlab/Simulink sowie dem Embedded Coder von MathWorks. Es wird damit Software nach DO-178B (bis DAL A/B) sowie nach IEC 61508 (bis SIL3) entwickelt. Zudem entwickelt SILVER ATENA HiL-Testsysteme, auf denen die Tests der entwickelten Systeme im Verifikationspfad erfolgen.

Die Tests im Entwicklungspfad finden nach Möglichkeit hauptsächlich auf der Modellebene statt (Offline-Tests), der Code für das Zielsystem wird durch Autocode-Generierung mit Hilfe des speziell konfigurierten Embedded Coders erzeugt. Im Vortrag soll dabei auf die Möglichkeiten, Vorteile und Grenzen von modellbasierten Tests sowie deren Wiederverwendung auf den HiL-Testsystemen eingeganden werden. Über konkrete Beispiele soll dabei auch der mögliche Umfang sowie Einsparpotentiale bzgl. Zeit und Aufwand aufgezeigt werden.
 

Stefan Miller, Dr. Ralf Bogusch: A model-based functional test approach to verify system requirements

Model-based testing is a promising approach to create a suite of test cases from test models. In the traditional approach individual test cases are derived manually by analyzing the requirements that need to be covered by tests. In order to address the costly test case development, we have been developing and applying the idea of automatic test case generation. Testers using the model-based testing approach concentrate on a test model, rather than bother with cumbersome specification of individual test cases. We use extended UML Activity Diagrams to model the system behaviour. Requirements are linked to the test model to enable traceability between requirements and the verification evidence as well as to assess the requirements-based test coverage. Compared to Use Case Diagrams and Sequence Diagrams, the abstraction level given by Activity Diagrams is well suited to the specification of black-box functional tests at system or aircraft level. After the test model has been specified, appropriate test cases are created automatically by searching the paths in the Activity Diagram that refer to certain requirements to verify. Based on the Airbus A400M Military Mission Management System project, we report on our experience with developing methods and tools to support model-based testing as well as the lessons learned when transferring these techniques into testing organisations.