Sommersemester 2009SW in sicherheitsrelevanten Systemen Software in sicherheitsrelevanten Systemen...

Sommersemester 2009 SW in sicherheitsrelevanten Systemen

Software in sicherheitsrelevanten Systemen

Ralf PingerSommersemester 2009


Organisatorisches• Stundenzahl: 2V + 1Ü • Vorlesung:

Do. 08:00 - 09:30 Uhr in IZ 161– Do, 07.05.08 – Do, 14.05.09 – Do, 28.05.09 – Blockveranstaltung

Exkursionswoche 02. - 05.06.2009

– Do, 11.06.09– Do, 25.06.09 – Do, 02.07.09– Do, 09.07.09

• Block: VL + UE vom 02.06. – 05.06. (Ex-Woche):– Di 02.06.: 8:00 - 16:00– Mi 03.06.: 8:00 - 16:00– Do 04.06.: 8:00 - 16:00– Fr 05.06.: 8:00 - 11:30

– Inhalt: praktischer Umgang mit SCADE

– Schulung erfolgt durch Esterel

• Sprechstunde: nach Vereinbarung

• Prüfung: nach Vereinbarung• Kontakt:

[email protected]


Inhalt

1. Motivation2. RAMS/Normen3. SCADE/modellbasierte Entwicklung4. Qualifizierung von

Entwicklungswerkzeugen


1. Motivation

• Zusammenstoß zweier S-Bahnen im Bahnhof Flughafen Hannover-Langenhagen, 29.06.00

Bahnhof Flughafen

S-Bahn 5712 (verspätet)S-Bahn 5711

PZB - Indusi

Signal

Weiche


Signal

• übermittelt Erlaubnis zur Einfahrt

• übermittelt erlaubte Geschwindigkeit


Weiche


PZB – Indusi• Punktförmige Zugbeeinflussung -

PZB (induktive Zugsicherung)

• Vermeidung von Gefährdungen und Unfällen durch Zwangsbremsung

• Übertragung der Signalstellung an der Strecke auf das Fahrzeug

• punktförmig, da nur an bestimmten Punkten eine Beeinflussung stattfinden kann

• PZB lediglich Unterstützung des Fahrers


Funktionen der PZB/Indusi• Die Wachsamkeitsprüfung überwacht, dass der

Triebfahrzeugführer (Tf) beim Passieren eines Halt ankündenden Signals die Aufnahme des Signalbegriffs durch eine Tastenbedienung bestätigt.

• Die Bremswegüberwachung überwacht den Bremsvorgang vor einem Halt zeigenden Signal. Dies erfolgt fahrzeugseitig durch diskrete Prüfpunkte (bei Altsystemen) oder kontinuierliche Überwachungskurven.

• Die Fahrsperre löst beim Passieren eines Halt zeigenden Signals eine Zwangsbremsung aus.


Übertragungsprinzip Indusi


Sicherungsstufen PZB/Indusi• 500-Hz-Magnete 250 bis 150 m vor Hauptsignalen, die

besondere Gefahrenpunkte decken.-> falls zu schnell dann Zwangsbremsung (ZB)

• 1000-Hz-Magnet am Vorsignal bzw. Überwachungssignal eines Bahnübergangs-> Wachsamkeitstaste innerhalb 4 s, sonst ZB-> falls zu schnell dann ZB

• 2000-Hz-Magnet am Hauptsignal-> immer ZB


Französische Alternative zur Indusi

• Krokodil (1920er Jahre)• Signalbegriff wird als

positive oder negative Spannung dargestellt (+/- 20 V)


Alternativen zur Indusi• Eurobalisen • komplexere

Datenübertragung möglich (mehrere Bytes)


Live-Demo Zugsicherung(am Beispiel der

belgischen Bahn)


Randbedingungen• 5711 stand ab 09:53 Uhr

abfahrbereit vor Ausfahrsignal, geplante Abfahrt 10:10 Uhr

• 5712 hat 7 Minuten Verspätung, erwartete Ankunftszeit 10:11 Uhr

• 5712 erhält Erlaubnis zur Einfahrt in Bahnhof

• 5711 steht vor Halt zeigendem Signal!


Ausgangssituation

Bahnhof Flughafen

S-Bahn 5712 (verspätet)S-Bahn 5711

PZB - Indusi

Signal

Weiche


Was ist passiert?• 5711 startet um 10:10 Uhr• Ausfahrsignal für 5711 stand auf Halt• Indusi erzeugt Zwangsbremsung für 5711• Tf von 5711 drückt Freitaste und fährt wieder

los!• 5711 fährt die Einfahrweiche auf• 5712 war zu diesem Zeitpunkt schon an seinem

Einfahrsignal vorbei -> keine ZB mehr möglich!• Noch im Tunnel stoßen 5711 und 5712 frontal

zusammen!


Unfallfolgen

• 16 Personen verletzt• 3.600.000 DM Sachschaden• Wiederinbetriebnahme der Strecke erst

am 30.06.00, 04:00 Uhr, einen Tag später


Fazit• keine kausale Beteiligung technischer

Komponenten/Einrichtungen• 5711 erhielt Zwangsbremsung• Ursache:

unerlaubte Weiterfahrt von 5711• Auszug aus Regelwerk:

„Ist ein Zug an einem Halt zeigenden Hauptsignal (...) unzulässig vorbeigefahren, ist nach dem Anhalten der Fahrdienstleiter sofort zu verständigen. Dies gilt auch bei einer Zwangsbremsung durch PZB an einem Hauptsignal (...), das eine Fahrtstellung (...) zeigt.“

Menschliches Versagen als Ursache


Fazit 2

• System hat die Fehlhandlung des Triebfahrzeugführers erkannt und hat eingegriffen

• nach erfolgter technischer Reaktion übernimmt der Mensch wieder die Verantwortung!

• offenbar hat der Mensch die Zwangsbremsung nicht dem Hauptsignal zugeordnet!


Gründe für Zwangsbremsung

• Indusi am Halt-Signal (Indusi)

• Sicherheitsfahrschalter (Sifa) – Totmannknopf

• Zurückrollen des Zuges• Störung im

Fahrzeuggerät• Zwangsbremsung

unbekannter Ursache


menschliches Versagen?• Ist das menschliche Versagen

vorprogrammiert?

• 22 aktenkundige Fälle zwischen 1994 und 2000: Tf fährt nach Zwangsbremsung durch Indusi unerlaubt weiter!

• Forderung nach optischer Signalisierung bei „ZB durch Indusi“

Systeme müssen von Menschen beherrscht werden können!


zweites Beispiel – Genthin 1939

• 22.12.1939: D10 Berlin – Köln fährt in Brandenburg Reichsbahn mit 12 Minuten Verspätung ab (viele Reisende, lange Zeit für Aus- und Einsteigen)

• D10 muss bei Kade halten, da sich im Abschnitt davor (Genthin) noch der Militärzug 176 befindet

• D10 hat damit 27 Minuten Verspätung


Unglück von Genthin• D 180 Berlin Neunkirchen (Saar) folgt D10• D 180 lief auf und wurde mehrfach „gestutzt“

(Vorsignal auf Halt, Hauptsignal dann aber auf Fahrt)

• Lokführer von D 180 „übersieht“ im Nebel Halt zeigendes Vorsignal und Hauptsignal bei Belicke

• Fahrdienstleiter gibt Haltsignale und benachrichtigt Schrankenbude 89 und Stellwerkswärter in Genthin Ost


Fahrt nach Genthin

• D 180 sieht nun nur noch „Fahrt“-Signale – die von D 10!

• Wärter in Schrankenbude 89 schwenkt Kreiselsignal („Halt“), Knallkapseln konnte er nicht mehr auslegen

• Lokführer sieht den Wärter nicht, da dieser zu tief steht

• Wärter in Genthin Ost könnte D 180 noch stoppen – er hat höhere Position


In Genthin Ost

• Stellwerkswärter reagiert überstürzt auf Meldung vom Blockwärter Belicke

• Gibt Schutzhaltesignal mit elektrischer Signallampe (kreisförmig schwingend)

• Er vergisst die Signale auf Halt zu stellen• D 10 sieht die Warnlampe, die für D 180

bestimmt war• D 10 leitet Schnellbremsung ein• D 180 hat „Fahrt-frei“ nach Genthin (von D10)


Unfall Folgen

• D 180 fährt mit 100 km/h auf den im Bahnhof stehenden D 10 auf

• 186 Menschen sterben• 106 Menschen verletztGrößte Eisenbahnkatastrophe in

