Home

Seminar Sicherheitskritische Systeme

1. Abbildung 4 Vererbungshierarchie der neuen Memory Klassen Ebenso unterst tzt das RTJ Memory Management die Reservierung von Speicher f r Threads F r einen individuellen Thread kann der maximale Speicherverbrauch bei der Erstellung angegeben werden Beispiel 5 public class ThinkMemoryExample implements Runnable public void run ScopedMemory ma try ma new ScopedMemory 65536L if ma instanceof MemoryArea throw new Exception Return object is not instance of MemoryArea long size ma size if size lt 0 throw new Exception Memory size is less than_ 0 catch Exception e System out printin Example exception try 4 ma enter new Runnable public void run system OUt pr ne ln PO Thinking catch Exception e System out println enter Runnable failed 3 3 Synchronization Es wurden zus tzlich zu dem normalen Java Thread zwei zus tzliche Threads RealtimeThread und No HeapRealtimeThread eingef hrt Da diese unterschiedliche Priorit ten haben treten zwangsl ufig Probleme bei der Synchronisation zwischen diesen Threads auf Aber zumindest f r die Synchronisation eines norma len Java Threads mit einem NoHeapRealtimeThread werden durch RTJ 3 Queue Klassen bereitgestellt WaitFreeWriteQueue WaitFreeReadQueue WaitFreeDequeue die es erm glichen ohne Verz gerung und Blockierung gemeinsam auf Objekte zuzugreifen Dies ist ab
2. Unfallh ufigkeit Vorkommende Ereignisse w hrend des Betriebs des Systems H ufig Muss wahrscheinlich st ndig experimentiert werden Wahrscheinlich Wahrscheinlich oft vorzukommen Gelegentlich Wahrscheinlich mehre Male vorzukommen Entfernt Wahrscheinlich ab und zu vorzukommen Unwahrscheinlich Unwahrscheinlich aber wird au ergew hnlich vorkommen Unglaublich Extrem unwahrscheinlich dass das Ereignis vorkommt Beispiel aus dem Neigemodul des Shuttles Risikoanalyse nach den Kriterien definiert in den zwei Tabelle Zu 1 Marginal Entfernt S Zu 2 Marginal Wahrscheinlich Zu 3 Critical Entfernt Zu 4 Katastrophal Unwahrscheinlich 6 Entwurf Es bestehen zwei grundlegende Verfahren des Entwurfs die meistens nur in Kombination angewendet sollten Das erste Verfahren ist die Benutzung von Entwurfmuster das hei t die Benutzung von Standards und etablierte Code das zweite ist die Benutzung von Informationen die aus der Hazard Analyse gewonnen werden In dieser Ausarbeitung wird der zweite Fall n her betrachtet und spater fur das Fallbeispiel des Neigemoduls des Shuttles eingesetzt wird Der Entwurf basierend aus der Hazard Analyse legt vier Designprinzipien fest Diese Designprinzipien sind in ihrer Reihenfolge einzuhalten die Anwendung einzelner ist unvollst ndig um alle Gefahren von vornherein zu beseitigen Diese Designprinzipien die den n chsten Unterkapiteln erkl rt werden sind Hazard elimination H
3. Bei sicherheitskritischen Systemen handelt es sich zumeist um real time control systems Beispiele f r solche Systeme sind e Herz Lungen Maschinen e Atomreaktoren e Airbags e Flugkontrollsysteme 1 2 3 Hoch integrierte Systeme Hoch integrierte Systeme bilden sozusagen die Obermenge der sicherheitskriti schen Systeme In dieser enthalten sind auch andere kritische Systeme wie z B Sicherheitssysteme bei Banken Einem hoch integrierten System muss also zugetraut werden dass es zuverl ssig arbeitet da es sonst zu einem inakzeptablen Verlust oder Schaden kommen kann 1 2 4 Vertrauenswiirdige Systeme Die Zuverl ssigkeit eines Computersystems ist die Eigenschaft die ein gerecht fertigtes Vertrauen des Systems schafft Genau diese Eigenschaft liegt den ver trauensw rdigen Systemen zu Grunde Zwei elementare Aspekte solcher Systeme sind erstens das Vertrauen dass das System so funktioniert wie es seine Spezifikationen beschreiben und zweitens das Vertrauen dass Gefahren vom System vermieden werden Definiert man jetzt noch Vertrauensw rdigkeit als eine Kombination aus Funktionsf higkeit Verf gbarkeit Sicherheit und Vertraulichkeit w re es ohne weiteres m glich ver trauensw rdige Systeme als abstrakten Oberbegriff aller bisher angesprochenen Systeme zu sehen Von einer solchen Abstraktion sollte allerdings Abstand ge nommen werden da diese nur zu Verst ndnisproblemen aufgrund ihrer zu breit gefacherten D
4. V O x Pet Abbildung 8 Namensgebung einer Objekt Lebenslinie 1 9 4 3 Abbildung 8 zeigt eine gelaufige Benennung fur eine Lebenslinie die ein Objekt reprasentiert Es kann auch nur dir Auspragung oder die Klasse verwendet werden Zeitverlaufslinie nderungen von Zust nden Attributen und g ltigen Bedingungen einer Lebenslinie werden mit Hilfe einer Zeitverlaufslinie in Abh ngigkeit von der Zeit oder speziellen Ereignissen dargestellt Die Zust nde einer Le benslinie werden untereinander angeordnet siehe Abbildung 9 Mit Hilfe der Zeitverlaufslinie wird die zeitliche Reihenfolge der Zust nde angegeben Eine vertikale Linie symbolisiert einen Zustandswechsel eine horizontale Linie das verweilen in einem Zustand Da in realen Systemen Zustandswechsel nicht zeitlos sind k nnen Zustandswechsel auch durch schr g verlaufende Zeitverlaufslinien dargestellt werden siehe Abbildung 10 Der Ausl ser f r einen Zustands bergang kann als Text an den entsprechenden Punkten der Zeitverlaufslinie vermerkt werden Zustand 1 Zustand 2 Zustand 3 Abbildung 9 Zeitverlaufslinie 1 sd Fahrstuhlt r offen E beim Offnen E m UL z beim Y t t 0 5 Schlie en unterbrochen nicht unterbrochen unterbrechen 2 7 gt w af E O 2 in 9 A 0 2 t now sek Abbildung 10 Zeitbedingungen einer Fahrstuhlt r 1 Mit Hilfe der Zeitskal
5. 0 3 LS Qualtatssienerune Y artis ew A os es Ge ee ee A 4 123 1 Einleitung 2g u ar te ee 2 ws OK Bg mee Ba ee Aa 4 1 3 2 Wie wird die Qualit tssicherung angewendet 4 1 4 Qualit tskontrolle os zu 4 02 aa 5 LAL Emnet 2d s e Bowe BOS Bw BB Oe ES 5 1 4 2 Wie wird die Qualit tskontrolle durchgef hrt 6 Lo Qu ualt tsstandards 20 s ee ER ale RL A AE a 6 Lo Se 000 so a AA A ee 6 152 ISOTEC 9126 66 3 tna oO paa An 64 8 BS se 7 1 5 3 Sonstige Standards 2 u daa Ste as 7 2 Zertifizierung 8 2 Einleitung loca Gog al bad aog a ed A ed Ae Od SS 8 2 2 Arten der ZerLiizierung su e ks arans ws a Bre th we Sree tw re 9 2 2 1 Organisationen oder Individuen 9 2 2 2 Werkzeuge oder Methoden 9 2 2 3 Systeme oder Produkte 2 22 22 2 nm nn 10 2 3 Ziele der Zertifizierung 2 za a ns ea OE we ES 10 Dal SS aces ne SG a re ee es es DE 10 QAM gt SNAG TAI e a ae m He E ER a ee ae 10 2 4 2 Zweck des Safety Case 2 2 nen 11 2 4 3 Probleme bei der Entwicklung 11 2 5 Der Prozess der System Zertifizierung 22 2 2 222m 11 2 6 Zertifizier ngsst ndards 4 4 4 5 44 0 8 i004 bw eu 4s 12 20 IEO OOS 2 2 2 er en we Be ee Bu eek 12 202 DOSIS 4 5662 5 62 a ee ee De ee ae 13 2 6 3 Sonstige Standards kasi ar 14 3 Schlussfolgerung 14 Abbildungsverzeichnis 1 Bestandteile des Qualit tsmanagements 2 Expertengruppen bei der Entwicklung
6. Kunde Minuten Abbildung 17 Eine WaschstraBe mit einer Wertverlaufslinie 1 6 Fazit Die neueste Version der UML ist um einiges kompakter geworden als ihre Vorg nger Die grundlegenden Konzepte der Infrastruktur wurden angepasst womit ein wichtiger Schritt in Richtung Wiederverwendung und Straffung der Konzepte getan wurde Leider ist die neue UML 2 nicht vollst ndig Abw rts kompatibel Durch das ver nderte Aussehen einiger grafischer Notationsele mente kann es bei Umsteigern anf nglich zu Verwechslungen kommen Auch einige eingef hrte Bezeichnungen und Namen wurden ge ndert was eben falls f r Benutzer fr herer Versionen verwirrend sein kann Mit Hilfe der in der UML 2 neu eingef hrten Timing Diagramme ist es nun m glich auch zeitkritische Systeme wie z B ABS Systeme oder Atomkraftwer ke zu modellieren 7 Literaturverzeichnis 1 2 S 4 5 6 7 8 Jeckle Rupp Hahn Zengler Queins UML 2 glasklar Hanser Verlag 2004 www uml glasklar de Fowler Martin UML Distilled Third Edition Addison Wesley 2004 www uml org Oestereich Bernd www oose de uml UML 2 0 Infrastructure Final Adopted Specifcation www omg org technology documents modeling spec _catalog htm UML UML 2 0 Superstructure Final Adopted specification www omg org technology documents modeling spec catalog htm UML Jeckle Rupp Hahn Zengler Queins UML 2 0 Evolution oder Degeneration www jeckle de UML2Artikel OS in
7. RT Mods haben aber auch bei der Entwicklung einen entscheidenden Nachteil Hat das RT Mod einen Program mierfehler so st rzt bei Auftreten des Fehlers nicht nur der Realzeitproze ab sondern das gesamte Linuxsystem Deshalb gibt es zur Vereinfachung der Entwicklung von Realzeitprozessen ein spezielles RT Mod genannt Process RTMod Es f hrt selbst keinen RealzeitprozeB aus sondern verteilt Rechenzeit f r Realzeit an gekennzeichnete User Mode RT Prozesse Dadurch ist der Entwickler in der Lage Realzeitprozesse bei der Entwicklung im User Mode laufen zu lassen wobei er auf alle Realzeitfunktion von KURT Zugriff hat St rzt der User Mode RT Proze ab so kann das restliche Linuxsystem weiterlaufen Nachteilig bei User Mode RT Prozessen ist jedoch eine wesentlich h here Latenz als bei RTMods die durch Kontextwechsel und den Overhead von System Calls verursacht wird 3 2 4 Performance von KURT Die Performance von KURT wird ebenso wie der Performance von UTIME mit einer leeren Schleife gemessen die alle 10ms durchlaufen werden soll Dabei l t man 1 10 20 oder 30 dieser Prozesse gleichzeitig laufen 16 100 16 8 90 gt l L 14 7 Al 80 127 6 70F 10 5 sob 2 2 2 E Cc E C 4p 9 g gt gt 50F 8 D4 oO 5 5 Oo aL S gob x als ES A x 30 at 4 2 20F 2 tr 10F 1 0 0 0 0 4 6 8 10 12 14 16 6 8 10 12 14 4 6 8 10 12
8. oooooonnnnconccnnoncnnnnnccnnnnnnnnnnnnonnnnonononnccnnnnnnonos 3 Testability Testbarkeit Verifiability Verifizierbarkeit oooooonncnocccnnnonononcncnnnno 3 Recoverability Wiederherstellbarkett u a 3 1 Ar thmetische Laufzeit berwachung operational ar thmetic ue 3 Maintainability Wartbarkeit Extendability Erweiterbarkeit und W iederverwendb arkeit 22er 10 IO sSubsets sere ea een 10 A FS AMC MAS SUC AAA Pp o O 11 A VON Oi ea 11 1 Die Entstehung der Sprache 1 1 Motivation Die Geschichte von Ada begann 1 4 Das amerikanische Verteidigungsministerium U S Department of Defense DoD lies den Aufwand f r die zuk nftige Erstellung und Pflege von Programmsystemen 1m Bereich des Verteidigungswesen absch tzen Die Kosten sind auf ber 3 Milliarden US Dollar j hrlich taxiert worden eine Summe die noch f r heutige Zeiten drei ig Jahre sp ter enorm ist Hauptursachen f r die immensen Kosten waren e Im Bereich des Verteidigungsministeriums waren aufgrund vieler unterschiedlicher Hardware Plattformen Hunderte verschiedene Programmiersprachen im Einsatz Mehr als die h lfte der betreuten Software war f r eingebettete Systeme bestimmt die in speziellen Umgebungen zur Einsatz kommen wie z B Sensor und Waffentechnik e Die entstandene Spezialisierung benachteiligte das DoD bei der Auftragsvergabe da im Falle einer eingef hrten Systemumgebung die Auswahl der m glich
9. Universitat Siegen Fachgruppe fiir Praktische Informatik eingereicht bei Diplom Informatiker Dr J rg Niere vorgelegt von Christian D rner Sommersemester 2004 Siegen April 2004 Zusammenfassung Das Qualit tsmanagement und die Zertifizierung spielen eine wichtige Rolle im Zusammenhang mit sicherheitskritischen Systemen Sie sind Grundbausteine f r die Entwicklung und Implementierung eines sicherheitskritischen Systems Qua lit tsmanagement und Zertifizierung sind eng miteinander verkn pft wobei das Qualit tsmanagement sozusagen die Vorstufe der Zertifizierung darstellt Beide Vorg nge laufen parallel zur Entwicklung und Produktion ab und es existiert eine Vielzahl an Standards und Normen Im Falle des Qualit tsmanagements sorgen sie f r die korrekte Umsetzung der Qualit tssicherung und Qualit tskontrolle Bei der Zertifizierung beschreiben sie hingegen Anforderungen an das System die erf llt werden m ssen um das angestrebte Zertifikat zu erhalten Der so senannte Safety Case ist dabei ein wichtiger Bestandteil zu Demonstration der Sicherheit des entwickelten Systems Inhaltsverzeichnis 1 Qualit tsmanagement 1 KE AAA 1 L2 AMICI INO e 2 u 4 nu ded ne Ds Gp tere we DS eth we BS eee ont ee 1 1 2 1 Definition Sicherheit rn 2 1 2 2 Sicherheitskritische Systeme 0 8 4 2 1 2 3 Hoch integrierte Systeme 2 2 2 2 m nn nen 3 1 2 4 Vertrauenswiirdige Systeme
10. he angepasst Direkt nach dem Start oder bei der Landung werden beispielsweise keine Ausweichempfehlungen ausgege ben In dieser Phase ist zum einen die Wahrscheinlichkeit f r Fehlalarme sehr hoch aus serdem gibt es meist keine M glichkeit Ausweichbewegungen vorzunehmen Ausserdem wird durch die Towerkontrolle des Flughafens sichergestellt dass keine Kollisionen auftre ten k nnen Wenn Ausweichempfehlungen gegeben werden wird dem TCAS System des Eindring lings mitgeteilt ob ein Steigen oder Fallen des Flugzeuges angeordet worden ist Damit wird sichergestellt dass beide Flugzeuge auf entgegengesetzen Ausweichkurs gehen 3 2 4 Mensch Maschine Interface Der allgemeine berblick ber die Verkehrssituation wird meist auf dem sogenannten pri m ren Display gegeben Es bietet eine graphische Darstellung des eigenen Flugzeuges und aller anderen Flugobjekte in Reichweite Relative H he und Distanz werden angezeigt wenn m glich auch der Kurs des Eindringlings Eine Navigationsempfehlung wird am Dis play dargestellt und zus tzlich einmal ber eine akustische Meldung signalisiert Bei einer Ausweichempfehlung wird zus tzlich zur normalen Anzeige auf dem Display mehrmals die richtige Handlung angesagt also beispielsweise Steigen steigen bei Ann herung ei nes Flugzeugs von unten 3 2 5 Probleme Zur Einf hrung des TCAS Systems wurde es von den Piloten nur als rgernis betrachtet Die gro e Anzahl von Fehlalarmen erzeu
11. n ver beider Maschinen reichten nicht aus um die Kollision zu verhindern 3 2 Das TCAS System 3 2 1 Hintergrund Mehrere Flugzeugkollisionen in der Luft gaben in den f nfziger Jahren in den USA den An sto f r die Erforschung von Ann herungswarnsystemen Eine detailierte Aufstellung der Entwicklung dieser Systeme findet man unter allstar Unterschiedliche Konzepte und Ide en wurden diskutiert bis im Jahre 1981 die Amerikanische Flugsicherheitsbeh rde ein Pro gramm zur Entwicklung des TCAS Systems startete Ein weiteres Ungl ck im Jahr 1986 in Kalifornien f hrte dann letztendlich dazu dass 1994 ein Gesetz verabschiedet wurde dass die Nutzung dieses Systems in allen Flugzeugen ab einer bestimmten Sitzplatzanzahl in Amerika vorschreibt Mittlerweile ist die Nutzung auch in Europa und vielen anderen L ndern Pflicht 3 2 2 Einstufung Das Traffic Alert and Collision Avoidance System ist ein Ann herungswarnsystem das einen Zusammensto zweier Flugzeuge in der Luft verhindern soll Es soll dem Piloten unterst tzen kann aber nicht die Kontrolle des Flugverkehrs vom Boden ersetzen Da es nur ein Warnsystem ist muss der Pilot angemessen auf die Hinweise und Warnungen des Systems reagieren es greift nicht in die Flugzeugsteuerung ein eddh Man unterscheidet drei unterschiedliche Versionen des Systems TCAS I das einfachs te und billigeste gibt dem Pilot nur eine Anzeige des Verkehrs und eine Navigationsemp fehlung aus
12. nahmen im Design die Wahrscheinlichkeit des Vorkommens eines Hazards vermindern oder ausschlie en k nnen aber alle Gefahren lassen sich nicht ausschlie en Dieser Bereich der Informatik ist einen Zukunftweisenden Bereich auf Grund der immer steigenden Anzahl von eingebetteten Softwaresysteme in der Industrie 8 Literatur www first fhg de sergio public hazard html 2 www theoinf tu lmenau de ISCRA hazard html 3 Safety Critical Computer Systems Neil Storey Addison Wesley Longman 1996 4 http wwwecs upb de cs ag schaefer Lehre Lehrveranstaltungen Seminare AEIzZS y 5 http wwwes upb de cs ag schaefer Lehre Lehrveranstaltungen Seminare AEIzS f 6 http wwwes upb de cs ag schaefer Lehre Lehrveranstaltungen Seminare AEIzS Abgaben Folien 8_Entwurfsmuster_ASeibel p df 7 http www railcab de Untersuchung der Programmiersprache Ada zur Implementierung sicherheitskritischer Systeme Seminararbeit im Fach Informatik im Rahmen des Seminars Sicherheitskritische Systeme an der Universitat Siegen Fachgruppe fiir Praktische Informatik eingereicht bei Dr J rg Niere vorgelegt von Peter Sakwerda Sommersemester 2004 Inhalt 1 Die Entstehung Ger Sprachen un 3 AWA Nee Ke 1226 yo eae ee ce ee SD ST re PS ee ee Ee 3 1 2 DE Umsezuns seen HE 3 Li Adas Anwendunssbereiche anne a gc ave ee Pera ave aes 4 2 Anforderungsspezifikationen an eine Programmiersprache zur Implementierung von sic
13. ufig von den deutschen und amerikanischen Verteidi gungsministerien f r die Realisierung derartiger Softwareanforderungen verwendet wird Aber Java bietet viele entscheidende Vorteile gegen ber anderen den anderen Programmiersprachen e Java wird von einer sehr breiten Anwendergemeinde verwendet e Java ist auf sehr vielen verschiedenen Plattformen wie PDA Handy PC usw verf gbar und kann dort mit geringen bis gar keinen Codeanpassungen sofort ausgef hrt werden Es gibt aber auch Einschr nkungen weil gerade im Bereich der Embedded Systeme sehr be srenzte Ressourcen f r die Java Virtual Machine JVM zur Verf gung stehen Dort gibt es zum Beispiel nur sehr leistungsschwache Benutzerschnittstellen User Interfaces UIs im Gegensatz zur PC Welt Ebenso sind Speicher und Rechenleistung meistens sehr knapp be messen so dass das Java nun doch mit anderen Bibliotheken speziell f r diese Umgebungen ausgestattet werden muss Somit ist also ein Java Programm nur eingeschr nkt auf allen Plattformen nutzbar Die folgenden Punke geh ren grob zu den Entwicklungsrichtlinen zu Java und beruhen auf dem Bestreben nicht die gleichen oder hnliche Fehler zu machen wie sie bei der Erstellung anderer Programmiersprachen passiert sind e Die Probleml sung f r die der Code erstellt wird wird auf einer hohen Abstraktionsebene beschrieben weil Java eine Hochsprache ist Die Sprache Java ist also Prozessorunabh ngig leichter lesbar f r Mensch
14. 5 4 5 Sprungmarke Sprungmarken verbessern die Lesbarkeit von Timing Diagrammen mit vielen Lebenslinien Sie unterbrechen eine Nachrichtenlinie ohne dabei die Semantik der Interaktion zu beeintr chtigen Sie werden haupts ch lich bei weit voneinander entfernten Lebenslinien eingesetzt Das Ti ming Diagramm ist das einzige Interaktionsdiagramm das Sprungmar ken definiert chrich Abbildung 13 Sprungmarken an Nachrichten 1 sd Fahrstuhl aktiv betriebsbereit 5 E E a E e i iles aktivieren geschiossen Fahrstuhlt r aktivieren aktiviert Steuerung betriebsbereit Abbildung 14 Verwendung von Sprungmarken 1 5 4 6 Wertverlaufslinie Die Wertverlaufslinie bietet eine alternative zur Zeitverlaufslinie Sie kommt zum Einsatz wenn sehr viele Lebenslinien viele Zustande oder Folge von Wert nderungen dargestellt werden sollen Bei zu vielen Zu st nden wird die Lebenslinie schnell un bersichtlich Da die Zeitver laufslinie immer nur genau einen Zustand einnehmen kann k nnen die Zust nde auch horizontal angeordnet werden Die Zeit die eine Lebens linie in einem Zustand verweilt wird durch die Breite einer Wabe symbo lisiert Zustands nderungen werden durch die Kreuzungspunkte darge stellt Abbildung 15 Notation der Wertverlaufslinie 1 sd Januar bis August DIVIDIDOS Jan Feb Marz April Mai Juni Juli August Abbildung 16 Tageszahlen eines Monats 1 Waschstralie
15. Fehlern machen Systematische Fehler umfassen beispielsweise alle Software Fehler die zu den Design Fehlern geh ren Fehler in der Spezifikation geh ren auch zu dieser Kategorie Da sie nicht zuf llig auftreten lassen sich nicht ber statistische Auswertungen verhersagen 1 4 3 Unterscheidung ber die Fehlerdauer Permanente Fehler bleiben unbegrenzt oder solange bis sie behoben werden bestehen Dazu geh ren Design Fehler Fehler in der Spezifikation wie auch viele Hardware Defekte Viele Permanente Fehler scheinen periodische Fehler zu sein weil sie nur zeitweise in Erscheinung treten Periodische Fehler treten kurzzeitig aber wiederholt auf Kontaktprobleme aufgrund von kalten L tstellen oder Korrosion an Steckverbindern geh ren unter anderem zu dieser Fehlerklasse Sie sind sehr schwierig zu erkennen und zu beheben da die Fehlererkennung im Moment des Fehlereintretens passieren muss Kurzzeitige Fehler sind beispielsweise die Auswirkung von H henstrahlung auf Spei chership oder der Absturz eines Computers aufgrund eines kurzzeitigen berspannungs impulses Obwohl der Fehler nicht mehr auftritt Kann die Fehlfunktion die er verursacht hat nat rlich weiter bestehen bleiben 1 4 4 Sonstige Unterscheidungen Andere Definitionen wie beispielsweise die Unterscheidung zwischen Hardware und Soft warefehler sind so verbreitet dass es keiner weiteren Erl uterung bedarf Es macht allerdings wenig Sinn die bekannte Klasse
16. Ma e ausgelastet war Die Regionale Kontrollbeh rde ECAR hatte es au erdem vers umt die kritischen Bereiche des FE Netzes genauer untersuchen und FE hatte einige vereinbarte Standards ein wenig zu seinen Gunsten gedehnt Die gesamten Vorf lle sorgten daf r dass die Bedienern in den Leitst nden sehr wenig Spielraum hatten um auftretene Probleme zu l sen Au erdem waren sie nicht ausreichend f r Notf lle geschult Dies verst rkte die Probleme durch mangelhaftes Verst ndnis und Netzplanung nat rlich noch 2 2 2 Ungen gendes Situationsbewusstsein und technische Probleme bei FE Ab 14 14 fielen in der Kontrollzentrale von FE nacheinander die Elektronischen Warn und Logfunktionen die kritische Netzzust nde und Ausf lle wichtiger Komponenten mel den aus Wenig sp ter fiel dann der Hauptserver aufgrund eines Softwarefehler aus Der automatisch einspringende Backupserver kam mit der Anzahl der aufgelaufenen Warn meldungen nicht zurecht und ging um 14 54 offline Der Fehler im von FE verwendete Visualisierungs und Bediensystem X A 21 GE Energy XA 21 der zu dem Ausfall ge f hrt hatte wurde erst nach wochenlangen Quellcode Untersuchungen gefunden 7Im folgenden abgek rzt als FE North American Electric Reliability Council Obwohl aufgrund der vielen Klimaanlagen ein hoher Bedarf an kapazitiver Blindleistung war OBlindleistung ist wichtig um die Spannungsh he im Netz zu stabilisieren Ohne kapazitive Blindl
17. Monat Jahr die nicht im g ltigen Wertebereich liegt Zum Beispiel negative Zahlen Auffinden der Aquivalenzklasse 1 Wenn der Eingabewert als Wertebereich spezifiziert wird zum Beispiel die Variable kann einen Wert zwischen 1 und 12 annehmen so bildet man eine g ltige Aquivalenzklasse 1 lt x lt 12 und zwei ung ltigen Aquivalenzklassen x lt 1 und x gt 12 2 Wenn der Eingabewert als Anzahl der Werte spezifiziert wird zum Beispiel es k nnen bis zu vier Besitzer f r ein Haus registriert sein so bildet man eine Aquivalenzklasse mit giiltigen Werten und zwei Klassen mit ungiiltigen Werten kein Besitzer und mehr als vier Besitzer 3 Wenn die Eingabebedingung eine Situation mit muss sein verlangt zum Beispiel das erste Zeichen des Merkmals muss ein Buchstabe sein so bildet man eine giiltige Aquivalenzklasse es ist ein Buchstabe und eine ungiiltige Aquivalenzklasse es ist kein Buchstabe 4 Falls die Eingangbedingung als Menge vom g ltigen Eingabewert spezifiziert wird so bildet man eine g ltige Aquivalenzklasse die aus allen Elementen der Menge besteht und eine ung ltige Aquivalenzklasse au erhalb dieser g ltigen Menge 5 Wenn man vermutet dass die Elemente in einer Aquivalenzklasse vom Programm nicht gleichwertig behandelt werden so spalte man die Aquivalenzklasse in kleinere Aquivalenzklassen auf Vorteile der quivalenzklassenbildung 1 quivalenzklassenbildung ist die Basis
18. Ohio Slammer Neil Storey Safety Critical Computer Systems Pearson Prentice Hall 1996 Giese Universitat Paderborn Vorlesungs folien zu SkS SCCS I 66 88 2x pdf http wwwces upb de cs hg index_dt html Bruce Schneier Beyond Fear Copernicus Books 2003 http www allstar fiu edu aero TCAS htm http www eddh de topics tcas html http www aerowinx de html tcas html http www caasd org proj tcas http www stuttgarter zeitung de stz page detail php 235807 http www bfu web de flusiinfo V 163_jb2002 pdf http www bfu web de flusiinfo V 163_jb2002 pdf Seite 25 http www flugzeug absturz de newsarchiv php jahr 2004 amp monat 03 amp id 1054 http www tagesschau de aktuell meldungen 0 1185 0ID989014 00 html http www tagesschau de aktuell meldungen 0 1185 0ID891722_TYP1_NAVSPM2 989868_REF 00 htm http www daserste de wwiewissen thema_dyn id 3htua724orhvp52v cm asp http www heise de newsticker meldung 39436 http www heute t online de ZDFheute artikel 1 0 1367 WIRT 0 2060897 00 html http www heute t online de ZDFheute artikel 7 0 1367 MAG 0 2060103 00 html https reports energy gov BlackoutFinal Web pdf http www gepower com prod_serv products scada_software en xa2 1 htm http www securityfocus com news 6767 Qualitatsmanagement amp Zertifizierung bei sicherheitskritischen Systemen Seminararbeit im Fach Informatik im Rahmen des Seminars Sicherheitskritische Systeme an der
19. Safety vs Security Im Englischen unterscheidet man zwischen Safety und Security Leider gibt es in der Deut schen Sprache keine Unterscheidung dieser Begriffe Ich besch ftige mich im Rahmen dieser Ausarbeitung aber nur mit der Sicherheit die man als Safety bezeichnet Unter Security versteht man die Verhinderung von nachteiligen Konsequenzen der be absichtlichen und unerw nschten Aktionen von anderen Authorisierter Zugang beispiels weise wird also nicht unterbunden Safety ist die Eigenschaft eines Systemes dass es unter keinen umst nden Menschliches Leben oder allgemein seine Umwelt gef hrdet Im Ge gensatz zur Security umfasst dass sowohl beabsichtigte als auch unbeabsichtigte Aktionen von anderen als auch Unf lle und Fehler in Systemen 1 1 3 Was ist Sicherheit Die Sicherheitsaspekte von Computersystemen lassen sich in drei verschiedene Katego rieren einteilen Primare Sicherheit umfasst die Risiken die unmittelbar von einem System ausgehen Bei einer Waschmaschine w ren dies beispielsweise die Gef hrdung durch Stromschl ge durch auslaufendes Wasser oder ein durch einen Fehler in der Elektronik verursachter Brand Funktionelle Sicherheit befasst sich mit den Gef hrdungen die von der durch das SkS kontrollierten Anlage ausgehen k nnen Sie h ngt also von der korrekten Funktion der Hardware oder Software des Computersystems ab Indirekte Sicherheit besteht sowohl aus indirekten Auswirkung der Fehler von SkS als
20. T J Jennings F J Maclennan P F Farrow and J R Garnsworthy SPARK The SPADE Ada Kernel 3rd ed Program Validation Limited 1 0 GNAT Ada 5 Reference Manual Verifikation Validation und Testen von Sicherheitskritischen Systeme Seminararbeit im Fach Informatik im Rahmen des Seminars Sicherheitskritische Systeme an der Universit t Siegen Fachgruppe f r Praktische Informatik eingereicht bei Dr J rg Niere vorgelegt von Chandra Kurnia Jaya Sommersemester 2004 Inhaltsverzeichnis 1 Beispiele f r Fehler in Software 3 2 Verifikation Validierung und Testen ccccccssssssccccssssssscccssssseees 4 3 Bl ack BoX Test can ac BR Ba 5 3 1 quivalenzklassenbildung eenennen 6 3 2 GIen2WertanalySe EP COPIE PO ee ern 10 3 3 Test spezieller Werte Grenzwertanalyse nnnnn 13 34 U rsache W ckUnss Graph dio 14 AE WY TRICO Box Test AA E E ecieswsawseeteseren KO Al Beweis dorch Made prue 18 5 Black Box Test gegen White Box Test ccccccccscccccccscccces 21 O LEstpFINZIDien sarah 22 Le ZUSaMMENIaSssUD8 nun 24 8 LiteraturverzeichniS esescccesecococcococcececocoecococcecocoesecococcosoccesococcecosoesoe 25 1 Beispiele f r Fehler in Software Im Bereich der Medizin gibt es auf Grund von Softwarefehlern viele Todesf lle Mehrere Patienten starben nachdem sie wegen Krebs mit Therac 25 bestrahlt wurden Wegen einer zu hohen Str
21. Verwendung von handels blicher Software und Hardware f r Sicherheitskritische Anwendungen ist abzulehnen da dadurch keine ausreichende Ver l sslichkeit sichergestellt werden kann wie dieses Beispiel zeigt Leider wird durch zunehmenden Kostendruck wohl die Verwendung von ungeeigneter Hard und Software in Sicherheitskritischen Bereichen zunehmen so dass in Zukunft wohl vermehrt mit Ausf llen von kritischen Infrastrukturen zu rechnen ist 2Ungeniigend im Sinne einer schlechten Architektur 3 Der Flugzeugabsturz bei berlingen am Bodensee 3 1 Einleitung Am O1 Juli 2002 um 23 35 32 Uhr sto en in etwa 11 000 Meter H he ber dem nord westlichen Bodenseeufer eine russische Tupolew 154 der Bashkirian Airlines und eine Boeing 757 Frachtmaschine im rechten Winkel zusammen und st rzen ab Alle 71 In sassen sterben Die Tupolew hatte 69 Menschen an Bord berwiegend Schulkinder aus Ufa Hauptstadt der russischen Teilrepublik Baschkirien In der Boeing sa en Pilot und Co Pilot Auszug aus der Stuttgarter Zeitung Technische M ngel bei der Schweizer Flugsicherung und Fehler des Fluglotsen f hrten zu dem Zusammensto Die Piloten der Tupolev bekamen vom Lotsen und dem bordeige nen TCAS System wiederspr chliche Informationen sie treffen die falsche Entscheidung und befolgten die Anweisungen des Fluglotsen Die Boing flog entsprechend den Anwei sungen von TCAS Die kurz vor der Kollision bei Sichtkontakt eingeleiteten Ausweichma
22. Visualisierungsystem kriti sche Fehler aufweisen k nnen dadurch neue gef hrlichere Situationen verursacht werden Der Fehler im XA 21 System trat nur bei einer extremen H ufung von bestimmten Einga bedaten auf auf die w hrend der Produktion wohl nicht getestet wurde Das der Fehler erst nach mehrw chigen Codeaudit gefunden wurde weist zus tzlich auf die zu hohe Komple xit t und eventuell eine ungen gende Implementation hin Der scharfe Wettbewerb und der dadurch entstehende Preisdruck hat sicherlich auch einen gro en Anteil an dem Ereignis gehabt Sicherheit und Verf gbarkeit gibt es nicht umsonst selbst durch so banale Ursachen wie mangelhaftes zur ckschneiden der B ume k nnen erhebliche Probleme auftreten An Schulungen sichereren Systeme Wartung und einer ausreichenden Netzauslegung sollte man auch nicht sparen dies hat dieses Ereignis deutlich gezeigt Da das verwendete System auf ein handels bliches Unix Betriebsystem aufsetzt k n nen auch dadurch neue Gef hrungen auftreten Neue Visualisierungs und Steuersoftware f r Kraftwerke oder Industrieanwendungen verwenden mittlerweile auch Microsoft Win dows als Betriebsystem Kritische Prozessdaten werden teilweise ber ffentliche Daten netze wie das Internet bef rdert Wie in Ohio Slammer beschrieben drang der Windows Wurm Slammer Anfang 2003 in ein Kraftwerk in Ohio ein und deaktivierte f r mehrere Stunden ein Sicherheits system und die Datennetze Die
23. Zudem sind die Komponenten meist auch schon getestet e Java unterst tzt verteilte Systeme Die meisten modernen Systeme bestehen aus einem Netzwerk aktiver Komponenten die zusammen f r die L sung von Aufgaben verwendet werden Um eine sinnvolle Verteilung der Einzelaufgaben zu machen muss man dieses Netzwerk als Ganzes sehen Und damit ist es auch von gro em Vorteil dieses Netwerk bis zu einem gewissen Grad als Ganzes programmieren zu K nnen e Java gew hrleistet eine wohl definierte Ausf hrungssemantik da jeder Befehl in allen Ein zelheiten dokumentiert ist JavaDoc Diese Dokumentation enth lt alle m glichen Parame ter und deren Beschreibung m gliche Ausnahmen und deren Quellen und vieles mehr Alle diese Beschreibungen haben dasselbe Format Es gibt keine versteckten Parameter und es wird genau beschrieben was der jeweilige Befehl bewirkt 3 Merkmale von Real time Java Die Programmiersprache Java ist nicht als Echtzeit Programmiersprache konzipiert worden deshalb wurde ein Spracherweiterung RTJ f r Java entwickelt die in Verbindung mit einer neuen eigenen Virtual Machi ne RTJVM die Echtzeit Anforderungen erf llt Man hat versucht sich bei der Entwicklung der Erweiterung an folgende Leitlinien zu halten e Die Erweiterung muss Abw rtskompatibilit t gew hrleisten denn sonst w rde man den al ten Code gar nicht wieder verwenden k nnen und man h tte auch eine neue Programmier sprache entwickeln k nnen e
24. auch aus M ngeln im Mensch Maschine Interface Auch nicht funktionale Eigenschaften wie beispielsweise die Bearbeitungsdauer einer Anforderung geh ren zu dieser Kategorie 1 1 4 Formen von SkS Man unterteilt SkS anhand ihrer Funktion in Kontrollsysteme und Schutzsysteme Kontrollsysteme werden benutzt um die einwandfreie Funktion einer Anlage sicherzu stellen Dies kann beispielsweise ein System sein was die Temperatur eines Kessel inner halb eines bestimmten Bereiches regelt um einen chemischen Prozess aufrecht zu erhalten Ein Versagen dieses Systems w rde eine unmittelbare Gef hrdung darstellen wenn die An lage gef hrliche Stoffe verarbeitet Im folgenden wird die Abk rzung SkS f r den Begriff Sicherheitskritische Systeme verwendet Der Begriff Anlage kann sowohl eine Fabrik als auch einzelne begrenzte Ausr stungen oder Einrichtungen bezeichnen 3Mit dem Begriff Computersystem sind alle Arten von programmierbaren Steuerungen wie Speicherpro grammierbare Steuerungen und Microcontroller als auch zur normale PCs mit Steuerungsaufgaben gemeint Das Versagen eines Kontrollsystemes ist also dann sicherheitskritisch wenn keine alterna tiven Schutzsysteme eine Abweichung vom sicheren Zustand verhindern k nnen und eine au er Kontrolle geratene Anlage eine Gef hrdung darstellt Schutzsysteme benutzen Sensoren um Fehlerbedingungen festzustellen und leiten ge gebenfalls Ma nahmen ein um ihre Auswirkungen
25. des British Standard Institute hervor Heutzutage wird er unter dem Namen ISO 9000 von der Inter national Organization for Standard zation definiert In Europa ist der Standard auch unter der Bezeichnung EN 2900x bekannt Unternehmen die ihr Qualit tsmanagement System nach diesem Standard aus richten k nnen sich dies entsprechend ISO 9000 zertifizieren lassen Der Stan dard ist einer der weltweit wichtigsten industriellen Qualit tsstandards Mehr als 500 000 Organisationen in 160 L ndern wenden den ISO 9000 Standard an 5 Die neueste Revision ISO 9000 2000 datiert auf das Jahr 2000 ISO 9000 spezifiziert die Anforderungen eines Qualit tsmanagement Systems und besch ftigt sich mit der Qualit tssicherung und Qualit tskontrolle Er stellt Siehe 4 f r weitere Informationen nicht die Qualit t eines Produktes sicher sondern bescheinigt vor allem dass der Ablauf des Produktionsprozesses richtig durchgef hrt und berpr ft wurde 1 5 2 ISO IEC 9126 Der ISO IEC 9126 Standard bezieht sich prim r auf die Qualit tskontrolle bei Computer Software Der Standard definiert sechs Charakteristika die die Qua lit t von Software determinieren 2 S 354 E Funktionalit t Attribute die daf r sorgen dass die spezifizierten Eigen schaften eingehalten werden Funktionen sind nur solche die implizierte oder festgelegte Bed rfnisse befriedigen Zuverl ssigkeit Attribute die zeigen dass die Leistungsf hi
26. des Menschlichen Fehlers auch Menschliches Versagen genannt als eigene Klasse zu definieren Jedes Versagen eines SkS aufgrund eines Problems w hrend der Entwicklungs Implementierungs oder Wartungs phase stellt letztendlich Menschliches Versagen dar Dazu geh ren insbesondere auch Fehl bedienungen aufgrund einer mangelhaften Mensch Maschinen Schnittstelle Auch diese Fehler lassen sich auf eine Schw che im Entwicklungsprozess zur ckf hren 1 5 Fehlervermeidung Techniken zur Fehlervermeidung zielen darauf ab die Fehler die w hrend der Designphase von SkS entstehen zu entfernen Solche Probleme entstehen haupts chlich durch Schw chen in der Spezifikation Da nat rliche Sprachen immer ungenau sind ist es unm glich mit ihnen etwas unmissverst ndlich zu beschreiben Auch eine korrekte Beschreibung die f r eine sicherere Funktion notwendig w re wird durch sie nicht unterst tzt Digitale Systeme verhalten sich im Gegensatz zu analogen nicht stetig Wegen dieser Eigenschaft und weil digitale Systeme sich aufgrund der Vielzahl an Kombinationsm g lichkeiten ihrer Eingangsbelegungen nicht vollst ndig testen lassen brauchen wir ein an deres Verfahren um ihr Verhalten zu untersuchen Formale Methoden die auf der diskreten Mathematik und mathematischen Logik basieren bieten f r diese Probleme eine L sung Sie erlauben es die Charakteristiken eines Sys tems in einer formalen pr zisen Sprache zu beschreiben Diese kann u
27. eine weitere Schwierigkeit Es kann passieren dass der Programmierer die Spezifikation falsch verstanden hat In diesem Fall kann der Programmierer nicht bemerken dass es einen Widerspruch zwischen der Spezifikation und seinem Quellcode gibt Testf lle m ssen f r ung ltige und unerwartete Eingabedaten ebenso wie f r g ltige und erwartete Eingabedaten definiert werden 1 Diese Aussage besagt dass der Tester nicht die ung ltigen und unerwarteten Daten vernachl ssigen soll Die ung ltigen und erwarteten Daten sind sehr n tzlich um das Verhalten einer Software bei der extremen Bedingung zu analysieren Der schwerwiegende Fehler zum Beispiel Programmabsturz oder Endlosschleife kann dadurch vermieden werden Die Ergebnisse von Tests m ssen gr ndlich untersucht und analysiert werden 1 Das ist das wichtigste Prinzip Man sollte den Fehler m glichst in der fr heren Phase der Softwareentwicklung entdecken Wenn man den Fehler in einer sp teren Phase entdeckt ist es sehr schwierig diesen Fehler zu lokalisieren und zu reparieren Viele Programmierer sind mit ihrem Programm so vertraut dass sie Details in den Ergebnissen bersehen Au erdem ist es sehr leicht einen Fehler zu bersehen weil die Ausdr cke von Testergebnisse sehr lang sind Ein Fehler kommt manchmal nur in einem falschen Buchstaben vor Die Wahrscheinlichkeit in einem bestimmten Segment des Programmcodes in der n heren Umgebung eines bereits bekannten Fehler
28. existieren CASE Werkzeuge wie Rational Software von Rational Rose die Reverse Engineering PSM nach PIM erm glichen wenn auch ziemlich viele Randbedingungen innerhalb der automatisch generierten Quellcode beachtet werden m ssen Das neue transformierte Modell kann auch auf andere Plattformen portiert werden Glossar Model Driven Architecture MDA Plattform Independent Model PIM Plattform Specific Model PSM Unified Modeling Language UML Model Mapping Meta Object Facilities MOF Metamodel InfraStuktur UML Profile Interface Definition Language IDL Referenzen Die MDA modell getriebene Architektur ist ein Konzept von OMG die die funktionale Spezifikationen eines Systems von der Implementierungsspezifikationen trennt Ein Model von Subsystemen das keinerlei Informationen ber spezifische Plattformen oder Technologien enthalt Ein technologieunabhangiges Modell eines Softwaresystems Ein PSM ist ein implementierungsnahes Modell eines Softwaresystems das aus dem PIM generiert wird Im MDA bildet PSM ist die Vorstufe zur Codegenerierung Eine Sammlung von mehreren Modellierungssprachen die berwiegend f r die Modellierung von objektorientierter Softwaresystemen eingesetzt wird Ein Model ist eine abstrakte Reprasentation von Teil der Funktionalitat Struktur und oder das Verhalten eines Systems Eine Reihe von Regeln und Techniken die benutzt werden um ein Model zu ndern
29. gar nicht genau bestimmbar Deshalb ist es um so wichtiger diese Latenzen kurz zu halten um die Zeit zwischen geplanter und tats chlicher Ausf hrung zu minimieren Echtzeitprozesse neben normalen Prozessen Die Unterst tzung von Echtzeitprozessen neben normalen Prozes sen erm glicht da auf dem Echtzeitsystem sowohl zeitkritische Aufgaben als auch zeitlich unkritische Aufgaben erf llt werden k nnen Zeitkritische Aufgaben k nnen von den unkritischen Teilaufgaben befreit werden Sie sind dadurch schneller ausf hrbar und das Gesamtsystem wird akkurater Kommunikation von Echtzeit und Nichtechtzeitprozessen Direkt aus der Anforderung Echtzeitprozesse und normale Prozesse zu unterst tzen folgt die Anforderung da diese auch kommunizieren k nnen damit die Teilaufgaben untereinander koordiniert werden k nnen Die Kommunikation beider Prozesstypen darf die Echt zeitprozesse nat rlich nicht behindern Synchrone und Asynchrone Echtzeitprozesse Echtzeitprozesse m ssen synchron und asynchron gestartet werden k nnen Synchrone Prozesse werden in regelm igen Zeitabst nden gestartet w hrend asynchrone Prozesse v llig unregelm ig beispielsweise durch Interrupts gestartet werden Wenn man die Anforderungen optimal l sen m chte entstehen bis heute nicht l sbare Probleme Die Berechnung f r die Verteilung der Rechenzeit auf die Echtzeitprozesse so da diese ihre Deadline einhalten is NP vollst ndig Ein Scheduler mit NP vollst
30. in einen Versicherungsvertrag Eingabe vertragsbeginn geburtsdatum Hilsvariable diff_Monat Monat vertragsbeginn Monat geburtsdatum diff_Jahr Jahr vertragsbeginn Jahr geburtsdatum technisches_Eintrittsalter Bedingung Fehler vertragsbeginn lt geburtsdatum diff_Jahr vertragsbeginn gt geburtsdatum und 5 lt diff Monat lt 6 diff_Jahr 1 vertragsbeginn gt geburtsdatum und diff Monat gt 6 diff_Jahr 1 vertragsbeginn gt geburtsdatum und diff Monat lt 5 Ti j Testfall in Aquivalenzklasse i an der Grenze zu Klasse j Testfall Ausgew hltes Testdatum Eingabe Ausgabe Geburts Vertrags Ausgabe datum beginn soll T1 2 Vertragsbeginn Fehler 02 02 2001 01 02 2001 Fehler Tag vor Geburtsdatum T2 1 Vertragsbeginn O 01 06 1975 0 Geburtsdatum T2 3 diff_Monat 6 diff_Jahr 01 12 2001 26 T2 4 diff Monat 5 diff Jahr 01 01 2001 26 T3 2 diff_Monat 7 diff_Jahr 1 01 12 2001 27 T4 2 diff Monat 6 diff Jahr 1 01 01 2001 25 Wir k nnen leicht verstehen dass wir hier diff Monat 5 6 6 7 f r den Grenzwert benutzen AuBerdem wird hier untersucht wie sich das Programm bei falschen Werten hier Vertragsbeginn Tag vor Geburtsdatum verh lt Einige Richtlinien bei Bildung des Grenzwertes 1 Wenn ein Wertebereich f r die Eingabebedingung in der Spezifikation steht so muss man Testf lle f r den unteren und oberen Grenzwert entwerfen die direkt neben den Grenzw
31. interrupt unterbrechen und dann bei der R ckkehr zu dem catch Block den Thread sauber beenden 3 7 Physical memory access Der physikalische Speicherzugriff kann wie oben beschrieben zum Zweck des Zugriffs auf DMA Bereiche verwendet werden Es besteht aber auch die M glichkeit einfache Datentypen im RawMemory abzulegen Dazu muss aber beachtet werden dass diese zum auslesen wieder in den jeweiligen Typ gecastet werden m ssen Durch diese Art des Speicherzugriffs st man auch in der Lage Treiber n Java zu schreiben oder auch spezielle Arten von Speicher anzusprechen z B Batterie Gepufferten Speicher ROM oder Flash Speicher Die Byte Order wird automatisch aus den Umgebungsvariablen verwendet 3 8 Exceptions Da die Echtzeit Programmierung wieder neuartige Ausnahmen hervorbringen kann wurden fiir die Real Time Erweiterungen einige neue Exceptions geschaffen wie OffsetOutOfBoundsException aber da diese nur f r die Echtzeitsteuerung vorgesehen sind sollten sie nicht so einfach wie durch catch Exception e abgefangen werden man sollte also darauf achten dass im alten Java Code nur die Exceptions abgefangen werden die nur dort auftreten k nnen und nicht aus irgendwelchen Gr nden diese neuen Exceptions die dann unbeabsichtigter Weise falsch behandelt werden k nnten Eine Ausnahme bildet die Asynchronously InterruptedException die geh rt zu den java lang interruptedExceptions und muss dann auch dementspre chend abgefange
32. kommt es oft vor dass Berechnungen nach einer Bestimmten Zeit unter oder abgebrochen werden m ssen obwohl sie nicht beendet sind Oder dass die Berechnung mit steigender An zahl der Iterationen immer genauer wird und man nach einer erst zur Laufzeit bestimmten Zeit ein m glichst genaues Ergebnis haben will Dazu wird die Kontrolle dem berechnenden Thread einfach asynchron entzo gen Aber dabei m ssen folgende Prinzipien bei RTJ beachtet werden e Es muss explizit angegeben werden dass eine Methode asynchron unterbrochen werden kann mittels throws AsynchronouslyInterruptedException W rde dies n mlich nicht der Fall sein k me es bei altem nicht realtime fahigen Code zu unbestimmten Zust nden und damit w re das System gest rt e Auch in Threads in denen der asynchrone Kontrolltransfer gestattet ist kann es Abschnitte geben die synchron sind und dann nat rlich nicht unterbrochen werden k nnen Es muss je de Methode die unterbrochen werden darf explizit die throws Anweisung enthalten Wenn dies nicht der Fall ist kann diese Methode nicht unterbrochen werden auch wenn ihr Aufruf innerhalb einer Methode steht die unterbrochen werden darf e Die Kontrolle kehrt nicht zu der Stelle zur ck an der der asynchrone Kontrolltransfer statt fand Dies ist auch nicht notwendig denn dies kann aber durch den AsyncEventHandler er reicht werden e Der asynchrone Kontrolltransfer wird durch Ausl sen einer AsynchronouslyInterruptedEx ce
33. ndigen Algorithmus w rde zuviel Rechenzeit verbrauchen so da man sich mit anderen Algorithmen behelfen mu 2 4 Scheduling unter Linux Linux nutzt einen modularen Ansatz um verschiedenen Prozessen verschiedene Scheduling Verfahren zur Verf gung zu stellen In einem Standard Linux Kernel gibt es drei Scheduling Algorithmen SCHED_OTHER Der normal Time Sharing Scheduler Dieser wird standardm ig f r Prozesse verwendet Den Prozessen k nnen Priorit ten von 20 bis 20 zugewiesen werden wobei 0 die Ausgangspriorit t ist 20 ist die niedrigste Priorit t und 20 die h chste Zus tzlich werden diese statischen Priorit ten durch dynamische Werte angepa t Die dynamische Priorit t des aktuell laufenden Prozess wird erh ht damit dieser schwerer verdr ngt werden kann denn eine Verdr ngung h tte einen Kontextwechsel zur Folge und der Durchsatz des Systems w rde gemindert Desweiteren wird dementsprechend wie ein Prozess seine Zeitscheibe ausnutzt die dynamische Priorit t angepa t damit h ufig blockierende Prozesse nicht benachteiligt werden SCHED_FIFO und SCHED_RR Diese beiden Schedulerstrategien sind f r weiche Echtzeitprozesse vorgesehen Es gibt jedoch keine Unterst tzung f r Deadlines oder hnliches Das gesamte Timing ist vom Prozess selbst zu managen Innerhalb dieser beiden Schedulerstrategien gibt es auch Priorit ten Der Prozess mit der h chsten Priorit t wird dem Prozessor zugewiesen Bei SCHED_FIFO wird von zwei Pr
34. oder in ein anderes Model zu transformieren MOF ist eine Beschreibungssprache fur alle Modellierungssprache der OMG Mit MOF standardisierte Metamodelle und die Konzepte werden benutzt um andere Metamodelle zu definieren Ein Model das eine Modellierungssprache definiert mit dem einen Model im UML definiert wird Die UML Modelle basieren auf Meta Modelle Model von Modellen Definiert f r UML UML Profile Stereotypen UML Profile sind der Standardmechanismus zur Erweiterung des Sprachumfangs der UML Sie enthalten Sprachkonzepte die uber Basis UML Konstrukte wie Klassen und Assoziationen Stereotypen und Modellierungsregeln festgelegt werden Wird verwendet die Schnittstellen vor allem bei CORBA JAVA o zu definieren 1 http www codegeneration net 2 http www klasse nl english mda mda introduction html 3 http www omg org technology documents formal mof htm 4 http www omg org mda 5 http gentleware com products documentation poseidon_users_guide generate html codeGen Real Time Linux Ein Uberblick Seminararbeit im Fach Informatik im Rahmen des Seminars Sicherheitskritische Systeme an der Universit t Siegen Facheruppe f r Praktische Informatik eingereicht bel Dr J rg Niere vorgelegt von Marcus Klein Sommersemester 2004 Inhaltsverzeichnis 1 Einleitung 2 Warum ist nicht jedes Betriebssystem echtzeitf hig 2 1 Aufgaben eines Betriebssystems 2 Opti
35. property holds e R Release is the logical dual of the U operator It requires that the second property holds along the path where the second property holds However the first property is not required to hold eventually But these 5 operators can be used to describe properties of only one path through the tree so there are two quantifiers for the Temporal Logic to describe the branching structure in the computation tree With these two path quantifiers it is possible that describe properties of all of the paths or some of the paths through the tree e A always for all computation paths eE exists for some computation paths Three are three main ways to represent Temporal Logic e CTL Computation Tree Logic a powerful and complex logic Often we need only the subset fragment of CTL such as LTL or CTL in order determined properties specify e CTL Computation Tree Logic Branching time describes all possible time lines CTL has the same operators like CTL however it has syntactic restrictions t means that each temporal logical operator must directly follow one of these two path quantifiers A or E So for the CTL we have the following 10 basis operators AX and EX AF and EF AG and EG AU and EU AR and ER e LTL Linear Temporal Logic Linear time describes single possible time line All LTL formulas are properties of paths as opposed to states An LTL formula is interpreted with re
36. start button the microwave oven begins to cook lt gt AG start gt AF cooking Now we describe the CTL formulas in another way that only path quantifiers and the classical logic operators in the formulas This step serves for the better and more efficient execution of the algorithm Then for the first CTL Formal we get AG start gt AF cooking AG start v AF cooking Through 2 times negating we get 7AG start v AF cooking Because of AGO EF 6 we get EF start A EG cooking Now we have the correct form We divide the CTL formula into several partial formulas and the conditions in those partial formulas are true We begin from simple partial formulas to the more complicated formulas until all of the formulas are true e S start S3 S4 e S cooking S1 S2 S4 e S EG cooking S1 S2 S4 all conditions lie on a path e S start A EG cooking S4 e S EF start A EG cooking S1 2 S3 S4 can be followed with S4 e S EF start A EG a cooking The starting condition S1 does not lie in this formula so the formula is not valid And in the fact the microwave oven works like that because it s not allowed that the microwave oven starts to work before someone closes the door for safety reasons Therefore the model does not fulfill this specification The model should however absolutely fulfill the second CTL formula otherwise we could not use the microwave oven To
37. umgewandelt werden Um die automatische Codegenerierung zu unterst tzen k nnen auch Markierungen ins PIM eingef gt werden die in einem UML Profil definiert sind Anhand dieser Markierungen kann der Codegenerator die Umwandlung pr ziser durchf hren Durch die N he der PSM Modelle zur Implementierungsplattform kann mit Hilfe der Templates relativ leicht und automatisch in Quellcode der Implementierungssprache bersetzt werden public interface extends EJBObject N SO ORE ___ public String get_author Book public void set_author public String get_publisher pee public void set_publisher eeset_author iget_publisher y Eset publisher Abbildung 6 Codegenerierung aus dem PSM 3 6 3 PSM nach PSM Die PSM Modelle k nnen auch bei Bedarf weiter verfeinert werden um die fehlende Implementierungsdetails zu erg nzen oder auch in ein anderes Zielplattform zu Transformieren Der Umfang der erforderlichen nderungen an Modellen ist von der Performance des benutzten Generators abh ngig 3 6 4 PSM nach PIM Diese Transformation wird meistens bei bestehenden Systemen eingesetzt um aus dem PSM Modell ein PIM Modell zu erzeugen Die Transformation von PSM ins PIM erm glicht die Abstraktion von Modellen der existierenden plattformspezifischen Implementierungen zu plattformunabh ngigen Modellen Der Transformationsprozess st allerdings recht schwierig da die Informationen ber Metamodelle fehlen es
38. und Fehler Danach werden einige praktische analyt sche Techniken vorgestellt Jeder Teil wird von einem Beispiel gefolgt 4 1 Gefahr Hazard Gefahr ist eine S tuation in welcher eine echte Bedrohung oder eine potentielle Bedrohung f r Menschen und Umgebung besteht Aus dieser Bedrohung kann ein Unfall entstehen Es wird also eine Betrachtung der inneren und der u eren Bedrohung des Systems durchgef hrt Die Untersuchung kann bei gr eren Systemen sehr schwer sein weil die Kombinationen von Ereignissen auch untersucht werden m ssen Es st n der Wirklichkeit leider n cht immer m glich alles im Voraus zu sehen Deswegen muss man bei jedem System mit einer verborgenen Rest Gefahr rechnen 4 2 Fehler Ein Fehler ist die Ursache f r unerw nschte Resultate und kann bei den Menschen Bediener oder bei den Maschinen liegen Aus der Umgebung k nnen auch unerwartete Zust nde kommen die ebenso unerw nschte Resultate erzwingen 1 Klassifizierung der Fehler Quelle Entwicklungsfehler Laufzeitfehler Art Permanente Sporadische Bedingte Fehlertolerante Bereich Wert Zeit unaufgeforderte Aktionen Beispiel Hazard Analyse des Neigemoduls des Shuttles In dem folgenden Beispiel wird auf m gliche Hazards und ihre Folge gesucht 1 Defekt des Chassis e Aufh ngung verbiegt sich e Unvorhergesehene Kr fte auf Fahrzeugteile Kette von Besch digungen eS 2 Komfort Verlust e Unwohlsein bei den Passag
39. ungl cklicher Umst nde zu dem Ungl ck f hrte 3 3 1 Technische M ngel bei der Flugsicherung Zum Zeitpunkt des Ungl cks war die Schweizer Flugsicherung Skyguide nicht voll ein satzf hig Aufgrund von Wartungsarbeiten war das Bodenkollisionswarnsystem STCA nicht funktionsf hig Dadurch bekam der Lotse keine fr hzeitige Kollisionswarnung sondern musste die Flugbahnen visuell auf Kollisionen berwachen Kurz vor der Katastrophe ver suchte eine benachbarte Bodenkontrolle den Lotsen telefonisch zu erreichen aufgrund von Wartungsarbeiten an der Telefonanlage und St rungen an der Ersatzleitung kam aber kei ne Verbindung zustande Dem Lotsen war der Ausfall der Warnsysteme nicht bewusst dadurch musste er falsche Annahmen ber den von ihm betreuten Luftraum machen Auf grund der ausgefallenen Telefonleitung konnten auch benachbarte Flugsicherungen keine Warnmeldung an ihn weitergeben 3 3 2 Stress und berlastung Zum Zeitpunkt des Ungl cks war der Fluglotse alleine er musste einen Kollegen der gerade Pause machte vertreten Zus tzlich zu der erh hten Arbeitsbelastung und dem Ausfall der technischen Uberwachungseinrichtung hatte er also die doppelte Arbeitsbelastung zu be w ltigen Dieser erh hte Druck beg nstigte sicherlich die Verwechslung von zwei Flugzeu gen auf dem Radarschirm aufgrund er die falschen Anweisung gab Verwechslung Tagesschau Durch den Ausfall des Telefons konnte er ein Flugzeug nicht an eine
40. weitere Fehler zu finden ist berproportional hoch 1 Zum Beispiel Wenn es zwei Module A und B gibt und der Tester hat 20 Fehler in A und 3 Fehler in B entdeckt dann wird er mehr zus tzliche Fehler in A als in B finden Es lohnt sich fiir den Tester im Modul eines bereits bekannten Fehlers noch nach weiterem Fehler zu suchen Zu jedem Test geh rt die Definition des erwarteten Ergebnisses vor dem Beginn des Test 1 Wenn man das erwartete Ergebnis n cht vorher definiert besteht die Gefahr e n plausibles aber fehlerhaftes Ergebnis als korrekt zu betrachten Au erdem wenn man die erwarteten Ergebnisse schriftlich vorher definiert werden unn tzlichen Diskussionen vermieden Ein Programm zu untersuchen um festzustellen ob es tut was es tun sollte ist nur die eine H lfte der Schlacht Die andere H lfte besteht darin zu untersuchen ob das Programm etwas tut was es nicht tun soll Es ist aber auch ein Fehler wenn das Programm das tut was es nicht tun soll Testen ist definiert als die Ausf hrung eines Programms mit der erkl rten Absicht Fehler zu finden 1 Es ist dem Tester gelungen wenn er den Fehler im Programm gefunden hat Au erdem wird seine Arbeit an der Anzahl des gefundenen Fehler gemessen Der Tester muss einen guten Testfall entwerfen E n guter Testfall st dadurch gekennzeichnet dass er einen bisher unbekannten Fehler entdeckt Planen Sie nie einen Test in der Annahme dass keine Fehler gefunden wer
41. wird ein Uberblick tiber die Echtzeit Programmiersprache Real time Java gegeben 1 Einf hrung Bei sicherheitskritischen Systemen wird verlangt dass diese in einer festgelegten Zeitspanne und mit einer vorher genau definierten Aktion auf ein bestimmtes Ereignis reagieren Es darf kein m gliches Ereignis un behandelt bleiben da es in diesen Systemen keine undefinierten Zust nde geben darf Die Aktionen d rfen wiederum auch nicht zu unbestimmten Zust nden f hren Es ist also extrem wichtig dass man immer ohne Einschr nkungen genau vorhersagen k nnen muss wie und wie schnell das System reagiert In der heutigen Zeit werden diese Anforderungen an Systeme nicht mehr wie fr her direkt in spezieller Hardware und schnellem Maschinencode umgesetzt sondern zunehmend in Embedded Systemen Diese bestehen meist aus allgemeiner nicht zu hoch spezialisierter Hardware einem Betriebssystem und darauf laufenden Applikationen Auf das Betriebssystem und dessen Anforderungen geht das Seminar Sicherheits kritische Systeme Real time Linux Ein berblick von Marcus Klein 1 genauer ein Hier werde ich mich mit Real time Java RTJ besch ftigen Mit dieser Echtzeit Programmiersprache k nnen Applikationen f r diese Echtzeit Systeme erstellt werden 2 Warum wird Java als Basis verwendet Es gibt bereits Programmiersprachen die f r die Erstellung von Echtzeit Anwendungen verwendet werden Da existiert zum Beispiel Ada dass bis jetzt noch h
42. zu messen wird ein Prozess verwendet der alle 10ms eine Schleife durchlaufen soll Die Genauigkeit der Einhaltung von 10ms gibt einen Aufschlu dar ber inwieweit sich die Aufl sung der Timer im Kernel verbessert hat Der Prozess l uft unter der Schedulerstrategie SCHED_FIFO Die Abbildung 3 zeigt unter a die Genauigkeit der Schleife mit den Ver nderungen von UTIME im Kernel und unter b die Genauigkeit mit einem Standardkernel Da in einem Standardkernel der Timerinterrupt selbst eine Aufl sung von 10ms hat wird der Timer f r die Messschleife nur alle zwei Timerinterrupts ausgef hrt Dadurch wird die Schleife nur alle 20ms durchlaufen Im Teilbild a ist deutlich zu erkennen da die Einhaltung von 10ms innerhalb der Schleife sehr gut eingehalten werden Die Verbesserungen der zweiten Implementierung lassen die Kurve noch etwas steiler werden Alle Messungen wurden auf Systemen mit einem 133MHz oder einem 200MHz Pentium Prozessor durchgef hrt 0 05 T T T T T T Adjusted UTIME Standard Linux and UTIME with NTP 0 05 0 1 0 15 Deviation seconds 0 2 f Standard Linux 4 0 25F 4 0 3 0 2 4 6 8 10 12 14 Hours Abbildung 2 Abweichung der Softwareuhr 50 50 45 45 40 40 35 357 BQ 30 Q 30 G o gt gt 25 25 6 Ko aL 20 amp 20 15 15 10F 10 5 5 92 94 96 98 10 102 104 106 108 11 9 192 19 4 19 6 19 8 20 20 2 20 4 206 208 21 Ti
43. zu mindern Sie werden auch Not Abschaltsysteme genannt Eine Notabschaltung in einem Kernkraftwerk w re ein solches System Es w rde bei er h hter Temperatur des Reaktorkernes die Kernspaltung durch Einf hren von Neutronenab sorbern zum Stillstand bringen 1 1 5 Unterscheidung Hochintegrierte Systeme SkS Als Hochintegrierte Systeme bezeichnet man die Systeme die verl sslich arbeiten m ssen wobei andernfalls gro e Verluste oder hoher Schaden auftreten k nnen Dies schlie t die SkS mit ein umfasst aber beispielsweise auch Kommunikationssatelliten oder Telefon und Internetvermittlungsknoten Bei dem Versagen eines Hochintegrierten System muss also nicht zwangsl ufig Leben oder die Umwelt gef hrdet sein 1 2 Risiken Wir sind es in unserem t glichen Leben gew hnt die Risiken in unserer Umwelt zu ber ck sichtigen und ihnen durch geeignete Massnahmen auszuweichen bzw sie zu verringern Diese berlegungen beeinflussen viele grundlegenden Dinge beispielsweise wo wir woh nen was f r ein Auto wir fahren und was wir essen Mit Risiken im Bereich der SkS l sst sich leider nicht so intutiv umgehen Hier brauchen wir einige Definitionen um Grundlagen f r eine Bewertung zu schaffen Eine Gef hrdung stellt eine M glichkeit f r eine potentielle Gefahr dar Wenn sie in einem Ereignis jemand beeintr chtigt bezeichnet man sie als Unfall Ein Unfall ist also ein unbeabsichtigtes Ereignis oder eine Kette davon dass Tod Verle
44. 1 Timing Diagramme finden dann Anwendung wenn genaue zeitliche Uber gange wichtig sind wenn lokale oder globale Daten f r den Sachverhalt we niger interessant sind und wenn nicht mehrere Varianten auf einmal gezeigt werden sollen 5 2 Anwendungsbeispiel td Alkoholkontrolle fluchen pusten warten Piston Ende Strafh he Alkomat erklaren Polizist Alkoholwert auswerten Alkomat betriebsbereit d 0 10 20 Sek Abbildung 5 Der zeitliche Ablauf einer n chtlichen Alkoholkontrolle 1 Abbildung 5 zeigt ein m gliches Szenario bei einer Alkoholkontrolle Zu nachst wird dem Fahrer die Bedienung des Alkomaten erklart Durch das pusten des Fahrers wechselt der Alkomat seinen Zustand und beginnt mit der Auswertung Nach einer bestimmten Zeit fordert der Polizist den Fahrer auf das pusten zu beenden Nach einer Wartezeit liefert der Alkomat dem Polizisten den Alkoholwert Danach wird dem Fahrer die Hohe der Strafe mitgeteilt 5 3 Anwendung im Projekt Timing Diagramme kommen vor allem dann zum Einsatz wenn das Zeitliche Verhalten eines Systems eine entscheidende Rolle spielt Es kann z B die Funktionalitat einer elektronischen Schaltung oder eine vollautomatische Waschstra e modelliert werden Insbesondere bei sicherheitskritischen Sys temen bei denen es auf den exakten Eintrittszeitpunkt von Ereignissen an kommt muss das Zeitverhalten definiert werden Timing Diagramme be schr nken
45. 14 6 8 10 12 14 16 Time difference between consecutive loops milliseconds Time difference between consecutive loops milliseconds Time difference between consecutive loops milliseconds Time difference between consecutive loops milliseconds a 1 Process b 10 Process c 20 Process d 30 Process Abbild 8 Effektivitat des Scheduler SCHED_FIFO 100 100 100 100 90F 90 90 90F 80 80 80 80 70F 70F 70r 70F Q oor Q 60 Q 6o 2 Gor ec i oO gt gt gt gt O 50 50F 50F 50F hei en o o Oo e a 40H aS 40H S 40H a 40H 30F 30 30r 30F 20 20 207 20F 10F 10F 10F 10F 0 0 0 0 4 4 6 8 10 12 14 4 6 8 10 12 14 Time difference between consecutive loops milliseconds Time difference between consecutive loops milliseconds 6 8 10 12 14 Time difference between consecutive loops milliseconds a 1 Process 6 8 10 12 14 Time difference between consecutive loops milliseconds b 10 Process c 20 Process Abbildung 9 Effektivitat des Scheduler SCHED_KURT d 30 Process Abbild 8 zeigt wie genau die 10ms vom FIFO Scheduler des Linuxkerns eingehalten werden Es ist deutlich zu erkennen daB mit zunehmender ProzeBanzahl die zeitliche Genauigkeit immer schlechter wird Abbildung 9 zeigt die Ergebnisse des gleichen Tests jedoch wird diesmal der Scheduler von KURT f r die Realzeitprozesse eingesetzt Der Scheduler ist in der Lage sogar 30 Prozesse alle 10ms laufen zu lassen Bei der Registrierung der Pr
46. 9 999 also 5 2 Minuten Ausfall pro Jahr Eine h here Verf gbarkeit ist nur mit unverh ltnism ssig hohen Aufwand zu erreichen und wird nur in wirklich sehr kritischen Systemen verwirklicht St rungssichere Systeme bieten die erstrebenswerte M glichkeit im Falle eines Feh lers in einen sicheren Zustand berzugehen Bei einer Ampelsteuerung w re dies beispiels weise der Zustand Alle Ampeln auf Halt Leider l sst sich dies bei manchen SkS nicht erreichen f r ein Flugzeug ist beispielsweise der einzig sichere Zustand am Boden Als Systemintegrit t bezeichnet man die F higkeit eines Systems Fehler in seinen eigenen Operationen zu erkennen und mitzuteilen Dass ist wichtig um gegebenenfalls in einen si cheren Zustand berzugehen damit fehlerhafte Handlungen oder pr sentierte Informatio nen des SkS nicht zu gef hrlichen Zust nden f hren Die Datenintegrit t ist die F higkeit Schaden an seinen Daten zu verhindern aufgetretene Fehler zu erkennen und wenn m g lich zu beheben Diese Anforderung ist auch bei verschiedenen nicht sicherheitskritischen Systemen von Bedeutung beispielsweise im Banken oder E Commerce Bereich Zur Systemwiederherstellung im Falle eines Fehlers ist es wichtig ihn zu erkennen und nach einem Neustart schnell wieder in dem vorherigen Zustand weiterzuarbeiten Wenn ein System keinen sicheren Zustand besitzt ist diese Eigenschaft von besonderer Bedeu tung Wartungsfreundlichkeit ist die F higkeit ein
47. Einmal Code schreiben und berall ausf hren WORA Prinzip e Vorhersagbare Ausf hrung des Code e Sofortige Verf gbarkeit und weitere Verbesserungen sp ter RTJ ist noch in der Entwicklungsphase aber dennoch k nnen schon die ersten Programme geschrieben werden weil schon einige Grundprinzipien die in der Spezifikation als Minimum Implementations of the RTSJ genannt werden umgesetzt worden sind e Keine syntaktischen Erweiterungen e Erlaubt wie Java selbst verschiedene Variationen von Implementations Entscheidungen 3 1 Das ur Java musste in folgenden Bereichen berarbeitet werden um den Echtzeitkriterien zu gen gen Scheduling F r die Echtzeitprogrammierung ist es extrem wichtig dass Code in einem bestimmten zeitlichen Rahmen oder zu einer vorhersagbaren Zeit ausgef hrt wird Deshalb erben diese Klassen mit diesem Code in RTJ von dem Interface Schedulable Damit wird gew hrleistet dass ein Scheduler mit diesen Threads zur Laufzeit umgehen kann Aber das reicht noch nicht aus dass diese Threads auch in der gew nschten Zeit und Reihen folge abgearbeitet werden lt lt Interface gt gt SchedulinaP Schedulable chequling arameters i vs Se S Sa A a n PriorityParameters ug Sa En 2 ii Su N gt re ImportanceParameters x i 7 a a Fi lt l e ReleaseParam
48. O Aktivit t Das Problem der gesperrten Interrupts verdeutlich Abbildung 12 Die linke Grafik stellt die Genauigkeit des KURT Schedulers dar wobei von einem normalen Proze auf die Festplatte zugegriffen wurde Rechts der gleiche Test ohne Festplatteaktivit t im Hintergrund Die Sperrung von Interrupts durch das Disk Subsystem hat zur Folge da die RT Events deutlich schlechter eingehalten werden k nnen 4 Ausblick KURT erzielt bereits sehr gute Ergebnisse um Prozesse in Realzeit auszuf hren Es k nnen RT Events mit einer Genauigkeit von lus definiert werden und sogar unter hoher Last werden Deadlines gut eingehalten aufgrund des eindeutigen Plans des Schedulers Dennoch bleibt ein wichtiges Problem Die Sperrung von Interrupts stort deutlich die Einhaltung von RTEvents In der Release Note des aktuellsten KURT f r den Kernel 2 4 18 wird der Preemption Patch und der Lock Breaking Patch vorausgesetzt Der Lock Breaking Patch unterbindet Locks die innerhalb vom Kernel lange gehalten werden wahrend der Preemption Patch Interrupts in vielen Kernelfunktionen erlaubt die vorher Interruptsperren hatten Leider gibt es keine Dokumentation dar ber inwieweit die Einbindung dieser Patches Verbesserungen im System bewirken Genausowenig ist die symmetrische Multiprozessorunterst tzung dokumentiert Der Kernel 2 6 beeinhaltet bereits diese Patches und noch einige Verbesserungen die Latenzen im System vermindern Eine Portierung von KURT
49. Priorit t einen Prozesses umso weiter erh ht je n her er an seine Deadline kommt Beide Verfahren k nnen eine Einhaltung von Deadlines nicht garantieren 3 Ein weitere Ansatz besteht darin ein konventionelles Scheduling zu nehmen und das System nur wenig auszu lasten damit jederzeit m glichst viel Rechenzeit zur Verf gung steht Aufgrund dieser vielen freien Rechenzeit k nnen Prozesse versuchen ihre Deadlines einzuhalten Es wird ebenfalls keine Garantie f r die Einhaltung der Deadlines gegeben 4 Der letzte Ansatz setzt ebenfalls wie der erste feste Eintr ge f r das Scheduling ein jedoch werden diese Eintr ge zu dem Zeitpunkt berechnet an dem der zugeh rige Prozess im System angemeldet wird Dabei kann berwacht werden ob gen gend Rechenzeit f r einen neuen Echtzeitproze zur Verf gung steht und der Proze kann abgewiesen werden falls dies nicht der Fall ist Dieser Ansatz bietet die besten M glichkeiten um die Einhaltung von Deadlines zu gew hrleisten 3 1 Welche Projekte implementieren Echtzeitf higkeit f r Linux Es gibt zur Zeit drei konkurrierende Projekte die Linux echtzeitf hig machen Dazu z hlt RTLinux von der Firma FSMLabs RTAI Real Time Application Interface von DIAPM Dipartimento di Ingegneria Aerospaziale Politecnico di Milano und KURT Kansas University Real Time entwickelt von dem Information and Telecommunication Technology Center ITTC an der University of Kansas KURT ist das am besten do
50. Prozessor gelassen Dazu m ssen alle Register f r den kommenden Prozess geladen werden Dieser Vorgang ist verst ndlich wenn von einem Programm zum anderen gewechselt werden soll er tritt aber wesentlich h ufiger auf Ein system call trap tritt im Prinzip jedesmal auf sobald ein Programm auf eine Resource also auf eine Funktion im Betriebssystem zugreift Sogar die Hardware kann auf Funktionen im Kernel zugreifen n mlich ber Interrupts Interrupts Interrupts werden von der Hardware an die CPU gesendet um dem Betriebssystem zu signalisieren da es zur Steuerung der Hardware t tig werden mu Meist wird einem Treiber signalisiert da die Ausgabe von Daten abgeschlossen ist oder Daten bereitstehen die eingelesen werden sollen Dabei wird meist ein Prozess vom Prozessor verdr ngt so da ein Kontextwechsel auftritt und schon einige Zeit vergeht bis der Kernel auf den Interrupt reagiert Der Timerinterrupt wird dazu verwendet den Prozessen Rechenzeit zuzuteilen Der Timerinterrupt tritt regelm ig auf und bei jedem Auftritt kann der Kernel berpr fen an welchen Prozess demn chst Rechenzeit vergeben wird Speicherverwaltung und Swapping Eine weitere Aufgabe des Betriebssystems ist die Verwaltung des Arbeitsspeichers Der im System vorhandene Ar beitsspeicher mu f r die vielen Prozesse aufgeteilt werden Daf r wird der Speicher hierarchisch in mehreren Gr enstufen in Seiten eingeteilt Hierarchische Gr enstufen si
51. Seminar Sicherheitskritische Systeme 7 und 8 Oktober 2004 Universitat Siegen Inhalt Beispiele f r SkS u a Stromausfall in USA Bodenseeungl ck TCAS System Begriffskl rung Vortragender Henning Westerholt Qualit tsmanagement f r SKS und Zertifizierung Vortragender Christian D rner Risiko und Gefahrenanalysen und deren Ber cksichtigung beim Entwurf von SkS Vortragender Kelen Yo Rodrigue Untersuchung der Programmiersprache ADA zur Implementierung sicherheitskritischer Systeme Vortragender Peter Sakwerda Testen Validierung Verifikation von SkS Vortragender Chandra Jaya Modelchecking Eine Einf hrung Vortragender Yuguo Sun UML 2 0 Unified Modelling Language inklusive Semantik Vortragender Christoph Hardt Codegenerierung f r UML 2 0 Modelle Vortragender Beyhan Gogeli Real time Linux Ein berblick Vortragender Marcus Klein Real Time Java Ein berblick Vortragender Frank K ther WindowsCE als Real T me Betriebssystem Vortragender Henning Peuser Begriffserkl4rungen und Beispiele f r Sicherheitskritischer Systeme Seminararbeit im Fach Informatik im Rahmen des Seminars Sicherheitskritische Systeme an der Universitat Siegen Fachgruppe fiir Praktische Informatik eingereicht bei Dr J rg Niere vorgelegt von Henning Westerholt Sommersemester 2004 Siegen April 2004 Inhaltsverzeichnis 1 Begrifflichkeiten Sicherheitskritischer Systeme LI Alleememe Def
52. Start now new RelativeTime 1500 0 Tick every 1 5 seconds handler timer starti CEVA Thread sleep 20000 77 Run for 20 sesconds catch Exception e timer removeHandler handler System exit 0 4 Fazit Diese Erweiterungen sorgen daf r dass Java als Echtzeit Programmiersprache verwendet werden kann Die ersten Projekte mit Real Time Java laufen bereits obwohl noch nicht der volle Funktionsumfang in die RTJVM integriert ist Zudem ist wie bereits oben genannt die Spezifikation nicht abgeschlossen weshalb RTJ auch nicht auf so breiter Ebene verwendet wird Ebenso ist es noch ein Problem dass f r die bisher erh ltlichen RTJVMs nicht einheitlich arbeiten weil die Spezifikation nur die Sprache selbst beschreibt und nicht die Umsetzung der Sprachelemente auf das Be triebssystems insbesondere wie schnell System reagieren soll Deshalb werden bei einigen RTJVMs noch keine harten Echtzeitanforderungen erf llbar sein wie bei einem Test einer RTVM auf Real Time Linux KURT festgestellt wurde 4 Hinzu kommt dass zwar von mehreren Firmen an Real Time Java Virtual Ma chines gearbeitet wird aber diese nicht frei erh ltlich s nd 5 Literatur 1 Klein Marcus Sicherheitskritische Systeme Real time Linux Ein berblick Siegen 2004 2 3 4 5 6 Eilers S nke Real Time Java Seminar Asynchrone Ereignisse und Asynchroner Kontrolltransfer in Real Time Java http parsys informatik uni ol
53. UML Modelle sind deklarative Modelle wie auf IDL basierende Objektmodelle Die UML Modelle k nnen sowohl graphisch als auch textuell ausgedr ckt werden Die PIM Modelle beschreiben Geschaftsverhalten und funktionalitaten eines Systems vollig unabhangig von den technischen Details bzw Eigenschaften der zu Grunde liegenden Plattform Die Modelle von verschiedenen Systemen werden in einem plattform unabhangigen Modell 3 4 PSM Plattform Specific Model Plattformspezifische Modelle werden genau so wie plattformunabhangige Modelle meistens mit UML spezifiziert Bei denn PSM Modellen haben die UML Profile eine besondere Rolle Sie erm glichen dem Softwaredesigner plattformspezifische Eigenschaften n das Modell einzubinden F r die spezifischen Technologien wurden bereits einige Profile definiert Z B UML Profil f r CORBA UML Profil f r JAVA 3 5 Templates Die Mapping beinhaltet Templates Die Templates sind parametrisierte Modelle die detailliert die Transformationsregeln spezifizieren Die Templates sind mit Entwurfsmustern vergleichbar aber sie enthalten plattform spezifische Informationen um die Transformationen der Modelle durchzuf hren Die Templates k nnen auch benutzt werden von einem Entwurfsmuster in einem anderen Entwurfsmuster zu transformieren 3 6 Abbildung der Modelle Mapping Durch die Mapping werden Modelle ineinander transformiert Die Transformation l uft strikt nach den festgelegten und exakt spezifi
54. a kann die Verweildauer in einem Zustand genau angegeben werden Das Ende einer Zeitverlaufslinie wird durch ein Stoppereignis modelliert siehe Abbildung 11 x Abbildung 11 Stoppereignis einer Zeitverlaufslinie 1 5 4 4 Nachricht Der Informationsfluss zwischen den einzelnen Kommunikationspartner wird durch Nachrichten verk rpert Eine Nachricht wird durch einen Pfeil zwischen den Zeitverlaufslinien dargestellt und ist immer vom sender zum Empfanger gerichtet Jede Nachricht muss benannt wer den Man unterscheidet zwischen synchronen und asynchronen Nach richten Bei synchroner Kommunikation wartet der Sender auf eine Antwortnachricht des Empf ngers bevor er seine Abarbeitung fortsetzt Nach dem senden einer asynchronen Nachricht setzt der Sender seiner Abarbeitung direkt fort Die verschiedenen Typen k nnen durch die Pfeilspitze unterschieden werden siehe Abbildung 12 Asynchrone Nachrichten haben eine offene synchrone eine ausgef llte Pfeilspitze Antwortnachrichten werden gestrichelt gezeichnet und haben eine aus gef llte Spitze Abbildung 12 Notation von Nachrichten 1 Da in Timing Diagrammen der zeitliche Verlauf von Zustands nderun gen im Vordergrund steht interessieren haupts chlich Nachrichten die solche nderungen ausl sen Nachrichten die verz gert beim Empf n ger ankommen werden durch schr ge Pfeile dargestellt Mit Hilfe der Zeitskala kann die Dauer der Nachrichten bermittlung exakt bestimmt werden
55. ach nochmaliger Beurteilung im M rz 1 kamen zwei Entwicklerteams weiter die abschlie ende Entscheidung fand M rz April 1 statt Die franz sische Arbeitsgruppe unter Leitung von Jean Ichbiah von CII Honeywell wurde zum Sieger erkoren die Sprache erhielt den Namen Ada benannt nach Ada Augusta Countess of Lovelace die im 1 Jahrhundert die ersten theoretisch lauff higen Programme f r die von Charles Babbage konstruierte Analytische Maschine geschrieben hatte und damit die erste Programmiererin war Die endg ltige Sprachdefinition legte das US Verteidigungsministerium 1 O fest 1 3 wurde der ANSI Standard Ada 3 1 4 der ISO Standard vergeben Kra 6 1 3 Ada s An endungsbereiche Ada wird haupts chlich im milit rischen Bereich und in der Raum und Luftfahrt eingesetzt 1 3 wurde Ada als einzige Programmiersprache f r defense mission critical applications definiert 1 6 wurde Ada zur einzigen Programmiersprache f r alle C I Systeme der NATO Um ein Beispiel aus dem zivilen Bereich zu nennen ist die Software der Boeing zu ADA geschrieben In Grunds tzlich ist Ada besonders zu empfehlen bei der Erstellung von gro en langlebigen Softwareprojekten 2 Anforderungsspezifi ationen an eine Programmiersprache zur Implementierung von sicherheits ritischer S steme 2 1 Allgemeine Anforderungen an S S Die allgemeinen Anforderungen an sicherheitskritische Systeme s nd laut Loe04 w e folgt definiert e Fun tionale S stemanf
56. ache bei der Entwicklung und der Produktion eines Systems eine bestimmte Methodik anzuwenden zur Erleichterung und zum berpr fen der Arbeitsschritte Bei der Entwicklung sicherheitskritischer Systemen wird auch die hnliche Arbeitsweise privilegiert Sicherheitskritische Systeme sind Systeme bei denen ein Fehler dazu f hren kann dass das Leben einer Person gef hrdet wird oder die Umwelt besch digt wird Es existieren viele gute bekannte Beispiele f r sicherheitskritische Systeme in verschiedenen Anwendungsbereichen medizinischen Ger ten Flugzeugsteuerungssystemen Waffen und Atomkraftwerksystemen Manche modernen Informationssysteme sind allgemein gesehen sicherheitskritisch geworden weil bei einem Fehler finanzielle Verluste und sogar lebensbedrohliche Zust nde daraus resultieren k nnen Daher wird schnell ersichtlich warum die Entwicklung solcher Systemen nicht auf die leichte Schulter genommen werden kann Daher muss die Analyse und der Design bei sicherheitskritischen Systemen sorgf ltig durchgef hrt werden denn Hazards auch Gefahren genannt k nnen viele Menschen das Leben kosten wenn es zum Unfall kommen w rde Die Risiko und Gefahrenanalyse ist der Teil der Entwicklung wo das zu entworfenem System auf m gliche Gefahren und Risiko analysiert wird das Ergebnis wird nach klassifiziert und unter Ber cksichtigung bei dem Entwurf genommen indem verschiedene Prinzipien angewendet werden um das System auf Fehler zu reduzieren bzw g
57. agramme Interaktionsubersichtsdiagramme neu Sequenzdiagramme Timingdiagramme neu Das Kompositionsstrukturdiagramm Diese Diagrammart wurde bei UML 2 0 neu eingef hrt und dient der Darstellung der internen Struktur eines Klassifiziers und seinen Beziehungen zu anderen Systemteilen Diese Diagrammart besch ftigt sich mit der Struktur der einzelnen Architekturkomponenten und mit deren Zusammenhang zwischen den Architekturkomponenten Dieses Diagramm dient haupts chlich zur abstrakten Dokumentation des Zusammenwirkens der einzelnen Architekturkomponenten In einem Top Down Prozess k nnen die Bestandteile des Systems verfeinert werden Das Interaktions bersichtsdiagramm In dem Interaktions bersichtdiagrammen wird eine Menge von Interaktionen in einer h heren Abstraktionsebene dargestellt Diese Diagrammart ist f r kleine und mittelgro e Projekte sinnvoll da mit zunehmendem Komplexitatsgrad der Softwaresysteme ziemlich aufwendig ist diese Diagramme zu erstellen In dem Interaktions bersichtsdiagrammen werden die Kontrollmechanismen des Aktivitatsdiagramms genutzt Das Timingdiagramm Mit den Timingdiagrammen werden unter Angabe der exakten zeitlichen Bedingungen die Zustands nderungen eines Klassifiziers beschrieben Diese Diagrammart ist vor allem in der Digitaltechnik sehr sinnvoll Das Aktivit tsdiagramm Die Spezifikation der Aktivitatsdiagramme wurde komplett berarbeitet Der Semantik dieser Diagramm
58. ahlendosis wurden ihre Zellen nachhaltig gesch digt Das medizinische Ger t Therac 25 ist ein linearer Teilchenbeschleuniger zur Strahlentherapie f r d e krebskranken Patienten Insgesamt sind 11 Therac 25 Ger te in Kanada und USA installiert Das Bild zeigt die Software von Therac 25 PATIENT NAME TEST TREATMENT MODE FIA BEAM TYPE A ENERGY MeV 25 ACTUAL PRESCRIBED UNIT RATE MINUTE i 200 MONITOR UNITS 0 AG 200 TIME MIN 0 27 00 GANTRY ROTATION DEG VERIFIED COLLIMA TOR ROTATION DEG VERIFIED COLLIMA TOR X UM VERIFIED COLLIMATOR Y CM 3 VERIFIED WEDGE NUMBER VERIFIED ACCESSORY NUMBER VERIFIED DATE 84 OCT 26 SYSTEM BEAM READY OP MODE TREAT AUTO MIME 12 55 8 TREAT REAT PAUSE A RAY 173777 OPRID T25V02 R03 REASON OPERATOR COMMAND Abbildung 1 1 Darstellung des Benutzer Interfaces Bei Fehlfunktionen wurden Fehlermeldungen auf dem Bildschirm dargestellt Der h ufigste Fehler war Malfunction 54 Diese Meldung ist sehr kryptisch und in der Dokumentation wurde Malfunction 54 kurz als dose input 2 beschrieben Da Fehler sehr oft auftraten wurden diese Fehler als nicht schlimm von den Operatoren betrachtet Die Operatoren setzten damit die Behandlung fort Sie wussten nicht dass die nichts sagende Fehlermeldung Malfunction 54 bedeutete dass die Strahlendosis mit der die Patienten bestrahlt wurden entweder zu hoch oder zu niedrig war Als schlie lich das Therac 25 System n her unte
59. ally a finite automaton A is a five tuple 2 0 A QO F with e gt is the finite alphabet e Q is the finite set of states e A CQx gt x Qis the transition relation e Q0 c Qis the set of initial states e FC Qis the set of final states By using the automata theoretic approach to model checking it is possible in many cases to avoid construction the entire state space of the modelled system This is because the states of the automaton are generated only when needed while checking the emptiness of its intersection with the property automaton S This tactic is called on the fly mode checking The modelled system is converted into a corresponding B chi automaton A and the negation of the specification is translated into another automaton S Then the emptiness of the intersection of A and is checked If the intersection is not empty a counterexample 1s reported Instead of constructing the automata for both A and S first we will only construct the property automaton S We then use it to guide the construction of the system automaton A while computing the intersection In this way we may frequently construct only a small portion of the state space before we find a counterexample to the property being checked One advantage of on the fly model checking is that when computing the intersection of the system automaton A with the property automaton S some states of A may never be generated at all Another advantage of the on
60. and indeed a number of companies such as AT amp T Fujitsu Intel IBM Lucent Motorola and Siemens are beginning to use model checking as part of their design process 7 References 1 Dong Wei Wang Li and Qi Zhi Chang Journal of computer research amp development June 2001 2 Dr H Giese URL http www uni paderborn de Vorlesung Safety Critical Computer Systems Techniques for Safety Software Model Checking 2003 3 Markus M ller Olm David Schmidt and Bernhard Steffen Model Checking A Tutorial Introduction 1999 4 Javier Esparza David Hansel Peter Rossmanith and Stefan Schwoon Efficient Algorithms for Model Checking Pushdown Systems URL www sinc sunysb edu Stu pyang slides pushdown ppt June 2001 5 Dragana Cvijanovic Model Checking URL www cs ucl ac uk staff W Emmerich lectures 3C05 02 03 aswel7 essay pdf 2001 6 S Merz Model Checking A tutorial Overview Institut fur Infomatik Universitat Munchen 2001 7 Edmund M Clark Jr Orna Grumberg and Doron A Peled Model Checking 1999 8 Neil Immerman Model Checking URL http www cs umass edu immerman modelCheck 2004 9 Martin Leucker and Rafa Somla Parallel Model Checking for LTL CTL and L 2 Electronic Notes in Theoretical Computer Science 89 No 1 2003 URL http www elsevier nl locate entcs volume89 html 2003 10 Joost Pieter katoen Concepts Algorithms and amp Tool for Model Checking Friedrich Alexander Universitat Erla
61. anke dar ber zu machen wie sicher das Flugzeug ist In der Realitat kann eine Fehlfunktion oder ein Bedienungsfehler mit dem keiner gerechnet hat zu t dlichen Folgen f hren Also bei der Entwicklung eines sicherheitsrelevanten Systems muss man f r alles was geschehen kann immer einer Ausweg bereithalten zum Verhindern dass solche Fehler nicht eintreten Jede Kleinigkeit die nicht vorher gesehen wurde stellt eine latente Gefahr dar Ein Prinzip bei den sicherheitsrelevanten Systemen ist Ausf lle und Umst nde mit denen zu rechnen ist d rfen nicht gef hrlich auswirken 1 Das ist der Grund warum es lebensnotwendig ist so viele Gefahren wie m glich im Voraus zu identifizieren An diesem Punkt spielt die Gefahrenanalyse eine entscheidende Rolle Um das System auf potentielle Gefahren hin zu untersuchen k nnen viele Techniken benutzt werden aber diese Techniken k nnen nicht die menschliche Kreativit t ersetzen Noch besonders wichtig ist zu wissen dass die Analyse ein Prozess ist der vor und w hrend der Systementwicklung abl uft Jede Entwicklungsphase bringt neue Erkenntnisse und dadurch k nnen neue Gefahren identifiziert werden Und es wird dabei ein Dokument mit dem Namen Gefahrenanalyse erzeugt also mittels dieses Dokuments wird bei dem Entwurf des Systems versucht alle Gefahren zu mindern oder zu eliminieren F r ein klares Verst ndnis dieses Kapitels werden einige Therme zuerst definiert Es handelt sich um Gefahr
62. anz auszuschlie en bis zufriedene Ergebnisse erreicht werden In dieser Seminararbeit wird au er der Definition von Begriffe ein konkretes Beispiel des Neigemoduls des Shuttles betrachtet Das Beispiel stammt aus der Universit t Paderborn wo an einem Projekt genannt SHUTTLE der Neuen Bahntechnik Paderborn gearbeitet wird 2 Pr sentation des Neigemoduls des Shuttles Der Shuttle der hier behandeln wird geh rt zu der Forschungsinitiative Neue Bahntechnik Paderborn Das Ziel ist die Kombination des herk mmlichen mechanischen Tragen und F hren auf dem bestehenden Schienennetz mit dem fortschrittlichen verschlei freien Linearantrieb Zus tzlich soll durch intelligente Fahrwerkstechnik ein h herer Fahrkomfort erzielt werden 7 Abbildung I Shuttle 2 1 Funktionsweise der Neigetechnik Wagenkasten Abbildung 2 Wagenkasten Das Feder und Neigemodul ist eine Kombination einer niederfrequent abgestimmten passiven Aufh ngung des Wagenkastens mittels einer Luftfeder Sekund rfederung mit einer aktiven Fu punktverstellung so dass der Wagenkasten aktiv ged mpft und geneigt werden kann 7 Abbildung 3 Neigetechnik 2 2 Problemstellung Fur die Regelung der Fu punktverstellung werden die ben tigten Informationen von Sensoren zur Verf gung gestellt und mittels einer Mehrgr enregelung verarbeitet Durch diese aktive Federungstechnik wird eine weitgehend dynamische Entkopplung des Wagenkastens vor allem im oberen Frequ
63. art an die Petri Netze angelehnt Es sind folgende erg nzende Elemente hinzugef gt strukturierte Knoten Entscheidungsknoten Schleifenknoten Mengenverarbeitungsknoten etc Das Aktivit tsdiagramm Die Aktivitatsdiagramme k nnen Vor und Nachbedingungen haben und die Aktivit ten k nnen Ein und Ausgaben haben Das Verhalten an Verzeigungs und Verbindungsknoten k nnen pr ziser beschrieben werden Es d rfen mehrere Startknoten geben die dann zu parallelen Abl ufen f hren 3 Quelltextgenerierung aus den UML Diagrammen Die Codegenerierung aus dem UML 2 0 Diagrammen basiert auf Model Driven Architecture MDA MDA ist ein ziemlich neuer Standard von OMG Mit MDA soll eine erhebliche Steigerung der Entwicklungsprozess erreicht werden Aus formal eindeutigen Modellen konnen durch Generatoren automatisch Code erzeugt werden Durch den Einsatz der Generatoren und die formal eindeutig definierten Modellierungssprachen wird auch dar ber hinaus die Softwarequalitat gesteigert Die Qualit t des automatisch erzeugten Quellcode ist gleich bleibend was zu einem h heren Grad der Wiederverwendung f hrt Plattform independet Plattform specific Templates Code Model PIM gt Model PSM ee Abbildung 1 Die Stufen der Codegenerierung Die Codegenerierung von den UML Diagrammen l uft in unterschiedlichen Stufen ab s ehe Abbildung 1 Einer von wichtigsten Kon
64. as einzige ist mit dem ein berechenbares Verhalten fiir Echtzeitprozesse erreicht werden kann RT Events Die RT Events f r jeden Echtzeitprozess RT Proze m ssen im Voraus definiert werden Es gibt zwei M glichkeiten dies zu tun 1 Handelt es sich um einen Proze der nur sporadisch zu bestimmten Zeitpunkten gestartet werden mu so werden diese Zeitpunkte beim Starten des Prozesses definiert Diese definierten Zeitpunkte m ssen nicht zwingend im Arbeitsspeicher RT_FROM_MEM abgelegt werden es besteht auch die M glichkeit diese Daten als Datei auf einem Datentr ger RT_FROM_DISK abzulegen Die Zeitpunkte werden dann vom Kern rechtzeitig geladen Sind die RT Events im Arbeitsspeicher abgelegt besteht die M glichkeit diese RT Events zu wiederholen 2 F r periodische Prozesse gibt es die M glichkeit da zum Start des Prozesses nur die Dauer der Periode und die Anzahl der Wiederholungen spezifiziert wird Der Kern plant dann f r diesen periodischen Proze die entsprechenden RT Events ein F r beide M glichkeiten pr ft der KURT Core ob gen gend Rechenzeit f r die Echtzeitprozesse zur Verf gung steht Bei periodischen Prozessen kann der Zeitpunkt f r den ersten RT Event definiert werden wird dies nicht getan bestimmt der Scheduler den Zeitpunkt f r den ersten RT Event so da der Proze bestm glich in den Plan pa t Zus tzlich zum Zeitpunkt f r den RT Event mu die Dauer f r die Abarbeitung eines RT Events definie
65. ation results In case of a negative result the user is often provided with an error trace This can be used as a counterexample for the checked property and can help the designer in tracking down where the error occurred In this case analysing the error trace may require a modification to the system and reapplication of the Model Checking algorithm An error trace can also result from incorrect modelling of the system or from an incorrect specification often called a false negative The error trace can also be useful in identifying and fixing these two problems A final possibility is that the verification task will fail to terminate normally due to the size of the model which is too large to fit into the computer memory In this case it may be necessary to redo the verification after changing some of the parameters of the model checker or by adjusting the model 2 4 A simple example with microwave oven cooking Here is a simple example with microwave oven cooking for the Process of Model Checking Step 1 Modelling with the Kripke Structure M S SO R L eS S1 82 S3 S4 e Sl 1s the initial state e R S1 S2 S2 S1 S1 S4 154 S2 S2 S3 83 S2 83 53 e L S1 f close start cooking L S2 close start cooking L S3 close start cooking L S4 close start cooking The Kripke Structure M describes the states S1 S2 S3 S4 of a microwave oven The initial state S1 mean
66. auerhafte lalsche Umsetzung AN LN 4 3 2 Top Down und Bottom Up Suche Bei der Bottom Up Suche wird von dem Defekt einer kleinen Komponente ausgegangen und untersucht welche bergeordneten Module dadurch getroffen werden Es wird f r jede Komponente im System diese Untersuchung durchgef hrt was einen sehr hohen Aufwand bedeuten kann Wenn die Ausf lle kombiniert sind kann das schlecht sein weil diese Untersuchung keine Unterst tzung f r die Untersuchung von Kombinationen von Ausf llen bietet 1 FMEA Failure modes and effects analysis Anlage Module d Funktionierendes Modu ausgefalenes Modu Abbildung 5 Fehlerfortpflanzung und Modulhierarchie 1 Die FMEA bedeutet auf Deutsch Fehlerm glichkeiten und Einfluss Analyse Sie wurde in den 60er Jahren bei der NASA und bei Appolo Programm erstmals eingesetzt Das Verfahren hat dank des Kraftwerksbaus einen breiten Eingang in die Automobilindustrie gefunden Es handelt sich um eine pr ventive Qualit tssicherung Dabei wird ein System detailliert auf m glichen Fehler und deren Ursachen und Wirkungen untersucht Die Resultate werden aufgezeigt sowie Ma nahmen zur Fehlervermeidung und Fehlerentdeckung beschrieben Da alle Komponentenfehler unter Ber cksichtigt werden eignet sich diese Ann herung besonders gut f r F lle wo ein einziger Fehler zur gef hrlichen Situation f hren kann Die Nachteile bei dieser Prozedur sind dass keine Kombinationen von Ausf l
67. auf Deutsch Fehlerbaumanalyse Jetzt handelt es sich um ein Beispiel f r die R ckw rts Suche Bei diesem Verfahren geht man von einer Gefahr aus und arbeitet R ckw rts um die Ursache herauszufinden Logische AND OR Symbole charakterisieren die Beziehungen zwischen den Ereignissen Es wird also beispielsweise durch ein AND Symbol dargestellt dass ein Ereignis dann eintritt wenn zwei oder mehrere andere Ereignisse gleichzeitig stattfinden Analog f r OR Zus tzlich wird es durch verschiedene Symbole zwischen elementaren Ereignissen Kreis und Fehlerereignissen unterscheidet die durch andere Ereignisse hervorgerufen werden Rechteck sowie Ereignissen deren Ursachen bislang noch ungekl rt sind Raute Der Prozess der Ursachenfindung und Dokumentation durch Boolescher Algebra wird solange fortgesetzt bis die grundlegenden Ereignissen erreicht werden die selbst keine Ursache haben bzw deren Ursachen man nicht weiter betrachten m chte 1 Beispiel aus dem Neigemodul des Shuttles a Kurzfristige falsche Neigung kurzfristige ihi abweichende falsche Neigung falsche Berschmine falsche Umsetzung ind vorn System erkannt und augeelichen Falsche Sergorwerte Lalsche Eichung i Hardware falsche Werarbe ttine ISoflware b Langfristige falsche Neigung Motil Enigleisung Langfristige Hohe Geschwindieken ae lalsche Neigung Ausbleiben der Neibrenmsune dauerhafte balsche Berschmng d
68. auf den Kernel 2 6 k nnte die Exaktheit des System weiter verbessern Literatur 1 2 3 4 5 Nordmann Michael 21 11 2001 Echtzeit fiir Linux Ausarbeitung zum Seminar Linux und Apache Fach hochschule Wedel http www fh wedel de si seminare ws01 Ausarbeitung 6 linuxrt LinuxRTO htm Information and Telecommunication Technology Center 6 10 2003 KURT Linux Homepage University of Kansas http www ittc ukans edu kurt Information and Telecommunication Technology Center 24 3 2000 Old KURT Linux Homepage University of Kansas http www ittc ukans edu kurt old index html Srinivasan Balaji 1998 A Firm Real Time System Implementation using Commercial Off The Shelf Hardware and Free Software University of Kansas Hill Robert 1998 Improving Linux Real Time Support Scheduling 1 O Subsystem and Network Quality of Service Integration University of Kansas Real Time Java Ein Uberblick Seminararbeit im Fach Informatik im Rahmen des Seminars Sicherheitskritische Systeme an der Universitat Siegen Fachgruppe fiir Praktische Informatik eingereicht bei Dr J rg Niere vorgelegt von Frank Christoph K ther Sommersemester 2004 Real Time Java Ein Uberblick Frank Ch Kother Wenn man sicherheitskritische Systeme betrachtet kommt man an einer Programmiersprache mit der man diese Systeme bzw das Verhalten dieser Systeme festlegen kann nicht vorbet In diesem Seminar
69. azahlen Einschr nkung der Ein Ausgabe Verbot der Polymorphie Verbot der Rekursion Verbot reentranter Programmteile Mit dem flexiblen Einsatz von Spracheinschrankungen eignet sich Ada fur den Einsatz in SkS wobei ein leichtsinniger Umgang damit auch fatale Folgen haben kann Eine Ariane 5 Rakete ist abgest rzt weil aus Performance Gr nden die Ausnahmebehandlung eingeschr nkt worden ist und so ein Softwarefehler nicht abgefangen werden konnte Dies zeigt uns eigentlich dass auch sichere Programmiersprachen unsichere Programme produzieren k nnen und dass letztendlich der Entwickler f r die Sicherheit verantwortlich ist 5 Anhang 5 1 Literaturverzeichnis Sto 6 Gol 5 Kra 6 Gol 2 Gie03 G1e04 Loe04 Carr 0 Ada 5 Neil Storey Safety Critical Computer Systems Addison Wesley 1 6 S J Goldsack Ada for specifications possibilities and limitations Cambridge University Press 1 5 K P Kratzer Ada Eine Einf hrung f r Programmierer Hanser 1 6 S J Goldsack Programming Embedded Systems with ADA Prentice Hall 1 2 Giese H Folien zur Vorlesung Software Engineering for Safety Critical Computer Systems Universitat Paderborn WS 02 03 Giese H Folien zur Vorlesung Software Engineering for Safety Critical Computer Systems Universitat Paderborn WS03 04 Loper C Anforderungsanalyse und Anforderungsdefinition fur sicherheitskritische Systeme Universitat Paderborn WS03 04 B A Carr
70. azard reduction Hazard control und Damage minimizat on 5 6 1 Hazard elimination Ziel hier ist das System so weit wie m glich sicherer zu gestalten durch das Anwenden von mehreren Techniken Der Ausgangspunkt st die Komplexit t des Systems zu vereinfachen was die berschaubarkeit und die Verifizierbarkeit erh ht es sollten auch statt monolithische Sprache objektorientierte Programmiersprache ausgew hlt Der weitere Punkt ist die Entkopplung von Systemteile das reduziert ungewollte Interaktionen und erm glicht eine leichte Gruppierung und Eingrenzen der systemkritischen Funktionen Schlie lich kommt die Eliminierung von menschlichen Fehlern und die Reduzierung gef hrlicher Bedingungen 5 Beispiel aus dem Neigemodul des Shuttles a Geschwindigkeitsreduzierung L st z B den Hazard Komfortverlust b Ausreichender Abstand zu Hindernisse neben der Bahnstrecke Tunnel Br ckenpfeiler Parallelgleis c Absicherung der Gep ckst cke im Inneren d Ausschalten der Neigetechnik Shuttle kann sich nun nicht mehr in Gegenspur neigen Hazard des Komfortverlustes bleibt 6 2 Hazard reduction Unf lle sind unwahrscheinlich je unwahrscheinlicher der daf r verantwortliche Hazard ist die Wahrscheinlichkeit f r einen Hazard kann man senken indem die Bedingungen die zu einem Hazard f hren reduziert werden 6 Dieser Teil hat viel mit der Software zu tun also sie wird so entwickelt dass
71. bei beim KURT Scheduler unter b nur Echtzeitprozesse zugelassen werden w hrend unter c im Hintergrund zus tzlich normale Prozesse von Linux ausgef hrt werden Normale Prozesse beeinflussen den KURT Scheduler bei seiner Arbeit nicht solange nicht uber langere Zeitraume die Interrupts deaktiviert werden 100 90 80 70 on O o o of events E o 30 Focused Kernel Module Focused User Process 10 Mixed Kernel Module Mixed User Process 0 10 20 30 40 50 60 70 80 90 100 Difference between scheduled and actual event time microseconds Abbildung 11 SCHED_ALL_PROCS und SCHED_KURT_PROCS im Vergleich Den Vergleich von RT Mods und User Mode RT Prozessen zeigt Abbildung 11 Zusatzlich wird SCHED_KURT_PROCS Focused und SCHED_ALL_PROCS Mixed des KURT Scheduler unterschieden Gut zu erkennen ist daB User Mode RT Prozesse durchschnittliche 14s sp ter ausgef hrt werden als RT Mods was durch den Kontextwechsel zu erkl ren ist u 1 process 10 processes 20 processes E os 30 processes of events of events Pee O gt 1 process A o i 10 processes i 10r Re A ios 20 processes 10 ae a 30 processes Old ej L L 1 L 0 5 5 6 7 8 9 10 11 12 14 5 5 6 7 8 9 10 12 14 15 Time difference between consecutive loops milliseconds Time difference between consecutive loops milliseconds Abbildung 12 Zeiten mit Hintergrund I
72. beiten kann wobei die Daten zuf llig oder zu bestimmten Zeitpunkten eintreffen Unter sofort verarbeiten versteht man dabei da zu einem bestimmten Zeitpunkt die Abarbeitung beendet sein mu so da das Ergebnis der Abarbeitung zu diesem Zeitpunkt verwendet werden kann Kann das System die Abarbeitung zu einem bestimmten Zeitpunkt nicht einhalten so unterscheidet man zwischen zwei F llen Weiche und harte Echtzeitf higkeit Weiche und harte Echtzeitf higkeit werden anhand des Schadens unterschieden der bei der berschreitung der Zeitvorgaben auftritt Handelt es sich dabei um einen kleinen Schaden oder gar nur einen st renden Effekt so spricht man von weichen Echtzeitanforderungen Diese werden z B an die Wiedergabe von digital gespeicherten Video und Audioinformationen gestellt Tritt jedoch bei Verletzung der Zeitvorgaben sofort der maximale Schaden ein so liegen harte Echtzeitanforderungen an das System vor Dazu geh rt z B das Ausl sen des Airbags im Auto Wird er nicht rechtzeitig gez ndet so prallt das Gesicht auf das Lenkrad Um Software f r Echtzeitsysteme auf unterschiedlichen Rechnern komfortable einsetzen zu k nnen ist ein Betrieb ssystem notwendig das zwischen Hardware und Software ein komfortable Schnittstelle zur Verf gung stellt Diejenigen Aspekte von Betriebssystem die bei Echtzeitsystemen eine Rolle spielen werden im folgenden beleuchtet Danach wird eine konkrete Umsetzung betrachtet die das Betriebssy
73. benachbarte Flugsi cherung bergeben auch dadurch wurde seine Belastung erh ht bergabe Tagesschau 3 3 3 Probleme durch TCAS Durch die anf nglichen Probleme wurde das Vertrauen der Piloten in die Verl sslichkeit des Systems untergraben Obwohl bei der Entwicklung von TCAS formale Methoden an gewendet wurden Storey Konnten die Probleme des Systems in der Realit t dadurch nicht erkannt werden Ein ausreichendes Testen mit reellen Daten wie sp ter durchgef hrt w re sehr sinnvoll f r eine schnelle Akzeptanz von TCAS gewesen Dann h tten die Piloten der Tupolev vielleicht eher ihrem Warnsystem vertraut als der Flugsicherung 3 3 4 Formelle Probleme Es ist in den Internationalen Bestimmungen zum Flugverkehr unzureichend spezifiziert ge wesen wie sich Piloten im Falle eines Konflikt von Bodenkontrolle und TCAS System 7Bundesstelle f r Flugunfalluntersuchung verhalten sollen Eine direkte Anweisung an deutlich sichtbarer Stelle fehlte man konnte die vorhandenen Bestimmungen unterschiedlich auslegen Da von Ausgabe der Ausweich empfehlung bis zur Kollision weniger als 40 Sekunden vergehen kann dem Piloten eine genau durchdachte Entscheidung nicht zugemutet werden Empfehlung BFU 3 4 Anmerkungen und Konsequenzen Die Optimierungen an der Software des TCAS Systems sind nahezu abgeschlossen In der als final bezeichneten Version die auch in Europa vorgeschrieben ist ist noch einmal eine Reduktion der Fehlalarme e
74. bstrak tionsschicht bereitzustellen Dies ist notwendig damit den Anwendungsprogrammen eine einheitliche Schnittstelle bereitgestellt wird und die Komplexit t der Hardware verborgen bleibt Diese grunds tzliche Aufgabe l t sich noch wie folgt aufgliedern wobei ich nur Aspekte betrachte die f r Realzeitanwendungen von Bedeutung sind Resourcenverwaltung In einem Rechner wird eine Vielzahl an Ressourcen zur Verf gung gestellt Dazu geh ren z B Datenspeicher Grafikausgabe Soundausgabe Netzwerkzugriff und hnliches Aufgabe des Betriebssystem ist einerseits wie bereits erw hnt die Komplexit t der Hardware zu verbergen Ein gutes Beispiel daf r sind Ethernetkontroller Der ak tuellen Kernel 2 6 6 stellt 31 Treiberfamilien f r 10 oder 100 MBit Ethernetkontroller bereit Das Betriebssystem bernimmt die spezifische Ansteuerung des Kontrollers und stellt den Anwendungsprogrammen eine einheitliche Ether netschnittstelle bereit Anderseits mu das Betriebssystem den Zugriff auf die Hardware organisieren und koordinieren M chten zwei Anwendungsprogramm gleichzeitig Daten ber das Netzwerk bertragen so mu das Betriebssystem steuern welches Programm wann auf das Netzwerk zugreifen darf Multitasking und Kontextwechsel Ein besondere Aufgabe der Ressourcenverwaltung ist die Verwaltung der CPU bzw der Rechenzeit und die Verteilung dieser an die Anwendungsprogramme Bei dieser Aufgabe unterst tzen aktuelle Prozessoren das Betriebs
75. c boolean operators v disjunction A conjunction negation gt implication and lt gt equivalence We also have the first order operators existence and V universality Good for describing static conditions e Temporal Logic an extension of Classical logic which incorporates special operators that cater for time With Temporal Logic we can specify how components protocols objects modules procedures and functions behave as time progresses The specification is done with Temporal Logic statements that make assertions about properties and relationships in the past present and the future It is convenient to use Temporal Logic to express temporal relationships between events and so Temporal Logic is widely used for specification formulas The formulas are interpreted over Kripke structures which can model computation Therefore Temporal Logic s very useful in formal verification There are five basic temporal operators for the Temporal Logic to describes how static conditions change over time e X next time requires that a property holds in the next state of the path e F in the future requires that a property will hold at some state on the path e G globally requires that a property holds at every state on the path e U until combines two properties It holds if there is a state on the path where the second property holds and at every proceeding state on the path the first
76. ch die Transponderantwort die H he des anderen Flugzeugs fest gestellt werden Etwa jede Sekunde wird so eine berpr fung des umgebenen Luftraums durchgef hrt Nun sch tzt das System die Entwicklung der Situation ab indem es die An n herungen der einzelnen georteten Flugzeuge hochrechnet TCAS berpr ft nur die An herungsrate um die zugrundeliegenden Algorithmen m glichst einfach zu halten Die Ausgabe von Warnungen wird ber zwei Mechanismen festgelegt Bei schnell be wegenden oder Objekten auf direkten Kollisionskurs wird die Einhaltung des Tau Be reichs berpr ft Tau ist definiert als die Zeit die ein Eindringling bis zum n chsten Ann herungspunkt braucht Damit passt sie sich an die Geschwindigkeit und Richtung des Ein dringlings an Vor einem schnellen Flugzeug auf Kollisionskurs wird also fr her gewarnt als vor einem langsamen Objekt auf einem schr gen Kurs Wenn aber ein Flugobjekt sich langsam ann hert und zus tzlich auch nur einen wenig unterschiedlichen Kurs hat w rde eine Kontrolle von Tau nicht mehr ausreichen um auszuweichen Deshalb wird zus tzlich der Mindestabstand f r Objekte berpr ft Wenn ein Objekt diese Schwelle unterschrei tet wird auch eine Warnung ausgegeben Wenn keine genauen H henangaben von dem eindringenden Flugobjekt verf gbar sind wird ein fester Wert angenommen Reelle Werte f r diese Paramter findet man unter aerowinx Diese Systemparameter werden abh ngig von der Flugh
77. che Wirkungs Graph Wenn die Spezifikation zu kompliziert ist gibt es viele Ursachen und Wirkungen Der Graph sieht kompliziert aus 4 White Box Test Eingabe Ausgabe Der Tester muss die innere Struktur des Programms und den Quellcode kennen weil die innere Struktur des Programms bei dieser Strategie getestet wird Bel dieser Strategie definiert der Tester die Testdaten mit Kenntnis der Programmlogik zum Beispiel if else Verzweigung Das wichtige Prinzip beim White Box Test ist 1 Jeder Programmpfad muss mindestens einmal durchlaufen werden 2 Jeder Modul jede Funktion muss mindestens einmal benutzt werden Einige wichtige Verfahren von White Box Test l Beweis durch Widerspr che 2 Testdeckungsgrad logic coverage testing 4 1 Beweis durch Widerspr che Beweis durch Widerspr che bedeutet dass man von der Annahme ausgeht e n unsicherer Zustand kann durch Ausf hrung des Programms herbeigef hrt werden Man analysiert den Code und zeigt dass die Vorbedingungen f r das Erreichen des unsicheren Zustands durch die Nachbedingungen aller Programmpfade die zu diesem Zustand f hren k nnen ausgeschlossen werden Um diese Methode zu verdeutlichen wird hier ein einfaches sicherheitskritischens medizinisches System verwendet Dieses System heisst Insulindosiersystem Insulindosiersystem ist ein Ger t das den Blutzuckergehalt berwacht und gibt falls erforderlich eine angemessene Insulindosis aus Das Bild zeigt
78. chrieben Das Qualit tsmanage ment wird im Unternehmen normalerweise mittels eines so genannten Qualit ts management Systems umgesetzt Die International Organization for Standardization kurz ISO definiert in ihrem Standard ISO 9000 ein Qualit tsmanagement System folgenderma en Definition 1 Qualit tsmanagement System The organizational structure responsibilities procedures processes and resources for implementing quality ma nagement 2 S 348 Bevor es m glich ist n her auf Qualit tssicherung und Qualit tskontrolle einzu gehen sind noch ein paar weitere Definitionen notwendig Fiir weitere Informationen siehe 1 2 Anmerkung Mehr als 500 000 Organisationen in 160 L ndern wenden den ISO 9000 Stan dard an 5 N here Informationen zu ISO 9000 finden sich in Abschnitt 1 5 1 Qualit tsmanagement Qualit tssicherung Qualit tskontrolle Fertigungsprozess Produkte In in Abbildung 1 Bestandteile des Qualit tsmanagements 1 2 1 Definition Sicherheit Ein weiterer wichtiger Terminus der in diesem Artikel immer wieder auftaucht ist der Begriff Sicherheit Dieses Schlagwort muss allerdings genauer abgegrenzt werden da es einen relativ gro en Spielraum der Interpretation offen l sst Unter Sicherheit wird im Zusammenhang mit sicherheitskritischen Systemen nur das Risiko f r das menschliche Leben oder der Umgebung angesehen nicht aber die Sicherheit der Privatsph re oder der nationalen Sicherhe
79. d to make them easier to use by engineers 1 Relatively straightforward extensions of current systems one problem with current systems is how to make the specification language more expressive and easier to use Some type of timing diagram notation may be more natural for engineers than CTL 2 Require more theoretical work one direction for research is to develop even more concise techniques for representing Boolean functions When better representations are developed they can easily be incorporated into model checking algorithms 3 Use abstraction and compositional reasoning techniques to handle more complex systems There have been some attempts to automate abstraction techniques for hardware Some work has also recently appeared on automatic application of compositional methods 4 probabilistic verification It may be possible to tell not only whether a failure is possible in a system but also what the probability of the failure occurring is If such an analysis were performed failures with extremely low probabilities of actually occurring could be safely ignored 5 The ability to reason automatically about entire families of finite state systems Such families arise frequently in the design of reactive systems in both hardware and software We have focused on finite model structures but recent research shows that effective Model Checking is possible also for certain classes of finitely presented infinite structures 6 Investigati
80. den 7 Zusammenfassung Black Box Test und White Box Test werden zur Validation einer Software eingesetzt Durch Black Box Test und White Box Test wird untersucht ob eine Software der Spezifikation und dem Kundenwunsch entspricht oder nicht Mit Black Box Test wird vor allem untersucht ob die Software seiner Spezifikation entspricht Es gibt drei wichtigen Methoden quivalenzklassenbildung Grenzwertanalyse und Test spezieller Werte Bei der quivalenzklassenbildung werden die Eingabedaten eines Programms in eine endliche Anzahl von Aquivalenzklassen unterteilt Mit Hilfe der Grenzwertanalyse werden Werte an den Grenzen von Aquivalenzklassen untersucht Aquivalenzklassenbildung und Grenzwertanalyse haben einen gemeinsamen Nachteil Sie k nnen keine Wechselwirkung bzw Zusammenh nge zwischen Eingabedaten untersuchen Mit Hilfe der Ursache Wirkungs Graphen wird dieser Nachteil behoben Ein Ursache Wirkungs Graph ist eine formale Sprache in die eine Spezifikation aus der nat rlichen Sprache bersetzt wird Aquivalenzklassenbildung und Grenzwertanalyse k nnen entweder als eine Schaltung der Digitallogik oder als einen kombinatorischen logischen Graph dargestellt werden Mit White Box Tests wird sichergestellt dass das Programm keinen ungetesteten Code enth lt Bei dieser Methode wird jeder Programmpfad mindestens einmal durchlaufen F r die Erstellung der effektiven Testf lle zur Fehlerabdeckung st die Kombination von Black Box Test u
81. denburg de hybrid rtjava rtasync ppt Stand 28 07 2004 Eisma Aldo Developing Embedded Systems Using the Java Programming Language http www netobjectdays org pdt 00 slides eisma pdf Stand 27 09 2000 Selvarajan Dinesh Implementation of Real Time Java using KURT http www ittc ku edu research thesis documents dinesh_selvarajan pdf Stand 08 01 2004 Gu Lin The Real Time Specification for Java http www cs virginia edu qc9b cs85 1 vm 1 ppt Stand 24 06 2004 Bollella Greg Brosgol Ben Dibble Peter Furr Steve Gosling James Hardin David Turnbull Mark Belliardi Rudy DRAFT The Real Time Specification for Java http www rtj org latest pdf Stand 31 07 2002
82. der Modelle Mapping 3 6 1 PIM nach PIM 3 6 2 PIM nach PSM 3 6 3 PSM nach PSM 3 6 4 PSM nach PIM 1 Einleitung Die UML enth lt die Konventionen mit denen Softwaredesigner und Entwickler Softwareprojekte eindeutig spezifizieren modellieren und dokumentieren k nnen Mit UML 2 0 eingef hrte Erweiterungen und Verbesserungen lassen sich noch besser zur Modellierung komponentenbasierter Systeme einsetzen Das Hauptziel bei der Definition von UML 2 0 war die sog MDA Model Driven Architecture Mit diesem Konzept lassen sich mit den speziellen Softwarewerkzeugen ausf hrbare Programme theoretisch direkt aus den Modellen erzeugen Dazu m ssten aber Compiler bzw Interpreter f r die jeweilige Plattformen existieren die plattformspezifischen Modelle ausf hrbar zu machen Solche Compiler oder Interpreter existieren nur n Nischenbereichen bzw n der Diskussion 2 Vergleich des UML 2 0 und des Vorg ngerversions 1 x Mit UML 2 0 ist es M glich 14 verschiedene Diagramme zu erfassen d e verschiedene Aspekte des Systems modellieren berwiegend alle Diagrammarten wurden berarbeitet und mit neuen Elementen ausgestattet e Strukturdiagramme o Klassendiagramme o Kompositionsstrukturdiagramme neu o Komponentendiagramme o Paketdiagramme o Verteilungsdiagramme o Objektdiagramme e Verhaltensdiagramme o Aktivitatsdiagramme o Zustandsautomat Diagramme o Anwendungsfalldiagramme o Interaktionsdiagramme Kommunikationsdi
83. des Safety Case 1 Qualitatsmanagement 1 1 Qualit t Bevor es m glich ist sich mit Qualit tsmanagement auseinander zu setzen muss zun chst einmal der Terminus Qualit t n her betrachtet werden In der Litera tur kursieren mehrere Definitionen die den Begriff n her beschreiben So wird Qualit t zum Beispiel mit den folgenden Eigenschaften beschrieben e Tauglichkeit der Nutzung e bereinstimmung mit den Anforderungen oder Bedingungen e Alle Merkmale und Charakteristika eines Produktes oder einer Dienstlei stung die sicherstellen dass der zuvor bestimmte Bedarf befriedigt wird Im Hinblick auf sicherheitskritische Systeme und deren gehobenen Anspruch auf Qualit t sollte man den Qualit tsbegriff als eine Kombination aus diesen Eigen schaften ansehen So k nnte man Qualit t als einen Prozess beschreiben der daf r sorgt dass die gefertigten Produkte ihren Zweck mit einer m glichst gerin gen Zahl an M ngeln erf llen Nachfolgend soll dieser Qualit tsbegriff als Grundlage dienen 1 2 Einleitung Was verstehen wir also unter Qualit tsmanagement Das Qualit tsmanagement ist als Oberbegriff zu verstehen der eine m glichst gute Mischung aus Qualit tssicherung und Qualit tskontrolle vereint vlg Ab bildung 1 um die besten Ergebnisse im Form eines qualitativen Produktes zu erzielen Diese beiden essentiellen Bestandteile des Qualit tsmanagements werden in den Abschnitten 1 3 und 1 4 noch genauer bes
84. dex html 8 Abbildungen Abb Abb Abb Abb Abb Abb Abb Abb Abb Abb Abb Abb Abb Abb Abb Abb Abb 9 1 Die Diagrammtypen der UML 2 2 Grundelemente der Interaktionsmodellierung in ihren Diagrammvarianten 3 Grundprinzip einer Interaktion hier in Sequenzdiagrammform 4 Das Timing Diagramm und seiner Elemente 9 6 7 8 Der zeitliche Ablauf einer n chtlichen Alkoholkontrolle Interaktionsrahmen eines Timing Diagramms mit Zeitskala Notation von Lebenslinien in Timing Diagrammen Namensgebung einer Objekt Lebenslinie Zeitverlaufslinie 10 Zeitbedingungen einer Fahrstuhlt r 11 Stoppereignis einer Zeitverlaufslinie 12 Notation von Nachrichten 13 Sprungmarken an Nachrichten 14 Verwendung von Sprungmarken 15 Notation der Wertverlaufslinie 16 Tageszahlen eines Monats 17 Eine Waschstra e mit einer Wertverlaufslinie UML 2 0 Quelltextgenerierung Seminararbeit im Fach Informatik im Rahmen des Seminars Sicherheitskritische Systeme an der Universit t Siegen Facheruppe f r Praktische Informatik eingereicht bel Dr J rg Niere vorgelegt von Beyhan Goelgeli Sommersemester 2004 1 EINLEITUNG 2 VERGLEICH DES UML 2 0 UND DES VORG NGERVERSIONS 1 X 3 QUELLTEXTGENERIERUNG AUS DEN UML DIAGRAMMEN 3 1 Model Driven Architecture MDA 3 2 MOF 3 3 PIM Plattform Independent Model 3 4 PSM Plattform Specific Model 3 5 Templates 3 6 Abbildung
85. die Wahrscheinlichkeit des Eintreten eines Hazard auf mehrere Weisen reduziert wird Es werden passive und aktive Safeguards eingesetzt Monitoring f r kritische Funktionen mit Hilfe von Entwurfmuster Lockouts um den Zugang zu kritischen Prozessen oder Zust nden zu erschweren Lockins um das Verlassen eines sicheren Zustandes zu erschweren und Interlocks die wie Semaphore funktionieren Weitere Verfahren sind die Benutzung von Redundanzen um zum Beispiel das System von willk rlichen Hardwarefehlern zu sch tzen und die Wiederherstellung der alteren Daten 1m Falle eines Fehlers 6 Beispiel aus dem Neigemodul des Shuttles a Model Checking der Software b Sensoren an Fahrzeugende und spitze Anbringen von Redundanten Sensoren c M glichst lokale berpr fung von Aktoren und Sensoren Kontrollsoftware direkt an Sensoren und Aktoren die Fehlermeldung an Zentralsoftware senden kann 6 3 Hazard control Es gibt Hazards die n tig sind weil sie nur schwer auszuweichen sind Wenn das der Fall ist muss ein solcher Zustand nur so kurz wie m glich besucht werden das hei t die Aufenthaltszeit in einem unsicheren Zustand muss moglichst reduziert werden Um das zu erreichen gibt es der Fail Safe Design Dies ist Charakterisiert durch so genannte Fallback Zustande in denen das System zur ckkehren kann sobald ein r skanter Zustand entdeckt wird Die bekannteste Fallback Zust nde sind das partielle Shutdown mit minimaler Funktional
86. die Arbeitsweise eines Insulindosiersystems lutparameter B Blut E Nm Befehl fiir die Pumpensteuerung wa Insulinbedarf Insulin Quellcode f r die Insulinabgabe COPYRIGHT 1994 by Ian Sommerville Die abgegebene Insulinmenge ist eine Funktion des Blutzuckerspiegels der zuletzt abgegebenen Dosis und der Zeit zu der die letzte Dosis verabreicht wurde CurrentDose computeInsulin Sicherheits berpr fung Anpassung der aktuellen Dosis wenn n tig if Anweisung 1 if previousDose 0 if currentDose gt 16 currentDose 16 else if currentDose gt previousDose 2 currentDose previousDose 2 1f Anweisung 2 if currentDose lt minimumDose currentDose 0 else if currentDose gt maxDose currentDose maxDose administerInsulin currentDose Die Vorbedingung f r den unsicheren Zustand in diesem F lle ist currentDose gt maxDose Jetzt miissen wir zeigen dass alle Programmpfade 1m Widerspruch zu dieser unsicheren Annahme stehen Wenn dies der Fall ist kann die unsichere Bedingung nicht wahr sein Also ist das System sicher Wenn wir den Code analysieren gibt es drei m gliche Programmpfade die zum Aufruf der Methode administerInsulin f hren l Keiner der Zweige der f Anweisung 2 wird ausgef hrt Das kann nur geschehen wenn currentDose gr sser oder gleich minimumDose und kleiner oder gleich maxDose ist 2 Der then Zweig von if Anweisung 2 w
87. die erste ausgefallene Leitung wurde die Belastung der anderen verst rkt sie wurden mehr erw rmt und sanken dadurch noch mehr durch Deshalb wurde die Wahrscheinlichkeit f r einen Ausfall gr er und Versuche die Leitungen wieder zu benutzen schlugen wieder nach kurzer Zeit wegen einem Kurzschluss fehl Nachdem diese drei Leitungen ausgefallen waren wurden die verbliebenden 138 KV Leitungen weit ber ihre Spezifikation hinaus belastet Von 15 39 bis 15 58 fielen sieben Leitungen von ihnen aus alle ber hrten aufgrund von berlastung benachbarte Leitungen B ume oder den Grund 2 2 4 Falsche oder keine Echtzeit berwachungsdaten und mangelhafte Zusammen arbeit Von 12 15 bis 16 04 war der State Estimator ein Werkzeug zur Entscheidungshilfe bei MISO nicht funktionsf hig Ausserdem fehlten Onlinedaten von einer speziellen Stromlei tung aufgelaufene Fehlermeldungen aus dem Netz von FE wurden nicht automatisch mit ber cksichtigt Deshalb war der Reliability Coordinator nicht in der Lage fr hzeitig die Probleme zu erkennen und FE bei der L sung zu helfen Auch nachdem mehrere Leitun gen ausgefallen waren benutzte MISO immer noch die alten Vorhersagewerte des Flow gate monitoring tool einem Werkzeug zur Vorhersage bzw Berechnung des Stromfluss Deshalb fiel es MISO nicht auf dass ab 15 05 sich das Netz von FE in einem kriti schen Zustand befand die sogenannte n 1 Bedingung verletzte Diese besagt das ein Netz im
88. die ihn bei der Navigation unterst tzen soll Die Reichweite liegt bei etwa 6 NM ein eventuelles Ausweichen muss entweder ber Sicht erfolgen oder von der Bodenkontrolle unterst tzt werden Es erlaubt dem Piloten dann um 300 ft zu steigen seitliche Ausweichbewegungen sind nicht erlaubt Dieses System ist f r alle Flugzeuge mit 10 bis 30 Sitzpl tzen in den USA obligatorisch Zus tzlich zu dieser Funktionalit t unter st tzt das TCAS II System auch vertikale Ausweichempfehlungen bei einer Reichweite von ca 16 NM Die Piloten k nnen also ohne auf die Bodenkontrolle zu warten selbst schnell ausweichen Dieses System erlaubt es um 2500 ft zu steigen oder abzusinken Die Ausweichempfehlungen sind sowohl vorbeugend also den Rat die momentane Geschwin digkeit und H he beizubehalten als auch aktiv die sofortige Aktion erfordern Es ist f r Flugzeuge ab 30 Sitzpl tzen in den Vereinigten Staaten Pflicht TCAS HI arbeitet ber eine 13Im Englischen als Traffic Advisory TA bezeichnet l4Seemeile oder auch nautische Meile INM 1 852km 5 m Englischen als Resolution Advisory RA bezeichnet Reichweite von etwa 20 NM und ber cksichtigt dann auch die M glichkeit des seitlichen Ausweichens 3 2 3 Technische Funktionsweise TCAS ist ein aktives System Es fragt von Flugzeugen in Reichweite ihre Transponder ab Luftfahrzeuge ohne Transponder werden nicht erkannt Durch die Laufzeit des Signals kann die Entfernung dur
89. e systems that can be verified to 10 20 10430 states but still there are a vast number of systems that are too complex to handle Typical verification tasks still take modern sequential computers to their memory limits or use the accumulated memory of parallel computers It is important to find techniques that can be used in conjunction with existing approaches have been introduced allowing for complex systems to be model checked Five such techniques are equivalence compositional reasoning abstraction symmetry and induction 3 3 1 Equivalence Equivalence is a technique to transform models into equivalent but smaller models that satisfy the same properties that means replace a large structure by a smaller structure which satisfies the same properties to avoid the state explosion problem Most precisely Given a logic L and a structure M try to find a smaller structure M that satisfies exactly notion of equivalence between structures that can be efficiently computed and guarantees that two structures satisfy the same set of formulas in L Simulation equivalence and bisimulation equivalence are some of most common notions of semantic equivalence Informally speaking two models are bisimilar if each transition in the once model can be simulated by the other and vice versa 3 3 2 Compositional Reasoning Compositional verification is a technique to decompose properties in sub properties such that each sub property can be checked fo
90. ee ka 2 3 Weiterer Verlauf der Ereignisse sia was seat ds res 24 ANMerk neen u ar ar Ehe BOE Stee te ES ws a 3 Der Flugzeugabsturz bei berlingen am Bodensee Del Mine tun An m ee Rares th ke aay ea er an ar Bee 32 Das TICAS System dd Sa e a a En re a RSE E 32 1 Ablintererind se 2 8 402 0er al le at dees Bears 332 2 CAINS AUD ins Ge Se o Br A Ban 3 2 3 Technische Funktionsweise a 0 3 2 4 Mensch Maschine Interface 3 23 Probleme un ark A E ES aia ra A Sa AA A IS Oe ph ee Ae Se a A 3 3 1 Technische M ngel bei der Flugsicherung 3 3 2 Stress und berlastung 2 2 2 Coon 3 5 5 Probleme durch TEAS 2 2 24 2 2 as zu kek 3 3 4 Formelle Probleme 5 secdha woe oe ed a kant 2 3 4 Anmerkungen und Konsequenzen 1 Begrifflichkeiten Sicherheitskritischer Systeme Exakte Definitionen sind fiir grundlegend fiir den Entwurf und das Design von SkS Dieser Teil dieser Arbeit soll helfen Unklarheiten die bei der Verwendung der oft auch umgangs sprachlich genutzten Begriffe fters auftreten auszur umen Alle Definitionen in diesem Abschnitt sind an die Ver ffentlichungen von Storey und Giese angelehnt 1 1 Allgemeine Definitionen 1 1 1 Was sind Sicherheitskritische Systeme Als Sicherheitskritische Systeme oder auch Sicherheitsrelevante Systeme bezeichnet man Systeme die die Sicherheit einer Anlage garantieren bzw sie unterst tzen 1 1 2
91. efinition 2 4 Spezifikation Spezifikation ist ein Test der die Syntax und Semantik eines bestimmten Bestandteiles beschreibt bzw eine deklarative Beschreibung was etwas ist oder tut 9 Definition 2 5 Testen Das Testen ist der Prozess ein Programm auf systematische Art und Weise auszuf hren um Fehler zu finden 10 W hrend die Verifikation den Output einer Entwicklungsphase auf die Korrektheit mit der vorherigen Phase untersucht wird die Validation benutzt um das Gesamtsystem mit den Kundenanforderungen zu vergleichen Die zentrale T tigkeit bei Validation ist das Testen Das Gesamtsystem wird bei Ende des Prozess getestet ob es den Kundenanforderungen entspricht oder nicht Ein eigenes Kapitel ist dem Testen gewidmet deswegen wird es an dieser Stelle nicht erkl rt Die zentrale T tigkeit be1 der Verifikation ist der Beweis mit der formalen Verifikation Dieser Beweis wird nicht n dieser Ausarbeitung behandelt Validation Tf Validation T Verification mt 1 Verification Verification Verification Verification Verification Verification Abbildung 2 1 Entwicklungsphase mit dem formalen Verifikationsnprozess Es gibt zwei grundlegende Strategie fiir das Testen von Software Die erste Strategie wird Black Box Test genannt Black Box Test bedeutet dass der Tester nicht die Kenntnisse ber das interne Verhalten und die Struktur des Programms hat Die zweite Strategie wird White Box Test genannt Um diese Tes
92. efinition f hrt Siehe 3 f r n here Informationen 1 3 Qualit tssicherung 1 3 1 Einleitung Nach diesen einleitenden Begriffsabgrenzungen ist es nun m glich wieder zum eigentlichen Thema zur ckzukehren ISO 9000 definiert Qualit tssicherung wie folgt Definition 2 All those planned and systematic actions necessary to provide ade quate confidence that a product or service will satisfy given requirements for qua lity 2 S 348 Wie Abbildung 1 bereits deutlich gemacht hat besch ftigt sich die Qualit ts sicherung mit dem Fertigungsprozess von Produkten Das hei t die Qualit ts sicherung muss daf r sorgen dass die Entwicklung bzw Design und Test Operationen richtig ausgef hrt werden Sie erstreckt sich somit auf diese drei Aufgabenbereiche 1 Definition des Fertigungsprozesses und des eingesetzten Management Systems 2 Management der Ressourcen 3 Pr fende und qualit tsverbessernde Aktionen Bei sicherheitskritischen Systemen stehen neben der Verbesserung der Qualit t des Produktes auch die Verbesserung der Entwicklung und Produktionseffizienz sowie die Bereitstellung einer Basis f r die Rechtfertigung der Sicherheit Safety Case vgl Abschnitt 2 4 im zentralen Blickfeld Da Sicherheit nicht alleine durch Testen demonstriert werden kann kommt auch hier der Qualit tssicherung eine besondere Bedeutung zu Sie muss aufgrund der eingesetzten Methoden bei Entwicklung und Fertigung zur Akzepta
93. eifen kann Fiir diese Anforderungen muss die RTJVM direkte Zugriffe auf den Speicher zulassen wodurch ein gro er Teil ihrer Schutzfunktion anderer Anwendungen vor Java Anwendungen verloren gehen w rde wenn es nicht die Klasse RealtimeSecurity geben w rde Diese stellt Methoden die die Anwendungen schiitzen sollen bereit doch in der Spezifikation sind keine Details zu der genauen Funktion dieser Befehle genannt Folgende Speichertypen wurden neu geschaffen e scoped Memory In dieser Speicherart wird die Lebenszeit eines Objekts durch die vor handenen Referenzen auf den die Threads in diesem Speicher begrenzt Existiert also keine Referenz mehr auf einen Thread in diesem Speicher wird dieser freigegeben e physical Memory Dieser Speicher wird f r Objekte verwendet die Spezielle physikali sche Speicherbereiche ben tigen wie z B einen DMA Adressbereich e immortal Memory In diesem Speicher werden Objekte abgelegt die zur gesamten Lauf zeit der Anwendung existieren Hier r umt die Garbage Collection nie auf Dieser Bereich ist bis zum Ende der Anwendung belegt e Heap Memory Dieser Speicher entspricht dem Heap Hier wird die Lebenszeit eines Ob jekts durch seine Sichtbarkeit begrenzt Dies ist also die traditionelle Speicherart der Ja vaVM lt lt abstract gt gt MemoryArea HeapMemory ScopedMemory ImmortalMemory ImmortalPhysicallMemory
94. ein Fehler die Funktion des Gesamtverbunds Im Gegensatz dazu werden Fehler bei der dynamischen Redundanz kontrolliert Ein oder mehrere Module des Systems werden in Bereitschaft gehalten und bei erkennen eines Fehlers gegen das fehlerhafte Modul aus getauscht Die hybride Redundanz stellt eine Mischform der beiden genannten Typen dar Ausserdem erstrebenswert ist es wenn m glich einen zus tzlichem nicht programmier baren Kanal zu benutzen da ein solches System aufgrund seiner geringeren Komplexit t leichter zu beherschen ist Redundanz in Software l sst sich zum einen durch mehrere unterschiedliche Implemen tierungen die wieder mit einem Entscheider verbunden sind erreichen Alternativ kann man eine Implementation mit mehreren redundant ausgelegte Programmbl cken verwen den wobei nach Ausf hrung eines Blockes jeweils das Ergebnis berpr ft und im Fehler fall zum n chsten Block bergegangen wird Aufgrund des hohen Aufwands und damit der hohen Kosten von Softwareredundanz werden diese M glichkeiten nur bei sehr kritischen Systemen eingesetzt Informationsredundanz wird haupts chlich in der Kommunikationstechnik eingesetzt Ohne das Verwenden von Techniken wie Parit tsbits Checksummen und Fehlererkennende bzw korrigierende Codes w re eine funktionierende Daten bertragung ber gr ere Ent fernungen nicht m glich Unter zeitliche Redundanz versteht man beispielsweise dass ein bestimmter Signalpe gel ber eine de
95. einmaligen Phase am Ende des Projektes 2 6 Zertifizierungsstandards 2 6 1 IEC 61508 Der erste Entwurf dieses Standards wurde unter der Bezeichnung IEC 1508 Func tional Safety Safety Related Systems 1995 herausgegeben Sp ter wurde er in IEC 61508 umbenannt Der Standard beschaftigt sich primar mit sicherheitsrelevanten Systemen die elektrische elektronische oder programmierbare elektronische Systeme als Be standteile enthalten Au erdem gibt er generelle Anweisungen die relevant f r alle Formen von sicherheitskritischen Systemen sind wie zum Beispiel die n tigen Elemente der Lebenszyklus Phasen und der Dokumentation Der Standard um fasst nicht nur die Kontrollelemente der Einrichtung sondern auch alle externen risiko mindernden Anlagen Er spezifiziert allerdings keine Individuen die f r die Umsetzung gewisser Auf gaben verantwortlich sind Ein Schl ssel Element des Standards ist die Tatsache dass es sich um einen generischen Standard handelt der nicht auf einen bestimmten Industriebereich beschr nkt ist 2 6 2 DO 178B Der DO 178B Software Consideration in Airborne Systems and Equipment Cer tification wird in den USA und Europa unter unterschiedlichen Bezeichnungen herausgegeben So hei t er in den USA RTCA C167 DO 178B und in Europa EUROCAE ED 12B Ublicherweise wird er jedoch schlicht mit DO 178B bezeich net Die Letzte Revision stammt aus dem Jahr 1992 Obwohl es sich bei dem Standard um einen indu
96. eistung zur Kompensation bricht die Spannung zusammen 11 Alle Zeiten in diesem Kapitel in EDT Eastern Daylight Time Durch den Ausfall wurden die Netzzustandsdaten nicht mehr aktualisiert ein Umstand der den Bedienern aber erst sehr viel sp ter auffiel Auch nach einen Neustart des Server der die brigen Fehler beseitigte blieb das Alarmsystem offline Die IT Ingenieure von FE hielten keinerlei R cksprache mit den Bedienern sie f hrten keine Funktions berpr fung im Kontrollraum durch Das verwendete System war insgesamt nicht auf dem neusten Stand es gab keinerlei Erfahrung bei den Systemingeneuren mit dieser Art von Fehler Einigen Bedienern fiel die fehlerhafte Funktion des Systems mehrmals auf sie vers umten es aber dies ihren Kolle gen mitzuteilen Auch mehrere telefonische Meldungen ber Probleme von benachbarten Kontrollgebieten sorgten nicht daf r dass die Bediener von einem Fehler in ihrem System ausgingen Dies wurde dadurch beg nstigt dass die Bediener r umlich getrennt unterge bracht waren und auch kein gemeinsames Logbuch benutzten Die Bediener waren f r Notf lle nicht gen gend ausgebildet es dauerte sehr lange bis sie das Versagen ihres Sys tems akzeptierten 2 2 3 Unzureichendes Beschneiden der B ume Von 15 05 bis 15 41 fielen drei 345 KV Leitungen im Netz von FE aufgrund von Kontakt mit zu hoch gewachsenen B umen aus Dadurch sank die Spannung im Netz auf knapp 93 Prozent der Nennspannung Durch
97. em and to reduce the state space The reduced model can be used to simplify the verification of properties of the original model expressed by a temporal logic formula 3 3 5 Induction Induction involves reasoning automatically about entire families of finite state systems Such families arise frequently in the design of reactive systems in both hardware and software Typically circuit and protocol designs are parameterized that is they define an infinite family of systems For example a circuit designed to add two integers has the width of the integers n as a parameter a bus protocol may be designed to accommodate an arbitrary number of processors and a mutual exclusion protocol can be given for a parameterized number of processes We would like to be enable to check that every system in a given family satisfied some temporal logic property In many interesting cases it is possible to provide a form of invariant process that represents the behavior of an arbitrary members of the family Using this invariant we can then check the property for all of the members of the family at once An inductive argument is used to verify that the invariant is an appropriate representative 4 Model Checking for real time Systems Computers are frequently used in critical applications where predictable response times are essential for correctness Such systems are called real time systems Examples of such applications include controllers for aircraft ind
98. en es gibt Kontrollstrukturen komplexere Datentypen Syntax und Typ berpr fung e Java ist leichter in vollem Umfang zu erlernen wie C weil man bei der Spezifikation von Java darauf geachtet hat die Fehler die bei der Entwicklung von C C und anderen Pro grammiersprachen gemacht worden sind zu vermeiden Und man legte sehr viel Wert dar auf viele Sachen zu vereinfachen e Java ist relativ sicher da es auf einer Virtual Machine VM l uft die nur eingeschr nkten Zugriff auf die Hardware und die Software zur Laufzeit hat Der Code l uft quas n einer Sandbox Dieser Zugriff muss bei Real Time Java aber etwas gelockert sein gegen ber dem normalen Java dazu aber mehr m weiteren Verlauf dieses Seminars e Java unterst tzt das dynamische Laden neuer Klassen so das zur Kompilezeit nicht alle Klassen in der endg ltigen Form vorliegen m ssen sondern auch noch sp ter zur Laufzeit nachgereicht bzw aktualisiert werden k nnen e Java unterst tzt Objekt und Thread Erstellung zur Laufzeit Man kann also diese Vorg nge direkt mit Java zur Laufzeit beeinflussen und von lokalen Situationen abh ngig machen e Java wurde auch entworfen um Code Komponenten zu integrieren und wieder zu verwen den Damit sich Funktionsbibliotheken anlegen und verbreiten lassen Dies ist generell bei heutigen Programmiersprachen wichtig damit dadurch Arbeitszeit gespart werden kann weil nicht st ndig das Rad neu erfunden wird
99. en Lieferanten klein meistens auf einen Anbieter begrenzt war So konnte oft der Anbieter den Preis bestimmen anderseits konnten die Entwicklungskosten f r eine Spezialumgebung nur auf ein Projekt umgelegt werden und nicht auf mehrere verschiedene Anwendungen Projekte e Der gr ere Teil der verwendeten Programmiersprachen ist einfach veraltet gewesen die Neuerstellung von Software war teilweise teuerer als die Wartung 1 5 wurde innerhalb der DoD eine Kommission Higher Order Language Working Group kurz HOLWG gegr ndet deren Aufgabe war die M glichkeit der Vereinheitlichung der Programmierwerkzeuge zu untersuchen Die Kommission stellte in mehreren Schritten Anforderungskataloge auf untersuchte bereits vorhandenen und eingef hrte Sprachen am Ma stab der Anforderungen und kam zu dem Ergebnis das keine der untersuchten Programmiersprechen ber alle erforderlichen Merkmale verf gt Es hat sich dabei aber rausgestellt das es m glich sei eine neue Sprache zu Entwickeln die Eine volle Realisierung der Anforderungen darstelle so wurde der Grundstein f r die Entstehung von ADA gelegt 1 2 Die Umsetzung Als man 1 6 aus den gestellten Anforderungen an die neue Programmiersprache eine formale Sprachspezifikation aufgestellte hat das DoD die Entwicklung einer dieser Spezifikation entsprechenden Sprache international ausgeschrieben Insgesamt wurden 1 Sprachvorschl ge eingereicht von denen wurden erst mal 4 weiterentwickelt N
100. en Vermeidung getroffen wurden Des Weiteren muss er zeigen dass die Integrit t des Systems f r dessen Anwendung angemessen ist In manchen F llen muss der Beweis erbracht werden dass das System einem be stimmten Standard entspricht Au erdem m ssen Nachweise ber die eingesetz ten Entwicklungs und Testmethoden erbracht werden um die Angemessenheit ihres Designs zu berpr fen Zusatzlich ist es notwendig erschwerende Argumente anzufiihren um dem An spruch der Systemsicherheit gerecht zu werden Um diese Beweise zu erbringen wird im allgemeinen der so genannte Safety Case siehe Abschnitt 2 4 entwickelt AbschlieBend bleibt noch anzumerken dass die Zertifizierung eines Produktes nicht dessen Sicherheit beweist und den Hersteller somit nicht von seinen mora lischen oder rechtm igen Pflichten entbindet 2 2 Arten der Zertifizierung Zertifikate gibt es f r unterschiedliche Objekte Hier sollen die wichtigsten kurz vorgestellt werden Die Zertifizierung von Systemen oder Produkten ist dabei die Wichtigste f r diesen Artikel 2 2 1 Organisationen oder Individuen Das Ziel dieser Zertifizierung ist es dass die beglaubigte Organisation ein be stimmtes Ma an Erfahrung aufweist und die vereinbarten Standards erf llt Dabei ist es vergleichsweise leicht die Verfahren die angewendet werden auf Korrektheit zu berpr fen Schwieriger wird es zu berpr fen mit welcher Kom petenz diese durchgef hrt werde
101. en ein hohes Ma an Flexibilit t und Abstraktion steigert aber auch enorm die Komplexit t der Programme was wiederum zu Folge hat dass die logische G ltigkeit der Anweisungen f r den Entwickler nicht immer erkennbar ist Grundsatzlich ist es empfehlenswert diese Konstrukte in SkS nicht einzusetzen 3 3 2 Initialisierungsfehler initialilising failure Grunds tzlich ist ein Initialisierung der Datenobjekte optional Deshalb ist es im herk mmlichen Ada nicht erkennbar ob ein skalarer Wert korrekt vorbelegt wurde Die Verantwortung fir die Initialisierung wird aber nicht komplett den Programmier berlassen auf Wunsch wird dies durch ein entsprechendes Pragma vom Laufzeitsystem bernommen Das Pragma Normalize_Scalare belegt alle Skalarwerte mit einer Vorbelegung die nach M glichkeit nicht dem legalen Wertebereich des Skalartyps entnommen ist Auf diese Weise kann sp ter sicher und nicht aufgrund eines Zufalls erkannt werden ob eine Vorbelegung berhaupt erfolgt ist Zu diesem Zweck steht ein Attribut Valid zur Verf gung dass sie legale Vorbelegung der Skalare verifiziert 3 3 3 Ausdruc saus ertungsfehler expression evaluation error Die Laufzeit berwachung Ausnahmenmechanismus berwacht die korrekte Ausf hrung der Ausdr cke Bei unerwarteten Ereignissen wird eine Ausnahme ausgel st die durch eine Behandlungsroutine abgefangen wird 3 4 Performance Leistung Performance einer Programmiersprache l sst kann eige
102. en einwandfreien und sicheren Betrieb ist der Regionalbezirk ECAR einem Unterbe reich der NERC zust ndig Ausserdem existieren mehrere Reliability Coordinator die den einwandfreien Betrieb der einzelnen Kontrollgebiete untereinander sicherstellen Das betreffenden Gebiet in dem der Zusammenbruch begann wurde von MISO und PJM betreut Im folgenden werde ich die Gr nde die zur der Katastrophe f hrten einzeln auf f hren 2 2 1 Mangelhaftes Systemverst ndnis und berlastung des Netzes Sowohl bei der berwachungsbeh rde ECAR als auch bei FE war das Verst ndnis f r die kritischen Punkte des Netzes von FE nicht gegeben Der 14 August war ein warmer Sommertag mit normaler Netzlast Mehrere Generatoren waren an diesem Tag wegen Wartung au er Betrieb au erdem waren mehrere gro e Kondensatorb nke f r eine Rou tineinspektion vom Netz getrennt Ab Mittags fielen dann mehrere Stromleitungen und ein Kraftwerk dass viel Blindleistung lieferte aus Dies in Verbindung mit der steigenden Last am Nachmittag sorgte dafiir dass die Spannung im Netz immer weiter abnahm Trotz dieser widrigen Umst nde und Ausf lle war das Netz von FE bis 15 05 stabil obwohl es in mehreren Parametern an den Grenzen der Vorschriften von NERC operierte Diese Ausf lle oder eventuell das warme Wetter sind also nicht f r die die Katastrophe verantwortlich Es war den Verantwortlichen bei FE aber nicht bewusst dass ihr Netz in diesem
103. enden Systemreaktionen modelliert werden sollen stellt die UML verschiedene Diagrammtypen zur Verf gung Dies sind die folgenden vier Diagramme Sequenzdiagramm Kommunikationsdiagramm Timing Diagramm Interaktionsubersichtsdiagramm Es besteht ebenfalls die M glichkeit im Rahmen der UML Erweiterungsmechanismen eigene Diagramme zu entwerfen Abbildung 2 zeigt die drei m glichen Varianten zum darstellen von Lebenslinie und Nachricht am Beispiel eines Kochs der an einem Herd Kommunikationspart ner die Temperatur einstellt Nachricht Abbildung 2 Grundelemente der Interaktionsmodellierung in ihren Diagrammvarianten 1 4 Modellierung von Interaktionen Von Interaktionen spricht man immer dann wenn zwei oder mehre Einheiten mit einander kommunizieren Die Grundelemente von Interaktionen sind die Lebens linien die die einzelnen Kommunikationspartner reprasentieren und die Nachrich ten die zwischen den Kommunikationspartnern versendet werden Bei der Nach richt kann es sich um verschiedenes handeln z B der Aufruf oder die R ckant wort einer Operation bei einer Klasse ein Zeitsignal das setzen einer Variablen oder ein logisches analytisches Ereignis wie K ufer unterschreibt Vertrag Das Grundprinzip einer Interaktion wird in Abbildung 3 dargestellt Abbildung 3 Grundprinzip einer Interaktion hier in Sequenzdiagrammform 1 5 Timing Diagramme Timing Diagramme werden schon seit la
104. enzbereich erreicht d h die von den Unebenheiten in der Schiene quer und vertikal eingeleiteten St rungen werden so gut wie nicht mehr auf den Wagenkasten bertragen Es resultiert daraus dass der Fahrkomfort in vertikaler und horizontaler Richtung bisher noch nicht erreicht wird 7 3 Systemanforderungen und Sicherheitsanforderungen Bevor man zu Hazard und Risikoanalyse geht soll die Anforderungen an das System richtig spezifiziert werden Die Anforderungsspezifikation steht am Anfang jedes Entwicklungsprozesses und dient als Grundlage fur die Realisierung eines technischen Systems seine Bedeutung ist sehr gro Bei sicherheitskritischen Systemen unterscheidet man zwei wichtige Arten von Anforderungen Systemanforderungen und Sicherheitsanforderungen Sie werden im Folgenden vorgestellt 3 1 Systemanforderungen Systemanforderungen sind die Anforderungen an das gesamte System sie werden in funktionalen nicht funktionalen und internen Anforderungen unterteilt l Funktionale Systemanforderungen e Safety S cherheit e Correctness Korrektheit e Trustability Vertrauensw rdigkeit 2 Nicht Funktionale Systemanforderungen e Reliability Funktionsf higkeit Availability Verf gbarkeit Performance Leistung Effizienz Speicherplatz 3 Interne Systemanforderungen 1 Entwicklung e Understandability Verst ndlichkeit e Testability Testbarkeit e Verifiability Verifizierbarkeit il Wartung e Recoverability Wiederherstellbar
105. er Qualit tskontrolle mit der sich der nachfolgende Abschnitt besch ftigt 1 4 Qualit tskontrolle 1 4 1 Einleitung Zu Beginn sei auch hier die Definition von Qualit tskontrolle nach ISO 9000 dargestellt Definition 3 The operational techniques and activities that are used to fulfil requirements for quality 2 S 351 Das Ziel der Qualit tskontrolle ist es daf r zu sorgen dass m glichst keine fehlerhaften Produkte das Unternehmen verlassen Das hei t die Qualit tskon trolle muss sicher stellen dass das Endprodukt die zuvor festgelegten Spezifika tionen erf llt Sollte dies nicht der Fall sein so muss sie f r eine entsprechende Anpassung des Produktionsprozesses sorgen Bei Hardwarekomponenten muss nicht nur deren Funktionalit t berpr ft wer den sondern auch komplexere Charakteristika wie die Zuverl ssigkeit Haltbarkeit und Sicherheit Ungl cklicherweise sind solche Charakteristika nicht allzu leicht zu messen da es hier nicht immer Standardgr en als Ma stab gibt und das Messen an sich auch Probleme bereitet Bei Software sind die Probleme noch exorbitanter Erstens ist es generell unm glich ein Programm komplett zu testen um seine bereinstimmung mit den funk tionalen Aspekten der Spezifikation zu determinieren Zweitens beinhalten die Anforderungen an Software Eigenschaften wie Verl sslichkeit Effizienz oder Por tierbarkeit Hier tritt auch wieder das Problem auf dass diese extrem schwer zu messen si
106. er nicht fiir die Kommunikation zwischen Real timeThread und NoHeapRealtimeThread m glich Hier muss der Programmierer selbst darauf zu achten oder er sollte diese Konstellation besser vermeiden 3 4 Asynchronous event handling In einer Echtzeit Umgebung muss ein System jederzeit zu unbestimmten Zeiten und mit unbestimmten Fre quenzen oder komplett asynchron auf ein Ereignis reagieren Diese Ereignisse k nnen von einem anderen Prozess oder auch von Au en v a Hardware Interrupt ausgel st werden Deshalb wurden asynchrone Ereig nisbehandlungen eingef hrt In RTJ gibt es 2 Klassen hierf r AsyncEvent steht f r ein Ereignis das ausgel st werden kann Dieses kann beispielsweise ein POSIX Signal ein Hardware Interrupt oder ein berechnetes Ereignis sein Diese werden mittels bindTo mit den externen Ereignisquellen verbunden Bei Eintreten eines der verbundenen Ereignisse startet AsyncEvent die entspre chenden Behandlungsroutinen der zweiten Klasse Objekte der Klasse AsyncEventHandler die vorher be reits mittels addHandler oder setHandler festgelegt wurden lt lt Interface gt gt lt lt Interface gt gt Schedulable gt java lang Runnable Y N N lt lt implements gt gt gt SS AsyncEventHandler BoundAsyncEventHandler Abbildung 5 Vererbungshierarchie von BoundAsyncEvent Diese Ereignisbehandlung kann aber auch k n
107. er ns new PriorityScheduler Scheduler setDefaultScheduler ns MemoryParameters memory new MemoryParameters 60000L 600001 RealtimeThread think new RealtimeThread pp ap boolean b ns setlfFeasible think ap memory if b think start catch Exception e System sOUL printe lind Schedulersanple Exception Scheduler PriorityScheduler Abbildung 2 Vererbungshierarchie von PriorityScheduler Um Priorit ten feiner skalieren zu k nnen wurden 2 weitere Threadtypen eingef hrt bei denen man diese genau definieren kann Zudem k nnen bei diesen Typen auch noch genau die Speicheranforderungen ange geben werden um die neuen Speichertypen zu nutzen siehe Memory Management e NoHeapRealtimeThread Dieser Thread wird mit der h chsten Priorit t ausgef hrt und kann nicht mal durch die Garbage Collection unterbrochen werden Dieser Threadtyp ist al so f r h chst zeitkritische Threads gedacht Damit durch die hohe Priorit t bei Heapzugriff keine Inkonsistenzen entstehen darf in diesen Threads der Heap nicht verwendet werden e RealtimeThread Die Priorit t dieses Thread liegt ber der des normalen java lang Thread und unter den NoHeapRealtimeThread Die genaue Zuordnung wird durch die RealtimePa rameter getroffen lt lt Interface gt gt java lang Thread java lang Runnable A E a _ lt lt imp
108. ert liegen Zum Beispiel die Eingabewerte liegen zwischen 5 lt x lt 6 so entwirft man Testf lle f r die Situation mit 5 6 und 6 7 Wenn die Ein oder Ausgabe eines Programms eine geordnete Menge zum Beispiel lineare Liste oder Tabelle st muss man Testf lle d e aus dem ersten und letzten Elemente der Menge bestehen konstruieren Wenn die Eingabebedingung als Anzahl der Werte spezifiziert wird muss man sowohl das Maximum und das Minimum als die g ltigen Eingabewerte als auch ein weniger und ein hoher als das Minimum und das Maximum als die ung ltigen Eingabewerte entwerfen Zum Beispiel es k nnen von ein bis zu vier Besitzer f r ein Haus registriert wird Man soll Testf lle f r 0 1 Besitzer und 4 5 Besitzer entwerfen Vorteile der Grenzwertanalyse 1 Grenzwertanalyse verbessert die quivalenzklassenbildung denn die Grenzwertanalyse untersucht die Werte an den Grenzen der quivalenzklassen Wir wissen schon dass Fehler h ufiger an den Grenzen von quivalenzklassen zu finden sind als innerhalb dieser Klassen Grenzwertanalyse ist bei richtiger Anwendung eine der nitzlichsten Methoden f r den Testfallentwurf Nachteile der Grenzwertanalyse l Es ist schwierig Rezepte f r die Grenzwertanalyse zu geben denn dieses Verfahren erfordert die Kreativit t vom Tester f r das gegebene Problem Es ist schwierig alle relevanten Grenzwerte zu bestimmen Es werden nur einzelne Ein
109. es Graphen Man verbindet danach Ursache und Wirkung mit den Operatoren aus der booleschen Algebra AND OR NOT 4 Der Graph wird mit Kommentaren versehen die Kombinationen von Ursachen und oder Wirkungen angeben die aufgrund kontextabh ngiger Beschr nkungen nicht m glich sind 5 Der Graph wird in eine Entscheidungstabelle umgesetzt Jede Spalte stellt einen Testfall dar 6 Die Spalten in der Entscheidungstabelle werden in die Testf lle konvertiert Zum besseren Verst ndnis eines Ursache Wirkungs Graphen wird hier ein Beispiel angef hrt Angenommen wir haben eine Spezifikation f r eine Methode die dem Benutzer erlaubt eine Suche nach einem Buchstabe in einer vorhandenen Zeichenkette durchzuf hren Die Spezifikation besagt dass der Benutzer die L nge von Zeichenkette bis zu 80 und den zu suchenden Buchstabe bestimmen kann Wenn der gew nschte Buchstabe in der Zeichenkette erscheint wird seine Position berichtet Wenn der gew nschte Buchstabe nicht in der Zeichenkette erscheint wird eine Meldung nicht gefunden ausgegeben Wenn ein Index verwendet wird der nicht im zul ssigen Bereich liegt wird eine Fehlermeldung out of range ausgegeben Jetzt werden die Ursachen und die Wirkungen anhand der Spezifikation festgelegt Die Ursachen sind C1 Positive Ganzzahl von 1 bis 80 C2 Der zu suchende Buchstabe ist in der Zeichenkette Die Wirkungen sind El Die Ganzzahl ist out of range E2 Die P
110. es Systems gewartet zu werden Als Wartung bezeichnet man die Handlungen die n tig sind um ein System in oder wieder in die f r ihn bestimmten Arbeitsbedingungen zu bringen Diese Anforderung kann auch quantitativ ausgedr ckt werden dann bezeichnet man sie oft als mean time to repair Verl sslichkeit ist die Eigenschaft eines Systems die es rechtfertigt sein Vertrauen in es zu setzen und damit von entscheidener Wichtigkeit f r SkS Sie setzt sich zusammen aus den verschiedenen genannten Anforderungen die je nach System unterschiedlich gewichtet werden 1 3 2 Konflikte zwischen Systemanforderungen Bei der Verwirklichung eines SkS muss abgewogen werden welche der oben aufgef hrten Anforderungen priorisiert wird Es treten unvermeidlich Konflikte zwischen den verschie denen Systemanforderungen auf So erlaubt es ein St rungssicheres System jederzeit in den sicheren Zustand berzugehen Es w re dann sehr sicher seine Verf gbarkeit und Zu verl ssigkeit w rde aber zu w nschen brig lassen Wenn so ein SKS in einer Anlage im plementiert w rde wo jeder Stillstand hohe Kosten verursacht w rde sein wirtschaftlicher Erfolg sicherlich ausbleiben Da die Sicherheit nat rlich nicht vollkommen vernachl ssigt werden darf muss ein akzeptabler Kompromiss gefunden werden 1 3 3 Sicherheitsanforderungen Der Einsatz eines SkS ist selbstverst ndlich nur dann sinnvoll wenn es eine Aufgabe er f llt Diese wird in den Sicherhei
111. ese Unterteilung ist f r die Charakterisierung von Threadverhalten gedacht Denn durch diese Zeittypen kann festgelegt werden in welchem zeitlichen Zusammenhang Threads gestartet werden d h ein Thread soll periodisch aufgerufen werden oder zu einem bestimmten Zeitpunkt oder hnliches Die Timer arbeiten nat rlich auf der Basis dieser genauen Zeit Die Klasse Clock gibt die die Zeitbasis und die Aufl sung der Ticks vor sie wird von jedem Timer ben tigt Es gibt zwei verschiedene Timer zum einen den OneShotTimer und zum anderen den PeriodicTimer Der OneShotTimer l st zu einem bestimmten Zeitpunkt ein AsyncEvent aus und der PeriodicTimer immer in bestimmten Intervallen Beispiel import javax realtime public class OSTimer static boolean stopLooping false public static void main String args AsyncEventHandler handler new AsynckventHandler public void handleAsyncEvent 1 stopLooping true bi OneShotTimer timer new OneShot Timer new RelativeTime 10000 0 handler timer start while stopLooping System OUE PrIine la Running try Thread sleep 1000 catch Exception e System exit 0 Import Javyax reale me public class PTimer public static void main String args AsyncEventHandler handler new AsynckventHandler public void handleAsyncEvent SysteM OUL PEInE IRA tack by PeriodicTimer timer new PeriodicTimer null
112. eters Y V W ProcessingGroupParameters A AperiodicParameters PeriodicParameters N SporadicParameters MemoryParameters Abbildung 1 Schnittstellenbeschreibung von Schedulable Es gibt bereits verschiedene Scheduler Algorithmen die den unterschiedlichen Anforderungen an die Abar beitungsreihenfolge und geschwindigkeit erf llen Deshalb besteht die M glichkeit statt dem Standard Scheduler einen Eigenen mit den gew nschten Merkmalen anzupassen Dieser Standard Scheduler ist fixed priority pre emptive mit mindestens 28 Priorit tsstufen und ist in RTJ die Klasse PriorityScheduler Diese erbt von Scheduler von der alle Scheduler erben m ssen In diesem Zusammenhang meint fixed priority dass dem Thread zur Erstellung die Priorit t fest zugeord net und zur gesamten Laufzeit nicht ver ndert wird Preemptiv hei t dass dem Thread sobald ein laufbe reiter Thread mit h herer Priorit t verf gbar ist der Prozessor entzogen wird und der Thread mit der h heren Priorit t weiter rechnen darf Beispiel 5 public class ThinkExample p blic static void F nf 4 Object o PriorityParameters pp new Prior tyParameters 10 AperiodicParameters ap new AperiodicParameters new RelativeTime 5000L 0 new RelativeTime 5000L 0 null null cLy 4 system out printin ThinkExample PrioritySchedul
113. exity 1 2 System Verification via Model Checking Model checking is a general term for a collection of related formal methods a technique offering the potential to guarantee correct functional behaviour of a system with respect to its specification In the last two decades model checking has emerged as a promising and powerful approach to automatic verification of systems Model Checking has been conceived as an automatic verification technique for finite state systems performing an exhaustive search of the state space of the system in order to determine if some specification is true or not Given sufficient resources the procedure will always terminate with a yes no answer Since subtle errors in the design of safety critical systems that often elude traditional verification techniques can be discovered in this way and since it has proven to be cost efficient Model Checking is being adopted as a standard procedure for the quality assurance of reactive systems Just like deductive method the model checking is also logic based But contrary to deductive method the main advantage of model checking is that at least for finite state systems it can be performed fully automatically and efficiently That means an enormous facilitation of work and saving of time This is why now Model Checking is used by many companies such like Intel IBM Microsoft Siemens 2 The Process of Model Checking The Process of Model Checking can be separated int
114. f r die Grenzwertanalyse 2 quivalenzklassenbildung ist ein geeignetes Verfahren um aus Spezifikationen repr sentative Testf lle abzuleiten Nachteile von der Aquivalenzklassenbildung l Es werden nur einzelne Eingaben betrachtet Beziehungen Wechselwirkungen zwischen Werten werden nicht behandelt 3 2 Grenzwertanalyse Boundary Value Analysis Grenzwertanalyse ist auf der Aquivalenzklassenbildung basierend denn Grenzwertanalyse benutzt Testdaten von Aquivalenzklassen welche nur die Werte an den R ndern ber cksichtigt Erfahrungen haben gezeigt dass viele Fehler in der N he von R ndern stecken deswegen wird dieses Verfahren sehr oft benutzt um die Fehler an den R ndern zu entdecken Das Bild zeigt den Unterschied zwischen Grenzwertanalyse und Aquivalenzklassenbildung Grenzwertanalyse Grenzwertanalyse Wir betrachten das erste Beispiel COPYRIGHT 1994 by George E Thaller All rights reserved Function Black Box Grenzwerte Testprogramm me include lt stdio h gt main inti n wd day month year printf n TESTFALL TAG MONAT JAHR WOCHENTAG year 1994 n 1l for 1 3 1 lt n i f 1 3 day 1 month 1 1f 1 4 day 31 month 12 if 1 5 day 0 month 1 if i 6 day 32 month if i 7 day 7 month 0 if 1 8 day 7 month 13 wd week_d day month year printf 2d 2d 2ld Ad ld n I day month year wd I
115. ffy die zeitliche Aufl sung der Kernels Listing 1 Pseudo Code fur die Linux Timer Interrupt Service Routine void timer_interrupt jiffies 4 run_timer_list update_process_times schedule_process Listing 1 zeigt den Pseudo Code fiir die Linux Timer Interrupt Service Routine TISR In dieser wird zuerst die Variable jiffies inkrementiert Das Z hlen der jiffies ergibt die Softwareuhr Danach wird der Kopf der Timerliste nach f lligen Timern durchsucht und diese werden ausgef hrt Danach werden einige andere Daten aktualisiert und zuletzt wird ein Prozess ausgew hlt dem nach der TISR Rechenzeit zugewiesen wird Man erkennt da der Timerinterrupt alle 10ms einerseits der Herzschlag heartbeat des Systems ist und da Timer eine maximale Aufl sung von 10ms haben Dies reicht f r Echtzeitsystem nicht aus Der erste naive Ansatz w re also die Aufl sung zu erh hen und somit die Periode des Timerinterrupts k rzer zu w hlen Sinnvoll f r ein Echtzeitsystem w re eine Aufl sung von lus Dies hat jedoch die negative Auswirkungen Der Kernel mu 10000 mal fter die TISR durchlaufen was einen nicht mehr zu vertretenden Overhead produzieren w rde bzw die TISR w rde immer wieder durchlaufen wenn sie l nger als 1us dauert Es mu m glich sein da Timer genau auf die Mikrosekunde geplant werden k nnen wobei jedoch nicht zwin gend jede Mikrosekunde ein Timer vorhanden ist Also mu auch nicht zwingend jede Mikrose
116. finierte Zeit anstehen muss bevor er registriert wird Damit unterdr ckt man wirkungsvoll kurzzeitige Fehler Wiederholte Berechnungen mit anschlie endem Er gebnisvergleich geh ren auch zu dieser Kategorie 2 Der Stromausfall am 14 August 2003 in den USA 2 1 Einleitung In einigen Gebieten an der Ostk ste der USA unter anderem in New York Detroit und in Kanada wo vor allem Ottawa und Toronto betroffen waren fiel am 14 August 2003 nachmittags New Yorker Ortszeit der Strom weitr umig aus Acht Staaten im Nordos ten der USA und Teile Kanadas mussten bis zu f nf Tage lang ohne elektrische Energie auskommen dabei waren an die 50 Millionen Menschen betroffen Insgesamt wurde ein Beispielsweise ein System bestehend aus einfachen Relais und Sensoren die fest miteinander verdrahtet sind Schaden von sch tzungsweise 6 Mrd US verursacht alleine 1 Mrd davon in New York Meldung Heise Schaden ZDF Am Ende der Kettenreaktion die zu dem Ausfall f hr te fehlte eine Leistung von 61 Gigawatt in den Netzen der Stromversorger Leistung ZDF Wie im offiziellen Untersuchungsbericht Report US Canada Taskforce berichtet fielen insgesamt 265 Kraftwerke aus 2 2 Gr nde Im Untersuchungsbericht werden vier Gr nde f r den Zusammenbruch des Stromnetzes genannt Der Zusammenbruch begann in Ohio in einer Kontrollgebiet dass von der Firma First Energy einem Zusammenschluss von mehreren Stromversorgern betrieben wurde F r d
117. gaben betrachtet Beziehungen und Wechselwirkungen zwischen Werten werden nicht behandelt 3 3 Test spezieller Werte Error Guessing Das Error Guessing ist im eigentlichen Sinne keine Testmethode sondern dient zur Erweiterung und Optimierung von Testf llen Diese Methode beruht auf der Erfahrung und dem Wissen des Testers und muss nicht von der Spezifikation abgeleitet werden Aufgrund seiner langj hr gen T tigkeit als Tester oder Programmierer kennt dieser zum Beispiel die h ufig aufgetretenen Fehler Bei dieser Methode ist es schwierig die Vorgehensweise anzugeben da es ein intuitiver Prozess ist Prinzipiell legt man eine Liste m glicher Fehler oder fehleranf lliger Situationen an und definiert damit die neuen Testf lle Beispiele f r Error Guessing 1 Der Wert 0 als Eingabewert zeigt oft eine fehleranf llige Situation 2 Bei der Eingabe von Zeichenketten sind Sonderzeichen besonders sorgf ltig zu betrachten 3 Bei der Tabellenverarbeitung stellen kein Eintrag und ein Eintrag oft Sonderf lle dar 3 4 Ursache Wirkungs Graph Verbesserung von quivalenzklassen und Grenzwertanalyse quivalenzklassenbildung und Grenzwertanalyse haben eine gemeinsame Schw che s e k nnen keine Kombination von Eingabebedingung berpr fen Diese Schw che wird durch den Ursache Wirkungs Graph behoben Ein Ursache Wirkungs Graph ist eine formale Sprache in die eine Spezifikation aus der nat rlichen Sprache bersetzt wird De
118. ge quivalenzklassen m lt l und m gt 12 Es werden eine g ltige Aquivalenzklasse und zwei ung ltige Aquivalenzklassen f r den Tag gebildet Eine g ltige Aquivalenzklasse lt t lt 31 Zwei ung ltige Aquivalenzklasse t lt l undt gt 31 Beim Jahr haben wir aus der Sicht des Black Box Tests erst keine Kriterien um ein bestimmtes Jahr auszuw hlen Wir betrachten nun das zweite Beispiel Spezifikation zur Ableitung des technischen Eintrittsalters einer Person in einen Versicherungsvertrag Eingabe vertragsbeginn geburtsdatum Hilsvariable diff_Monat Monat vertragsbeginn Monat geburtsdatum diff_Jahr Jahr vertragsbeginn Jahr geburtsdatum technisches_Eintrittsalter Bedingung Fehler vertragsbeginn lt geburtsdatum diff_Jahr vertragsbeginn gt geburtsdatum und 5 lt diff Monat lt 6 diff_Jahr 1 vertragsbeginn gt geburtsdatum und diff Monat gt 6 diff_Jahr 1 vertragsbeginn gt geburtsdatum und diff Monat lt 5 Testfall Ausgew hltes Testdatum Aquivalenzklasse Geburts Vertrags Ausgabe datum beginn soll TI 1 Vertragsbeginn er 02 2001 01 01 2001 Fehler vor Geburtsdatum T2 2 diff_Monat im Poa PR 06 1975 01 08 2001 26 Interval 5 6 T3 3 diff Monat gt 6 diff Jahr 1 01 05 1975 01 12 2001 27 T4 4 diff Monat lt 5 diff Jahr 1 01 10 1975 01 01 2001 25 Klasse 1 ist eine Klasse ung ltiger Werte Weitere ung ltige Klassen sind Tag
119. gkeit von Software auf ihrem Anwendungsniveau unter festgelegten Bedingungen innerhalb einer festgelegten Zeit aufrecht erhalten werden kann Brauchbarkeit Attribute die den Aufwand der Anwendung sowie die individuelle Auswertung eines solchen Nutzens unter festgelegten Bedin gungen beschreiben Effizienz Attribute die die Leistungsf higkeit von Software und deren benutzte Ressourcen unter festgelegten Bedingungen vergleichen Haltbarkeit Attribute die den Aufwand einer durchzuf hrenden Anpas sung beschreiben Portierbarkeit Attribute die die bertragbarkeit von Software von einer Plattform auf eine andere Plattform beschreiben 1 5 3 Sonstige Standards Nach der Ausf hrung dieser beiden wichtigen Standards seien hier noch zur Kom plettierung ein paar weitere Standards aus dem zivilen und milit rischen Sektor genannt e Zivile Standards ANSI IEEE Standard 730 1989 Software Quality Assurance Plans 6 ASME Standard NQA 2a Quality Assurance Requirements for Nuclear Facility Applications T e Milit rische Standards International Electrotechnical Commission Genf Schweiz Department of Defence Standard 2168 Defense System Software Qua lity Program 8 Ministry of Defence Defence Standard 00 16 Guide to the Achievement of Quality in Software 9 NATO Quality Standard AQAP 150 Requirements for Quality Mana gement of Software Development 10 2 Zertifizie
120. gte nur zus tzlichen Stress Die erste Version der internen Software war viel zu empfindlich und zeigte einige interessante Probleme So wurden beispielsweise Transponder auf Br cken und Schiffe als Alarme gemeldet oder es wurde vor dem eigenen Flugzeug gewarnt Da Testfl ge sehr teuer sind und ein Testen unter reellen Bedingungen sehr schwierig zu simulieren war wurden die Logik letztlich 16 Als Eindringling wird allgemein das jeweils andere Flugzeug bezeichnet mittels aufgezeichneter Radardaten verfeinert caasd Nach mehreren Revisionen wurde dann aber eine hohe Reduktion der Fehlalarme erreicht Mittlerweile sehen die Piloten das System als verl sslich an unter anderen ist die Befolgung von Ausweichempfehlungen bei allen groBen Fluggesellschaften fiir sie Pflicht Durch die gro e Reichweite von TCAS neuere Versionen erreichen bis zu 60 NM wer den st ndig Objekte angezeigt die berhaupt keine Bedrohung darstellen Dadurch wird die Aufmerksamkeitsschwelle des Pilotens f r das System gesenkt Die hohen Geschwin digkeiten in der Luftfahrt erlauben es aber nicht die Reichweite zu senken da ansonsten die Zeit f r eine Reaktion nicht mehr ausreichen w rde 3 3 Gr nde Die BFU hat sich eingehend mit dem Unfallverlauf befasst In ihrem vorl ufigen Unter suchungsbericht Untersuchungsbericht BFU stellt sie den Verlauf des Ungl cks detailiert dar Es stellte sich heraus dass eine Verkettung unterschiedlicher teilweise
121. he SMV language and uses an OBDD based search algorithm to determine whether the system satisfies its specification The same as most of the model checking systems if it determines that a certain property has not been satisfied 1t will produce the counterexample proving the invalidity of the specification Symbolic Model Checking derives its power from efficient data structures for representation and manipulation of large sets of states By using the original CTL model checking algorithm of Clarke and Emerson with the new representation for state transition graphs t became possible to verify some examples that had more than 10420 states Since then various refinements of the OBDD based techniques by other researchers have pushed the state count up to more than 104120 The SMV system has been widely distributed and a large number of examples have now been verified with it Some examples provide convincing evidence that SMV can be used to debug real industrial designs In 1992 Clarke and his students used SMV to verify the IEEE Future cache coherence protocol They found a number of previously undetected errors in the design In 1992 Dill and his students found several errors ranging from initialized variables to subtle logical errors during the verification of the cache coherence protocol of the IEEE Scalable Coherent Interface 3 3 Alternative Methods Symbolic representations and partial order reduction have greatly increased the size of th
122. he first of these local properties using only the transmitter and the network the second using only the network and the third using only the network and the receiver By decomposing the verification in this way we never have to compose all of the processes and therefore avoid the state explosion phenomenon When this form of compositional reasoning is not feasible because of mutual dependencies between the components a more complex strategy is necessary In such cases when verifying a property of one component we must make assumptions about the behaviours of the other components The assumptions must later be discharged when the correctness of the other components is established This strategy is called assume guarantee reasoning 3 3 3 Abstraction Abstract interpretation 1s a technique to reduce the increase of the state space due to date by providing a mapping between the concrete date values in the system and a small set of abstract data values that suffices to check the properties of interest The abstract system 1s often much smaller than the actual system and as a result it is usually much simpler to verify properties at the abstract level For example in verifying the addition operation of a microprocessor we might require that the value in one register is eventually equal to the sum of the values in two other registers In such situations abstraction can be used to reduce the complexity of model checking There are two different ab
123. herneltskrilischer Syse men aaa 4 2 1 Alleemeine Antorderunsen an SKS ana aa a u RM EG 4 2 2 Allgemeine Anforderungen an eine Programmiersprache nach Carre 5 2 3 Probleme gew hnlicher Programmiersprachen nach Clutterbuck 0 5 2 4 Charakteristische Merkmale einer Prog sprache nach Cullyer u 0 5 2 5 Anforderungskatalog an eine Programmiersprache f r SkKS oocccncconnncnoccnnnnononnnnncnnnnos 6 3 Umsetzung der 55 Merkmale 1 Ada tad an 3 1 Allgemeine Merkmale von Ada a a 3 2 Reliabikiy Funktions imie ke een 3 2 1Lesichere Dale Paila 3 2 2 Wilkin iche Sprunpe wild Jump Sasse ec 3 2 3 berschreibung overwrites ucanneaaneeaneenneennennnesnneenneennennnennnennnennnennenneennennnnn 3 3 Avallabiliy Verlusbarkei names u 3 3 1 logische G ltigkeit logical soundness 0 2 0 0 cece cece cece a eececeeeceeaeeeeeseeeeeeaaeceeeeeeeeas 3 5 2 Initialisierunsstehletfiniti ahlisinge Tar a u dence 3 3 3 Ausdrucksauswertungsfehler expression evaluation error 3 4 Perlormance ES en AN 39 Zuverl ssiekeit Dependability anne u cae esezvumaetes 3 3 1 Mehrtlache Rererenzen alas een ec aie 3 5 2 Seiteneffekte durch Unterprogramme subprogram side effects 3 5 3 Speicher berwachung exhaustion of memory oocccoocccnnnoncnnnonccnnnnnnnnnonccnnnanicanonoss 3 6 Understandability Verst ndlichkelit
124. hler die bei anderen Programmiersprachen zu extremem Testaufwand f hren bei Ada schon w hrend der Kompilierzeit entdeckt werden Weiterhin wird die Software Revision durch einige Annexe unterst tzt Das Pragma Reviewable veranlasst die Darstellung des erzeugten Maschinencode sowie der Abbildung der Datenobjekte Es wird auch die Lebensdauer der Objekte die Art und Umfang der generierten Laufzeit berpr fungen und der Umfang des Laufzeitsystems selbst analysiert Das Pragma Inspection_Point legt die Wertzuordnung der betroffenen Objekte offen 3 Recoverabilit iederherstellbar eit Ada besitzt einen ausgekl gelten Mechanismus zur Ausl sung und Behandlung von Laufzeitfehlern exception handling man spricht allgemein von Ausnahmen Im Ada Laufzeitsystem sind einige Ausnahmesituationen vordefiniert die alle die m glichen Laufzeitfehler abdecken die sich rein aus der Semantik der Sprachdefinition ergeben Eine Ausnahmenbehandlung ist f r alle Ablaufstrukturen die in Ada vorgesehen sind m glich und sie bezieht sich auf die jeweilige Prozedur Funktion oder einen Anweisungsblock Im Zusammenhang mit der Ausf hrung spricht man allgemein auch von Rahmen die w hrend der Ausf hrung nach dem LIFO Prinzip eine Kette bilden Tritt der Kontrollfluss in einen Block ein oder es wird eine Prozedur aufgerufen so wird ein neuer untergeordneter Rahmen erzeugt Dieser wird beim verlassen der Prozedur oder des Blocks wieder entfernt Falls
125. ieren e Fliegende Objekte e Verletzungen 3 Entgleisung des Shuttles e Sperrung und Besch digung der Strecke e Personensch den 4 Zusammensto durch zu starke Neigung mit Gegenst nden e Personenschaden e Blockierung und Besch digung der Strecke 4 3 Techniken der Analyse Die Techniken der Hazard Analyse existieren in verschiedenen Formen Jede Technik bietet eine andere Einsicht in die Eigenschaften des Systems Manche Methoden finden ihre Anwendung in bestimmter Situation und erreichen eine Grenze bei ihrer Nutzung in anderen Bereichen Dabe kann man die Vielzahl dieser Technik in zwei Typen unterteilen Vorwarts und R ckw rts Suche und Top down und Bottom up Suche Die Bezeichnungen der Typen die n die n chsten Abschnitte tiefer betrachtet werden sagen schon viel ber deren Arbeitsstrategie um die Gefahren zu analys eren 4 3 1 Vorw rts und R ckw rts Suche Abbildung 5 Vorwarts und Ruckwarts Suche 1 Bei der Vorw rts Suche f ngt man immer bei einem Ereignis an und versucht die m glichen Folgen zu erwarten Man nennt das auch induktive Suche weil die Tatigkeit zeitlich nach vorn gerichtet wird Nun be der R ckw rts Suche geht man von einem gef hrlichen Zustand aus und versucht herauszufinden was die Ursache f r diesen Zustand ist Diese Methode wird als deduktive Suche bezeichnet Zeitlich gesehen im Gegensatz zur Vorw rts Suche wird nach hinten geschaut 2 FTA Fault tree analysis
126. initionen o ciar HF Bees dee ee SOR Ree a 1 1 1 Was sind Sicherheitskritische Systeme 1 1 2 DAN VSeOCCUTILY area weet a ragt A LS Was Ist Sicherheit 524 23 eu eae ho m 1 14 Formen von SKS 6 ito 44 dk Eee eher 1 1 5 Unterscheidung Hochintegrierte Systeme SkS 1 25 Riike gy bs a a as ae a es Lio Sicherheitskritetien abra SA a 0 Mok Bak ni an ei 1 3 1 Systemanforderungen 2 2 CE Emmen 1 3 2 Konflikte zwischen Systemanforderungen 1 3 3 Sicherheitsanforderungen 2 222 2222 nennen PR A O pa ate fe ds nn Se 1 4 1 Fehler Fehlfunktion und Systemausfall 2 222 1 4 2 Unterscheidung ber die Fehlerart 1 4 3 Unterscheidung ber die Fehlerdauer 1 4 4 Sonstige Unterscheidungen 0 1 5 Behlervermieidun 222 2 64 2 24 2 A EN 824 44 1 6 Eehlerbehebun mad a e a ua ne de E7 Echlerkennuns 28 os Kiew an ne Wie ee a aA WO Pehlettoleranz nr a a ee a amp ra aa A 2 Der Stromausfall am 14 August 2003 in den USA AL Einleitung sd e hk 8 a u a A We ae id UMSS dea E onde bs eS OR ae ek os RS de Be Be 2 2 1 Mangelhaftes Systemverst ndnis und berlastung des Netzes 2 2 2 Ungenigendes Situationsbewusstsein und technische Proble Meppel BE 3 5 2 4 AAA re Se ee Rte A 2 2 3 Unzureichendes Beschneiden der B ume 2 2 4 Falsche oder keine Echtzeit berwachungsdaten und mangel hatte Zusammenarbeit s lt acc 82 24 Ks sh sw
127. interrupts aktualisiert Dabei stellte sich heraus da die Softwareuhr noch recht ungenau l uft Diese Implementierung wurde ge ndert und es wird nun beim Booten ein Referenzwert des TSC und der Uhr gespeichert Die Softwareuhr wird anhand der Differenz zwischen dem TSC Wert zu einem Interrupt und dem Referenzwert aktualisiert Dadurch wird die Softwareuhr wesentlich genauer Die Funktione time_to_next_event berechnet den Zeitpunkt an dem der nachste Timerinterrupt auftreten muB und mit program_timer_chip wird dieser Zeitpunkt in den TIB programmiert Danach wird wie gehabt die Timerliste nach abgelaufenen Timern durchsucht und diese werden ausgef hrt Anschlie end wird nur bei Uberschrei ten einer Zeitscheibengrenze die Methoden f r den Heartbeat des Systems ausgef hrt Damit der Heartbeat nicht verloren geht wenn keine Timer vorhanden sind wird mindestens einmal pro Jiffy ein Pseudo Timer programmiert W rde dies nicht gemacht so ist z B vom Multitasking nicht mehr viel zu sp ren weil die Prozesse zu langsam gewechselt werden Die erste Implementierung sah eine Neuprogrammierung des TIB bei jedem Lauf der TISR vor Die wurde dahinge hend verbessert da der TIB nur dann neu programmiert wird wenn der n chste Timer nicht kurz auf den aktuellen folgt sondern es wird einfach der entsprechende Zeitraum mit Hilfe des TSC gewartet 3 2 2 Leistungsf higkeit von UTIME Die Leistungsf higkeit von UTIME zeigen die drei folgenden Messu
128. ird ausgef hrt In diesem Fall wird currentDose auf Null gesetzt Seine Nachbedingung lautet currentDose 0 3 Der else f Zweig der if Anweisung 2 wird ausgef hrt In diesem Fall wird currentDose auf maxDose gesetzt Die Nachbedingung lautet currentDose maxDose Uberdosis verabreicht administerinsulin CurrentDose gt maxDose Widerspruch Widerspruch Widerspruck CurrentD ose max Dose CurrentDose 0 currentDose gt minimum Dose und currentDose lt max Dose then Zweig else Zweig der 1f der 1f if Anweisung 2 Anweisung 2 Anweisung 2 ausgef hrt ausgef hrt nicht ausgef hrt In jedem der drei F lle widersprechen die Nachbedingungen der unsicheren Vorbedingung d h das System ist sicher 5 Black Box Test gegen White Box Test Wir haben schon gesehen wie man mit Black Box und White Box Verfahren das Programm testen kann Wir haben damit die Qualit t der Software erh ht weil einige Fehler beim Testen entdeckt werden Wir werden jetzt die Vorteile und die Nachteile von Black Box Test und White Box Test genauer betrachten Welches Verfahren ist besser Die Vorteile von Black Box Test l Der Tester muss d e Implementierung oder den Quellcode nicht kennen 2 Die Vorgehensweise ist einfacher als White Box Test 3 Der Tester macht n cht denselben Fehler w e der Implementierende Die Nachteile von Black Box Test 1 Man we nicht ob jeder Zweig durchlaufen
129. ising failures Auswertungsfehler expression evaluation errors 3 Performance Leistung Zeit Speicher Bedarf bounded space and time requirements 4 uverlassig eit Dependabilit Seiteneffekte durch Unterprogramme subprrogram side effects Speicheruberwachung exhaustion of memory Mehrfache Referenzen aliasing 5 Understandabilit Verstandlich eit einfache Definitionen simple Definitions Ausdruckstarker Code expressive power 6 Testabilit Testbar eit Verifiabilit Verifizierbar eit eindeutige Semantik semantics strenges mathematisches Modell model of maths Recoverabilit iederherstellbar eit arithmetische Laufzeit berwachung operational arithmetic Ausnahmenbehandlung exception handling Maintainabilit artbar eit Extendabilit Er eiterbar eit iederver endbar eit separate Paket bersetzung separate compilation sicheres subset safe subset Zus tzlich muss eine Programmiersprache Werkzeuge zur Verf gung stellen die den Entwicklern z B Verwaltungsarbeit abnehmen und ihn sonst mit hilfreichen features zur Seite stehen Eine gro e Nutzergemeinschaft ist ebenfalls von essentieller Bedeutung zur einen werden Fehler in der Entwicklungsumgebung haupts chlich in den Compilern eher entdeckt und beseitigt Zum anderen wird durch Erfahrungsaustausch ein Expertenwissen aufgebaut der gute Code liefert 3 Umsetzung der S S Mer male in Ada Im folgenden werden die ei
130. it Sicherheit ist da bei als eine Systemeigenschaft anzusehen daher haben alle Systembestandteile Hardware Software und Benutzer ihren Einfluss darauf Nach dieser einleitenden Definition von Sicherheit ist es nun m glich sicherheits kritische Systeme einzuordnen und abzugrenzen 1 2 2 Sicherheitskritische Systeme Ein sicherheitskritisches System l sst sich als ein System charakterisieren bei dessen inkorrekter Funktion Versagen es zu ernsthaften Konsequenzen T tung von Personen schweren Verletzungen schwerwiegenden Umweltsch den oder er heblichen Geldbu en kommen kann Diese etwas allgemeiner gehaltene Beschreibung l sst allerdings noch einen ge wissen Freiraum brig So k nnte man vier Unterarten von sicherheitskritischen Systemen bilden die zu unterschiedlichen Konsequenzen f hren e Lebens kritische Systeme e Missions kritische Systeme e Umwelt kritische Systeme e Kosten kritische Systeme Im Zusammenhang mit Qualit tsmanagement und Zertifizierung sind die ez akten Konsequenzen eines Systems allerdings nicht von so gro er Bedeutung daher reicht der Begriff sicherheitskritisch vollkommen aus Diese Definition grenzt zugleich die sicherheitskritischen Systeme weit genug ein denn Folgen wie unbefugte Einsicht Modifizierung oder L schung von Daten sind nicht unter den oben aufgef hrten Punkten zu finden Somit wird die Deckungs gleichheit mit dem zuvor gepr gten Sicherheitsbegriff gew hrleistet
131. it t und das Not Shutdown das keine Funktionalit t gew hrleistet da das System einfach heruntergefahren wird Die Alternative zu Fallback Zustande ist das Ausstatten des System mit extrem sicheren Hazard Detektoren 6 Beispiel aus dem Neigemodul des Shuttles Fallback Einrichtung von geeigneten Fallback Ebenen Zentralsoftware hat kurze Modulwege zu verschiedenen Fallback Ebenen 6 4 Damage minimization Ziel dieses Abschnitts ist das Reduzieren des Schaden nach einem Unfall wenn das passieren sollte denn das System an sich und somit auch die Software nichts mehr machen kann Es muss also ein point of no return definiert werden Dieser bestimmt ab wann ein Hazard unausweichlich ist 6 Beispiel aus dem Neigemodul des Shuttles a Extra Verstarkung des Chassis b Nicht bzw schwer entflammbare Materialien c Schnelle Vororthilfe 7 Zusammenfassung Bei sicherheitskritischen Systemen spielt die Hazard und Risikoanalyse eine schwerwiegende Rolle sie ist unumg nglich f r die Entwicklung des Systems Diese Analyse muss so gut wie m glich gemacht werden weil das Ergebnis unter Ber cksichtigung f r den Entwurf genommen wird Gem der Erfahrung hat sich gezeigt dass Fehler bei der Hazard Analyse und bei dem Design die nur nach der Entwicklung des Systems entdeckt werden sehr gro er Aufwand verursachen k nnen Das ist der Grund warum alles sehr genommen werden muss Aus dem Beispiel wird erkannt dass geeignete Ma
132. itpunkt die daf r notwendigen Aktionen ausf hren also bespielsweise ohne Verz gerung auf Interrupts reagieren Dazu mu ein laufender Proze nat rlich unter brochen werden Maximaler Durchsatz Darunter versteht man da so viel Programm wie m glich innerhalb eines gewissen Zeit raumes abgearbeitet werden soll Denn aufwendige Berechnungen sollen so schnell wie m glich abgeschlossen sein Minimale Antwortzeit Die Antwortzeiten des Systems sollen kurz sein denn der Anwender erwartet nach dem Bewegen der Maus oder nach einem Tastendruck sofort eine Reaktion auf dem Bildschirm Effizientes Scheduling Das Wechseln von Prozessen mu einerseits schnell gehen und andererseits mu die Zuteilung von Rechenzeit entsprechend den Erwartungen des Anwenders sein Der Scheduler mu also einen genauen berblick ber bisher vergebene Rechenzeit schnell berechnen um damit m glichst genau vorherzusagen welcher Proze weiterhin viel Rechenzeit ben tigen wird Dazu geh rt auch da Prozesse so h ufig gewechselt werden m ssen da der Schein der Nebenl ufigkeit gewahrt bleibt Dabei f llt auf da die Optimierung hinsichtlich der obigen Kriterien bereits schon nicht m glich ist weil sie sich bei der Realisierung widersprechen H ufiges Wechseln von Prozessen zieht einen gewissen Overhead im Be triebssystem nach sich wodurch der Durchsatz bereits nicht mehr maximal ist Linux wurde ebenfalls anhand der obigen Kriterien optimiert und erf ll
133. keit e Maintainability Wartbarkeit e Extendability Erweiterbarkeit e Portierbarkeit itii Wiederverwendbarkeit 4 3 2 Sicherheitsanforderungen Das System muss auch systemspezifische Sicherheitsanforderungen die mit der Funktion und Eigenschaften des Systems verbunden sind erfullen Um dies zu erreichen wird eine Reihe von Aufgaben geleistet Die Hauptstufen des Prozesses werden wie folgt gegliedert Identifikation der m t dem System verbundenen Gefahren durch Gefahrenanalyse Klassifizierung der Gefahren nach hrer Schwere Ermittlung von Methode um diese Gefahren zu mindern bzw ganz auszuschlie en Zuordnung geeigneter Reliability und Availability Anforderungen zu diesen Methoden Ermittlung eines geeigneten Safety Integrity Level und die dazu passende Methode ausw hlen Der Safety Integrity Level ist die Wahrscheinlichkeit dass das sicherheitsrelevante System zufrieden stellend die erforderlichen Sicherheitsfunktionen unter allen festgesetzten Bedingungen Zust nden innerhalb einer Zeitperiode durchgef hrt 4 Hazard Analyse Fast jeden Tag haben wir mit Maschinen zu tun denen wir blind unser Leben anvertrauen Es kann zu Hause in der Stra e oder am Arbeitsplatz sein Wir stellen uns selten Fragen uber ihre Sicherheit und Zuverlassigkeit weil es uns klar scheint dass die Menschen die diese Maschinen gebaut haben an alles ausgedacht haben Zum Beispiel fliegen wir in den Urlaub ohne uns viele Ged
134. kumentierte Projekt so da sich anhand dieses Projektes die notwendigen nderungen am Linux Kernel am besten aufzeigen lassen 3 2 KURT KURT wurde in 1998 auf dem Entwicklungskernel mit der Version 2 1 entwickelt und erfuhr in der Version 1 x noch einige Verbesserungen Im Dezember 1999 wurde der Patch f r die Kernel 2 2 5 2 2 9 und 2 2 13 bereitgestellt wobei KURT die Version 2 0 bekam Im November 2001 wurde die Portierung auf den Kernel 2 4 fertiggestellt Die zugrundeliegende Architektur wurde seit der Version 1 0 nicht ver ndert wobei diese in zwei Schritten en twickelt wurde Sie wird im folgenden vorgestellt 3 2 1 Verfeinerung der zeitlichen Aufl sung mit UTIME Die zeitliche Planung wird unter Linux mit Hilfe von Timern realisiert F r jeden Timer wird eine Struktur angelegt die den Zeitpunkt der F lligkeit des Timers und den dazu geh rigen Funktionspointer enth lt Alle Timer werden in einer doppelt verketteten Liste gespeichert wobei die Liste nach dem Zeitpunkt sortiert ist Dies hat zur Folge da das Einf gen von Timer die Komplexit t O n besitzt Fallige Timer k nnen jedoch in 0 1 gefunden werden da sich diese am Anfang der Liste befinden Die kleinste Zeiteinheit im Linuxkern betr gt auf x86 kompatiblen Prozessoren 10ms Diese Zeiteinheit wird als Jiffy bezeichnet Der Timerinterruptbaustein ist unter Linux so programmiert da er genau einmal pro jiffy einen Timerinterrupt ausl st Somit bestimmt der ji
135. kunde ein Timerinter rupt auftreten Dies wird von UTIME dadurch erreicht da der feste Timerinterrupt alle 10ms abgeschaltet wird Stattdessen wird der Timerinterruptbaustein TIB im sogenannten One Shot Modus betrieben Es wird genau der Zeitpunkt anhand der Timerliste berechnet wann der n chste Timerinterrupt auftreten mu und dieser wird dann im TIB programmiert Dies hat zur Folge da die Softwareuhr nicht mehr funktioniert und die Aufl sung der Variablen jiffies nicht mehr ausreicht Die Variable jiffies bekommt deshalb noch die Variable jiffies_u f r die Mikrosekunden in nerhalb eines jiffy und die Variable jiffies_intr f r das berschreiten einer Zeitscheibengrenze beiseite gestellt Zur Aktualisierung der Softwareuhr wird als erstes die Methode update_time innerhalb der neuen TISR Listing ausgef hrt Diese nutzt den Time Stamp Counter TSC der CPU welcher einmal pro Takt inkrementiert wird um die Variable jiffies_u zu aktualisieren berschreitet jiffies_u die L nge einer Zeitscheibe wird jiffies inkrementiert und jiffies_intr gesetzt Listing 2 Pseudo Code f r die UTIME Linux Timer Interrupt Service Routine void timer_interrupt update_time t time_to_next_event program_timer_chip t run_timer_list if jiffies_intr update_process_times schedule_process jiffies_intr 0 In der ersten Implementierung wurde die Softwareuhr anhand der Differenz des TSC Wertes zwischen zwei Timer
136. l Organization for Standardization ISO http www iso ch 2 Storey Neil Safety critical computer systems Harlow England 1996 Verlag Prentice Hall 3 Bennett S Real time Computer Control An Introduction 1994 Verlag Prentice Hall 4 Wikipedia Six Sigma http en wikipedia org wiki Six_Sigma Stand 30 03 2004 5 About ISO http www iso ch iso en prods services otherpubs pdf inbrief2002 en pdf Stand 26 03 2004 61 ANSI IEEE Standard 730 1989 Software Quality Assurance Plans New York 1989 Institute of Electrical and Electronic Engineers 7 ASME Standard NQA 2a Quality Assurance Requirements for Nuclear Facility Applications New York 1990 The American Society of Mechanical Engineers 8 Department of Defence Standard 2168 Defense System Software Quality Program Washington DC 1988 Department of Defence 9 Ministry of Defence Defence Standard 00 16 Guide to the Achievement of Quality in Software Glasgow 1984 Directorate of Standardization 10 NATO Quality Standard AQAP 150 Requirements for Quality Management of Software Development NATO International Staff Defence Support Division 1993 111 ESA PSS 05 0 Software Engineering Standards Paris 1991 European Space Agency 112 HSE Guidelines Programmable Electronic Systems in Safety Related Applications Vol 1 amp 2 London 1987 Her Majesty s Stationary Office 13 IEC International Standard 880 Software for Computers in the Safety S
137. lagene potentiell gef hrli che System eine akzeptable Sicherheit aufweist Des Weiteren beschreibt der Safety Case alle Risiken die bei der Nutzung des Systems auftreten k nnen sowie die m glichen Gefahren beim Versagen des Sy stems Weiterhin wird beschrieben was getan werden kann um die Wahrschein lichkeit des Auftretens eines Fehlers zu minimieren Der Safety Case dokumen tiert die Sicherheit des Systems w hrend seines gesamten Lebenszyklus Um den Safety Case auszuarbeiten bedarf es in der Regel eines enormen Zeit und Arbeitsaufwandes 2 4 2 Zweck des Safety Case Einer der wichtigsten Nutzen des Safety Case ist die Unterst tzung der Zerti fizierung da der Zertifizierer nach Beweisen suchen wird dass alle potentiellen Gefahren identifiziert und entsprechende Schritte veranlasst wurden um diese zu behandeln Genau diese Beweise liefert der Safety Case Ebenso liefert er die ben tigten Argumente die aufzeigen dass angemessene Entwicklungs und Testmethoden eingesetzt wurden Allgemein hilft der Safety Case bei der Minimierung des Projektrisikos denn po tentielle Schwachstellen k nnen so schon in einer fr hen Projektphase erkannt werden 2 4 3 Probleme bei der Entwicklung Die meisten Safety Cases werden mit Hilfe von einfachen Werkzeugen entwickelt verlassen sich aber auf manuelle Pr fungen um ihre Konsistenz und Vollst ndig keit zu versichern Das gr te Problem bei der Entwicklu
138. lem that not only appears for model checking but also for various other problems like performance analysis that are strongly based on state space exploration N co gt N q O ES 5 Z AS 6 T 8 Number of processes Figure State Explosion Problem Model Checking is increasingly used in the formal verification of hardware and software For concurrent system with small numbers of processes the number of states was usually fairly small and the approach was often quite practical In systems with many concurrent parts however the number of states in the global state transition graph was too large to handle See the figure Number of states typically grows exponentially in the number of process Much work over the past 10 15 years has gone into overcoming state space explosion Let us see some of the major techniques for tackling this problem 3 1 Based on Automata Theory 3 1 1 On the Fly Technology Explicit state model checking uses a graph to represent a Kripke structure with nodes for states and edges for transitions Extracting this structure from a concurrent system prior to model checking may result in a graph that is exponentially bigger than the system Algorithms based on the explicit state enumeration could be improved if only a fraction of the reachable pairs are explored A finite automaton is a mathematical model of a device that has a constant amount of memory independent of the size of its input Form
139. lements gt gt eu a lt lt lt Interface gt gt Realtime Thread gt gt Schedulable A lt lt implements gt gt NoHeapRealtime Thread Abbildung 3 Vererbungshierarchie von NoHeapRealtimeThread Beispiel import javax realtime public class Examplel public static void main String args NoHeapRealtimeThread nhrt new NoHeapRealtimeThread public void run System out printin This is a NoHeapRealtimeThread by RealtimeThread rt new RealtimeThread public void Ton 4 DVSLEM OUL print iln hus 15 a Realrtimerhread gt by nnrt start rt starti 5 3 2 Memory Management Der Garbage Collector in Java ist zwar eine sch ne Sache weil er sich automatisch darum k mmert dass nicht ben tigter Speicher frei gesetzt wird Dies kann aber zu einem Hindernis werden da dieser zum Einen mit nicht vorhersehbarer Zeit d e laufenden Threads blockiert Und zum Anderen Daten l schen kann die l ngerfristig von mehreren Threads ben tigt werden Ebenso ist es w nschenswert dass man mit Java auf spezielle Speicherbereiche zugreift um dort beispielsweise direkt Daten von Hardware mit DMA zu be kommen und dorthin zu senden Deshalb wurde das Memory Management berarbeitet und 4 Speicherarten geschaffen in denen die Garbage Collection unterschiedlich agieren darf und ber die man auch direkt auf physikalische Speicherbereiche zugr
140. len Um 16 09 38 fielen dann die letzten Leitungen die Michigan und Ohio belieferten aus und eine weitere Energiewelle von ca 4 GW suchte sich einen neuen Weg nach Michigan Diese Welle verursachte auf ihrem Weg sehr gro e Belastungen in den Netzkomponenten Dadurch fielen innerhalb von einigen Sekunden alle Leitungen und Kraftwerke auf dem Weg des Energieflusses aus das Netz teilte sich in mehrere Teilbereiche auf Von 16 10 46 bis 16 12 brach das Netz der Eastern Interconnection aufgrund der Aufteilung schlie lich vollst ndig auseinander Die einzelnen verbliebenden Inseln konnten die Balance zwischen Energieerzeugung und Verbrauch nicht halten und automatische Sicherheitsschaltungen schalteten die verbliebenden Kraftwerke und Leitungen ab Um 16 13 war der Prozess an seinem Ende angelangt und f nzig Millionen Menschen waren ohne Strom F r eine detai lierte Aufstellung sei auf den offiziellen Bericht Report US Canada Taskforce verwiesen 2 4 Anmerkungen An diesem Ereignis lassen viele Kernprobleme kritischer Infrastrukturen aufzeigen Die hohe Komplexit t sowohl des verwendeten XA 21 Systems als auch des ganzen Strom netzes machen es sehr schwierig es zu beherschen Weder FE noch die Kontrollbeh rde haben die kritischen Punkte des von ihnen versorgten Netzes erkannt Die hohe Komplexi t t erfordert die Verwendung von technischen Hilfsmitteln um berhaupt Entscheidungen treffen zu k nnen Wenn diese Werkzeuge wie das verwendete
141. len betrachtet werden k nnen und die Analyse sich mit viele Ausf lle besch ftigen muss die nicht zu Gefahren f hren Bei komplexen Systemen ist die Anwendung sehr teuer L sung ist FMEA nur in einer sp ten Entwicklungsstufe anzuwenden wo sie nur auf die kritischen Bereiche angewandt wird 1 Druck sinki Druck sinki Explosion Abbildung 5 Beispiel eines ETA Diagramms 1 5 Risiko Analyse Nachdem im vorherigen Kapitel die Gefahrenanalyse vorgestellt wurde wird in diesem Kapitel die Risikoanalyse vorgestellt Das Risiko wird oft als die Kombination aus der Wahrscheinlichkeit des Eintreffens und den Folgen einer Gefahr verstehen Das hei t Risiko Wahrscheinlichkeit Folgen Das Risiko wird pr sentiert als eine Quantifizierung der Gefahr Auf den ersten Blick schein diese Definition handhabbar zu sein aber wenn man tiefer analys ert w rd man schnell verstehen dass Wahrscheinlichkeit und Folgen nur grobe und subjektive Abschatzungen sind Alle Gefahren zu identifizieren ist in der Realit t eine schwere Sache und ebenso die Wahrscheinlichkeit zu bestimmen Zweitens muss man eine Ma einheit f r die Schwere eines Ungl cks finden und damit tats chlich einen Preis f r das Leben festlegen was zumindest ethische Probleme mit sich bringt Daher ist es schwer die Frage nach einem akzeptablen Risiko mit Zahlen zu beantworten 5 1 N here Betrachtung der Schwere der Folgen Alle Industrien die mit Sicherheit verwand
142. lig wohingegen sie in Deutschland und den USA verpflichtend ist Damit ein Produkt zertifiziert werden kann muss es die Konformit t mit dem zuvor festgelegten Standard beweisen Die Zertifizierung von Systemen bezieht sich zumeist auf das komplette System und nicht auf einzelne Komponenten Die Zertifizierung von Software ist besonders schwierig da hier ein zuverl ssi ges testen nur schwer m glich ist Daher basiert die Zertifizierung sowohl auf dem Entwicklungsprozess als auch auf der demonstrierten Leistung des Systems Dazu m ssen die angewendeten Methoden eingesch tzt werden und eine Bewer tung des Entwicklungsteams muss stattfinden Unvermeidlich bilden also Aspekte der Qualit tssicherung einen grundlegenden Teil dieser Einsch tzung 2 3 Ziele der Zertifizierung Nach diesem berblick bleibt nun noch die Frage nach dem Zweck der Zertifizie rung brig Als Ziele der Zertifizierung bei sicherheitskritischen Systemen sind die folgenden Punkte zu betrachten e Verbesserung der Sicherheit e Steigerung des Bewusstseins ber die Implikationen der Systemnutzung und Sicherheit e Das Erzwingen von minimalen Standards in Design und Herstellung inner halb der betroffenen Industrie e Ermutigung des Aufbaus einer professionellen Verantwortlichkeits Struktur 2 4 Safety Case 2 4 1 Einleitung Der Safety Case ist ein Dokument oder eine Sammlung von Dokumenten die glaubhafte Argumente pr sentieren dass das vorgesch
143. m Sinne eines Black Box Tests interessiert uns nicht was das Modul week_d mit den Werten macht und wie das Ergebnis zustande kommt Wir sehen nun das Ergebnis TESTFALL TAG MONAT JAHR WOCHENTAG 3 l 1 1994 6 4 31 12 1994 6 5 0 1 1994 5 6 32 1 1994 2 7 7 O 1994 2 8 7 13 1994 6 Wenn wir das Ergebnis mit dem Kalender vergleichen stellen wir fest dass die Eingabewerte ab Testfall 5 sind falsch Wir berpr fen hier zun chst die Grenzwerte vom Tag 0 1 31 und 32 und es hat sich herausgestellt dass der Eingabewerte O und 32 das falsche Ergebnis liefert Danach wird der Grenzwert f r den Monat untersucht Der Eingabewert 0 und 13 liefert das falsche Ergebnis Der Ausdruck Grenzwert bedeutet dass die benachbarten Werte auch ber cksichtigt werden sollen Beim Monat werden zum Beispiel nicht nur die Werte 1 und 12 sondern auch die benachbarten Werte 0 2 11 13 untersucht Warum ist das so Der Grund liegt darin dass der Fehler leicht beim Eintippen des Quellcodes auftreten kann Zum Beispiel lt 12 obwohl man eigentlich lt 12 gemeint hat Dieser Fl chtigkeitsfehler st sehr schwierig zu entdecken Wenn man den Grenzwert untersucht wird ein derartiger Fehler gefunden Wir betrachten nun das zweite Beispiel Dieses Beispiel ist identisch mit dem Beispiel von der Aquivalenzklasse und wir erweitern und untersuchen die Testf lle um die Grenzwerte Spezifikation zur Ableitung des technischen Eintrittsalters einer Person
144. me difference between consecutive loops ms Time difference between consecutive loops ms Abbildung 3 Einhaltung einer Schleifenzeit von 10ms 100 o 100 T _ 7 a u gt 90 F 90 ge 4 80 80 H 4 1 70 l 70 J l N 60 60 2 2 S S 50 504 5 Ss x z 40 40 i a i l 30 30 4 l I 1 20 l 20 1 I vad 107 if New System 7 107 ae New System ae Old System ee Old System 0 1 1 1 1 0 A aaa 1 1 1 fi L 4 8 8 5 9 9 5 10 10 5 11 11 5 12 0 0 2 0 4 0 6 0 8 1 1 2 1 4 1 6 1 8 2 Time difference between consecutive loops milliseconds Time difference between consecutive loops milliseconds a 10 millisecond period b 1 millisecond period Abbildung 4 10ms Schleife nach der Verbesserung Die letze Messung dokumentiert die Zeit die zwischen dem Timerinterrupt und dem Eintritt in die zum Timer geh rige Funktion vergeht Der dazu eingesetzte Prozess verwendet die Schedulerstrategie SCHED_FIFO Die Abbildung 5 zeigt innerhalb welcher Zeit die Routine nach dem Timerinterrupt betreten wird Man kann erkennen da zu den 15us f r die TISR noch ca 10us dazukommen bis im schnellstm glichen Fall die Funktion angesprungen wird Maximal vergehen 50s zwischen Interrupt und Eintritt in die Funktion Die zus tzlich Zeit zur Laufzeit der TISR wird durch den Kontextwechsel und die Umschaltung von Kernel Mode in den User Mode verursacht Desweite
145. mer in einem Zustand sein muss dass es auch nach einen Ausfall des wichtigs ten Generators oder Leitung verf gbar bleibt Wenn ein solcher Zustand eintritt muss der Netzbetreiber innerhalb einer halben Stunde Ma nahmen ergreifen um dieser Bedingung wieder zu gen gen Ausserdem fehlte es bei PJM und MISO an Vorschriften wie und wann mit Verletzun gen von NERC Vorschriften wie der n 1 Bedingung die an den Grenzen der jeweiligen Zustandigkeitsbereiche auftreten umgegangen werden soll Die Reliability Coordinatoren hatten nur ungen gend Einblick in die Struktur des FE Netzes auch deshalb waren sie sich unsicher wie die gemeldeten St rungen zu bewerten waren 2 3 Weiterer Verlauf der Ereignisse Um 15 59 fielen weitere f nf 138 KV Leitungen aus Dies verursachte schlie lich um 16 05 57 den Ausfall der 345 KV Leitung Sammy Star Bis zu diesem Zeitpunkt w re die Kaskade die zu dem Blackout fiihrte immer noch durch automatischen oder manuel len Lastabwurf zu verhindern gewesen Durch diesen Ausfall aber schalteten sich weitere Kraftwerke und Leitungen ab Um 16 09 06 fiel dann die Leitung East Lima Fostoria aus Dies verursachte eine Umkehrung des Energieflusses von Michigan nach Ontario ei ne nderung von etwa 700 MW Durch diesen abrupten Wechsel der Belastung fing das Stromsystem f r mehrere Sekunden an zu schwingen Dadurch wurde weiter Stress im System verursacht so dass weitere Stromerzeuger und Leitungen ausfie
146. mierungen konventioneller Betriebssysteme 3 Anforderungen f r ein echtzeitfahiges Linux DI NM 3 2 KURT 3 2 1 Verfeinerung der zeitlichen Aufl sung mit UTIME OO 2 2 Leistungsfahigkeit von U TIME 2 3 Realzeitscheduling mit KURT 2 4 Performance von KURT 4 Ausblick wil Oo Abbildungsverzeichnis Laufzeitvergleich der Timerinterrupt Service Routinen Abweichung der Softwareuhr Einhaltung einer Schleifenzeit von 10ms 10ms Schleife nach der Verbesserung 5 Zeitmessung vom Interrupt zur eingeplanten Routine 10 Effektivit t der Scheduler im Vergleich 11 SCHED_ALL_PROCS und SCHED_KURT_PROCS im Vergleich 12 Zeiten mit Hintergrund I O Aktivitat gt O Tabellenverzeichnis Listings 1 Pseudo Code f r die Linux Timer Interrupt Service Routine 2 Pseudo Code f r die UTIME Linux Timer Interrupt Service Routine 1 Einleitung In Sicherheitskritischen Systemen werden zunehmend Rechner mit flexibel nderbarer Software eingesetzt um andere starre meist in Hardware realisierte Systeme zu ersetzen Die Anforderung an den Rechner ist dabei in Echtzeit auf Ereignisse zu reagieren Soll dies mit einem Standardpersonalcomputer Standard PC realisiert werden mu die Software die Einhaltung der Anforderungen gew hrleisten Man spricht dann von einem Echtzeitsystem Was bedeutet der Begriff Echtzeitsystem Ein Echtzeitsystem ist ein System das st ndig anfallende Daten sofort verar
147. mme um eine pr zise Beschreibung des Zeitverhaltens von Objekten und Systemen zu erm glichen Das dritte neu eingef hrte Diagramm das Interaktions bersichtsdiagramm dient zur Darstellung der Abfolge mehrerer Verhaltensmodelle Durch die nderungen im Komponentendiagramm wird die Modellierung gan giger Marktstandards NET und J2EE besser unterst tzt Die Zustandsautomaten erm glichen eine verbesserte Verkn pfung von stati schen Elementen und dahinter liegenden Zustandsmodellen Alle weiteren Diagramme wie z B Use Case Objekt und Paketdiagramme wurden nur unwesentlich ver ndert 3 Interaktionsdiagramme Eines der Grundprinzipien der UML Sprachsch pfer war es grundlegende Kon zepte st rker in den Vordergrund zu stellen als Diagramme Dies wird bei der In teraktionsmodellierung besonders deutlich Es werden erst einmal nur grundle gende Konzepte definiert die zur Darstellung von Kommunikationssituationen er forderlich sind Dazu z hlen als bedeutendste Interaktionen Lebenslinien Nachrichten Kommunikationspartner und Sprachmittel zur Flusskontrolle Je nach Situation werden aber nicht alle UML Elemente in ihrer kompletten Nota tionstiefe ben tigt Aus diesem Grund wurden in der UML verschiedene Typen von Interaktionsdiagrammen definiert Je nachdem ob nur die beteiligten Kommu nikationspartner die exakte zeitliche Reihenfolge oder Kommunikationsfehler und die daraus resultier
148. n Werden hingegen Individuen zertifiziert wird diesen mittels des Zertifikates er laubt den gew hlten Beruf in diesem Sektor auszuf hren Speziell im Fall von sicherheitskritischen Systemen ist ein hoher Grad an Fachwissen Erfahrung und Training unter den Ingenieuren notwendig Als Beispiel sei hier die US Luftfahrtindustrie angef hrt Die FAA autorisiert Angestellte der Herstellerfirmen damit diese bestimmte Zertifizierungen inner halb des Unternehmens durchf hren Bei Boing und McDonnell Douglas Projek ten werden auf diese Art 90 95 aller Zertifizierungen durchgef hrt 2 2 2 2 Werkzeuge oder Methoden Die Werkzeuge und Entwicklungsmethoden die in der Produktion von sicherheits kritischen Systemen eingesetzt werden spielen eine wichtige Rolle um dessen Leistung zu determinieren Folglich setzen einige Standards Restriktionen die die Nutzung von Werkzeugen und Methoden einschr nken Besonders wichtig und weit verbreitet unter der Werkzeug Zertifizierung ist die Zertifizierung von Compilern Federal Aviation Authority US Luftfahrtbeh rde 2 2 3 Systeme oder Produkte Wie oben bereits erwahnt kann die Zertifizierung von Produkten in bestimmten Bereichen der Industrie notwendig sein Dies variiert allerdings stark von An wendungsgebiet zu Anwendungsgebiet und von Land zu Land Als Beispiel sei hier die Zertifizierung von elektronischen Ger ten in der Medizin angef hrt Diese ist in Gro britannien freiwil
149. n Chandra Kurnia Jaya Sommersemester 2004 Content INTRODUCTION 1 1 MOTIVATION PURPOSE OF SYSTEM VERIFICATION 1 2 SYSTEM VERIFICATION VIA MODEL CHECKING THE PROCESS OF MODEL CHECKING 2 1 MODELLING 2 2 SPECIFICATION 2 3 VERIFICATION 2 4 A SIMPLE EXAMPLE WITH MICROWAVE OVEN COOKING ALGORITHMS FOR MODEL CHECKING 3 1 BASED ON AUTOMATA THEORY 3 2 BASED ON SYMBOLIC STRUCTURE 3 3 ALTERNATIVE METHODS MODEL CHECKING FOR REAL TIME SYSTEMS 4 1 DISCRETE REAL TIME SYSTEM 4 2 CONTINUOUS REAL TIME SYSTEM 5 MODEL CHECKING DEVELOPING TREND 6 CONCLUSION REFERENCES 1 Introduction 1 1 Motivation Purpose of System Verification Computerised systems are more and more important to our everyday life Digital technology is now used to supervise critical functions of Aircrafts Trains Nuclear Industrial Plants amp Life Support Systems etc In computer science it s important that errors must be eliminated as promptly as possible otherwise it becomes much more expensive because errors cost often not only the money but also the human life for examples Pentium bug Intel Pentium chip released in 1994 produced error in floating point division Cost 475 million e ARIANE Failure In December 1996 the Ariane 5 rocket exploded 40 seconds after take off Software components threw an exception Cost 400 million Therac 25 Accident A software failure caused wrong dosages of x rays Cost Human Loss S
150. n z B Klasse Sch ler Klasse Buch Auf dieser Ebene werden die m glichen Zust nde eines Systems beschrieben Diese Ebene wird auch als Metadaten Modell die Modellebene genannt Die Objekte aus der MO s nd die Instanzen aus der Ebene MI Diese Ebene ist vergleichbar mit einem Quellcode eines Programms e Auf der Ebene M2 wird auch als Metamodell Ebene genannt werden Elemente spezifiziert die zur Modellierung auf der Ebene MI eingesetzt werden Auf dieser Ebene werden die Modelle mit zus tzlichen Elementen wie Variable Operationen erg nzt Diese Schicht ist das zentrale Element der UML Auf dieser Ebene beschriebenen Konzepte werden bei der UML Modellierung verwendet wie Z B Die Klassen Attribute Assoziationen Durch Diese MetaModell ist eine abstrakte Syntax der Modellierungssprache definiert Diese Ebene w rde mit EBNF einer Programmiersprache vergleichbar Alle Elemente die auf dieser Ebene zur Definition des Metamodells verwendet werden wird auf der Ebene M3 Meta Metamodell Ebene spezifiziert e Die Ebene M3 bildet die Infrastruktur der Metamodellarchitektur Dieser Schicht ist fur alle Modellierungssprachen die mit MOF definiert werden ist identisch Dieser Schicht wird auch MOF Ebene genannt weil die Regeln um MOF selbst zu beschreiben auf dieser Ebene beschrieben werden Zur Vervollstandigung der Analogie ware dieser Ebene die Definition der Syntax des EBNF 3 3 PIM Plattform Independent Model
151. n Systemen auf Sowohl vollkommende Perfektion im Design als auch absolute Sicherheit gegen zuf llige Fehler ist nicht erreichbar Das Auf treten von Fehlern kann die einwandfreie Funktion von SkS beeintr chtigen Deshalb sind klare Begrifflichkeiten und Definitionen hier besonders wichtig Fehler lassen sich ber ihre Eigenschaften in verschiedene Klassen einteilen Weiterhin muss definiert werden wie mit aufgetretenen Fehlern umgegangen wird wie Fehler erkannt und gegebenenfalls korrigiert werden k nnen 1 4 1 Fehler Fehlfunktion und Systemausfall Als Fehler bezeichnet man einen Defekt eine Fehlerursache im System der nicht notwen digerweise zu weiteren Problemen f hrt Eine Fehlfunktion oder Fehlzustand ist eine Ab weichung von der ben tigten Funktion des Systems Sie kann aus einem Fehler entstehen Systemausfall tritt auf wenn das System bei der Durchf hrung der ben tigten Funktionen scheitert Eine oder mehrere Fehlfunktionen k nnen zu diesem Zustand f hren 1 4 2 Unterscheidung ber die Fehlerart Fehler lassen sich ber die Art ihrer Entstehung in zwei unterschiedliche Klassen einteilen Zuf llige Fehler geh ren immer zu Hardware Komponenten von SkS Da Hardware auch wenn sie innerhalb ihrer optimalen Arbeitsumgebung eingesetzt wird immer aus fallen kann sind alle Systeme anf llig f r diesen Fehler ber statistische Auswertungen und Test lassen sich Aussagen ber das Auftreten und die Frequenz von zuf lligen
152. n werden 3 9 Time und Timers Bei Echtzeit Anwendungen steht wie der Name schon sagt die Zeit auch im Vordergrund Die Zeit aus dem normalen Java java util Date ist unzureichend da sie nicht genau genug ist und einige Funktionen fehlen lt lt Interface gt gt java lang Compareable i lt lt abstract gt gt HighResolution Time oe Absolute Time Relative Time 1 RationalTime Abbildung 7 Vererbungshierarchie der HigResolutionTime Klassen lt lt abstract gt gt AsyncEvent och et we lt lt abstract gt gt a HighResolutionTime Timer AsyncEventHandler OneShotTimer PeriodicTimer Abbildung 8 Vererbungshierarchie der Timer Klassen Deshalb wurde die HighResolutionTime eingef hrt Diese kann die die Zeit in Nanosekunden seit dem 01 01 1970 00 00 erfassen und wird dem entsprechend auch weit genug in die Zukunft reichen Hierzu wer den in der Spezifikation zu Realtime Java leider keine Angaben gemacht Diese Klasse wird aber nicht direkt verwendet sondern es erben von ihr nur andere Zeitdarstellungen e AbsoluteTime F r die Speicherung der absoluten Zeit seit dem 01 01 1970 e RealativeTime F r die Speicherung einer Zeitspanne e RationalTime F r die Speicherung einer Frequenz Di
153. nd bertragbarkeit von einer Hardware Plattform auf eine andere Schlussfolgern kann man daher dass Qualitatskontrolle von der Fahigkeit des Messens der Parameter des Produktes abh ngt das wir kontrollieren m chten 1 4 2 Wie wird die Qualit tskontrolle durchgef hrt Viele Unternehmen benutzen statistische Prozesse um die Qualit tskontrolle durchzuf hren und deren Fehler systematisch zu reduzieren Dabei werden zuf llig Exemplare des Output ausgew hlt ausprobiert und getestet Die dabei festge stellten Toleranzen zwischen den Spezifikationen und dem Produkt werden zur Anpassung des Produktionsprozesses genutzt um in Zukunft keine Produkte min derer Qualit t zu produzieren Eine recht popul re Methode in diesem Zusammenhang sind die so genannten sechs Sigma Stufen der Qualit t Ein Unternehmen das diese Qualit ts stufe erreicht schafft es seine Fehlerwahrscheinlichkeit auf unter vier Teile pro einer Million produzierter Teile zu senken 1 5 Qualit tsstandards Aus den vorherigen Abschnitten geht hervor dass Standards z B ISO 9000 existieren die bei der Herstellung von qualitativ hochwertigen Produkten mit helfen Qualitdtsstandards existieren seit ber 150 Jahren Zu Beginn wurden sie vor allem im Eisenbahnsektor verwendet Hier seien nun zwei der wichtigsten Qua lit tsstandards kurz vorgestellt 1 5 1 ISO 9000 Der Standard geht urspr ngliche aus dem BS 5750 Standard
154. nd Luftfahrt sowie den milit rischen Sektor beliefert als Vorraussetzung f r die Erteilung von Auftr gen gelten st das Interesse nach Ada Produkten wie Werkzeugen aber auch nach Expertenwissen gro Viele Unternehmen vor allem Compilerhersteller bieten Ada Schulungen wo man sich das Wissen aneignen kann au erdem ist Ada oft n der Literatur beschrieben worden Ada ist als eine Universalsprache entwickelt worden die ein breites Spektrum von Anwendungsszenarien abdeckt Aus diesem Grund ist die Sprache sehr volumin s es ist eine Vielzahl von Konstrukten in den Sprachkern aufgenommen worden die sich nicht ganz so gut f r den Einsatz in sicherheitskritischen Systemen eignen Viele dieser Punkte tauchen in dem Anforderungskatalog den ich im Kapitel 2 5 aufgestellt habe und sind im Kapitel 3 schon beschrieben und beurteilt worden In einigen Punkten erkennt man dass die Sicherheitsmassnahmen die Ada standardm ig mit sich bringt nicht ausreichend sind Die Entwickler von Ada Haben dies auch erkannt und haben deshalb den schon teilweise beschriebenen Annex Sicherheit konzipiert durch welchen u a eine ganze Reihe von Sprachkonstrukten von der Benutzung ausgeschlossen werden kann Diese Restrictions betreffen folgende Bereiche e Prozesse und gesch tzte Typen Einschr nkung oder Verbot Verwaltung des Speichers Einschr nkung oder Verbot Verbot der Ausnahmebehandlung Einschr nkung der verwendbaren Datentypen z B keine Gleitkomm
155. nd White Box Test zu empfehlen da jede Methode jeweils Nachteile und Vorteile hat Man nennt diese Kombination Broken Box Test oder Grey Box Test Die oben beschriebenen Verfahren erh hen die Qualit t und die Sicherheit der entwickelten Software Absolute Sicherheit kann keines der Verfahren garantieren Pr fe die Br cke die dich Fragen soll Sprichwort 8 Literaturverzeichnis 1 Georg Erwin Thaller Verifikation und Validation Vieweg 1994 2 Ian Sommerville Software Engineering Addison Wesley 2000 3 Glenford J Myers Methodisches Testen von Programmen Oldenbourg 1991 4 Neil Storey Safety Critical Computer Systems Prentince Hall 1996 5 Edward Kit Sofware Testing in The Real World Addison Wesley 1995 6 Ilene Burnstein Practical Software Testing Springer 2003 7 Helmurt Balzert Lehrbuch Grundlagen der Informatik Spektrum 1999 8 Hauptseminar Prof Huckle Therac 25 http www5 in tum de lehre seminar semsoft unterlagen_02 therac website 9 Torsten Bresser Validieren und Verifikation inkl Testen Model Checking und Theorem Proving Seminar 2004 10 Friederike Nickl Qualitdtssicherung und Testen sepis Verifikation Validation und Testen von Sicherheitskritischen Systeme Seminararbeit im Fach Informatik im Rahmen des Seminars Sicherheitskritische Systeme an der Universit t Siegen Fachgruppe f r Praktische Informatik eingereicht bei Dr J rg Niere vorgelegt vo
156. nd notwendig um den Speicherverbrauch f r die Kontrolle dieser Seiten klein zu halten Die Seiten werden dann an die Prozesse vergeben Dabei steht jedem Proze im Prinzip der gesamte adressierbare Speicher von 4GB zur Verf gung Aufgabe des Betriebssystem ist nun mit Hilfe der Memory Management Unit MMU im Prozessor nur die jeweils von einem Prozess benutzen Speicherseiten auf den real im System vorhandenen Arbeitsspeicher abzubilden Ist der real vorhandene Arbeitsspeicher zu klein um alle angeforderten Speicherseiten zu speichern so kann der Kernel Speicherseiten die lange nicht benutzt wurden auf ein anderes Medium meist die Festplatte auslagern Das hat den Vorteil das der verfugbare Arbeitsspeicher innerhalb des Betriebssystem groBer sein kann als der tatsachlich vorhandene Der Nachteil ist da ein Prozess recht lange mu bis er auf seinen Speicher zugreifen kann weil das Betriebssystem diesen Teil ausgelagert hat Die Speicherverwaltung hat auch noch einen Nutzen f r das Multitasking Der Kernel wird sofort dar ber in formiert wenn ein Prozess auf Speicher versucht zuzugreifen den er vorher nicht angefordert hat Dadurch wird vermieden da sich Programme gegenseitig negativ beeinflussen k nnen Cold Caches Der Zugriff von Prozessen auf den Arbeitsspeicher kann auch noch durch einen anderen Effekt als den der Auslagerung stark gebremst werden Diesen Effekt bezeichnet man als Cold Caches Die Geschwindigkeit v
157. ng stellt die Tatsache dar dass die Inhalte des Safety Case stets multidisziplin r sind Das f hrt dazu dass das Entwick lungsteam Experten aus verschiedenen Fachgebieten als Mitglieder haben sollte vgl Abbildung 2 Der Knackpunkt eines solchen Teams ist die Kommunikation zwischen den einzelnen Personen denn diese benutzen zum Teil recht unterschied liche Fachsprachen 2 5 Der Prozess der System Zertifizierung Obwohl der Zertifizierungsprozess in der letzten Phase des Projektes durchgef hrt wird sollte er genau wie die Verifikation schon in einer fr hen Phase mit in die Planungen einflie en Der Entwickler sollte schon fr hzeitig Kontakt zum Zertifizierer aufnehmen um Problemen aus dem Weg zu gehen und das Verst ndnis zwischen den Parteien zu verbessern Auf diese Weise kann der Zertifizierungsprozess erheblich erleichtert werden W hrend der Entwicklung muss der Entwickler den Zertifizierer mit Dokumenten Sundards Intention oo O Astessors IRF E SS Designers 1 gehe Spec ification 3 Abbildung 2 Expertengruppen bei der Entwicklung des Safety Case Operators versorgen die darlegen dass die Bedingungen des zuvor festgelegten Zertifizie rungsplans eingehalten werden Ebenso werden zu bestimmten Abschnitten des Projektes Daten zur Kontrolle vorgelegt Daher kann man bei der Zertifizierung eher von einem lang andauernden Prozess sprechen der parallel zur Entwicklung abl uft als von einer
158. ngem erfolgreich in der Elektrotechnik angewendet um das zeitliche Verhalten digitaler Schaltungen zu beschreiben Seit Version 2 0 ist es nun auch in der UML verf gbar Hauptaufgabe des Dia gramms ist es zu zeigen wann sich verschiedene Interaktionspartner in welchem Zustand befinden 5 1 berblick Das Timing Diagramm erm glicht die pr zise Analyse und Darstellung des zeitlichen Verhaltens von Klassen Akteuren Komponenten Schnittstellen usw Dazu enth lt es folgende Notationselemente Lebenslinien und die dazu geh rigen Bedingungen Zust nde und Attri butwerte Nachrichten Zeitbedingungen Zeitverlaufslinien Die Lebenslinien sind breite Streifen die die Zustande bzw Bedingungen enthalten Mehrere Lebenslinien werden vertikal angeordnet Die Zeitachse wird horizontal angetragen Sie wird blicherweise mit einer Zeitskala verse hen Die Zeitverlaufslinie jeder Lebenslinie zeigt an wann sich die Lebensli nie in welchem Zustand befindet Waagrechte Linien beschreiben einen Zu stand senkrechte Linien einen Zustandswechsel Nachrichten werden durch Pfeile zwischen den einzelnen Zeitverlaufslinien dargestellt Abbildung 4 zeigt eine bersicht ber die h ufigsten Notationselemente am Beispiel ei ner FuBgangerampel k d 6 d gt grun Ampe gehen nicht betriebsbereit gehen aktivieren aktiv Fuliganger wartend O 10 20 30 Abbildung 4 Das Timing Diagramm und seiner Elemente
159. ngen Nuernberg 1999 11 Prof Dr Wolfgang Thomas RWTH Aachen Vorlesungsmaterial Model Checking WS 2003 04 URL http www 17 informatik rwth aachen de d teaching ws0304 modelchk 12 Prof Dr Javier Esparza Vorlesung Model Checking SS 2003 URL http www informatik uni stuttgart de fmi szs teaching ss2003 modelchecking folien pdf 13 Model Checking Uberblick URL http www software kompetenz de 2885 14 Prof Dr H Peter Gumm Vorlesungsmaterial Model Checking URL http www mathematik uni marburg de tschroed vor01SSModelChecking html 15 Definition of model checking from NIST URL http www nist gov dads HTML modelcheckng html 16 Fakult t f r Informatik der Technischen Universit t Miinchen Hauptseminar im SS 2002 Model Checking URL http wwwbrauer informatik tu muenchen de seminare model checking SS2002 End Of Document UML 2 0 und die Modellierung von Realtime Systemen Seminararbeit im Fach Informatik im Rahmen des Seminars Sicherheitskritische Systeme an der Universit t Siegen Facheruppe f r Praktische Informatik eingereicht bei Dr J rg Niere vorgelegt von Christoph Hardt Sommersemester 2004 Inhaltsverzeichnis Einleitung Neuerungen der UML 2 0 Interaktionsdiagramme Modellierung von Interaktionen oF OO N Timing Diagramme 5 1 Uberblick 5 2 Anwendungsbeispiel 5 3 Anwendung im Projekt 5 4 Notationselemente 5 4 1 Interaktion In
160. ngen Die erste Messung dokumentiert die Laufzeit der neuen TISR von UTIME 100 T 90r 80r 60 H1 of interrupts an o T 407 I 3or I id Standard Linux A Old UTIME New UTIME 1 L 1 1 l 0 5 10 15 20 25 30 35 40 Timer interrupt processing time microseconds Abbildung 1 Laufzeitvergleich der Timerinterrupt Service Routinen Die Abbildung 1 zeigt den prozentualen Anteil der Durchl ufe der TISR in Abh ngigkeit von der Durchlaufzeit Die Linie stellt dar welcher Anteil innerhalb einer bestimmten Laufzeit liegt Die meisten Timer Interrupts konnten mit der originalen TISR innerhalb lus abgearbeitet werden Alle waren jedoch unterhalb von 5us UTIME erh ht leider die Laufzeit durch die TISR auf ca 15us Ursache daf r sind die Berechnungen f r die Softwareuhr und f r den n chsten Timerinterrupt als auch die Programmierung des TIB Ein weitere Messung ergab da die Programmierung des TIB alleine Aus ben tigt Somit ist auch klar warum bei der Neuimplementierung der TISR nur noch ca 7us ben tigt Abbild 2 zeigt die Abweichung der Softwareuhr unter Standard Linux unter UTIME und unter dem verbesserten UTIME Man kann deutlich erkennen da der TSC wesentlich genauer arbeitet als der TIB und da bei der Verbesserung der Architektur nocheinmal die Genauigkeit stark gesteigert werden konnte Um die Verbesserung der Aufl sung von Timern
161. nmissverst ndlich interpretiert werden und ihre Korrektheit kann unter anderem auch durch Hilfsprogramme bewiesen werden Das Anwenden von formalen Methoden w hrend dem vollst ndigen Entwicklungspro zess ist aber noch sehr aufwendig Es lohnt sich nur bei SkS mit extrem hohen Integrit ts anforderungen Aber auch ein begrenzter Einsatz kann aber das Vertrauen in die Verl ss lichkeit des entwickelten Systems steigern Auch die Anwendung von formalen Methoden kann aber nicht sicherstellen dass die Kunden oder Sicherheitsanforderungen richtig erfasst worden sind dass die erstellte Spezifikation korrekt im Sinne ihrer eigentlichen Sicherheits Aufgabe ist 1 6 Fehlerbehebung Ausf hrliches Testen zur Fehlerbehebung sowohl von Hardware als auch Software soll sicherstellen dass m glichst wenig Fehler im fertigen System vor seinem Einsatz vorhan den sind Testen ist also der Prozess um ein System zu verifizieren oder es zu validieren Zu diesem Prozess geh rt beispielsweise dass direkte Ausf hren des Programmes als auch die Analyse des Quelltextes und des Designs Allgemein kann man davon ausgehen dass je sp ter ein Fehler gefunden wird desto aufwendiger und teuerer ist seine Behebung Nicht nur aus diesem Grund ist es wichtig beim Entwurf von SkS im voraus das Testen einzuplanen und gegebenfalls durch entspre chende Vorkehrungen beim Design zu erleichtern Da das Testen aller m glichen Eingangswerte bei digitalen Systemen aufg
162. ntlich nur im Vergleich zu einer anderen Programmiersprache ausdr cken Ada ist im Vergleicht z B zum C Code eher langsam die Ursache hierf r ist dass Ada neben der eigentlich zu realisierenden Funktion auch permanente und umfassende Laufzeit berpr fungen bereit stellt Der Vollst ndigkeit halber sei erw hnt dass die Ada Compiler fast immer hochoptimierend sind und sehr effizienten Maschinencode liefern Kra 6 3 5 uverlassig eit Dependabilit 3 5 1 Mehrfache Referenzen aliasing In Ada k nnen dynamische Datenstrukturen Objekte erzeugt werden Auf diese Strukturen kann durch sogenannte Zugriffsobjekte bzw Zeigerobjekte zugegriffen werden Mehrere Zugriffsobjekte k nnen auf die gleiche dynamische Struktur verweisen im Klartext in Ada ist aliasing m glich 3 5 2 Seiteneffe te durch Unterprogramme subprogram side effects Unterprogramme werden in Ada entweder durch Prozeduren oder durch Funktionen realisiert Bei der Parameter bergabe der Prozeduren unterscheidet man drei Arten der bergabe IN OUT und IN OUT Die reine Wertvorbelegung Ubergabeart IN stellt kein Problem dar hier wird lediglich eine Kopie des Wertes der Prozedur bergeben Bei den bergabearten OUT und IN OUT ist ein Schreibzugriff auf den bergabeparameter m glich Der ge nderte Parameter wird nach Beendigung der Prozedur an den Aktualparameter aus dem Aufruf r ck bermittelt es k nnen also Seiteneffekte auftreten Der Gebrauch von Funktionen i
163. nun eine Ausnahmesituation im einem grade bearbeitenden Rahmen eintritt und ist im betreffenden Ausnahmebehandlungsteil eine entsprechende Ausnahmesituation mit einer Anweisungsfolge angef hrt so geht der Kontrollfluss auf diese Anweisungsfolge ber Die Ausnahme ist damit beendet Danach wird der Rahmen der die Ausnahmenbehandlung enth lt auf jeden Fall abgeschlossen und die Programmausf hrung wird mit dem bergeordneten Rahmen fortgesetzt 3 1 Arithmetische Laufzeit ber achung operational arithmetic Die arithmetische Laufzeit berwachung bernimmt ebenfalls der Ausnahmenmechanismus In Ada 3 gab es noch eine spezielle Ausnahme Numeric_Error die jedoch bei neueren Implementierungen der Sprache auf jeden Fall jedoch in Ada 5 von Constraint_Error voll abgedeckt wird 3 Maintainabilit artbar eit Extendabilit Er eiterbar eit und iederver endbar eit Das im Ada benutzte Package Konzept bietet die Moglichkeit groBe Softwareprojekte zu gliedern und zu Modularisieren e Die separate Compilierbarkeit von Ada Units also Unterprogrammen erleichtert die Wartung und fordert die Wiederverwendbarkeit Weiterhin kennt Ada generische Einheiten die nochmals die Wiederverwendbarkeit der Ada Unterprogramme steigert Diese Einheiten sind eigentlich Programm Schablonen f r welche eine Parameter vereinbart worden sind 3 10 sicheres Subset Ada besitzt eine sicheres Subset SPARK SPARK ist eine Teilsprache von Ada zum Compilieren
164. nz des Systems beitragen 1 3 2 Wie wird die Qualit tssicherung angewendet Wie bereits erw hnt ist die Definition der notwendigen Verfahren und des dazu geh rigen Management Systems ein grundlegender Bestandteil der Qualit tssi cherung Weiterhin muss bei der Umsetzung eine klare Zuordnung von Aufgaben und Personen stattfinden um eine klare Aufgabenverteilung zu gew hrleisten Im Falle von sicherheitskritischen Systemen werden die Management Struktu ren normalerweise mit Hilfe von halb formalisierten Methoden beschrieben um eine m glichst unmissverst ndliche Beschreibung zu erhalten Bei der letztendlichen Umsetzung der Qualit tssicherung haben diese drei Punkte eine zentrale Bedeutung 1 Ressourcen Die ben tigten Fachkenntnisse f r jedes Mitglied des Teams werden ermittelt um sicherzustellen dass diese menschlichen Ressourcen verf gbar sind 2 Pr fung Es wird gepr ft ob die Methoden richtig angewendet werden und ob diese erfolgreich sind Dies wird sichergestellt durch das Sammeln von Daten und deren anschlie ende Diskussion Dazu bedarf es unter An derem einer Pr fung von Proben der benutzten Dokumente 3 Qualit tsplan Dieser gibt eine detaillierte Auskunft ber die Ma nahmen der Qualit tssicherung des konkreten Projektes Der Prozess der Qualit tssicherung ist ein notwendiger aber nicht ausrei chender Bestandteil um die Qualit t des Endproduktes zu garantieren Dazu bedarf es auch d
165. nzelnen Punkte aus dem Anforderungskatalog untersucht und deren Umsetzung in Ada erl utert 3 1 Allgemeine Mer male von Ada Die Programmiersprache Ada wird durch die im Kapitel 1 2 bereits erw hnten Standards definiert Eine Validierung eines Ada Compilers gegen den Ada Sprachstandard ist notwendig sonst darf man den Namen Ada nicht verwenden weiterhin sichert die Validierung die Portierbar eit zwischen verschiedenen Compilerherstellern und Hardwareplattformen Ada geh rt zu den Programmiersprachen ber die Objektorientierung und andere moderne Software Engineering Methoden wie Datenkapselung und Information Hiding verbreitet wurden Zudem beherrscht Ada Multitas ing innerhalb eines Programms k nnen mehrere Tasks definiert werden die als selbst ndige Threads laufen Dadurch kann man elegant die Behandlung von asynchronen Ereignissen und Datenstr men programmieren Ada hat definierte Schnittstellen zu anderen Programmiersprachen wie z B C FORTRAN und COBOL Dadurch lassen sich vorhandene Komponenten elegant in ein Programm einbinden 3 2 Reliabilit Fun tionsf hig eit 3 2 1 sichere Datent pen Ada ist eine streng typisierte Sprache implizierte Typkonvertierungen finden nicht statt Datenobjekte werden durch ein Typsystem kategorisiert f r jede Operation ist genau festgelegt welchen Typs die Operanden sein d rfen und welchen Typs das Ergebnis sein wird Das vorgegebene Typsystem kann durch den Programmier nach Bedarf erweiter
166. o modelling specification and verification 2 1 Modelling First of all we convert the system which should be examined into a formalism accepted by a Model Checking tool For the modelling of systems we use finite automats In many cases this is only a compilation task but we should not underestimate this task because if we made any mistake during the conversion it could means that the result of the verification would be worthless In other cases owing to limitations on time and memory the modelling of a design may require the use of abstraction It is not so simply to provide this automat because on the one hand relevant or important points must be represented in the automat on the other hand unnecessary details should be eliminated For example when modelling digital circuits it is useful to reason in terms of gates and Boolean values rather than actual voltage levels Likewise when reasoning about a communication protocol we may want to focus on the exchange of messages and ignore the actual contents of the messages A state is a snapshot or instantaneous description of the system that captures the values of the variables at a particular instant of time We also need to know how the state of the system changes as the result of some action of the system We can describe the change by giving the state before the action occurs and the state after the action occurs Such a pair of states determines a transition of the system The compu
167. o the correctness of the software based systems should be guaranteed Currently testing simulation deductive verification and model checking are four principal techniques for ensuring the correctness of hardware and software systems Simulation and Testing Simulation works with the abstraction of a kind of the system or a model Compared with simulation testing 1s performed on the actual product In both cases Simulation and Testing send the test signal at input point and check the signal at the output signal However It is not enough that we only use tests and Simulation to prove whether a system always hold itself correctly in certain situations On the one hand they can become very expensive and on the other hand in the case of complex asynchronous systems these techniques can cover only a limited set of possible behaviours e Deductive Verification The verification with deductive methods uses a quantity of axioms and proof rules It is quite lengthy very time consuming and can only be used by experts and therefore is rarely used e Model Checking Model checking is an approach to verification where the system to be verified is viewed as a model and the property to be proved of the system is given as a logical formula Model Checking differs from traditional program verification methods mainly in two crucial aspects firstly t does not aim of being fully general and secondly it is fully algorithmic and of low computational compl
168. on Model Checking techniques combined with theorem proving Both model checkers and theorem proves will be needed to establish the correctness of complex circuits Theorem provers seen necessary for reasoning about those parts of a complex microprocessor like the floating point arithmetic unit that require relatively deep mathematical knowledge The problem is how to combine the two very different styles of reasoning into a single framework so that a user can smoothly integrate the results obtained by each 6 Conclusion In this article we give a brief overview of the main system verification techniques with a particular focus on the model checking technique Model checking is an important technique to verify the correctness of software and hardware systems Validation of model checkers s a very important issue due to their automatic nature It can ensure the correctness of critical application such as communication protocol or digital circuit In this article two main tactics separately based on automata theory and symbolic structure for concurrent systems are described and the methods to solve state explosion problem are given Then the methods of model checking for real time systems is introduced and developing trend of Model Checking is analysed The techniques described in this article have already been used to find nontrivial errors in circuit and protocol designs Current model checking tools work sufficiently well to be of use in industry
169. on Prozessoren entwickelt sich wie bisher schneller als die von Arbeitsspeichern Deshalb ist der Einsatz von Caches notwendig die schneller und kleiner sind als Arbeitsspeicher Da Prozesse meist nur auf einen kleinen Teil im Arbeitsspeicher zugreifen kann dieser Teil im Cache gehalten werden und so wesentlich schneller auf die Informationen zugegriffen werden Wechselt das Betriebssystem nun zu h ufig die Prozesse und greifen diese Prozess auf v llig verschiedene Arbeitsspeicherbereiche zu so liegt der Bereich f r einen Prozess oft nicht im Cache und es mu auf den langsameren Arbeitsspeicher zugegriffen werden 2 2 Optimierungen konventioneller Betriebssysteme Einem Betriebssystem hat wie in Abschnitt 2 1 aufgefihrt viele Aufgabe zu erledigen Dabei soll ein Betriebssystem aber auch einen m glichst weiten Einsatzbereich haben Das hat zur Folge da Betriebssysteme auf den durchschnitt lichen Fall hin optimiert werden Dabei betrachtet man folgende Zielsetzungen Maximale Ressourcenauslastung Jede Ressource im Rechner soll bis an die durch die Hardware gesetzte Grenze ausgelastet werden Beispielweise sollte eine Datei ber ein 100 MBit Netzwerk mit 10 MByte s bertragen werden oder von einer Festplatte die eine Lesegeschwindigkeit von 10 MByte s hat sollte mit 10 MByte s gelesen werden k nnen weil der Anwender darauf wartet das die bertragung abgeschlossen wird Um dies zu erreichen mu das Betriebssystem immer zum richtigen Ze
170. on of the search engine of the model checker by performing the reduction at the level of the system specification that 1s syntactically The subset of the states that need to be explored is thus determined before the actual searching takes place In the purely partial order approach the construction of the interleaved expansion of parallel components is avoided by directly constructing a partial order representation of the state space from the system specification An interleaving representation is thus never generated and needs never to be stored 3 2 Based on Symbolic Structure In the fall of 1987 McMillan a graduate student at Carnegie Mellon University realized that by using a symbolic representation for the state transition graphs which based on the use of BDD Binary Decision Diagrams much larger systems could be verified A state of the system is symbolically represented by an assignment of boolean values to the set of state variables A Boolean formula and thus its BDD is a compact representation of the set of the states represented by the assignments which make the formula true The transition relation can therefore be expressed as a boolean formula in terms of two sets of variables one set encoding the old state and the other encoding the new This formula is then represented by a binary decision diagram Then Model Checking algorithm is based on computing fixpoints The fixpoints are sets of states that represent various
171. orderungen Safety Sicherheit Correctness Korrektheit Trustability Vertrauensw rdigkeit e Nicht Fun tionale S stemanforderungen Reliability Funktionsfahigkeit Availability Verf gbarkeit Performance Leistung Zuverl ssigkeit Dependability e Interne S stemanforderungen Entwicklung o Understandability Verst ndlichkeit o Testability Testbarkeit o Vertfiability Verifizierbarkeit Wartung o Recoverability Wiederherstellbarkeit o Maintainability Wartbarkeit o Extendability Erweiterbarkeit Wiederverwendbarkeit Die funktionalen Systemanforderungen sind erst mal fiir die Untersuchung von Ada nicht von primarer Bedeutung da sie das Gesamtsystem beschreiben Bedeutungsvoll sind die nichtfunktionalen und internen Systemanforderungen Sie beschreiben einzelne Anforderungen die alle Systemkomponenten im einem sicherheitskritischen System erf llen sollten sei es Soft oder Hardware Fur die Untersuchung einer Programmiersprache sind die Anforderungen etwas zu grob klassifiziert sie m ssen etwas feiner unter Ber cksichtigung Softwaretechnischer Gesichtpunkte graduiert werden Milit rischen Angaben laut der Webseite http page mi fu berlin de vratisla Militinf militinf htm 2 2 Allgemeine Anforderungen an eine Programmiersprache nach arr Carr nannte 1 O Carr 0 sechs Kriterien die f r die Eignung bzw den Einsatz von Programmiersprachen in hoch integrierten Systemen besonders
172. osition des Buchstabens in der Zeichenkette E3 Der Buchstabe wird in der Zeichenkette nicht gefunden Der Verhaltnis der semantische Inhalt wird wie folgt beschrieben Wenn C1 und C2 dann E2 Wenn C1 und nicht C2 dann E3 Wenn nicht C1 dann El Im n chstens Schritt wird der Graph entwickelt Die Ursacheknoten werden auf einem Blatt Papier links und die Wirkungsknoten rechts notiert A Der n chste Schritt ist Entscheidungstabelle zu bilden Testfall TI T2 ci a En 0 E2 E3 id T1 T2 T3 sind Testf lle El E2 E3 sind die Wirkung effect C1 C2 sind die Ursache cause O stellt den Zustand nicht vorhanden falsch dar 1 stellt den Zustand vorhanden wahr dar stellt den Zustand do not care olol lola un m Der Tester kann die Entscheidungstabelle benutzen um das Programm zu testen Zum Beispiel Wenn die vorhandene Zeichenkette abcde ist sind die m glichen Testfalle wie folgt Der zu suchende Ausgabe Buchstabe C 3 W Nicht gefunden Out of range Die Vorteile von Ursache Wirkungs Graph 1 Der Graph der von der Spezifikation abgeleitet wird erlaubt eine vollst ndige Kontrolle der Spezifikation 2 Unbest ndigkeiten Ungenauigkeiten werden leicht ermittelt 3 Beziehungen und Wechselwirkungen zwischen Werten werden behandelt und die Schw che von Aquivalenzklassenbildung und Grenzwertanalyse werden damit abgedeckt Die Nachteile von Ursa
173. ozesse wurde eine Laufzeit von 300us angegeben so da das System nahezu vollausgelastet ist KURT verweigert gem seinem Plan das Starten von weiteren Prozessen um das System nicht zu berlasten Der FIFO Scheduler l t auch bei Vollauslastung weitere Prozessen zu 100 T T T T Tr 7 Fij T T 100 T T T T 100 T gt E H m 1 process J fo ee 1 process fo fo mm 1 process 90 oe 10 processes 90 10 processes 90 gt 10 processes po 20 processes 20 processes SS 20 processes ie e 30 processes 30 processes f fo ees 30 processes 80 ea 4 80 4 80 4 r pe 70 IR 4 70 70 y sot i 4 2 60 2 sol 4 c c gt gt gt 7 0 50 4 0 50 J t O J O O a 40 al 1 40 AS 40 a ze t 30 a 4 30 4 30 4 if 20 ww 4 20 4 20 7 I t 10F et i 4 10F 7 10 4 A oe 0 gt al 1 1 1 1 0 1 fi 1 1 0 1 fi 1 1 i 1 1 fi 5 6 7 8 9 10 11 12 13 14 15 5 6 7 8 9 10 11 12 13 14 15 5 6 7 8 9 10 11 12 13 14 15 Time difference between consecutive loops milliseconds Time difference between consecutive loops milliseconds Time difference between consecutive loops milliseconds a FIFO b KURT SCHED_KURT_PROCS Mode c KURT SCHED_ALL_PROCS Mode Abbildung 10 Effektivitat der Scheduler im Vergleich Abbildung 10 zeigt nochmal die Genauigkeit des FIFO Scheduler im Vergleich zum KURT Scheduler wo
174. ozessen mit der gleicher Priorit t derjenige auf den Prozessor gelassen der zuerst gekommen ist Dieser bleibt solange auf dem Prozessor bis er sich beendet Bei SCHED_RR werden Prozesse mit der gleichen Priorit t nach dem Round Robin Verfahren f r jeweils eine Zeitscheibe auf den Prozessor gelassen Alle Prozesse werden in der gleichen Warteschlange eingereiht so da der Scheduler die gesamte Warteschlange durchsuchen mu um einen Proze Rechenzeit zuteilen zu k nnen Somit hat der Scheduler von Linux eine Kom plexit t der Klasse O n 3 Wie kann man Realzeitbetriebssysteme implementieren Die Theorie fiir Realzeitsysteme hat vier verschiedene Ansatze hervorgebracht Diese vier verschiedene Paradigmen nach denen man Scheduling in Echtzeitbetriebssystemen realisieren kann sehen wie folgt aus 1 Das Scheduling wird anhand von statischen Eintragen gemacht Diese werden bei der Implementierung des gesamten Realzeitsystems berechnet wobei die Laufzeiten und die Deadlines aller Echtzeitprozesse berticksich tigt werden Zur Laufzeit laBt sich an dem Scheduling nichts mehr verandern Dies hat ein statisches System zur Folge was f r KURT nicht in Frage kommt 2 Der zweite Ansatz verwendet Prioritaten und preemptives Scheduling Zu diesem Ansatz zahlen die Ver fahren Rate Monotonic und Earliest Deadline First Rate Monotonic vergibt die Priorit ten proportional zur Laufzeit eines Prozesses w hrend Earliest Deadline First die
175. pression evaluation errors 2 4 Chara teristische Mer male einer Prog sprache nach Cull er Cullyer untersuchte 1 0 mehrere Programmiersprachen mit dem Ziel rauszufinden welche der gegebenen Sprachen sich besonders f r den Einsatz in hoch integrierten Systemen eignet Er differenzierte einige ausgew hlte Programmiersprachen nach folgenden Faktoren willk rliche Spr nge wild Jumps berschreibung overwrites eindeutige Semantik semantics strenges mathematisches Modell model of maths arithmetische Laufzeit berwachung operational arithmetic sichere Datentypen data typing Ausnahmenbehandlung exception handling sicheres subset safe subset Speicher berwachung exhaustion of memory separate Paket bersetzung separate compilation gut verstandlich well understood gt es war mir leider nicht m glich sein Artikel The Choice of Computer Languages for use in Safety Critical Systems zu beschaffen 2 5 Anforderungs atalog an eine Programmiersprache f rS S Diese Merkmale zusammengefasst erstellen ein Anforderungskatalog mit welchem die Programmiersprache Ada bez glich der Eignung f r den Einsatz in sicherheitskritischen Systemen untersuchen werden kann 1 Reliabilit Fun tionsfahig eit sichere Datentypen data typing willk rliche Spr nge wild Jumps berschreibung overwrites 2 Availabilit Verf gbar eit logische G ltigkeit logical soundness Initialisierungsfehler initial
176. ption erreicht was durch den Methodenaufruf interrupt auf einen RealtimeThread oder fire auf die AsynchronouslyInterruptedException e Durch den asynchronen Kontrolltransfer ist es m glich einen sichereren Threadabbruch zu haben wie mit der stop oder destroy Anweisung Denn stop ist veraltet und destroy ist unsicher da es den Speicherbereich nicht wieder frei gibt e Bei der Modellierung des asynchronen Kontrolltransfer als Exception muss darauf geachtet werden dass nur der gew nschte Handler und nicht irgendwelche Universal Handler ange sto en werden e In geschachtelten Threads die einen Asynchronen Kontrolltransfer erlauben darf der Innere nichts vom u eren wissen aber der Innere darf durch den u eren unterbrochen werden sobald dies der Innere gestattet Prinzip der Datenkapselung muss erhalten bleiben 3 6 Asynchronous thread termination In dem normalen Java ist es schwierig einen Thread sauber zu unterbrechen Dies ist zum Beispiel dann n tig wenn sich durch ein u eres Ereignis die Parameter f r den gerade in Berechnung befindlichen Thread se ndert haben und diese Berechnung nun so berfl ssig ist Es gab den Befehl stop aber dieser konnte bei Ausf hrung Objekte im Speicher zur ck lassen Der andere Befehl destroy kann hingegen zu Deadlocks f hren wenn gerade dieser Thread alle anderen blockiert Aber durch die RTJ Erweiterung kann man den Thread bei einem asynchronen Ereignis mittels
177. r Graph entspricht einer Schaltung der Digitallogik Es sind dabei nur die Operatoren aus der Booleschen Algebra als Vorkenntnisse notwendig Beispiel fiir die Notation eines Ursache Wirkungs Graphs Identit t NOT Jeder Knoten kann den Wert 0 oder 1 annehmen Die Funktion der Identit t besagt wenn a 1 ist dann b 1 ist ansonsten b 0 Die NOT Funktion besagt wenn a ist dann b 0 ist ansonsten b 1 Die AND Funktion besagt wenn a 1 und b 1 sind dann c 1 ist ansonsten c 0 Die OR Funktion besagt wenn a oder b oder c 1 ist dann d 1 ansonsten d 0 Die Testf lle werden wie folgt entwickelt 1 Der Tester muss die komplexe Spezifikation der Software in kleinere Stiicke zerlegen Zum Beispiel ein Programm in einzelne Methoden 2 Der Tester muss Ursachen und Wirkungen der Spezifikation festlegen Eine Ursache ist eine Eingangsbedingung oder eine Aquivalenzklasse von Eingangsbedingungen Eine Wirkung ist eine Ausgangsbedingung oder eine Systemtransformation eine Nachwirkung die die Eingabe auf den Zustand des Programms oder Systems hat Ursachen und Wirkungen werden definiert indem man die Spezifikation Wort f r Wort liest und alle Worte die Ursachen und Wirkungen beschreiben unterstreicht 3 Der semantische Inhalt der Spezifikation wird analysiert und in einen booleschen Graphen transformiert Die Ursache wird in die linke Seite des Graphs geschrieben und die Wirkung in die rechte Seite d
178. r a part of the state space and the combination of the sub properties implies the required global property Efficient algorithms for compositional verification can extend the applicability of formal verification methods to much larger and more interesting systems The compositional Reasoning technique exploits the modular structure of systems composed of multiple processes running in parallel To simplify the specification of such a system the specifications for such systems can often be decomposed into properties that describe the behaviour of small parts of the system An obvious strategy is to check each of the local properties using only the part of the system that it describes Then the complete system must satisfy the overall specification if each local property holds and if the conjunction of the local properties holds For Example we verify a communication protocol that is modelled by three definite state processes a transmitter some type of network and a receiver Suppose that the specification for the system 1s that data is eventually transmitted correctly from the sender to the receiver Such a specification might be decomposed into three local properties First the data should eventually be transmitter to the network Second the data should eventually be transferred correctly from one end of the network to the other Third the data should eventually be transferred correctly from the network to the receiver We might be able to verify t
179. rderungsanalyse und Modellierung von Geschaftsprozessen noch unabh ngig von der Z elplattform arbeiten k nnen Die MDA ist ein Schl ssel Konzept von OMG zur Modellierung von u a Softwaresystemen welche durch eine klare Trennung von Abstraktionsschichten die Wiederverwendbarkeit und Langlebigkeit der Modelle erm glicht Einer der wesentlichen Ziele von MDA ist es die Technologien wie CORBA XML J2EE und Net zu integrieren um so die Portabilit t von Software auf verschiedenen Plattformen unterst tzen zu k nnen Mit der MDA wird versucht die L cke zwischen Modellen und Quelletexten zu schlie en Die MDA beschreibt Modelle mit Hilfe der UML und unterscheidet zwischen zwei wichtigen Modellen bez glich ihrem Abstraktionsgrad PIM oder PSM Die PIM Modelle enthalten formale Spezifikationen der Strukturen und Funktionalitaten des Systems die von technischen Details abstrahieren Die PSM Modelle werden aus dem PIM anhand vorgegebener Transformationsregeln und schritte abgeleitet Ein weiteres zentrales Element von MDA ist das Mappen zwischen Modellen Die MDA erm glicht Modelle zwischen den verschiedenen Geschaftsbereichen oder zwischen den Modellebenen aufeinander abzubilden engl Mapping Das Mappen kann je nach Realisierungsgrad des MDA Konzeptes automatisch verlaufen Die Abbildung 2 stellt eine Metamodell Beschreibung der MDA dar MDA wird von verschiedenen Case Werkzeugen u a Rational Software von Rational Rose Visio von Micro
180. ren spielen hier die CPU Caches eine Rolle Mu die CPU Daten oder Befehle aus dem Arbeitsspeicher anstatt of events bh o T 0 l N weh 0 10 20 30 40 50 60 70 80 90 100 Difference between Scheduled Time and Timer Dispatch microseconds Abbildung 5 Zeitmessung vom Interrupt zur eingeplanten Routine Distribution of Time Between Scheduled Event and Actual Event Frequency 0 10 20 30 40 50 60 70 80 90 100 Time between Scheduled Event and Actual Execution microseconds Abbildung 6 Zeitmessung vom Interrupt zur eingeplanten Routine Verbesserung aus dem Cache lesen so wirkt sich dies auf die Laufzeit aus Die maximale Zeit von 504s mu bei der Planung von Deadlines f r Echtzeitprozesse ber cksichtigt werden Die Abbildung 6 zeigt die Verz gerung vom Interrupt bis zum Eintritt in die zum Timer zugeh rige Funktion nach der Verbesserung der Architektur Durch die Beschleunigung der TISR wird die Verz gerung deutlich verkleinert 3 2 3 Realzeitscheduling mit KURT KURT ist in zwei Teile aufgeteilt und zwar in den KURT Core und die RT Mods KURT Core Der Kern von KURT ist f r das Scheduling der Echtzeitevents RT Events zust ndig Er startet das entsprechende RTMod zur entsprechenden Zeit Um dies zu erreichen wird das Scheduling mit Hilfe eines eindeutigen Plans durchgefuhrt Es handelt sich also um einen sogenannten explicit plan scheduler Dieses Paradigma wurde gewahlt weil er zur Zeit d
181. rreicht worden unter anderem auch durch gro angeleg te Tests mit reellen Radardaten Eine Studie des Center for Advanced Aviation System Development kam 1994 zu dem Schluss dass die Verwendung von TCAS die Wahrschein lichkeit einer beinahen Kollision um 90 bis 98 Prozent verringert caasd Die BFU hat als Reaktion auf diese Katastrophe eine Empfehlung herausgegeben dass in Zukunft die Piloten bei wiederspr chlichen Anweisungen von TCAS und der Bodenkontrolle den An weisungen des TCAS Systems folgen sollen Empfehlung BFU Dies soll international durchgesetzt werden ausserdem erhalten die Piloten hnliche Anweisungen in den entspre chende Sicherheitsvorschriften der Fluggesellschaften Weitere Aufschl sse zum Ungl ck k nnte der offizielle Untersuchungsbericht geben der Mitte 2004 herausgeben werden soll Verz gerung BFU Bei der Schweizer Flugsicherung ist die Anzahl der Fluglotsen in der Nachtschicht erh ht worden auch stehen jetzt Notfall Handys zur Verf gung Skyguide DasErste Dadurch kann hoffentlich in Zukunft ein hnliches Ungl ck vermie den werden Literatur Storey Giese Schneier allstar eddh aerowinx caasd Stuttgarter Zeitung Untersuchungsbericht BFU Empfehlung BFU Verz gerung BFU Verwechslung Tagesschau bergabe Tagesschau Skyguide DasErste Meldung Heise Schaden ZDF Leistung ZDF Report US Canada Taskforce GE Energy XA 21
182. rsucht wurde stellte es sich heraus dass die Schwachstellen und die Fehler an der Software lagen Fazit Die Software der Maschine vor allem die kritischen Komponenten m ssen ausreichend getestet werden und d e Fehlermeldungen m ssen verst ndlich und lesbar dokumentiert werden 2 Verifikation Validierung und Testen In diesem Seminar wird das Thema Verifikation Validierung und Testen von sicherheitskritischen Systemen behandelt Diese Ausarbeitung wird sich vor allem auf das Testen von sicherheitskritischer Software konzentrieren Definition 2 1 Die sicherheitskritische Software Die sicherheiskritische Software ist Software deren Ausfall eine Auswirkung auf die Sicherheit haben k nnte oder gro en finanziellen Verlust oder sozialen Verlust verursachen k nnte 9 Definition 2 2 Verifikation Verifikation ist der Prozess des berpr fens der sicherstellt dass die Ausgabe einer Lebenszyklusphase die durch die vorhergehende Phase spezifizierten Anforderungen erf llt 9 Definition 2 3 Validation Validation ist der Prozess des Best tigens dass die Spezifikation einer Phase oder des Gesamtsystems passend zu und konsistent mit den Anforderungen des Kunden ist 9 Nach der Definition sind Verifikation und Validierung nicht dasselbe Der Unterschied zwischen ihnen wurde nach Boehm 1979 so ausgedr ckt Validierung Erstellen wir das richtige Produkt Verifikation Erstellen wir das Produkt richtig D
183. rt werden so da der Scheduler in der Lage ist ein berladen der CPU zu verhindern Passen die Zeitpunkte f r RTEvents oder die Abarbeitungszeit f r einen neuen RT Proze nicht mehr in den Plan so wei t KURT diesen neuen Proze zur ck Die Weiterentwicklung der Architektur erm glichte zus tzlich zu den zeitgesteuerten RT Prozessen eventges teuerte Eventgesteuert ist ein Proze dann wenn er vom Betriebssystem so lange blockiert wird bis das betreffende Ereignis eintrifft KURT nimmt eventgesteuerte Prozesse ohne Pr fung des Scheduling Plans an Erst in dem Moment in dem das Ereignis eintrifft pr ft der Scheduler ob im Plan ausreichend Rechenzeit f r den eventgesteuerten RT Proze frei ist und f hrt ihn gegebenenfalls aus Ist nicht ausreichend Rechenzeit vorhanden so bleibt der RT Proze bis zu einer L cke oder bis zu einem Timeout blockiert Wurde ein neuer RT Prozess erfolgreich von KURT angenommen so legt der Kern f r die RT Events Timer im Linuxkernel an wobei dieser Timer 50us vor dem RT Event gesetzt wird Sollte der Eintritt in den RT Proze vor schneller als in 50us erreicht werden so wird der TSC der CPU verwendet um den Eintritt bis zum eigentlichen RT Event zu verz gern Dieses wird gemacht weil die Zeiten vom Timerinterrupt bis zum Eintritt in den RT Proze wie oben beschrieben unterschiedlich sein k nnen Diese Schwankungen m ssen weitesgehend unterdr ckt werden Betriebsmodi Prim r werden zwei Betrieb
184. rund der groBen Anzahl von Kombinationen unm glich ist ist es wichtig einen Testplan aufzu stellen Hierbei m ssen die notwendige Testabdeckung und die verwendeten Methoden spezifiziert werden und im Anschluss darauf berpr ft werden ob sie f r die ben tigte Integrit t des Systems ausreichend sind gt Mit korrekt sind hier auch die Eigenschaften vollst ndig und konsistent gemeint Ausreichendes Testen beginnend von der Entwicklungsphase tiber die Validierung des Designs bis zur Fertigung des Entwurfes ist sehr wichtig um ein SkS mit ausreichender Verl ssichkeit zu entwickeln 1 7 Fehlerkennung Man benutzt Fehlererkennung um Probleme im fertigen System w hrend dem Betrieb zu erkennen so dass sie m glichst wenig Auswirkungen auf seine Funktion haben Zu diesen Techniken geh rt beispielsweise das Verwenden von Informationsredundanz Hardware berwachung durch Watchdog timer und eine allgemeine Funktionspr fung durch einge baute Pr froutinen beim Start 1 8 Fehlertoleranz Fehlertoleranz soll einen st rungsfreien Betrieb trotz dem Auftreten von Fehlern sicher stellen Die gebr uchlichste Methode um dies sicherzustellen ist das verwenden von Red undanz Bei der Hardware unterscheidet man zwischen der statischen Rendundanz wobei meh rere gleiche Hardwarekomponenten ber einen Entscheider mit dem Ausgang verbunden werden Der Entscheider maskiert das Ausfallen von not Modulen danach beintr ch tigt
185. rung 2 1 Einleitung Qualit tssicherung ist auf jeden Fall ein wichtiger Bestandteil um die Qualit t eines Produktes sicherzustellen In manchen Industrien ist die Qualit tssiche rung allerdings nicht ausreichend um ein Produkt an den Markt zu bringen So ist es in der Luftfahrtindustrie zum Beispiel nur dann erlaubt ein Flugzeug im Luftverkehr einzusetzen wenn dieses zuvor ein Luftt chtigkeitszertifikat erhalten hat In anderen Industrien sind Zertifikate nicht unbedingt notwendig doch es ist eindeutig erkennbar dass zertifizierte Produkte klar erkennbare Vorteile beim Marketing besitzen Doch was bedeutet Zertifizierung genau Als Zertifizierung bezeichnet man den Prozess der Ausgabe einer geschriebenen Versicherung Das Zertifikat durch eine unabh ngige externe Organisation um die bereinstimmung mit einem Standard einem Satz von Richtlinen oder eines hnlichen Dokumentes nachzuweisen Die Zertifizierung wird meist von staatlichen Beh rden oder von national ange sehenen Organisationen durchgef hrt um eine m glichst gro e Vertrauensbasis zu schaffen In manchen Industrien gibt es Regulierungsbeh rden die die Pro duktion berwachen und f r die Ausgabe von Zertifikaten verantwortlich sind Hervorzuheben sind hier die Luftfahrt und Atomindustrie Um ein Zertifikat zu erhalten muss der Entwickler in der Lage sein zu zeigen dass alle wichtigen Gefahren identifiziert wurden und entsprechende Ma nah men zu der
186. s als RTMod im plementiert so befindet sich der RT Proze innerhalb eines Kernelmoduls Dieses Kernelmodul kann zur Laufzeit zum of events of events 0 1 1 1 i 1 1 1 1 2 3 4 5 6 7 8 9 10 2 3 4 5 6 7 8 9 10 Duration of Disabled Interrupts microseconds Duration of Disabled Interrupts microseconds a Console b Network of events of events 9 10 Sa 140 160 180 200 0 0 20 40 60 80 1 2 3 4 5 6 7 8 Duration of Disabled Interrupts microseconds Duration of Disabled Interrupts microseconds c Disk d Process Management 8 Abbildung 7 Dauer der Sperrung von Interrupts Kernel hinzugeladen werden Es ergeben sich dadurch eine Reihe von Vorteilen die sich positiv auf das zeitliche Verhalten der Prozesse auswirken e RT Mods werden als Kernelmodule im gleichen Adressraum wie der Linuxkern ausgef hrt Dadurch entf llt der Kontextwechsel zwischen Kernelfunktionen und Funktionen des RTMods Die Zeiten vom Timerinterrupt bis zum Eintritt in das RI Mod wird k rzer e Das RTMod wird im Kernel Mode ausgef hrt so da auf Befehle der CPU zur ckgegriffen werden kann die nur im Kernel Mode zur Verf gung stehen e Ein RT Mod kann auf alle Services der Linuxkernels zugreifen Dieser Zugriff ist schneller weil der Kontextwech sel vermieden wird und es kann auf Funktionen zugegriffen werden die einem normalen User Mode Proze nicht zur Verf gung stehen
187. s the door is open the microwave oven does not work After someone closes the door state S1 will go to state S2 at that time 1f someone pushes the start up button the microwave oven will begin to work and go to state S3 It s not allowed that the microwave oven starts to work before he closes the door because it is very dangerous But if someone pushes the start up button before he closes the door the microwave oven will not work and go to state S4 Only after he closes the door the microwave oven will go to state S1 and in state S1 the microwave oven will begin to work only after he pushes the start up button again After cooking the microwave oven will go from state S3 back to state S2 And after opening the door the microwave oven will go from state S2 back to state S1 Figure Automat Graph of the Kripke Structure M of microwave oven Close Start Cooking Open the door Close the door Close 5 Start Cooking Close Close the door Start en Finish CRO Cooking Figure Automat Step 2 Specification with CTL Formal possible requirements of the microwave oven 1 Every time after someone pushes the start button the microwave oven begins to cook lt gt AG start gt AF cooking 2 If the door is closed and someone pushes the start button the microwave oven begins to cook lt gt AG close A start gt AF cooking Step 3 To the first CTL Formal Every time after someone pushes the
188. sf hrlich behandelt wird das Interaktions bersichtsdiagramm und das Kompositionsstrukturdiagramm Abbildung 1 zeigt eine bersicht ber alle Dia grammtypen der UML Diagramme der UML Struktur ME a i Verhaltens diagramme diagramme Klassen ree Aktivitats Use Case diag ramm be diagramm Diagramm Verteilungs Zustands diagramm automat Komponenten diagramm Paketdiagramm Timing Diagramm Abbildung 1 Die Diagrammtypen der UML 2 1 Neuerungen in der UML 2 im berblick Die meisten nderungen haben die Aktivit tsdiagramme erfahren Sie basie ren nun auf erweiterten Petri Netzen Durch die nderungen erh ht sich die Flexibilit t bei der Flussmodellierung Fur Verhaltensdiagramme steht alternativ zur grafischen Darstellung nun eine tabellarische Darstellung zur Verf gung Das Kollaborationsdiagramm wurde in Kommunikationsdiagramm umbenannt Bei Klassendiagrammen wurden einige Unsauberkeiten entfernt Sie bleiben allerdings gr tenteils unver ndert Sequenzdiagramme sind strukturier und zerlegbar Verteilungsdiagramme zeigen die Laufzeitaspekte einer Architekturumset zung Kommunikationsbeziehungen zwischen Einzelkomponenten Das neu eingef hrte Kompositionsstrukturdiagramm zeigt Interna von System teilen und deren Zusammenspiel in Form von Laufzeitinstanzen Ebenfalls neu eingef hrt wurden die aus der Elektrotechnik bekannten Timing Diagra
189. sich dabei haupts chlich auf Teile eines Systems bei denen ein Fehler im zeitlichen Verhalten zu einem kritischen Fehlverhalten des kom pletten Systems f hrt Meist ist es aus technischer Sicht unm glich das ge samte System mit Hilfe von Timing Diagrammen zu modellieren Das Timing Diagramm kann dabei immer nur den idealen Ablauf wiederge ben F r Alternative oder Parallele Abl ufe sieht die UML 2 keine Notations elemente vor 5 4 Notationselemente 5 4 1 Interaktion Interaktionsrahmen Das Timing Diagramm wird von einem rechteckigen Rahmen umgeben Der Name der Interaktion steht in einem F nfeck in der rechten oberen Ecke Der Rahmen umschlie t das komplette Diagramm Wenn das Diagramm nur eine Komponente enth lt ist der Rahmen gleichzeitig die Lebenslinie der Komponente F r die Darstellung konkreter Zeitpunkte und Zeitdifferenzen kann auf der unteren Linie des Rahmen ein Zeit skala aufgetragen werden Abbildung 6 zeigt einen Interaktionsrahmen mit Zeitskala r 3 5 7 Min Abbildung 6 Interaktionsrahmen eines Timing Diagramms mit Zeitskala 1 9 4 2 Lebenslinie Die Lebenslinie ist keine einfache Linie sondern ein Bereich Mehrere Lebenslinien werden durch durchgezogene horizontale Linien getrennt siehe Abbildung 7 m Abbildung 7 Notation von Lebenslinien in Timing Diagrammen 1 Jede Lebenslinie entspricht genau einem Teilnehmer einer Interaktion Sie muss den Namen des Kommunikationspartners enthalten
190. smodi in KURT eingesetzt Es gibt den normalen Modus in dem der Kernel Realzeit prozesse nicht ber cksichtigt und wie gewohnt den Time Sharing Scheduler f r konventionelle Prozesse einsetzt und es gibt den Realzeitmodus in dem ber den Plan Realzeitprozesse und ber den Time Sharing Scheduler konven tionelle Prozesse ausgef hrt werden Bei der Implementierung wurde festgestellt da einige Subsysteme im Kernel f r recht lange Zeitr ume Interrupts sperren Die Abbildung 7 zeigt die Messungen diesbez glich Es f llt besonders das Disk Subsystem mit Sperren der Interrupts f r bis zu 250s auf Folglich ist ein Proze in der Lage beim Zugriff auf Datentr ger den Timerinterrupt f r maximal 250us zu blockieren und somit evtl die Ausf hrung von Echtzeitprozessen zu st ren Damit der Entwickler dies unterbinden kann kann das Scheduling eingestellt werden Wird f r den Echtzeitscheduler SCHED_KURT_PROCS angegeben so wird die Ausf hrung von normalen Prozessen deaktiviert w hrend bei SCHED_ALL_PROCS normale Prozesse neben Echtzeitprozessen laufen d rfen Es stellte sich jedoch heraus da diese Unterteilung zu grob war und die Verbesserung der Architektur bringt die M glichkeit mit sich einzelne Subsysteme des Kernels zeitweise zu deaktivieren Damit kann der Entwickler genauer die Abl ufe im Realzeitsystem steuern RTMods und Process RTMod KURT bietet zwei M glichkeiten um Realzeitprozesse zu implementieren Wird der Realzeitprozes
191. soft und Poseidon von Gentleware unterst tzt lt lt Mapping von PIM zu PIM gt gt lt lt beschrieben mit gt gt rgestellt mit gt gt gt lt lt tellt mit gt gt lt lt lt m lt lt beschrieben mit gt gt lt lt Mapping PSM zu PSM gt gt lt lt unabh ngig von gt gt pping von lt lt Refact zu PSM gt gt PSM zu PIM gt gt aan lt lt h ngt ab von gt gt Abbildung 2 detaillierte Beschreibung der MDA 3 2 MOF Dadurch sollen sich Modelle und Metamodelle besser zwischen verschiedenen Werkzeugen austauschen lassen Ziel ist es Entwicklern und Designer eine gr ere Freiheit bei der Auswahl der verwendeten Tools zu erm glichen Die Meta Object Facility MOF ist eine abstrakte Beschreibungssprache die zur Erstellung und Verwaltung von plattform unabhangigen Metamodellen dient Beispiele solcher Metamodelle sind die UML und MOF selbst Dadurch sollen sich Modelle und Metamodelle besser zwischen verschiedenen Tools austauschen lassen Ziel ist es dabei den Entwicklern und Designern eine gr ere Freiheit bei der Auswahl der verwendeten Tools zu erm glichen Es gibt verschiedene Arten von Modellen die verschiedene Aspekte der Softwaresysteme beschreiben Um die Portabilitat dieser Modelle untereinander zu gew hrleisten braucht man eine eindeutige und einheitliche Spezifikationen um diese Modellierungssprachen z
192. spect to a fixed path Compare with CTL the LTL is perhaps more intuitive and can express some properties CTL cannot and vice versa We can translate LTL to Buchi automata And it is Linear because conceptually it s only about paths as opposed to computation trees CTL where paths can branch These 3 different variants of the Temporal Logic differ particularly in the availability of the temporal operators and path quantifiers as well as in the semantics of these operators So they will be applied in different ranges of hardware or software application area An important issue in specification is completeness Model checking provides means for checking that a model of the design satisfies a given specification but it is impossible to determine whether the given specification covers all the properties that the system should satisfy 2 3 Verification After we finish all preparations the Model Checking can begin Now one must decide whether for the given model of a system the Kripke structure and the specification with Temporal Logic are valid According to temporal logic we have CTL Model Checking CTL Model Checking and LTL Model Checking Finite state model Error trace Model Checker eS gt Line 5 _ Temporal logic formula Ba Line 13 Line 21 _ Ideally the verification is completely automatic However in practice it often involves human assistance One such manual activity s the analysis of the verific
193. sse keinen Fehler entdeckt so erwartet man dass alle anderen Testf lle keine Fehler entdecken Wir betrachten das erste Beispiel Das Testprogramm sieht so aus COPYRIGHT 1994 by George E Thaller All r ghts reserved Function Black Box Equivalence Partitioning include lt stdio h gt main int 1 z day month year printfC nTAG MONAT WOCHENTAG n n Test Case day 22 month 6 year 1994 Z week_d day month year printf 2d 2d ld n day month z Test Case 2 day 19 month 5 year 1994 Z week_d day month year printf 2d 2d ld n day month z Das Modul wird mit der folgenden Anweisung aufgerufen week_d day month year Wir interessieren uns nicht im Sinne eines Black Box Tests wie der Quellcode dieses Moduls aussieht und wie das Ergebnis berechnet wird Das Datum eines Tages wird als Parameter gegeben und das Ergebnis ist eine Zahl als Wochentag der Sonntag bekommt die Zahl 0 der Montag bekommt die Zahl 1 und dann so fort bis Samstag Wenn dieses Testprogramm ausgef hrt wird werden die folgenden Ergebnisse geliefert TAG MONAT WOCHENTAG 22 6 3 19 5 4 Wenn wir in den Kalender ansehen wissen wir dass die beiden Werte in Ordnung sind Es werden eine giiltige Aquivalenzklasse und zwei ungiiltige Aquivalenzklassen fiir den Monat im obigen Beispiel gebildet Eine giiltige Aquivalenzklasse l lt m lt 12 Zwei ung lti
194. st dagegen unkritisch weil bei den Funktionen nur die bergabeart IN f r die Parameter bergabe zugelassen ist und die kann wie schon bereits beschrieben keine Seiteneffekte ausl sen Bestandteil von Annex H Safety and Security 3 5 3 Speicher ber achung exhaustion of memor Die Speicher berwachung in Ada bernimmt der Ausnahmenmechanismus Alle Probleme mit der Speicherzuweisung werden der Ausnahme Storage_Error zugeordnet Die Ausnahme kann vornehmlich bei Speicherallokierung durch den NEW Operator auftreten wenn der Platz auf dem Heap bereits ersch pft ist Die Situation kann ebenfalls auftreten wenn bei einem Unterprogrammaufruf der ben tigte Speicherplatz f r lokale Variable nicht mehr vorhanden ist Die dynamische Speicherverwaltung stellt eine der gr ten Schwachstellen f r sicherheitskritische Systeme dar Wenn immer m glich sollte nach der Startup und Initialsierungsphase des Programmes auf dynamische Instanziierung verzichtet werden 3 6 Understandabilit Verstandlich eit Ada setzt an die Entwickler keine hohen Kompetenzen bez glich der Codeverstandlichkeit was ja eigentlich eine subjektive Meinung eines Programmierers ist Die Sprache besitzt einfache Definitionen und liefert einen ausdruckstarken Quellcode 3 Testabilit Testbar eit Verifiabilit Verifizierbar eit Ada Compiler f hrt Extensive Checks w hrend der Kompilierzeit durch Dies f hrt dazu dass die normalen Fl chtigkeitsfe
195. stem Linux an die Anforderungen an Echtzeitsysteme anpa t 2 Warum ist nicht jedes Betriebssystem echtzeitf hig Um in Anwendungen in Echtzeit auf Ereignisse reagieren zu k nnen oder um Daten in Echtzeit bereitzustellen re ichen nichtechtzeitf hig oder auch konventionelle Betriebssysteme oft nicht aus Aufgrund der immer wieder gesteigerten Rechenleistung sind heutige Personalcomputer PC in der Lage komprimierte Musikinformationen in Echtzeit zu dekomprimieren und wiederzugeben Dennoch sind jedem die dabei evtl auftretenden ungewollten Unter brechungspausen bekannt Die Ursache f r diese Tonaussetzer ist das Betriebssystem das einem anderen Programm Ressouren zuteilt die das Wiedergabeprogramm ben tigt h tte Man erkennt also leicht da konventionelle Betrieb ssystem weiche Echtzeitanforderungen unter Umst nden bereits nicht erf llen Wird der PC eingesetzt um eine Lichtschranke zu berwachen die die Hand eines Menschen vor den hohen Dr cken einer industriellen Presse sch tzen soll so wird besonders deutlich da das Betriebssystem auf gar keinen Fall dem falschen Prozess Rechnerresourcen zuteilen darf Um zu verstehen warum konventionelle Betriebssysteme diese Echtzeitanforderungen nicht erf llen mu man sich ein wenig die Aufgaben eines Betriebssystems anschauen 2 1 Aufgaben eines Betriebssystems Zu den grunds tzlichen Aufgaben eines Betriebssystems geh rt es f r die zugrundeliegende Hardware eine A
196. stlich durch Aufruf der fire Methode stattfinden die wieder um mit der handleEvent Methode des zugeh rigen AsyncEventHandler verkn pft ist AsyncE vent Instanz wird erstellt AsyncEvent Instanz wird mittels gt bindTo an Ereignis gebunden AsyncEventHandler Instanz en wird werden erstellt AsyncEventHandler Instanz wird mittels gt addHandler an AsyncEvent gebunden AsyncEvent removeHandler aufgerufen oder zugeh riger Ge Thread beendet e blockiert Ereignisbehandlung abgeschlossen gebundenes Ereignis eingetreten oder AsyncEventHandler E AsyncEvent fire wird ausgef hrt aufgerufen Abbildung 6 Aktivit tsdiagramm zu AsyncEvent Man kann sie sich wie asynchrone Threads vorstellen allerdings mit folgenden Unterschieden e beim Start werden bei einem AsyncEventHandler gewisse Parameter Objekte ReleasePa rameters SchedulingParameters und MemoryParameters mitgegeben die das Verhalten bei der Ausf hrung festlegen e AsyncEventHandler sind entweder blockiert oder werden ausgef hrt im Gegensatz zu Threads die warten und schlafen k nnen 2 e Threads k nnen eine lange Laufzeit haben w hrend AsycEventHandler m glichst wenig Code ausf hren und terminieren 2 e Threads m ssen unter Umst nden auf Ressourcen warten w hrend AsyncEventHandler m glichst bald ausgef hrt werden 2 3 5 Asynchronous transfer of control Bei Echtzeitprogrammierung
197. straction techniques The cone of influence reduction and data abstraction Both of these techniques are performed on a high level description of the system before the model for the system is constructed Therefore we avoid the construction of the unreduced model that might be too big to fit into memory 3 3 4 Symmetry Symmetry reduction approach applies to systems that are composed of components that are replicated in a regular manner It is possible to find symmetry in memories caches register files bus protocols network protocols anything that has a lot of replicated structure These reduction techniques are based on the observation that having symmetry in the system implies the existence of nontrivial permutation groups that preserve both the state labelling and the transition relation Such groups can be used to define an equivalence relation on the state space of the system The model induced by this relation is often smaller than the original model For example a large number of protocols involve a network of identical processes communicating in some fashion Hardware devices contain parts such as memories and register files that have many replicated elements These facts can be used to obtain reduced models for the system Having symmetry in a system implies the existence of a nontrivial permutation group that preserves the state transition graph Such a group can be used to define an equivalence relation on the state space of the syst
198. striespezifischen Standard der zi vilen Luftfahrtindustrie fiir die Entwicklung von Luftfahrt Software handelt wird DO 178B in einer Vielzahl von Branchen z B Atomindustrie als ein zu befol gendes Modell angesehen Er besch ftigt sich wie bereits erw hnt ausschlie lich mit Software Zu seinen Kernbestandteilen geh ren die Software Planung Entwicklung Verifizierung sowie die Software Qualit tssicherung Der Standard unterscheidet f nf Zertifizierungsstufen von Software die sich nach den Folgesch den eines Ausfalls bzw einer Fehlfunktion richten e Level A Katastrophale Folgen z B der Absturz des Flugzeuges e Level B Ernsthafte Folgen z B T tung oder Verst mmelung einzelner Personen e Level C Erhebliche Folgen z B Besch digung von Eigentum e Level D Geringf gige Folgen z B unn tiger Aufwand der Crew e Level E Keine Folgen Als popul res Beispiel f r den Einsatz von DO 178B in einer nicht Luftfahrt spezifischen Branche sei hier das Betriebssystem LynzOS von LynuxWorks an gef hrt Dieses Embedded Operating System ist ein gem DO 178B zertifi ziertes POSIX kompatibels Echtzeit Betriebssystem das als Grundbaustein f r ein sp ter zertifizierbares Gesamtsystem dient Radio Technical Commission for Aeronautics http www rtca org http www lynuxworks com 2 6 3 Sonstige Standards Neben diesen Standards existiert auch hier noch eine Reihe von anderen Stan dards im Zi
199. system indem sie zwei spezielle Betriebsmodi zur Verf gung stellen Unter Linux werden diese als Kernel Mode und User Mode bezeichnet Im Kernel Mode l uft lediglich der Kernel von Linux Der Kernel Mode erlaubt den Zugriff auf alle Register eines Prozessors und somit den Zugriff auf die Steuerung des Prozessors Im User Mode laufen alle Anwendungsprogramme unter Linux In diesem Modus ist der Zugriff auf die steuernden Register des Prozessors nicht erlaubt Beide Betriebsmodi sind dazu da das Multitasking also das scheinbar gleichzeitige Ausf hren von Programmen bzw Prozessen in besonderem Ma e zu unterst tzen Da lediglich der Kernel Zugriff auf die Steuerfunktionen hat ist er in der Lage sich selbst und Anwendungsprogramme untereinander vor Fehlern oder gar gezielten Angriffen zu sch tzen Protection Multitasking und Protection bedeuten aber einen gewissen Aufwand in Form von Rechenzeit Da alle steuernden Aufgaben nur vom Kernel durchgef hrt werden mu vom Programm in den Kernel gewechselt werden also vom User Mode in den Kernel Mode Dabei tritt jedesmal ein sogenannter Kontextwechsel auch system call trap genannt auf Das bedeutet da alle Register im Prozessor die vom vorher laufenden Prozess benutzt wurden vom Kernel gesichert werden m ssen Ansonsten w rden beim Kontextwechsel die Inhalte einiger Variable verloren gehen Sind die steuernden Aufgaben vom Kernel erledigt wird ein Anwendungsprozess wieder auf den
200. t auszuf hren muss der Tester ber Kenntnisse der inneren Struktur des Programms verf gen Die beiden Teststrategien werden hier ausf hrlich erkl rt 3 Black Box Test Eingabe Ausgabe gt Der Tester kennt beim Black Box Test nur was eine Funktion macht aber nicht wie diese Funktion arbeitet Der Tester muss nicht Programmierkenntnisse haben und er orientiert sich nur am Benutzerhandbuch Lastheft der Software Spezifikation der Software um die Testfalle als Eingabe zu definieren Die Ausgabe wird danach verglichen ob sie gleich ist mit der richtigen Ausgabe die in der Spezifikation steht Um alle Fehler zu finden muss ein vollst ndiger Test ausgef hrt werden Das bedeutet dass nicht nur alle zul ssigen Eingaben getestet werden m ssen sondern die fehlerhaften Eingaben m ssen auch getestet werden F r die Testfallbestimmung gibt es drei wichtige Verfahren Aquivalenzklassenbildung Equivalence Partitioning Grenzwertanalyse Boundary Value Analysis Test spezieller Werte Error Guessing 3 1 Aquivalenzklassenbildung Equivalence Partitioning Eine Aquivalenzklasse ist eine Menge von Eingabewerten die auf ein Programm eine gleichartige Wirkung aus ben Das bedeutet dass wenn ein Element in einer quivalenzklasse als Eingabe zu einem Fehler f hrt alle anderen Elemente n dieser Klasse mit der gr ten Wahrscheinlichkeit zu dem gleichen Fehler f hren werden Wenn ein Testfall in einer Aquivalenzkla
201. t sind klassifizieren Gefahren in Ausdr cke die ihre Schwere bezeichnen Es ist offensichtlich dass diese Klassifizierung von dem Industriezweig gemacht wird abh ngt Folgendes Beispiel aus militaren Systemen m Gro britannien zeigt es uns besser Tabelle 2 Schwere der Unfallklasse f r militare Systeme Klasse Definition Katastrophal Mehrfache Tote Kritisch Ein einzelner Tot bzw mehrfache schwere Verletzungen oder schwere berufliche Krankheiten Eine einzelne schwere Verletzung oder berufliche Krankheiten Marginal A ES bzw mehrfache untergeordnete kleinere Verletzungen oder untergeordnete kleinere berufliche Krankheiten Unwesentlich H chstens eine einzelne untergeordnete kleinere Verletzung oder untergeordnete kleinere berufliche Krankheiten 5 2 Nahere Betrachtung der Wahrscheinlichkeit Die Wahrscheinlichkeit des Eintreffens eines gefahrlichen Ereignisses kann in unterschiedlicher Art und Weise ausgedr ckt werden und wird qualitativ oder quantitativ gegeben Manchmal wird die Rate als die Anzahl von Ereignissen pro Stunde oder pro Jahr einer Operation bezeichnet Alternativ wird sie als die Anzahl der wahrscheinlichen eintreffenden Ereignisse wahrend der Lebenszeit der Einheit verstanden Ein weiteres Beispiel aus dem Militar definiert sechs Klassen von Gefahrenwahrscheinlichkeit die im folgende aufgezeigt werden Tabelle 2 Stufe der Unfallwahrscheinlichkeit f r militare Systeme
202. t so die Anforderungen eines Desktopbetriebssystems auf dem meist nur ein Programm l uft mit dem der Anwender interagiert als auch die Anforderungen eines Serverbetriebssystems auf dem viele Prozesse m glichst effizient die Resourcen zugeteilt bekommen 2 3 Anforderungen f r ein echtzeitf higes Linux Die bereits genannten Anforderungen an ein Echtzeitsystem sofortige Abarbeitung von Daten und Bereitstellung von Ergebnissen zu einem bestimmten Zeitpunkt Deadline lassen sich f r Linux als Betriebssystem genauer aufschl sseln wobei die von Linux bereitgestellte Funktionalit t nicht verloren gehen soll Optimierung auf den Worst Case Damit Linux in Echtzeit auf Ereignisse reagieren kann mu die Optimierung auf den durchschnittlichen Fall wegfallen und durch eine Optimierung auf den Worst Case ersetzt werden Hierbei handelt es sich nur um eine allgemeine Anforderung Deterministisches Verhalten Man mu versuchen das Scheduling deterministisch zu gestalten um sicherzustellen da Aufgaben zu den Deadlines fertiggestellt sind Aufgrund der Vielfalt der Konstellationen beim Scheduling wird ein vollst ndig deterministisches Verhalten nicht erreicht werden k nnen Das effiziente Scheduling mu durch ein vorhersagbares Scheduling ersetzt werden Kurze Latenzzeiten Kurze Latenzzeiten vereinfachen die Einhaltung der Deadlines Latenzen treten durch Kon textwechsel Kalte Caches und evtl Swapping auf und sind unter Umst nden
203. t werden solange die g ltigen Konventionen eingehalten werden 3 2 2 ill rlicheSpr nge ild umps Ada kennt einen GOTO Befehl und l sst willk rliche unkontrollierte Spr nge wild Jumps zu Mit einem Sprung kann eine Anweisungsfolge verlassen oder die Kontrolle innerhalb einer Anweisungsfolge weitergegeben werden Externe Spr nge in eine Anweisungsfolge wie z B n den Rumpf einer Schleife oder n einen der Zweige einer IF Anweisung sind nicht m glich Vom Einsatz von Sprungbefehlen in sicherheitsrelevanten Softwaresystemen ist dringen abzuraten sie sind f r den Leser eines Programms kaum nachvollziehbar Anmerkung des Autors In der Literatur befinden sich widerspr chliche Angaben laut Sto 6 sind unkontrollierte Spr nge nicht m glich in der Ada 5 Reference Manual von Gnat wird aber die GOTO ANWEISUNG ausf hrlich erl utert 3 2 3 berschreibung over rites Das Speichermanagement von Ada bietet einige Funktionen um die Datenkonsistenz im Speicher zu gew hrleisten Laut Sto 6 lassen sich diese jedoch umgehen was wiederum zur Fehlfunktionen f hren k nnte 3 3 Availabilit Verf gbar eit 3 3 1 logische G Itig eit logical soundness In ihren Grundz gen ist Ada sehr klar und logisch strukturiert was f r den Einsatz in SkS von essentieller Bedeutung ist Ada beherrst jedoch auch Konzepte der modernen Softwaretechnik wie berladung Vererbung und Polymorphismus Diese komfortablen Sprachkonstrukte schaff
204. tations of a reactive system can be defined in terms of its transitions A computation is an infinite sequence of states where each state is obtained from the previous state by some transition We use a type of state transition graph called a Kripke structure to model a system A Kripke structure is basically a graph having the reachable states of the system as nodes and state transitions of the system as edges It also contains a labelling of the states of the system with properties that hold in each state Definition Let AP be a non empty set of atomic propositions A Kripke structure over a set of atomic propositions AP is a four tuple M S SO R L where e S is a finite set of states e SO c S is the set of initial states e R CS x Sis a transition relation e L S gt 2 AP is a function that labels each state with the set of atomic propositions true in this state Computation trees e State Transiton Graph or Kripke Model e Unwind State Graph to obtain Infinite Tree Computation Trees Z N Fa N PE II 2 2 Specification The second step is specification that means we give the properties that the design must satisfy Usually this is achieved by using Temporal Logic A logic with a notion of time included In 1980s a verification technique called Temporal Logic Model Checking was developed independently by Clarke and Emmerson in the USA and Queille and Sifakis in France e Classical Logic with its basi
205. temporal properties of the concurrent system of predicate transformers that are obtained from the transition relation In the new implementations both the predicate transformers and the fixpoints are represented with BDD Therefore the explicit construction of the global state graph for the entire concurrent system could now be avoided The BDD technique is a technique to encode transition systems in terms of a compact model that is suite to represent boolean functions efficiently In a binary decision diagram the redundancy that is present in a decision tree is reduced A binary decision diagram is a binary decision tree in which isomorphic subtrees are collapsed and redundant vertices are omitted Because the symbolic representation captures some of the regularity in the state space determined by circuits and protocols it is possible to verify systems with an extremely large number of states The BDD technique cannot guarantee the avoidance of the state space explosion in all cases but provide a compact representation of several systems allowing these systems to be verified Later on McMillan developed a model checking system called SMV which is based on a language for describing hierarchical finite state concurrent systems Programs in the language can be annotated by specifications expressed in temporal logic The model checker extracts a transition system represented as an OBDD Bryant s ordered binary decision diagrams from a program in t
206. teraktionsrahmen 5 4 2 Lebenslinie 5 4 3 Zeitverlaufslinie 5 4 4 Nachricht 5 4 5 Sprungmarke 5 4 6 Wertverlaufslinie 6 Fazit 7 Literaturverzeichnis 8 Abbildungen Einleitung Die UML 2 0 ist das Ergebnis eines mehrjahrigen Entwicklungsprozesses der Mit te 2001 begann und vermutlich bis Ende 2004 mit der Verabschiedung der end gultigen Spezifikationen abgeschlossen sein wird Mit der UML 2 sollen einige grundlegende Anderungen verwirklicht werden Ein Ziel der Uberarbeitung war eine Reduzierung der Komplexit t und des Umfangs um die UML2 schneller zu erlernen und angemessen zu benutzen Au erdem sollte auf die Ver nderungen im Softwareentwicklungsmarkt der letzen Jahre eingegangen werden Zus tzlich sollten neue Anwendungsbereiche erschlossen werden wie zum Beispiel die Mo dellierung von technischen Systemen mit Echtzeitanforderungen Aus den Anforderungen entstanden haupts chlich zwei Dokumente Infrastructure 6 und Superstructure 7 die sich gegenseitig erg nzen Grundlegende Sprachkonstrukte und die Basisarchitektur wurden in der Infrastructure 6 festgehalten Die darauf aufbauenden Diagrammnotationen und die Semantik stehen in der Superstructure 7 Neuerungen in der UML 2 0 Die UML 2 0 besitzt 13 Diagrammtypen die gr tenteils schon in den 1 x Versio nen vorhanden waren und unterschiedlich starken Ver nderungen unterzogen wurden Komplett neu sind drei Diagramme das Timing Diagramm das sp ter noch au
207. the fly procedure is that a counterexample may be found before completing the construction of the intersection of the two automata Once a counterexample has been found and reported there is no need to complete the construction 3 1 2 Partial Oder Reduction Technology Systems that consist of a set of components that cooperatively solve a certain task are quite common in practice e g hardware systems communications protocols distributed systems and so on Typically such systems are specified as the parallel composition of n processes The state space of this specification equals in worst case the product of the state spaces of the components A major cause of this state space explosion is the representation of parallel is by means of interleaving Interleaving s based on the principle that a system run is a totally ordered sequence of actions In order to represent all possible runs of the systems all possible interleaving of actions of components need to be represented For checking a large class of properties however it 1s sufficient to check only some representative of all these interleaving For example if two processes both increment an integer variable in successive steps the end result is the same regardless of the order in which these assignments occur The underlying idea of this approach 1s to reduce the interleaving representation into a partial order representation System runs are now no longer totally ordered sequences but par
208. the second CTL Formal If the door is closed and someone pushes the start button the microwave oven begins to cook lt gt AG close A start gt AF cooking AG close A start gt AF cooking AG close A start v AF cooking AG close v start v AF cooking AG close v start v AF cooking 7 EF close A start A EG cooking Now the algorithm can be applied to the formula and we get e S close S2 S3 e S start S3 S4 e S cooking Sl S2 S4 e S EG cooking S1 S2 S4 eS close A start A EG cooking e S EF close A start A EG cooking e S EF close A start v EG cooking S1 S2 S3 S4 Since the initial condition S1 is contained in this quantity it means that our microwave oven described by the Kripke structure fulfills specification Therefore it is correct 3 Algorithms for Model Checking The initial implementation of the Model Checking problem set an explicit representation of the Kripke structure as a labelled directed graph For systems with limited number of processes where the number of possible states was rather small this approach proved to be practical However this method was unable to handle extensive number of states generated by complex concurrent systems One of the major problems in the application of model checking techniques to practical verification problems is so called state explosion problem The state space explosion problem is a prob
209. tially ordered sequences The partial order reduction is aimed at reducing the size of the sate space that needs to be searched by model checking algorithms It exploits the commutativity of concurrently executed transitions which result in the same state when executed n different orders The method consists of constructing a reduced state graph The full state graph which may be too big to fit in memory is never constructed The behaviours of the reduced graph are a subset of the behaviours of the full state graph The justification of the reduction method shows that the behaviours that are not present do not add any information More precisely it is possible to define an equivalence relation among behaviours such that the checked property cannot distinguish between equivalent behaviours If a behaviour is not present in the reduced state graph then an equivalent behaviour must be included There are basically three different techniques for partial order approaches towards model checking In dynamic partial order reduction a subset of the states that need to be explored is determined during the search procedure This embodies that the possible interesting successors of a given state are computed while exploring the current state Dynamic partial order reduction is the most popular and most developed technique it requires however a modification of the search procedure e Static partial order reduction techniques avoid the modificati
210. tsanforderungen genau spezifiziert Um sie zu definieren muss man die Gef hrdungen die von der Anlage ausgehen untersuchen einstufen und ent sprechende Methoden festlegen um mit ihnen umzugehen Weiterhin muss eine Entschei dung ber die notwendige Zuverl ssigkeit und Verf gbarkeit getroffen und insgesamt ein angemessenes Integrit tsniveau f r das SkS gefunden werden Im Anschluss daran sollte dann die Entwicklungsmethode entsprechend der Vorgaben ausgew hlt werden Sicherheitsanforderungen schreibt man im allgemeinen als Bedingungen beispielswei se w rde man bei einer Waschmaschine folgendes formulieren Erlaube es nicht die Trommel zu ffnen solange Wasser in der Maschine ist und der Waschgang noch nicht beendet ist Dies wird auch als W chtermechanismus bezeichnet Mechanismen dieser Art arbeiten meist mit Dingen wie Sperrgittern oder K figen Ein Sperrmechanismus hingegen gibt die gef hrliche Funktion immer nur dann frei wenn sichergestellt ist dass keine Gef hrdungen auftreten k nnen S e k nnen nur einge setzt werden wenn keine Verz gerungen auftreten die Anlage also sofort nach der Ab schaltung sicher ist Ein Beispiel f r so eine Schaltung w re eine sogenannte Zweihand steuerung einer Presse Hier wird die Funktion nur freigegeben wenn zwei unabh ngige Schalter gleichzeitig bet tigt werden also keine Hand des Bedieners mehr im Gefahrenbe reich ist 1 4 Fehler Fehler treten unvermeidlich in alle
211. tzungen Schaden an Um welt oder Material verursacht Als Vorfall bezeichnen wir ein unbeabsichtigtes Ereignis oder eine Kette davon dass keine Beeintr chtigung verursacht hat aber unter anderenUm st nden das Potential dazu gehabt h tte Die Wichtigkeit einer Gef hrdung h ngt von den Folgen des Unfalls ab die es verursa chen k nnte Ein Unfall der schwere Konsequenzen hat ist nur tolerierbar wenn er fast nie auftritt Ein Unfall mit minimalen Schaden ist sicherlich h ufiger tolerierbar Das Risiko eines Unfalls ist dementsprechend als die Kombination von Frequenz oder Wahrscheinlich keit seines Auftretens und den Konsequenzen definiert 1 3 Sicherheitskriterien 1 3 1 Systemanforderungen Zuverl ssigkeit ist die Wahrscheinlichkeit einer Komponente oder eines Systems ber ei ne bestimmte Zeit innerhalb einer gegebenen Umgebung zu funktionieren Dies bedeutet dass die Zuverl ssigkeit ber die Zeit abnimmt Das beispielsweise ein elektrisches Bauteil w e ein Kondensator ber eine Woche einwandfrei funktioniert ist sehr wahrscheinlich Das er aber ber zehn Jahre nicht ausf llt l sst sich nicht so einfach sicherstellen Die Ver f gbarkeit eines Systems ist die Wahrscheinlichkeit dass es jederzeit funktionieren wird Diese Gr e bleibt damit ber der Zeit konstant Eine Verf gbarkeit von 99 Prozent ist beispielsweise ein Ausfall von 3 65 Tagen im Jahr Hochverf gbare Systeme haben meist maximal eine Verf gbarkeit von 9
212. u beschreiben Die MOF umfasst all diese standardisierte Spezifikationen Mit MOF ist m glich alle andere Art von Modellen zu beschreiben Die MOF reduziert den Transformationsaufwand der Modelle untereinander Ohne abstrakte Beschreibungssprache MOF m sste man siehe Abbildung 3 pro Modell mindestens 3 Transformationen durchf hren Mit MOF als Beschreibungssprache ist nur eine MOF Mapping f r eine Modellierungssprache notwendig De ______ gt M4 M3 NA AN a S 7 a ES Ns a MOF EN Pi l P a Le sa Y _ XA y M2 M1 M2 SM Abbildung 3 Mapping der Modelle links ohne MOF rechts mit MOF Die Metamodellarchitektur Die Architektur von MOF besteht aus sog 4 Meta Ebenen n mlich MO M1 M2 und M3 siehe Abbildung 4 lt lt beschreibt gt gt lt lt Instanz von gt gt lt lt Instanzvon gt gt lt lt beschreibt gt gt lt lt Instanz von gt gt lt lt be eibt gt gt lt lt Insi z von gt gt Abbildung 4 4 Schichten Architektur von MOF e Auf der Ebene MO auch als User ebene bezeichnet werden konkrete Datenkonfigurationen eines Systems dargestellt Bezogen auf ein Programm w re dies der Ausf hrungszustand des Programms e Die Ebene MI beschreibt die Sprache zur Beschreibung von Dom ne
213. ustrial machinery and robots Due to the nature of such applications errors in real time systems can be extremely dangerous even fatal Guaranteeing the correctness of a complex real time system is an important and nontrivial task Because of this only conservative and usually special approaches to design and implementation are routinely used Some factors make the validation of real time systems particularly difficult The architecture of computer applications is becoming extremely complicated As a system increases in complexity so does the probability of introducing an error Moreover performance is becoming an important factor in the success of new applications Due to competition new products have to fully utilize the available resources A slow component can affect the performance of the whole system Consequently the task of verifying that new applications satisfy their timing specifications is more critical than ever before 4 1 Discrete real time System When time is discrete possible clock values can only occur at integer time values This type of model is appropriate for synchronous systems where all of the components are synchronized by a single global clock The duration between successive clock ticks 1s chosen as the basic unit for measuring time This model has been successfully used for reasoning about the correctness of synchronous hardware designs for many years Real time concurrent systems are particularly difficult to verif
214. vil und Milit rsektor Ein paar ausgew hlte Standards aus diesen Sektoren sind die folgenden e Zivile Standards ESA PSS 05 0 Software Engineering Standards 11 HSE Guidelines Programmable Electronic Systems in Safety Related Applications 12 IEC 880 Software for Computers in the Safety Systems of Nuclear Power Stations 13 e Milit r Standards DoD Defence Standard 5200 28 Trusted Computer Systems Evaluation Criteria 14 3 Schlussfolgerung Abschlie end bleibt anzumerken dass Qualit tsmanagement und Zertifizierung eng miteinander verkn pft sind Es ist unm glich ein Zertifikat zu erhalten ohne zuvor entsprechende Ma nahmen beim Qualit tsmanagement ergriffen zu haben Beim Qualit tsmanagement und der Zertifizierung handelt es sich jeweils um Prozesse die parallel zur Entwicklung und Produktion ablaufen Sicherheit befasst sich mit dem Ausschlie en und Reduzieren des Risikos von Unf llen und spielt daher auch ab einer sehr fr hen Projekt Phase eine wichtige Rolle Der Safety Case ist einer der wichtigsten Bestandteile um die Sicherheit des Systems zu demonstrieren und zu dokumentieren Die Entwicklung von sicherheitskritischen Systemen sollte von gut organisierten multidisziplin ren Teams durchgef hrt werden Dabei sollten Standards einge halten werden um am Ende ein m glicherweise ben tigtes Zertifikat ohne gro en Zusatzaufwand erwerben zu k nnen Literatur 1 Internationa
215. von SPARK werden sogar Ada Compiler benutzt aber SPARK ist eine eigenst ndige Ada hnliche Programmiersprache Der Hauptunterschied ist der dass viele Konzepte von Ada fehlen Der Sprachkern ist gegen ber den Standard Ada Sprachkern stark eingeschr nkt SPAK verzichtet auf e Ausnahmen Behandlung Generische Einheiten Zugriffstypen Zeiger Dynamische Speicherverwaltung Rekursive Unterprogramme 4 usammenfassung 4 1 Vor ort Es hort sich eigentlich ganz einfach eine Programmiersprache die f r den Einsatz in SkS empfohlen wird nach der hrer Eignung f r diesen Einsatz zu untersuchen Leider stellte sich die Aufgabe doch etwas schwieriger dar als ich mir erhofft habe sei es wegen der vielen widerspr chlichen Angaben in der Literatur oder durch das umfangreiche Sicherheitskonzept von Ada Nichts desto trotz hoffe ich eine objektive und vor allem technisch korrekte Beurteilung getroffen zu haben 4 2 eurteilung von Ada Im laufe der Jahre die Ada am Markt verf gbar ist sind eine Menge Werkzeuge teilweise komplette Entwicklungsumgebungen f r Ada entwickelt und programmiert worden Ada Compiler werden streng nach dem Ada Standard validiert es sollten nur solche Compiler eingesetzt werden die den Validierungsprozess erfolgreich abgeschlossen haben Diese Compiler haben sich durch den tausendfachen Einsatz in der Praxis als sehr zuverl ssig erwiesen Da fundierte Ada Kenntnisse in der Softwarebranche die den Raum u
216. wichtig sind Diese Kriterien sind 1 6 durch Sto 6 wie folgt zusammen gefasst worden logische G ltigkeit logical soundness einfache Definitionen simple Definitions Ausdruckstarker Code expressive power Sicherheit sequrity Verifizierbarkeit verifiability Zeit Speicher Bedarf bounded space and time requirements Keine der blichen 1m gro en still eingesetzten Sprachen erf llt all diese Kriterien Der Grund ist relativ einfach die sicherheitskritische Software repr sentiert nur einen Bruchteil der weltweit vertretenen Software Weiterhin wiedersprechen sich einige Kriterien wie z B wenn eine Sprache einen sehr ausdrucksstarken Code hat tendiert sie sehr Komplex zu werden das erschwert die Verifizierung erheblich Die Entwickler der Sprache sind also gezwungen Kompromisse zu finden damit m glichst alle Punkte optimal ber cksichtigt werden 2 3 Probleme ge hnlicher Programmiersprachen nach utterbuck ber die Jahre konnte die Fachwelt viele Erfahrungen ber die Zuverl ssigkeit der Systeme und ber die Art und vor allem die Ursachen von Fehlern sammeln die bei den meisten Programmiersprachen auftreten 1 2 listete Clutterbuck Sto 6 die vier meist vorkommenden Fehler in Programmen die mit unterschiedlichen Sprachen geschrieben worden e Seiteneffekte durch Unterprogramme subprrogram side effects e Mehrfache Referenzen aliasing e Initialisierungsfehler initialising failures Auswertungsfehler ex
217. wird 2 Man we nicht ob es unn tige Programmteile gibt 3 Man wei nicht ob es kritische Programmteile gibt Die Vorteile von White Box Test l Man kann sich sichern sein dass das Programm keinen ungetesteten Code enth lt 2 Wer den Quellcode kennt wei wo besonders sorgf ltig getestet werden muss Die Nachteile von White Box Test 1 Die Vorgehensweise ist aufw ndiger als der Black Box Test 2 White Box Test kann nicht beweisen dass das Programm seiner Spezifikation entspricht 6 Testprinzipien Nachdem wir einige Methode fiir Testen betrachtet haben wollen wir hier einige Testprinzipien kennen lernen Da das Testen stark von Psychologie beeinflusst wird werden hier einige Richtlinien die beim Testen als Leitfaden benutzt werden sollen erkl rt Ein Programmierer sollte nie versuchen sein eigenes Programm zu testen 1 Diese Aussage bedeutet aber nicht dass der Programmierer nicht testen darf Sie besagt dass das Testen effektiver durch eine externe Gruppe ausgef hrt wird Es gibt ein bekanntes Prinzip beim Testen Testen ist ein destruktiver Prozess Der Programmierer hat sein Programm fertig gemacht danach wird das Programm von ihm getestet Das ist schwierig f r den Programmierer weil er die Seite wechseln muss und jetzt eine destruktive T tigkeiten macht Er muss eine destruktive Einstellung gegen ber seinem Programm haben Zus tzlich zu diesem psychologischen Problem gibt es in der Praxis
218. y because their correctness depends on the actual times at which events occur An example of such a technique is static time slicing which divides time equally among all tasks Each task executes until its time slot has been used and then release the processor The resulting problem is easy to analyse but rather inefficient since all tasks are given equal resources regardless of their importance or resource utilization Rate monotonic scheduling theory RMS is a more powerful technique to analyse the behaviour of a real time system The RMS theory is applicable to systems described by a set of periodic tasks Each task corresponds to a concurrent process of the system and is characterized by its periodicity how often it executes and its executive time at each instantiation 4 2 Continuous real time System Continuous time s the natural model for asynchronous systems because the separation of events can be arbitrarily small This ability is desirable for representing causally independent events in an asynchronous system Moreover no assumptions need to be made about the speed of the environment when this model of time is assumed In order to model asynchronous systems using discrete time it is necessary to separate time by choosing some fixed time quantum so that the delay between any two events will be a multiple of this time quantum 5 Model Checking developing Trend There are a number of ways that model checkers can be improve
219. ystems of Nuclear Power Stations Genf 1986 International Electrontechnical Commission 14 DoD Defence Standard 5200 28 Trusted Computer Systems Evaluation Criteria Washington 1985 Department of Defence 115 Wikipedia http en wikipedia org 16 Giese H Safety Critical Computer Systems http www upb de cs ag schaefer Lehre Lehrveranstaltungen Vorlesungen SafetyCriticalComputerSystems WS0203 index html Stand 26 03 2004 17 Lund Quality http www quality de 18 h Isaksen Ulla Bowen Jonathan P Nissanke Nimal System and Software Safety in Critical Systems http www museophile lsbu ac uk pub jpb scs survey tr97 pdf Stand 26 03 2004 119 _ Validated Software http www validatedsoftware com what_is_DO178B html Stand 26 03 2004 20 u Functional safety and IEC 61508 http www iee org oncomms pn functionalsafety HLD pdf Stand 26 03 2004 Risiko und Gefahrenanalysen und deren Ber cksichtigung beim Entwurf von Sicherheitskritischen Systeme Seminararbeit im Fach Informatik im Rahmen des Seminars Sicherheitskritische Systeme an der Universitat Siegen Fachgruppe fiir Praktische Informatik eingereicht bei Dr J rg Niere vorgelegt von Kelen Yo Rodrigue Sommersemester 2004 Risiko und Gefahrenanalysen und deren Berucksichtigung beim Entwurf von Sicherheitskritischen Systeme 1 Einleitung Es ist heutzutage schon eine festgesetzte Tats
220. zepten von MDA ist dass die Idee von multiplen Ebenen von Modellen Die Codegenerierung f ngt bei der h chsten Ebene genannt PIM an Die Modelle auf dieser Ebene s nd mit einer plattformunabh ngigen Sprache spezifiziert Die Spezifikationen von PIM ist daher sehr abstrakt gehalten so dass alle m glichen software technischen Anforderungen erfassbar sind Der n chste darunter liegende Ebene ist plattform spezifisch kurz PSM genannt Diese Ebene PSM erweitert das PIM mit den notwendigen Strukturen so dass die Generatoren daraus Quellcode erzeugen k nnen Die Pfeile zwischen den Stufen bei Abbildung 1 bilden die Transformationen die durch Transformationsregeln geregelt werden Die Transformation zwischen plattform spezifischen Modell und Templates ist der entscheidende Teil fur die Codegenerierung des MDA Modells Die Ebene zwischen das plattform abhangigen Modell und das Template f hrt alle notwendigen Transformationen zwischen PSM und die Implementierungsspezifikation eines Systems durch Das bedeutet dass die Templates nur noch den Quellcode erzeugen m ssen nicht die in PSM spezifizierten Modelle interpretieren und anschlie end den Code erzeugen m ssen Das MDA Konzept entspricht n vereinfachter Form dem 3 Tier Modell Also Benutzerschicht Fachkonzeptschicht und Datenhaltungsschicht 3 1 Model Driven Architecture MDA Die Heutige Softwareentwicklung ist davon gepr gt dass die Softwareentwickler w hrend der Anfo
221. zierten Transformationsregeln ab Die Transformationsregeln enthalten Informationen w e die Modelle n ein anderes Modell Abbildung 5 Ubersicht der Transformationsvarianten 3 6 1 PIM nach PIM Diese Transformation wird benutzt wenn die Modelle wahrend dem Entwicklungsprozess erweitert gefiltert oder verfeinert werden ohne plattform abhangige Informationen zu nutzen Die PIM zu PIM Mappings werden meistens eingesetzt wenn die Modelle verfeinert werden m ssen 3 6 2 PIM nach PSM Die Transformation von plattformunabh ngigen Modellen an die speziellen Gegebenheiten einer technologie abhangigen Plattform spielt eine zentrale Rolle in dem MDA Konzept Die Transformation von PIM nach PSM verl uft automatisch Die Trennung von PIM und PSM Modelle bewirkt die Modelle einfacher zu verstehen denn die Aspekte der beiden Modelle werden nicht vermischt Diese Transformation ist essentiell wichtig f r die Codegenerierung weil zwei verschiedene Modelle aufeinander abgebildet werden die besondere Transformationsregeln erfordern Rem LAN lt lt PersistentObject gt gt poeu Book B author string Book E publisher string get author Efset author get publisher set publisher Abbildung 5 Transformat on von PIM in das PSM Falls fur die angestrebte Zielplattform ein Codegenerator existiert der die Transformation durchf hrt kann wie bei Abbildung 5 kann PIM in ein PSM Modell

Seminar Sicherheitskritische Systeme

Contents

Download Pdf Manuals

Related Search

Related Contents