Deutschland• weiterer Unfall in derselben Nacht mit 101

Toten, 28 Verletzten)


Ursachen

• menschliches Versagen des Lokführers von D 180 (Halt-Signal übersehen)

• menschliches Versagen des Stellwerkwärter Genthin Ost – Verwechselung von D 10 mit D 180, keine Signal-Halt-Stellung

Kette von menschlichen Fehlleistungen führte zum Unfall


Ursachen 2• Indusi bereits in den 20er Jahren erprobt• 1939 war die Indusi schon weit verbreitet• Strecke war mit Indusi-Spulen ausgestattet• Einrichtung an der Lok von D 180 fehlte, da zur

Reparatur!• Aufgrund von Lokmangel (Kriegszeiten) wurde

die Lok trotzdem eingesetzt!menschliches Versagen?• Zwangsbremsung hätte Zugunglück verhindert!• Lokführer bekam 3 Jahre Gefängnis!


Einfluss von Software auf Unfälle

• reine Software-Fehler können ebenfalls Ursachen für Katastrophen sein

• Beispielsweise Fehlfunktion im Fahrzeuggerät -> keine Bremsung

• Funktioniert die Software beim automatischen Fahren?

• Kann man überlappende Fahrstraßen im Stellwerk einstellen?


Beispiele für SW-Fehlverhalten

Kincardine in Ontario, Kanada, Schwerer Reaktorunfall 1990

ausgelöst durch einen Softwarefehler:

Beim Austausch eines abgebrannten Brennelementes geriet die computer-gesteuerte Umlademaschine in einen unkontrollierten Zustand. Als sie sich 40 cm über dem Schachtdeckel befand, wurden durch einen falschen Befehl im Code des Computers, der die Umlademaschine kontrollierte, zugleich alle 4 Bremsen des Hebezuges gelöst und das schwere Gerät fiel auf die Schachtabdeckung. Die Folge war der Austritt von 12.000 I hoch-radioaktivem schweren Wasser aus dem Leck, das in den Brennstoff-behälter geschlagen worden war.



Thule, Grönland, 1960In der US-Frühwarnstation wirdhöchste Alarmstufe ausgelöst.

Durch einen Computerfehler wurde der Mondaufgang als "Nuklearangriff" gewertet.

Ähnliche Fehler waren in der Folgezeit des Öfteren die Ursache für die Menschheit bedrohende Fehlalarme (in einem Fall wurden Wildgänse als einfliegende Formationen von Atomsprengköpfen missdeutet).



Die Objektiv-Linsen der Weltraum-sonde "Hubble" wichen nach einem computergesteuerten Schliff um einige zehntel Millimeter von der optimalen Krümmung ab. Der Fehler lag in der Programmierung der Schleifmaschine. Das Teleskop war daher nach dem Start in den Weltraum nur sehr einge-schränkt zu gebrauchen, lieferte zum großen Teil unscharfe Bilder. Ihm musste in einer Rettungsaktion, die Unsummen verschlang, im Weltraum eine 'Brille' verpasst werden, um die optimale scharfe Leistung wiederzugewinnen. Nur so konnte der Erfolg des gesamten Systems noch gerettet werden.


Software für sicherheitsrelevante Systeme

• Wie entwickelt man Software, die in sicherheitsrelevanten Systemen ausgeführt wird?

• Nicht Inhalt dieser VL:– Entwicklung der Hardware– Entwurf sicherheitsrelevanter

Betriebskonzepte


Definition SystemEin Beispiel:• system:

set of sub-systems or elements which interact according to a design

• sub-system: portion of a system which fulfils a specialised function.

• function: A mode of action or activity by which a product fulfils its purpose.

• element: a part of a product that has been determined to be a basic unit or building block. An element may be simple or complex.

• Problem: Die Definition von Begriffen wie System oder Funktion ist willkürlich,... und wahrscheinlich wird niemals eine universelle Definition gelingen.


Definition System Aber: Die Hauptaufgabe ist die Entwicklung hinreichend gefährdungsfreier Produkte. Die Sicherheit sollte nicht davon abhängen, ob eine Funktion von einem „System” oder „Element” erbracht wird.

Der Benutzer muss das zu betrachtende „System” klar und eindeutig definieren.


Definition SystemEin (Sub-)System zeichnet sich dadurch aus,

dass es sich von der Umgebung abgrenzen lässt (also Systemgrenze und Schnittstellen bekannt sind), unddass es eine wohldefinierte (beabsichtigte) Funktion erbringen soll


System

Sub- System

Umgebung

Sub- SystemSystemelement

HW SW

Definition System


• Checkliste:

Ist die Systemgrenze klar definiert?Sind an der Systemgrenze die Schnittstellen definiert?Sind die Ein- und Ausgaben auf diesen Schnittstellen definiert?Ist die Aufgabe, die das System erfüllen soll, klar definiert?Sind die Einsatzszenarien bekannt und dokumentiert?Ist die Systemstruktur bzw. Systemarchitektur dargestellt?Sind die einzelnen Architekturelemente definiert?Ist ihr Zusammenwirken eindeutig definiert?

Definition System


SCADE-Schulung• Zeit: 02.06.- 05.06.2009,

9:00 Uhr – 17:00 Uhr• Ort: Siemens AG, Ackerstraße 22• Raum: Gebäude 37, Raum 37235

bitte melden beim Eingang Ost, der Raum ist im Erdgeschoss rechts den Gang hinunter und dann auf der linken Seite


Lageplan Siemens AG


Definition RAMSSCenter

ofCompetence

Reliability

RAvailability

A

Maintainability

MSafety

S

Security

S

TOP


Zusammenhang zwischen RAM, S und S

Gefährdungim Betrieb

Techniknicht

verfügbar

Menschliches Versagen

Menschlicher Fehler

Rückfallebene

TechnischeÜberwachungversagt

ZufälligeAusfälle/Störungen

Systematische Fehler

Hier wird in der Regelangenom m en, dass der Menschkeine S icherheitsverantwortung

hat

Anforderung: Hazard Rate HR(alt: wrong side failure ra te) Anforderung: S IL

Anforderung: Verfügbarkeit A Anforderung an d ie m enschlicheZuverläss igkeit

Betrieb licheGefährdung

Subsystem -gefährdung

Normalbetrieb

Sabotage/Vorsatz

Zugriffskontrolle/ -schutz


Definitionen von Sicherheit Sicherheit nach Mü8004: “Die Fähigkeit einer Sicherungsanlage,

bei

• bestimmungsgemäßem Einsatz, • ordnungsgemäßer Instandhaltung und • vorschriftsmäßiger Handhabung

während einer vorgegebenen Brauchbarkeitsdauer Gefährdungen durch Funktionsversagen in dem Umfang, der nach dem Stand der Technik erforderlich ist, auch dann zu verhindern, wenn Bauelementeausfälle und

Störungen in der zu Beanspruchungsbeginn als fehlerfrei angesehenen Sicherungsanlage eintreten.”

D. h. eine Anlage ist (im Sinne der Mü8004) sicher oder nicht.

Sicherheit nach CENELEC: Freiheit von nicht akzeptierten Risiken.


MILITARY-STANDARD

MIL-STD-882System Safety: The application of engineering and management principles, criteria, and techniques to optimize all aspects of safety within the constraints of operational effectiveness, time, and cost throughout all phases of the system life cycle.

Software System Safety Handbook (MIL-STD)Purpose: Provide management and engineering guidelines to achieve a reasonable level of assurance that software will execute within the system context with an acceptable level of safety risk.


Sicherheit: Probleme Wie sicher sind die

Komponenten bzw. Anlagen?

Wie sicher müssen die Komponenten bzw. Anlagen sein?

Wie kann die Sicherheit glaubhaft gemacht werden?

Warum ist die eingesetzte SW/HW frei von systematischen Fehlern?


Was bedeutet RAMSS für Eisenbahnsignaltechnik?

Zwingend notwendige Produkteigenschaften, ohne Nachweis sind die Produkte nicht marktfähig

Funktionsversagen kann katastrophale Folgen haben (Unfälle)

Mangelnde Verfügbarkeit wird pönalisiert Das behauptete Sicherheitsniveau ist

weder durch Gebrauch noch Test positiv nachweisbar

Security wird bisher als Problem unterschätzt


Klassifikation von Fehlern• Zufällige Fehler

– Hardwarefehler als Folge von Alterung– Verschleiß– ausgefallene Transistoren

• Systematische Fehler– mangelhafter Entwurf– Programmierfehler– mangelhafte Auslegung der Hardware

• Unterscheidung– systematische Fehler treten nach Beseitigung nicht mehr auf– zufällige Fehler können sich jederzeit wiederholen

Übergang kann fließend sein: Unterdimensionierter Kühlkörper eines Transistors


Klassifikation von Fehlern 2• Hardware:

zufällige und systematische Fehler• Software:

nur systematische Fehler möglich!

• In dieser VL:Entwicklung von Software, die für die Ausführung auf einer Hardware gedacht ist, die sich für die Ausführung von Sicherheits-Funktionen eignet.

• geeignete Hardware: Erkennen von zufälligen Fehlern!Anschließend: Sicheren Zustand einnehmen


Rechnerarchitektur 1oo1D

Kanal

Eingabe

D

Ausgabe

SF

D SFDiagnose/Monitor Sicherheitsfunktion


Eigenschaften von 1oo1D• Diagnosekomponente ist eine Selbstprüfung• Falls ein Fehler erkannt wird, erfolgt die Ausführung

einer Sicherheitsfunktion (z. B. Abschalten, eingeschränkte Funktion, etc)

• Fehlerhafte Ausgaben werden nicht sofort unwirksam (Diagnose muss erst arbeiten!)

• Gemeinsame HW für Haupt- und Prüfprogramm: Was passiert wenn beide gleichermaßen versagen? Common Cause (gleiche Ursache für denselben Fehler)

• Überprüfung kann auch auf evtl. vorhanden Ausgabebaugruppen verlagert werden

• Geringe Kosten der HW


Rechnerarchitektur 1oo2

Kanal 1

Eingabe

Ausgabe

SF

Kanal 2

=

=

|

=

|

Vergleicher

Oder


Eigenschaften von 1oo2

• Verdoppelung der HW• zufälliger Fehler einer HW-Komponente

kann erkannt werden• fehlerhafte Ausgaben werden unterdrückt• Sicherheitsfunktion muss bei Abweichung

ausgeführt werden• Kanäle müssen synchron gehalten werden• Reduktion von common cause Fehlern



Kanal 1

Eingabe

Ausgabe

SF

Kanal 2

=

=

&

=

&

Vergleicher

Und

Warnung

Warnung


Eigenschaften von 2oo2• ähnlich 1oo2• fehlerhafte Ausgaben werden unterdrückt• Sicherheitsfunktion wird erst beim Erkennen eines

Fehlers in beiden Vergleichern ausgeführt! Weiterlaufen mit einem Kanal theoretisch möglich

• Es kann nicht erkannt werden, welcher Kanal den Fehler hat!

• Warnung notwendig, da nicht klar ob mit fehlerhaften Daten gearbeitet wird

• Kanäle müssen synchron gehalten werden• Reduktion von common cause Fehlern


Rechnerarchitektur 1oo2D

Kanal 1

Eingabe

Ausgabe

SF

Kanal 2

|

=

|

Vergleicher

Oder

D

D


Eigenschaften von 1oo2D

• Verdoppelung von 1oo1D• Erkennen des fehlerhaften Kanals unter

Einschränkungen von 1oo1D• fehlerhafte Ausgaben werden unterdrückt• fehlerhaften Kanal abschalten,

weiterarbeiten nach erstem Fehler möglich• Kanäle müssen synchron gehalten werden



Kanal 1

Eingabe Ausgabe

SF

Kanal 3

Kanal 2 Voter


Eigenschaften von 2oo3

• Verdreifachung der HW• Fehlerhafter Kanal kann erkannt werden• Weiterarbeiten nach erstem Fehler

möglich• Synchronisation noch schwieriger


Rechnerarchitektur XooY• genannten Prinzipien sind nur Beispiele und können beliebig

erweitert bzw. verändert werden• Notwendigkeit der einzusetzenden Architektur sollte aus einer

Risiko-Analyse abgeleitet werden• Vollständige Zweikanaligkeit verringert common cause Ausfälle• Hohes Maß an Ausfalloffenbarung durch Zwei- bzw.

Mehrkanaligkeit möglich• Durch HW-Vergleicher extrem schnelle Ausfalloffenbarung möglich• Durch Symmetrie und HW-Synchronisation sieht der Programmierer

in der Regel nur einen Kanal• Unabhängiges Abschalten durch Vergleicher möglich• Natürlich können auch die Übertragungsmedien mehrkanalig

ausgelegt werden!


Allgemeines zu Mehrkanaligkeit • Probleme:

– Enge Synchronisation und dichte Nachbarschaft der Kanäle machen das System empfindlich für common cause Einflüsse:

– Einflüsse über die Peripherie– Einflüsse über die Stromversorgung– Elektromagnetische Felder– Temperatur (von außen, aber auch durch Nachbarkanal)

• Gegenmaßnahmen– „Sichere“ Trennung der Peripherie vom Rechnerkern– Hoch überwachte Stromversorgung– Hochwirksame Schirmung


Definition SoftwareIntellektuelle Schöpfung, die Programme, Verfahren, Regeln und alle dazugehörige Dokumentation umfasst, die zum Betrieb eines Systems gehören.Anmerkung: Software ist unabhängig vom verwendeten Transportmedium

englische Übersetzungintellectual creation comprising the programs, procedures, rules and any associated documentation pertaining to the operation of a system.NOTE: Software is independent of the media used for transport

Quelle: EN 50128


Fehler in Software

• Software hat keine zufälligen Fehler, nur systematische Fehler!

• Gibt es nichttriviale fehlerfreie Software?• RAMS-Eigenschaften von Software sind

nicht quantifizierbar! -> im Gegensatz zu Hardware


Fishbone Analysis zur Identifikation von Gründen für Softwarefehler

Quelle: A Software Fault Prevention Approach in Coding and Root Cause AnalysisWeider D. Yu


CENELEC nach 50129

Da es nicht möglich ist, die Sicherheit gegen systematische Fehler mit quantitativen Methoden zu bestimmen, werden Sicherheitsanforderungsstufen verwendet, innerhalb derer Methoden, Werkzeuge und Techniken gruppiert werden, die – wenn sie richtig angewendet werden – ein angemessenes Maß an Vertrauen in die Realisierung eines Systems liefern, das die vorgegebene Sicherheitsanforderungsstufe erfüllt.


Sicherheitsanforderungsstufen für Software (SSAS)

SSAS = SIL der Systemfunktionen 5 SIL-Stufen

0 = nichtsichere Anwendungen 1 = niedrigste Anforderungsstufe 4 = höchste Anforderungsstufe

2 Klassen für sichere Anwendungen (1,2) und (3,4)

Maßnahmen sind notwendig bei unterschiedlichen SSAS innerhalb eines Systems


Software und SicherheitSystem-Anforderungsspezifikation,

System-SicherheitsanforderungsspezifikationSystem-Architekturbeschreibung und System-

Sicherheitsplan für das System entgegennehmen

Identifizieren aller der Software zugeordnetenSicherheitsfunktionen

Überprüfen aller der Software zugeordneten Sicher-heitsfunktionen und bestimmen der Software-

Sicherheitsanforderungsstufe

Erstellen der Software-Anforderungsspezifikationund der Software-Architekturspezifikation

Entwerfen, entwickeln und verifizieren/testen derSoftware entsprechend dem Software-

Qualitätssicherungsplan, der Software-Sicherheits-anforderungsstufe und dem Software-Lebenszyklus

Durchführung der Software-Validierung und Übergabe an die Projektierungsingenieure

Betrieb des Systems

Software-Wartung

SW-AnforderungenSW-Anforderungen

SW Architektur und DesignSW Architektur und Design

SW Implementierung und SW Implementierung und TestTest

SW-Abnahme / ZulassungSW-Abnahme / Zulassung


Eingliederung der EN50128

CENELEC-Normen

Eisenbahnsystem

Eisenbahnsignalsystem

Teilsystem Software

EN 50126

EN 50159

EN 50129

EN 50128


Anwendungsbereich

• Verfahren und technische Anforderungen für die Entwicklung• gesamter Bereich der Sicherheitsanwendungen• gilt für jegliche Software, die bei der Entwicklung und Realisierung von

Eisenbahnsteuerungs- und -überwachungssystemen verwendet wird, einschließlich:– Anwendungsprogrammierung;

– Betriebssysteme;

– unterstützende Werkzeuge;

– Firmware.

• Anwendungsprogrammierung schließt Programmierung in Hochsprache, Maschinensprache und speziellen Anwendungssprachen ein (z. B.: ladder logic bei speicherprogrammierbaren Steuerungen).

• gilt nicht rückwirkend (Ausnahme Wartung bei umfangreichen Änderungen)


Aufbau der Norm

Normativer Textteil Normativer Anhang A Informativer Anhang B

Normativer Text

Anhang B

Anhang AAuswahllisten zu

Methoden,

Maßnahmen

und Tools Informationen zuMethoden und Tools

Kapitel

Referenzen (B.nn)


Beispiel 1: Normativer Textteil

8 Software-Anforderungsspezifikation

8.1 Ziele

8.1.1Beschreiben eines Dokumentes, das einen vollständigen Satz von Anforderungen an die Software definiert, der alle Systemanforderungen in dem durch die Software-Sicherheitsanforderungsstufe festgelegten Umfang erfüllt. Es soll ein derart umfassendes Dokument für jeden Software-Ingenieur sein, daß es für ihn nicht erforderlich ist, zum Thema Anforderungen in irgendeinem anderen Dokument nachzusehen.

8.1.2Beschreibung der Software-Anforderungstestspezifikation.

8.2 Eingangsdokumente

1) System-Anforderungsspezifikation ...

8.3 Ausgangsdokumente

1) Software-Anforderungsspezifikation

2) Software-Anforderungstestspezifikation

8.4 Anforderungen

8.4.1Die Software-Anforderungsspezifikation muß die erforderlichen Eigenschaften der zu entwickelnden Software zum Ausdruck bringen und nicht die Verfahren, sie zu entwickeln. Diese Eigenschaften, die alle (außer der Sicherheit) in ISO/IEC 9126 definiert sind, müssen einschließen:

...


Tabelle A18: Halbformale Verfahren (D.7)Referenziert aus Abschnitt 8 und 10

TECHNIK/MASSNAHME Ref SSAS

0

SSAS

1

SSAS

2

SSAS

3

SSAS

4

1. Logik-/Funktionsblock-Diagramme – R R R HR HR

2. Ablaufdiagramme – R R R HR HR

3. Datenflußdiagramme B.12 R R R R R

4. Endliche Zustandsmaschinen/Zustands-Übergangsdiagramme

B.29 – R R HR HR

5. Zeit-Petri-Netze B.64 – R R HR HR

6. Entscheidungs-/Wahrheitstabellen B.14 R R R HR HR

Forderung:

Es muß ein geeigneter Satz von Techniken entsprechend der Software-Sicherheits-anforderungsstufe ausgewählt werden.

Beispiel 1 aus Anhang ATabelle A2: Software-Anforderungsspezifikation (Abschnitt 8)

TECHNIK/MASSNAHME Ref SSAS0

SSAS1

SSAS2

SSAS3

SSAS4

1. Formale Verfahren wie z. B. CCS, CSP,HOL, LOTOS, OBJ, Temporal Logic, VDM, Zund B

B.30 – R R HR HR

2. Halbformale Verfahren D.7 R R R HR HR

3. Strukturierte Verfahren wie z. B. JSD,MASCOT, SADT, SDL, SSADM undYourdon.

B.60 R HR HR HR HR

Forderungen:

1. Die Software-Anforderungsspezifikation erfordert immer eine Beschreibung desProblems in natürlicher Sprache und eine die Anwendung beschreibende mathemati-sche Darstellung

2. Die Tabelle spiegelt zusätzliche Anforderungen wider, die Spezifikation klar und prä-zise zu erstellen. Um der jeweiligen Software-Sicherheitsanforderungsstufe zu genü-gen, müssen eine oder mehrere der genannten Techniken ausgewählt werden.


Beispiel 1 aus Anhang B

• B.14 Entscheidungstabellen (Wahrheitstabellen) (en: Decision Tables (Truth Tables)) (zu Abschnitt 14 und D.7)

• Ziel: –Erstellen einer klaren und zusammenhängenden Spezifikation und Analyse komplexer logischer Kombinationen und Beziehungen.

• Beschreibung:–Diese verwandten Verfahren benutzen zweidimensionale Tabellen zur Kurzdarstellung logischer Beziehungen zwischen booleschen Programmvariablen.

–Durch die Kürze und die tabellarische Form eignen sich beide Verfahren zur Analyse komplexer logischer Kombinationen, ausgedrückt in codierter Form.

–Beide Verfahren können ausführt werden, falls sie als Spezifikation benutzt werden.


Beispiel 2 aus Anhang ATabelle A15: Programmiersprachen (D.4)

Referenziert aus Abschnitt 10

TECHNIK/MASSNAHME Ref SSAS

0

SSAS

1

SSAS

2

SSAS

3

SSAS

4

1. ADA B.62 R HR HR R R

2. MODULA-2 B.62 R HR HR R R

3. PASCAL B.62 R HR HR R R

4. Fortran 77 B.62 R R R R R

5. 'C' oder 'C++' (ohne Beschränkungen) B.62 R – – NR NR

6. Untermenge von 'C' oder 'C++' mitCodierstandards

B.62

B.38

R R R R R

7. PL/M B.62 R R R NR NR

8. BASIC B.62 R NR NR NR NR

9. Assembler B.62 R R R – –

10. Ladder Diagramme B.62 R R R R R

11. Funktionale Blöcke B.62 R R R R R

12. Anweisungsliste B.62 R R R R R


Beispiel 2 aus Anhang A (Fortsetzung)

Forderungen:

1. In Software-Sicherheitsanforderungsstufe 3 und 4 ändert sich bei Gebrauch einerUntermenge der Sprachen 1, 2, 3 und 4 die Empfehlung in ”HR"

2. Für bestimmte Anwendungen sind unter Umständen nur die Sprachen 7 und 9 verfüg-bar. In Software-Sicherheitsanforderungsstufe 3 und 4, in denen eine ”HR"-Auswahlnicht zur Verfügung steht, wird für eine Anhebung der Empfehlungsstufe auf ”R"dringend empfohlen, eine Untermenge dieser Sprachen zu verwenden und eindeutigfestgelegte Codierstandards zugrundezulegen.

3. Für Erläuterungen zur Begutachtung der Eignung einer Programmiersprache wird aufAbschnitt B.62, ”Geeignete Programmiersprache" in der Verfahrensübersicht ver-wiesen.

4. Wenn eine spezielle Programmiersprache nicht in der Tabelle aufgeführt wird, ist sienicht automatisch ausgeschlossen. Sie sollte aber mit B.62 übereinstimmen.


Beispiel 2 aus Anhang A (Fortsetzung)Ziel

Möglichst weitgehende Unterstützung der Anforderungen dieses Internationalen Standards, besonders bezüglich defensiver Programmierung, strenger Typisierung, strukturierter Programmierung und möglicherweise der Assertion-Technik. Die gewählte Programmiersprache soll mit einem Minimum an Aufwand zu leicht verifizierbarem Code führen und soll die Programmentwicklung, Verifikation und Wartung vereinfachen.

Beschreibung

Die Sprache sollte vollständig und eindeutig definiert sein. Die Sprache soll eher anwender- oder problemorientiert, weniger maschinenorientiert sein. Weit verbreitete Sprachen oder ihre Untermengen werden gegenüber Sprachen für spezielle Anwendungen bevorzugt.

Zusätzlich zu den schon erwähnten Merkmalen sollte die Sprache folgendes beinhalten:

– Blockstruktur;

– Kontrolle während der Übersetzungszeit;

– Kontrolle von Datentypen und -feldern während der Laufzeit; und

– Parameterkontrolle.

Die Sprache soll folgendes unterstützen:

– den Gebrauch kleiner und handhabbarer Module;

– Beschränkung des Zugriffs auf Daten in definierten Modulen;

– Definition von eingeschränkten Wertebereichen für Variable; und

– weitere Merkmale fehlerminimierender Konstrukte.

Es ist wünschenswert, daß die Sprache von einem geeigneten Übersetzer, angemessenen Biblio theken bereits bestehender Module, einem Debugger und Werkzeugen zur Versionsverwaltung und Entwicklung unterstützt wird.


Beispiel 2 aus Anhang A (Fortsetzung)

Fortsetzung B.62

Merkmale, die die Verifikation erschweren und deshalb vermieden werden sollten, sind folgende:

– unbedingte Sprünge, außer Unterprogrammaufrufen;

– Rekursionen;

– Zeiger, Stapelspeicher oder sonstige dynamische Variable oder Objekte;

– Interruptverarbeitung auf Quellcodeebene;

– mehrere Ein- oder Ausgänge bei Schleifen, Blöcken oder Unterprogrammen;

– implizite Variableninitialisierung oder -deklaration;

– variable Datensätze und Gleichartiges; und

– verfahrensabhängige Parameter.

Sprachen auf niederem Niveau, besonders Assemblersprachen, führen infolge ihrer Hardwareorientierung zu Problemen.


ProzeßProzeß

Ergebnisse

Phase

Software/Hardware-Integrationsphase

Software/Hardware-Integrationstestbericht

Software-Anforderungsspezifikationsphase

Software-AnforderungsspezifikationSoftware-AnforderungstestspezifikationSoftware-Anforderungsverifikationsbericht

Software-Begutachtungsphase

Software-Gutachten

Software-Wartungsphase

Software-WartungsaufzeichnungenSoftware-Wartungsprotokoll

Software-Planungsphase

Software-EntwicklungsplanSoftware-QualitätssicherungsplanSoftware-Konfigurationsmgm.-PlanSoftware-VerifikationsplanSoftware-IntegrationsplanSoftware/Hardware-IntegrationsplanSoftware-ValidationsplanSoftware-Wartungsplan

Codierphase

Software-Quellcode und ZusatzdokumentationSoftware-Quellcodeverifikationsbericht

System-AnforderungsspezifikationSystem-SicherheitsanforderungsspezifikationSystem-ArchitekturbeschreibungSystem-Sicherheitsplan

Software-Modulentwurfsphase

Software-ModulentwurfsspezifikationSoftware-Modultestspezifikation

Software-Modulverifikationsbericht

Software-Integrationsphase

Software-Integrationstestbericht

Software-Modultestbericht

Software-Validierung

Software-Validationsbericht

Software-Modultestphase

Software-EntwurfsspezifikationSoftware-Entwurfstestspezifikation

-Entwurfsverifikationsbericht

Software Architektur & Entwurfsphase

Software-ArchitekturspezifikationSoftware-EntwurfsspezifikationSoftware-Entwurfstestspezifikation

Software-Architektur und

VerVal


ProzeßProzeß

Ergebnisse

Phase






Software-Gutachten





Codierphase

















VerVal

System-Anforderungsspezifikation

System-Sicherheitsanforderungsspezifikation

System-Architekturbeschreibung

System-Sicherheitsplan

Software-Anforderungsspezifikationphase

Software-Anforderungsspezifikation

Software-Anforderungstestspezifikation

Software-Anforderungsverifikationsbericht


Software-Entwicklungsplan

Software-Qualitätssicherungsplan

Software-Konfigurationsmgm.-Plan

Software-Verifikationsplan

Software-Integrationsplan

Software/Hardware-Integrationsplan

Software-Validationsplan

Software-Wartungsplan


Software-Architekturspezifikation

Software-Entwurfsspezifikation

Software-Entwurfstestspezifikation

_______________________________________________

Software-Architektur und -Entwurfsverifikationsbericht

Software-Modulentwufsphase

Software-Modulentwufsspezifikation

Software-Modultestspezifikation

_______________________________



______________________



____________________________



______________________________________



_________________________



_______________________________

Software-Gutachten


___________________________________

Software-Wartungsaufzeichnungen

Software-Wartungsprotokoll


ProzeßProzeß

Ergebnisse

Phase






Software-Gutachten





Codierphase

















VerVal


Dokumente / Ergebnisse

Definitionen / Anforderungen zu den Phasen des Lebenszyklus‘ (Textteil)

Vorgaben von Maßnahmen und Tools (Anhang A)

Vorgaben zu Reviews (Verifikation)

Verfolgbarkeit der Anforderungen


Rollen und Unabhängigkeiten

EI, VER, VAL

EI VER, VAL

GUT

GUT

EI VER, VAL

PRJ MGR GUT

EI VAL

PRJ MGR

VER

GUT

Schlüssel: = kann dieselbe Person sein

= kann dieselbe Firma sein

STUFE 0

STUFEN 1 & 2

STUFEN 3 & 4

STUFEN 3 & 4

ODER

EI = Entwerfer

GUT = Gutachter

VER = Verifizierer

PRJ MGR = Projekt Manager

VAL = Validierer

Anerkannter Fachbetrieb:Der Gutachter kann auch der entwickelnden Firma unterstellt sein, wenn eine ausreichende Unabhängigkeit zur entwickelnden Abteilung gewährleistet ist

Voraussetzung:Anerkennung durch Zulassungsbehörde wie z.B. EBA


Aufgaben und Rollen

Software-Anforderungsspezifikation (Abschnitt 8) Entwerfer

Software-Anforderungstestspezifikation (Abschnitt 8) Validierer

Software-Architektur (Abschnitt 9) Entwerfer

Software-Entwurf und -Entwicklung (Abschnitt 10) Entwerfer

Software-Verifikation und -Testen (Abschnitt 11) Verifizierer

Software/Hardware-Integration (Abschnitt 12) Entwerfer

Software-Validierung (Abschnitt 13) Validierer

Software-Begutachtung (Abschnitt 14) Gutachter


Verifikation und Validation

• Verifikation: Analyse und Testen um festzustellen, ob das Ausgangsprodukt jeder Phase des Lebenszyklus die Anforderungen aus der vorhergehenden Phase erfüllt.

• Draft EN50128, Feb. 1998

• Validation: Analyse und Testen zur Demonstration, daß das Produkt in allen Belangen seine spezifizierten Anforderungen erfüllt.

• Draft EN50128, Feb. 1998

Wird richtig entwickelt

Ist das Richtige entwickelt worden?


Anwendungsspezifisch konfigurierbare Systeme


Anwendungsspezifisch konfigurierbare Systeme

Anforderungs-spezifikation

Systementwurf

Implementierung

Systemintegration

Systemzulassung

Verifikation

Verifikation

Verifikation

Verifikation

Anlagen-spezifikation

Installationsentwurf

Produktion

Installationstests

Abnahme undÜbergabe

Verifikation

Verifikation

Verifikation

Verifikation

Anlagen-validierung und-zertifizierung

System-validierungund-zertifizierung

Entwurf und Entwicklungdes generischen Systems

AnwendungsspezifischeProjektierung der Anlage

17.4.2.1 In der Phase des Softwa-reentwurfes ... muß ein Datengene-rierungsplan erstellt werden, um dieDokumentationsstruktur des Daten-generierungsprozesses festzulegen.... Der Plan muß festlegen, welcheVerfahren und Werkzeuge für dieDatengenerierung zu verwendensind, ... Der Plan muß die Anforde-rungen der Unabhängigkeit zwischenden für die Verifikation, Validierungund den Entwurf zuständigen Mitar-beitern festlegen.

17.4.2.3 In der Phase des Software-Entwurfs müssen die detailliertenSchnittstellen zwischen der gene-rischen Software und den anwen-dungsspezifischen Daten festge-legt werden..., z. B. als Ergebnis ei-ner Anforderung zur Benutzung einervorhandenen anwendungsspezi-fischen Sprache.

17.4.3.3 In der Phase des Soft-ware-Modulentwurfes muß einestrenge Trennung zwischen denSpeicherbereichen des Pro-grammcodes und der Daten er-zwungen werden, .... Ebenso solltenanwendungsspezifische Daten vonanderen Daten getrennt werden.

17.4.1.1 Spezifikation deranwendungsabhängigen AnforderungenDie Anforderungen für die Anwendung müssenfestgelegt werden. ...17.4.1.2 Entwurf der GesamtinstallationDie Systemarchitektur ist zu definieren und derUmfang und die Art der zu verwendenden generischenKomponenten festzulegen. ...17.4.1.3 DatengenerierungDie Aktivitäten zur Datengenerierung müssen dieErstellung der speziellen Information (z. B.Steuerungstabellen), die Erzeugung desDatenquellcodes und seine Compilierung, diePrüfung und andere Verifikationstätigkeiten sowie dasTesten der Anwendungsdaten umfassen.17.4.1.4 Integration und AbnahmeBei einigen Systemen werden dieanwendungsspezifischen Daten vor der Installation vorOrt für eine Werksprüfung mit der generischen Hard-und Software integriert. ... Schließlich muß das Systemvoll betriebsfähig übergeben und eine abschließendeAbnahme an der vollständigen Installationausgeführt werden.17.4.1.5 Validierung und BegutachtungAktivitäten zur Validierung und Begutachtung müssendas Verhalten auf jeder Stufe des Lebenszyklusauditieren.


Begutachtung

Vorgaben der Maßnahmen zur Begutachtung (Anhang A) Entwicklungsbegleitende Begutachtung

Zustimmung zum SW-Validierungsplan Zustimmung zu den Maßnahmen (Anhang A) der Entwicklung Zusätzliche Verifikations-/Validationsschritte

Analyseprozeß zur Feststellung, ob die Entwurfsinstanz und der Validierer ein Produkt zustande gebracht haben, das die spezifizierten Anforderungen erfüllt und um zu beurteilen, ob das Produkt für seinen gedachten Anwendungszweck geeignet ist.

To evaluate that the lifecycle processes and products resulting are such that the software is of the defined software safety integrity level and is fit for its intended use.


Begutachtung im EntwicklungsprozeßBegutachtung im Entwicklungsprozeß






Software-Gutachten





Codierphase

















VerifikationValidierung

Zustimmung

Begutachten

Begutachten

Begutachten ab SIL 3

Begutachten


Begutachten




Begutachten


Zusammenfassung EN 50128

Vorgaben für den Entwicklungsprozeß Festlegung von Maßnahmen und Tools Anforderungen an Dokumente Unabhängige Stellen


Modellbasierte Entwicklung


Ursprünge der modellbasierten EntwicklungErste Ansätze in den 80er Jahren mit den CASE-ToolsModellierungselemente waren: SA/SDEs gab viele Erfolge mit CASE-Tools

Qualitätsverbesserung Bessere Beherrschung der KomplexitätMehr Abstraktion mehr Plattformunabhängigkeit

Die CASE-Tools hatten aber auch noch einige Unzulänglichkeiten

Roundtrip-Engineering nicht möglich Formale Verifikation noch nicht ausgereiftTool-Entwicklung war nicht fortschrittlich genugModellelemente waren für viele Probleme nicht ausreichend


Was ist modellbasierte Entwicklung?

Model n

Code

Model 1

Model n - 1

Transformation

Transformation

Transformation

Modellbasierte Entwicklung definiert:

n Hierarchieebenen auf jeder Ebene eine (formale,

domänenspezifische) abstrakte Sprache

Transformationen zwischen den Hierarchieebenen

möglichst weitgehende Automatisierung der Transformationen


Motivation für modellbasierte Entwicklung

• Logisch funktionale Inhalte auf hoher Abstraktionsebene

• Unabhängig von konkreter Hardwareplattform lange Produktlebenszyklen

• Effizienzsteigerung in der Entwicklung

• Frühzeitige Fehleroffenbarung

• stärkere Verknüpfung von Implementierung und Dokumentation

• Qualitätssteigerung

• Einsatz von Analysewerkzeuge (z.B. Model Checker) Nachweis von Sicherheitseigenschaften

• Unterstützung der Zertifizierung von Systemen


Begriff „MDA“ und Abgrenzung (1)Eigenschaften der modellbasierten Entwicklung (MDA - model driven

architecture) sind:

– Verwendung von Modellen zur Softwareentwicklung zur Abstraktion– Verwendung von Generatoren/Transformatoren zur

Softwareentwicklung– Auch teilweise Automatisierung möglich (je nach fachlicher

Anforderung zwischen 20% und 100%)– Die erst Abstraktionsebene wird vollständig manuell erzeugt– Ziel ist die Steigerung der Softwarequalität– Schlagwort „Automation durch Formalisierung“ in frühen

Entwicklungsphasen– Definitionen MDA, MDSD, MDSE nicht einheitlich und weichen je

nach Literaturquelle voneinander ab


Begriff „MDA“ und Abgrenzung (2)– Die Modelltransformation erzeugt Modelle zur manuellen

Weiterbearbeitung– MDA erfordert anwendungsspezifische Frameworks– MDA erfordert plattformspezifische Generatoren– MDA kann - abhängig von der Vollständigkeit der

Codegenerierung – auch änderungsunfreundlich sein – MDA sagt nichts über den Abstraktionsgrad von Plattformen

aus– Plattformen können aufeinander aufbauen.– Logische Fortsetzung des Abstraktionsgedankens bei der

Entwicklung – manuelle Drahtverbindung, Maschinencode, Assembler, Programmiersprache, Modellierungssprache


MDA und OMG– Ein Gesamtmodell wird in mehrere Schichten

unterteilt:

• Computation Independent Model ► (CIM)für die umgangssprachliche Beschreibung

• Platform Independent Model ► (PIM)für die Geschäftsprozesse

• Platform Specific Model ► (PSM)für die Architektur und Services

• Codemodell ► für die Zielplattform


Modelltransformation


PIM und PSM bestimmen sich über Kontext


Ausführbare ModelleModelle, die durch die Verwendung eines Code-Generators

direkt ausgeführt bzw. interpretiert werden können.• Voraussetzung:

– Sprache zur Beschreibung von Algorithmen– Strukturen für die Ausführung (Simulationsumgebung)

• Ziel: vollständig ausführbare PIMs– Komplette Entwicklung auf Modellebene– Ausführung des Modells zum Testen– weitgehende Generierung des Codes

• Sehr gute Komponenten-Architektur – MDA erfordert immer noch „DENKARBEIT“


MDA und UML– Ein MDA-Modell ist eine abstrakte Repräsentation

von Struktur, Funktion oder Verhalten eines Systems– Ein MDA-Modell wird in der Regel in UML

beschrieben– UML-Diagramme sind nicht per se MDA-Modelle– Die Semantik der MDA-Modelle wird durch die

Verwendung einer entsprechenden Modellierungssprache formal definiert

– Es werden UML-Profile und entsprechende Transformationsregeln zwischen MDA-Modell und plattformspezifischem Modell eindeutig definiert


MOF – Meta Object Facility

• OMG standard• stellt Framework für das Management von

Metadaten zur Verfügung• Unterstützt die Entwicklung modell-

/metadatenbasierter Entwicklung• diverse UML-Profile verwenden MOF• XMI verwendet ebenfalls MOF


4 MOF-Ebenen• M0-Ebene - Konkret (Ausgeprägte Daten)• M1-Ebene - Modelle (z. B. logische Daten-,

Prozess- oder UML- bzw. Objekt-Modelle, die die Daten der M0-Ebene definieren)

• M2-Ebene - Sprachebene (Definieren, wie die Sprache über den Modellen von M1 aufgebaut und strukturiert sind)

• M3-Ebene - Meta-Sprache (Abstrakte Ebene, die zur Definition der M2-Ebene herangezogen wird)


M3-Ebene:

http://upload.wikimedia.org/wikipedia/de/6/68/MOF_Metamodel_144dpi.jpg


Wie viele Ebenen definiert MOF?

• 4 Ebenen sind nur ein Beispiel• Grundlagen sind Klasse und Instanz• MOF definiert die Möglichkeit von einer

Instanz zu ihrem Metaobjekt zu navigieren• Somit kann mit Hilfe von MOF jede

beliebige Anzahl von Ebenen definiert werden

• Mindestens zwei Ebenen


Automatendefinition in 3 Ebenen• M2:

{} Mengenlehre aus Mathematik -> Funktionen x Kartesischen Produkt

• M1:A = (Z, E, A, F) Z = {z1, … , zn) E = {e1, …, en) A = {a1, …, an) F: ZxE -> ZxA

• M0:A = ({1,2,3}, {tr}, {a, b, c}, ((1,tr) -> (2,a), (2,tr) -> (3,b), (3,tr) -> (1,c)))


Automatendefinition in 3 Ebenen

Aggregation [1:n]

Klasse

Assoziation n:m

Knoten Kante Bedingung

Aktion

Rollenname m:n

Rollenname [1:n]

Rollenname [1:n]

tr tr

tr

1 / c

2 / a3 / b

M2: M1:

M0:


Programmiersprachen in 4 Ebenen M3

• M3 - Definition der BNF (Backus-Naur-Form)

Definition =Endezeichen ;Logisches Oder |Option [ ... ]Optionale Wiederholung { ... }Gruppierung ( ... )Terminal- und Nichtterminalsymboleusw.



• M2: Syntax der Programmiersprache in BNF

Programm = 'PROGRAM' Bezeichner 'BEGIN' { Zuweisung [";"] } 'END' "." ; Bezeichner = Buchstabe { ( Buchstabe | Ziffer ) } ; Zahl = [ "-" ] Ziffer { Ziffer } ; String = '"' { AlleZeichen − '"'} '"' ; Zuweisung = Bezeichner ":=" ( Zahl | Bezeichner | String ) ;



• M1: ProgrammPROGRAM DEMO1

BEGIN A0:=3; B:=45; H:=-100023; C:=A; D123:=B34A; ESEL:=GIRAFFE; TEXTZEILE:="Hallo, Welt!";

END.



• M0: Programmausführung mit Instanzen/Daten


Meta-ProgrammierungMeta-Modellierung

• Definition von Domänen-Spezifischen Sprachen (DSL)

• Modelltransformation• Sprachumfang wird auf das Nötigste beschränkt• Schneller zu lernen als manche UML-Profile

Definition MARTE-Profile über 600 Seiten! • Guter Programmierzugang für Nicht-Informatiker

Wichtig für interdisziplinäre Entwicklung• Sprache nicht zu einfach wählen,

Abstraktionskonzepte nicht vergessen!• Qualitätssicherung der Modelltransformationen


Werkzeuge zur Meta-Programmierung/-Modellierung

• TOPCASED (Toolkit in Open Source for Critical Applications & Systems Development)

• EMF (Eclipse Modeling Framework)

• MetaEdit


SCADE


Grundlagen der SCADE-Modellierung

Modell

Takt

Eingänge Ausgänge

• SCADE-Modellierung beschreibt:

• SW-Regelkreisen und Signalverarbeitung (Differenzengleichungen)

• Endliche Zustandsmaschinen (Hierarchie, Parallelismus)

• Synchron getaktetes Modell


Grundlagen synchroner Programmierung

Gut geeignet für Regelungen und Endliche Automaten

Eingaben lesenReaktion berechnenAusgaben schreiben

Synchron = 0-Delay innerhalb eines Taktes fürKontrollflussSignalfluss

Vorteile: I/O und Berechnungen sind sauber getrennteinfaches Semantik, die auf Datenflüssen (Streams) beruht


Synchrone Hypothese

Wenn der Raum klein genug ist, können Sängerin und Publikum die

Schallgeschwindigkeit vernachlässigen.

Spezifizieren mit 0-DelayImplementieren mit vohersagbarem Delay


Synchrones Zeitmodell

• Zeit wird zu einer logischen Größe

Logische Zeit

Implementationszeit

i6

o7o5o1 o2 o6o4o3

i7i5i4i3i1 i2

i6

o7o5o1 o2 o6o4o3

i7i5i4i3i1 i2

WCET = garantiert keine ÜberlappungWCET: Worst Case Execution Time


Überblick über die SCADE-Syntax• Daten

– Starke Typisierung (bool, int, real, array, structure)– Nur statische Datentypen

• Datenfluss Beschreibung– Boole’sche Logik (not, and, or, etc.)– Arithmetik (+, -, *, /, mod, etc.)– Auswahl (if … then … else …; switch case)– Keine Schleifen – aber Map / Fold über Felder– Temporale Operatoren: Zugriff auf vorherige Datenflusswerte (fby=“followed

by”)

• Safe state machines– Synchrone Automaten– Hierarchie – Parallelismus


Scade Syntax - Datentypen• Grundtypen:

bool, int, real, char

• Nutzerdefinierte TypenAufzählungstypen

type COLORS = enum {RED, GREEN, BLUE};Strukturen

type Sensor = {valid: bool; value: real;};Arrays

type RealArray = real^5;type ElevatorButtons = int^(FLOORS);

• Typen der Zielsprachetype imported CanMessage;


SCADE Semantik• Ein Datenfluss ist eine unendliche Folge von Datenwerten

Cycle 1 2 3 4 5Cond false true true false true

not(cond) true false false true false

3.14 3.14 3.14 3.14 3.14 3.14

I 14 13 11 12 16I + 3.14 17.14 16.14 14.14 15.14 19.14fby(I; 2; 0) 0 0 14 13 11


Gleichungen• Syntaktische Gleichungen definieren Datenflüsse:• fib, aux: nat;• fib = fby(aux, 1, 0)• aux = fby(aux + fib, 1, 1);

Cycle 1 2 3 4 50 0 0 0 0 01 1 1 1 1 1aux 1 1 2 3 5fib 0 1 1 2 3aux + fib 1 2 3 5 8


Ein einfacher Zähler

node Counter (Reset: bool) returns (Count: int)Count = if Reset then 0 else 1 + fby(Count,1,0)


Zustandsmaschinen

Count: int last = 0;


Der last OperatorWenn Up aktiv ist

Count = last 'Count + 1;

Wenn Down aktiv istCount = last 'Count – 1;

last 'Count ist immer der letzte Wert von Count im gesamten Skope dieses Datenflusses

Wenn STAND_BY aktiv ist, behält Count seinen vorherigen Wert

Die Initialisierung von Count geschieht aufgrund der Deklaration

Count: int last = 0;


Parameter Polymorphismusnode toggle_sample (a, b: int) returns (c: int)var flag: boollet flag = fby(not flag, 1, true); c = if flag then a else btel

monomorphic

node toggle_sample (a, b: 'T) returns (c: 'T)var flag: boollet flag = fby(not flag, 1, true); c = if flag then a else btel

polymorphic


Array Map Operator (Beispiel: Elementweise Summe)

node SumScalar (a,b: int) returns (c: int)let

c = a + b;telnode SumArray(t,u: int^3) returns (v: int^3)let

v = (map SumScalar <<3>>) (t,u);telSumArray([1,2,3],[2,4,0]) [3,6,3]);


Array Fold Operator(Beispiel: akkumulierte Summe)

node AccumulatedSum(t: int^5) returns (v: int)letv = (fold SumScalar <<5>>) (t);tel

AccumulatedSum([1,2,3,4,5]) 15;


Qualitätssicherung von Entwicklungswerkzeugen


Was sagt die CENELEC-Norm?• CENELEC-Norm gilt auch für „unterstützende Werkzeuge“• „angemessener Satz an Werkzeugen“ soll eingesetzt werden.• Automatische Testwerkzeuge und integrierte Entwicklungswerkzeuge werden empfohlen. • Werkzeuge und Hilfsmittel sollten zum frühest möglichen Termin verfügbar sein.• Software-Werkzeuge müssen für den Zweck geeignet sein.

• In der Praxis:• Werkzeuge mit Validierung, Begutachtung und Zulassung!• Werkzeuge ohne Nachweis der Qualifizierung• Und alles was dazwischen ist• Neue Version der EN 50128 klassifiziert Werkzeuge:

– T1: Kein direkter oder indirekter Einfluss auf Code: Editoren, Requirements Management Tools– T2: Verifikations- und Testwerkzeuge: Fehler im Tool erzeugen keine Fehler im

Produkt, aber er bleibt evtl. unentdeckt– T3: Output hat direkten oder indirekten Einfluss auf das sicherheitsrelevante System

• Werkzeuge werden in Zukunft normativ stärker betrachtet


Qualifizierung von Werkzeugen? • Automatisierung manueller Tätigkeiten• Werkzeug besitzt deterministisches Fehlerverhalten• Mensch besitzt stochastisches Fehlerverhalten• Nachgelagerte Qualitätssicherung zum Fehlerfinden

-> keine Qualifizierung von Werkzeugen notwendig!

• Einsparen von Qualitätssicherungsschritten:-> Qualifizierung von Werkzeugen notwendig!

• Es gibt auch Werkzeuge, die weit über die Möglichkeiten manueller Tätigkeiten hinaus gehen:

– Compiler, – Model Checker, – färbende einrückende Editoren, – Debugger, etc.


Qualifizierung am Beispiel v. Generatoren/Compilern

• Generator durch Validierungssuite

• Vorwärts- Rückwärts mit Vergleich

• 2 mal diversitär Vorwärts mit Vergleich

• Test der Applikation mit Abdeckungsmessung auf Bytecode/Assembler-Ebene

• Generierung der Testfälle aus dem Modell mit Abdeckungsmessung

• Generierung der Testfälle aus einem Testmodell anschließende Abdeckungsmessung

• Formal beweisbare Übersetzung


Validierungssuite• Validierungssuite: Sammlung von

Testfällen (ausführlich)

• Bei Unvollständigkeit der Sammlung bleiben ungetestete Situationen übrig.

• Testendekriterien bleiben genauso entscheidend wie bei den Tests des sicherheitsrelevanten Systems

• Validierungssuite muss nicht besser sein als ein Test eines sicherheitsrelevanten Systems

• gängige Praxis bei der Validierung von Compilern

Gen

Model

Code

Soll/Ist-Vergleich

Validierungssuite


zweimal diversitär Vorwärts mit Vergleich

G1

M

G2

C1 C2Vergleich

• Setzen G1 und G2 auf denselben Spezifikationen auf?

• Können G1 und G2 wirklich unabhängig sein?

• diversitäre Auslegung des Vergleichers?

• In der Luftfahrt wird diversitäre Vorwärtsentwicklung im first und second level eingesetzt

• doppelter Transformationsaufwand (Kosten)

• Validierung der Ergebnisse bei jeder Übersetzung -> keine fehlenden Testfälle


Vorwärts- Rückwärts mit Vergleich• Diversität durch unterschiedliche

Aufgaben besser gegeben• Vergleich diversitär?• Falls Transformation nicht eineindeutig

ist, kann M‘ nicht wiederhergestellt werden.

• Evtl. zusätzliche Hilfen notwendig, damit M‘ aus dem Code herstellbar ist.

• Vergleicher kann mit Intelligenz ausgestattet werden (Äquivalenzvergleich)

• Validierung mit jeder Übersetzung. • Fehler in V mit anschließender

Fehlerverschleierung in R relativ unwahrscheinlich -> sehr gute Fehleroffenbarung

V

M

R

Code

M’Vergleich


Testfälle aus Modell mit Abdeckungsmessung

• Generierte Testfälle nur für die Korrektheit des Generators (Gen)

• Abdeckungsmessung soll die Güte der erzeugten Testfälle dokumentieren und nachweisen (optional).

• Validierung mit jeder Übersetzung und Testausführung -> keine offenen Testfälle

• Keine Funktionstests des Modells, die müssen noch gesondert formuliert und durchgeführt werden.

Gen

Model

Code

TestCase-Execution

Code-Coverage

Test-Case

Test-Gen


Abdeckungsmessung auf generiertem Code

• Generierte Code wird mit Testfällen aus der Validierung abgedeckt

• keine offene Funktionalität im Code vorhanden, da Testabdeckung gemacht

• Test der Generierung wird mit den ohnehin notwendigen Funktionstests kombiniert -> Einsparung intensiver Generator-Tests

• Abdeckungsmessungen können sehr aufwändig sein, bei sehr viel generiertem Code

• Abdeckungsmessungen können manuelle Argumentation für nicht abgedeckte Testfälle haben -> aufwändig

Gen

Model

Code

TestCase-Execution

Code-Coverage

Valid. Test-Case


Testmodell mit Abdeckungsmessung• ähnlich voriges Beispiel, allerdings

werden die Testfälle aus einem separaten Testmodell erzeugt.

• impliziter Funktionstest des Systems• korrekte Generierung wird über die

korrekte Testausführung nachgewiesen

• doppelter Modellierungsaufwand (Modell + Testmodell)

• Abdeckungsmessung weist Güte der generierten Testfälle nach

• Abgleich zwischen Modell und Testmodell kann anhand der Abdeckungsmessungen schwierig sein

Gen

Model

Code

TestCase-Execution

Code-Coverage

Test-Case

Test-Model

Test-Gen


Formal beweisbare Übersetzung• Korrektheit der Übersetzung

anhand eines formalen Nachweises auf der Ebenen der Sprachdefinitionen

• Formale Semantik der Sprachen notwendig

• Evtl. aufwändige Nachweise notwendig

• bisher noch keine industrielle Anwendung in der Breite möglich (Forschungsgegenstand)

Gen

Meta-M

Meta-C

FormalProof


Qualifizierung in der Praxis• Werkzeuge mit Validierung, Begutachtung und

Zulassung!• Werkzeuge ohne Nachweis der Qualifizierung• Und alles was dazwischen ist• In der Überarbeitung der CENELEC werden Werkzeuge

differenzierter betrachtet:– T1: Kein direkter oder indirekter Einfluss auf Code: Editoren,

Requirements Management Tools– T2: Verifikations- und Testwerkzeuge: Fehler im Tool erzeugen

keine Fehler im Produkt, aber er bleibt evtl. unentdeckt– T3: Output hat direkten oder indirekten Einfluss auf das

sicherheitsrelevante System• Werkzeuge werden in Zukunft normativ stärker

betrachtet


Formale Verifikation in SCADE


Model Checking von SCADE-Modellen

Durchführung: Verknüpfung mit synchronem ObserverAnwendung liefert Testscenario bzw. Nachweis

Grundlage Stalmarcks Algorithmus (Prover Technologies

Übersetzung SCADE Aussagenlogik + (Presburger) Arithmetik

Model Checking und Zertifizierung


Synchrone Observer

Design Verifier

Design<EreignisBehandlung>

Tim erC allback

Nachricht_von_ECAC

Anwender_Bef ehlStoerung_Ereignis

Pruef ung_Ereignis

Idle

1

E_Pruef ung

1

last 'HabeFertig_SM_EreignisBeh

2

E_Stoerung1

last 'HabeFertig_SM_EreignisBeh3

A_Ereignis

5

E_N achricht

1

last 'HabeFert ig_SM_EreignisBeh

1

las t 'HabeFertig_SM_EreignisBeh

4T_Ereignis

1

las t 'H abeFert ig_SM_EreignisBeh

Eigenschaft

JA NEIN + Testfall

2

Implies

Grundstellen

Ausf ahrt

Einfahrt

Frei

PRE

PRE

PRE

Property

PRE

Idee von Model Checking Eigenschaften werden als Observer in SCADE formuliert:

Design Verifier prüft, ob die einzige Ausgabe des Observers immer true ist.

Beispiel: SW-Komponente eines Achszählers


Formulierung von Eigenschaften

• Aussagenlogik: logische Operatoren and, or, implies, …

• Temporale Operatoren von SCADE: fby, pre und daraus abgeleitete

• Lineare Arithmetik (auch Presburger Arithmetik):

Integer: Multiplikation mit höchstens einer Variable

Real: Multiplikation und Division mit höchstens einer Variable

Linear Nicht linear5 * X + Y X * Y + 1Z / 2 - W Z / T - 5(T%3) * 2 W % P * 3

Mathematische Funktionen (sin, cos, sqrt) und Potenzen gehen nicht!


Einige abgeleitete temporale Operatoren

AlwaysAfterFirstCond: gleicht Input1 sobald Cond einmal true wird; vorher immer true


Einige abgeleitete temporale Operatoren

AtLeastNTick: wird immer dann true, wenn Input1 n-mal hintereinander true war; false sonst


Algorithmische Grundlagen des Model Checkers

• Hersteller: Prover Technologies

• Lösungsalgorithmen für das SAT-Problem; z.B. Davis-Putnam-Logemann-Loveland-(= DPLL-)Algorithmus

• Entscheidungsalgorithmen für Datengleichungen• Constraint solver• Stålmarks Algorithmus:

Eingabe: Aussagenlogische Formel

AusgabeEntweder: Beweis im Dilemma-Beweissystem dass die Formel Tautologie ist;

Oder: Belegung der Variablen, die die Formel false macht


Übersetzung SCADE in Aussagenlogik1. Automaten durch Datenflussbeschreibung ersetzen

2. Alle fby(…, n,…) durch fby(…,1, …) ersetzen

3. Hilfvariablen einführen, so dass nur noch fby(xi, 1, …) vorkommt Jetzt gibt es nur noch, Logik, Arithmetik, fby(xi, 1, …)

4. SCADE-Knoten node anObserver (x1, …, xn) returns (Prop: bool) wird übersetzt zu Boole’scher Funktionenf(i, x1, ..., xn, pre(x1), …, pre(xn))

5. Induktionsbeweis mit Stålmarks Algorithmus: Beweise a) f(true, x1, ..., xn, pre(x1), …, pre(xn))

b) f(false, x1, …, xn, pre(x1), ..., pre(xn)) f(false, y1, …, yn, x1, …, xn)


Beispiel

• node risingedge(x: bool) returns (y: bool);• y = x and fby(not(x), 1, false);

(Hilfvariable einführen)

z = not(x); y = x and fby(z, 1, false);

(Übersetzung in Boole‘sche Funktion – Gleichen werden zu logishen Äquivalenzen)

))())pre((())( false)(())pre(),pre(,,,( xzzxixzxizxzxif

Sommersemester 2009SW in sicherheitsrelevanten Systemen Software in sicherheitsrelevanten Systemen...

Documents

Transcript of Sommersemester 2009SW in sicherheitsrelevanten Systemen Software in sicherheitsrelevanten Systemen...