Home

Vergleich zwischen konventionellen und formalen

1. Projekt Eny y E ni Abbildung 2 6 Zuordnung von Prozessen zu Tasks In OSEK werden Anwendungen auf Tasks und Prozesse aufgeteilt Die Berechnungen finden in Prozessen statt die wiederum zu Tasks gruppiert werden k nnen Innerhalb einer Tasks werden die Prozesse sequentiell hintereinander abgearbeitet Auf einem Prozessor laufen mehrere Tasks quasi parallel Welche Task wann zur Ausf hrung kommt h ngt vom vorkonfigurierten Scheduling ab und beeinflusst das Echtzeitverhalten des Systems 21 Kapitel 3 Konventionelle Qualit tssicherungsverfahren Die Betonung in diesem Kapitel liest auf Qualit ts sicherungsmassnahmen die in der Industrie weit verbreitet sind 3 1 Qualit tssicherungsrichtlinien und standards im Unternehmen Ziel von Standards zur Qualit tssicherung ist die Erh hung und Gew hrleistung der Software Qualit t Dem Stand der Technik ange passte Prozesse und Methoden definieren einheitliche Anforderungen an die Software Entwicklung Sicherheitsstandards und richtlinien wie in der Luftfahrtindustrie z B DO 178B RCT existieren ebenfalls in der Automobilindustrie Ein Beispiel ist der IEC 61508 Standard Com Er stellt Anforderungen an die Entwicklung von sicherheitskritischen elek trischen elektronischen und programmierbaren elektronischen Systemen zur Erh hung der Sicherheit Es werden darin vier Sicherheitsstufen SIL definiert Ein SIL stellt ein Mass f r die Wahrschei
2. Das Steuerger t als Teil eines Regelkreises Kernprozess der Steuerger te Entwicklung AUTOSAR Software Architektur 2 2 2222 2 202 Zuordnung von Prozessen zu Tasks berblick ber g ngige Testmethoden Beispiel f r einen Kontrollflussgraphen Einordnung der Testsysteme 2 2 2222 2 00 Diversifizierender Testansatz 2 222200 Inklusionseigenschaft von Spezifikationssprachen Funktionen des T rsteuerger tes 2 222 22 Position der T rsteuerger te und Bedienelemente ASCET Toolkette 4 wos 4 sP8 28 Dre Di Projektstr ktut ios a i e tia y taai a a a e a Definition von Prozessen Scheduling EE KEE CTE XL eeben e as ee EE te 4 24 22 3 wa Beispiel f r ein STD nes 2 ae Modelchecking in AutoFOCUS 2 2 222 SSD zur Demonstation der Modelchecking Anbindung STD zur Demonstration der Modelchecking Anbindung DoorLock_Module in ASCET 2 2 22 22 Windows Module in ACHT 130 7 3 7 4 7 5 7 6 T T 7 8 7 9 8 1 8 2 8 3 8 4 8 5 8 6 8 7 9 1 9 2 FrontMotor in ACHT 75 DispatchCommand in ASCET 2 2 76 Testen mit ASCET 2 aaa 2282218284 79 Rapid Prototyping Aufbau 2 2 22 2 2 2 81 Hallsensoren zur Einklemmschutzerkennung 82 Signalverl ufe der Sensoren 2 2 22222 82 Zustandsbasiertes Quadrature Encoding 83 berblick ber das AutoFocus
3. 22 24 24 24 33 38 38 39 40 42 43 5 1 2 Hardwareeigenschaften 47 89 Dreck 3 au 2 aan est E bt de re a EE Se 48 5 2 1 Verriegeln 2 kn a Aa a ae be a aeg 48 5 2 2 e EE EE 48 5 3 Fensterheber 2 4 2 3 A 2a al air H 49 5 3 1 Fenster ffnen bzw schliessen 50 54 Beleuchtung s 22 5 6 ran es ae MEN en 50 6 Eingesetzte Werkzeuge 52 6 1 ASCET Werkzeugkette 2 2 aa a 52 6 1 1 ER MER ur 8er 53 6 52 ASCBET RP u 0 Sr ai a E 56 bl SASCHTFSE aa 2 ea er el 56 6 2 Unterst tzende Werkzeuge 2 22 22 57 6 2 1 IBM Rational Test RealTime 57 22 OFERE a ee a EE 57 6 3 E T a eh e ah ao pa R I A 58 6 3 1 System Structure Diagram SSD 59 6 3 2 State Transition Diagram STD 59 6 3 3 Extended Event Traces EET 60 6 3 4 Data Type Definitions DTD 61 6 3 5 Modelchecking Anbindung 61 7 Modellierung in ASCET 64 7 1 Modell des T rsteuerger tes 2 2 2 22200 64 7 1 1 Rahmenbedme ngen 4 2 3a st wer 2 64 7 1 2 Aufbau und Funktionsweise 2 2 2 2 69 7 2 Testen auf Modellebene Simulation 77 7 3 Testen auf Codeebene 78 7 4 Rapid Prototyping eat es ae ea a 80 8 Modellierung in AutoFocus 84 8 1 Modell des T rsteuerger ts 22 2 2000 84 8 1 1 Rahmenbedingungen 2 2 2222 84 8 1 2 Aufbau und Funktionsweise e 86 8 2 Testverfahren un 6 20 2 Di Aa ea ae 93 8 3 Modelchecking
4. 8 SE COLCOCOCOCOC Val MC_FrontMotor Front_Motor F_MOTOR_Up 9 amp amp not is_Msg MC_FrontMotor Top_Front 10 AE not is_Msg MC_FrontMotor MovingSensor_Front 1 12 OLOCOLOCOCOC 13 cc 14 Val MC_FrontMotor Front_Motor F_MOTOR_Down 15 Until 16 not is_Msg MC_FrontMotor Bottom_Front amp amp not is_Msg MC_FrontMotor MovingSensor_Front 17 II 18 Val MC_FrontMotor Bottom_Front F_UNTEN_Bottom 19 2 20 lI 21 C TDie Startup Zeit ist die Zeit die ben tigt wird um das Fenster in Bewegung zu setzen 8Die Nummerierung am linken Rand dient nur zur Referenzierung 98 22 Val MC_FrontMotor Front_Motor F_MOTOR_Down 23 EE O Val MC_FrontMotor Front_Motor F_MOTOR_Down 24 amp amp OCO Val MC_FrontMotor Front_Motor F_MOTOR_Down 25 amp amp COCOCO Val MC_FrontMotor Front_Motor F_MOTOR_Down 26 EE COCOCOCO Val MC_FrontMotor Front_Motor F_MOTOR_Down 27 EE COCOCOCOCO Val MC_FrontMotor Front_Motor F_MOTOR_Down 28 EE COCOCOCOCOCO Val MC_FrontMotor Front_Motor F_MOTOR_Down 29 EE COCOCOCOCOCOCO Val MC_FrontMotor Front_Motor F_MOTOR_Down 30 EE COCOCOCOCOCOCOCO Val MC_FrontMotor Front_Motor F_MOTOR_DoWwm St EE COLCOCOCOCOCOCOCOCO Val MC_FrontMotor Front_Motor F_MOTOR_DoWwm 32 33 3 35 Im Einzelnen bedeuten die Zeilen Zeile 1 F r alle Systemzust nde gelten Zeilen 2
5. Beispiel 7 1 7 Der Fahrer auf der linken Fahrzeugseite dr ckt die Ta ste zum manuellen Runterfahren des Beifahrerfensters Das rechte TSG erh lt ber den CAN Bus die neue Anweisung zum Herunterfahren der vorderen rechten Fensterscheibe Schritt 3 a Diese Anweisung wird an die Motoransteuerung weitergeleitet und f hrt zur Runterbewegung der Scheibe Schritt 3 b Danach bet tigt der Beifahrer auf der rech ten Seite die Taste zum manuellen Runterfahren derselben Fensterscheibe Anweisung vom selben Typ wie die des Fahrers Das TSG verarbei tet das Signal und leitet es an die Motoransteuerung weiter Schritt 3 a und 3 b W hrend sich die Scheibe noch in Bewegung befindet l sst der Fahrer nun die Taste los und ber den CAN Bus gelangt das Signal Neutrale Stellung an das Beifahrer TSG Da der Beifahrer aber noch die eigene Fensterhebertaste gedr ckt h lt zeigt dies folgerichtig keine Wirkung Bedingung in Schritt 1 trifft nicht zu Erst wenn der Bei fahrer seine Taste losl sst wird die Bedingung in Schritt 1 erf llt und Schritt 2 ausgef hrt 6 manueller Fensterbewegungsmodus mit gleicher Bewegungsrichtung Die Unterscheidung von Anweisungen erfolgt nach Eingang CAN Taste Mo dus manueller automatischer Fensterbewegung und Richtung hoch bzw runter 74 Front Motor bzw BackMotor trigger ate Ce iber OC BLO wi o Lr ltered trigger Out_B_LOW_WIN pe
6. Die Erstellung der Testdaten erfolgte zun chst nach demselben Sche ma wie in 7 2 um die grundlegende Funktionalit t zu testen Mit Hilfe der Code berdeckungsanalyse wurden dann Codestellen ausfindig gemacht die noch nicht dem Co Kriterium bzw der einfachen Be dingungs berdeckung gen gt haben Da die Umsetzung von ASCET Modellen hier fast ausschliesslich Zustandsautomaten in C Code oh ne gr ssere Hilfskonstruktionen erfolgt konnten die betreffenden Stellen den entsprechenden Modellteilen Verzweigungsbedingungen Transitio nen etc ohne Schwierigkeiten zugeordnet werden Damit konnten dann weitere Testdaten erzeugt werden um diese Stellen gezielt abzudecken 7 4 Rapid Prototyping Viele Aspekte wie z B das Fahrgef hl oder die Einwirkung einer rea len Umgebung auf das Steuerger t k nnen teilweise nicht oder nur un vollst ndig mit Hilfe einer Simulation erfasst werden Eine M glichkeit dieses Problem w hrend der Entwicklungsphase zu umgehen stellt das Rapid Prototyping dar Wie schon im Abschnitt 3 2 3 angedeutet wurde kann die Funktionalit t damit fr hzeitig getestet und abgesichert werden F r die Zwecke der Diplomarbeit standen eine Fahrzeugt r der Firma BMW und Rapid Prototyping Hardware der Firma ETAS zur Verf gung Der Aufbau f r das Rapid Prototyping Experiment wird in Bild 7 6 ver anschaulicht Das eigentlich in sp teren Entwicklungsstufen in der Fahrzeugt r ver SU Entwicklungs platt
7. 2 2 Eau ana nr ne 95 8 3 1 Verifikation des Einklemmschutzes 97 9 Evaluierung 103 9 1 Bewertung der Werkzeuge 103 9 1 1 Modellierung 255 22 SE Era BR Si 104 9 1 2 Zeitlicher Aufwand bei der Modellierung 105 9 1 3 Zusammenhang zwischen Modell und Code 108 9 2 Bewertung der Qualit tssicherungsmethoden 110 10 Fazit und Ausblick 117 A Spezifikationssprachen 120 AE GER a ea EE EE EE 120 SL Ya A EEE REIT 120 A 1 2 Semantik 3 2 2 8 zusam aa a ar al 120 ADS Di KREE EE 121 A2 We Be ee ae 121 A22 Semantik an Sees ae ee ee G 121 B Hardware Schnittstelle des T rsteuerger tes 123 B 1 Stecker S1 Anschluss von Elementen der Vordert r 123 B 2 Stecker S2 Anschluss von externen Elementen 124 C Modellierung in ASCET 126 Cl Benutzerdefinierte Datentypen 126 C 2 Nachrichten 2 2 2 oo oo nn 127 Abbildungsverzeichnis 130 Tabellenverzeichnis 132 Literaturverzeichnis 133 Kapitel 1 Einleitung Sowie fr her die Elektronik ihren Einzug in das allt gliche Leben gefun den hat spielt heutzutage die Software in eingebetteten Systemen eine zunehmend wichtigere Rolle Die Funktionalit t eines Produktes wird in vielen F llen massgeblich durch Software bestimmt In vielen Industrie zweigen stellt dies einen wettbewerbsentscheidenden Faktor dar Dies trifft ebenso auf den Automobilbausektor zu der zudem durch ho he Sicherheitsanforderungen an die Komponenten eines Kraftfahrzeuges gekenn
8. send mit der ASCET RP Erweiterung der entsprechende Code f r die Prototyping Hardware generiert und auf das Ger t geladen Damit l sst sich das Modell in der realen Umgebung ausf hren Die Funktionalit t kann damit schon fr hzeitig w hrend des Entwicklungsprozesses validiert werden 6 1 3 ASCET SE Der Schwerpunkt von ASCET MD bzw ASCET RP liegt in der Funkti onsentwicklung Im Gegensatz dazu konzentriert sich ASCET SE auf die Codegenerierung Bei der Codegenerierung f r die Zielplattform sind eingeschr nktere Ressourcen zu beachten Dazu geh ren zum Bei spiel der begrenzte Speicherplatz und die beschr nkten Datentypen der Zielplattform Ebenso kann eine Abbildung der Gleitpunktarithmetik in physikalischen Gleichungen auf die Fixpunktarithmetik vorgenommen werden ASCET SE kapselt die Unterschiede zwischen verschiedenen Plattformen so dass ASCET MD damit auf eine einheitliche Schnitt stelle zur ckgreifen kann Erst bei der Codegenerierung im Rahmen von ASCET SE werden target spezifische Aspekte ber cksichtigt 56 6 2 _ Unterst tzende Werkzeuge Die folgenden Abschnitte beschreiben die Werkzeuge die im Zusammen hang mit ASCET und den Testmethoden aus Abschnitt 7 3 Anwendung fanden 6 2 1 IBM Rational Test RealTime Zur berdeckungsanalyse bei der Anwendung von konventionellen Qua lit tssicherungsmassnahmen wurde auf das Testframework Test RealTi me von IBM Rational zur ckgegriffen Damit l sst sich C Co
9. wenn bei einem Systemtick eine CAN Nachricht anliegt erh lt entsprechender Kanal diesen Wert Tabelle 8 1 Schnittstellenkonvention in AutoFOCUs Annahmen an die Umgebung Die oben definierte Schnittstelle muss von der Umgebung eingehalten werden Notfalls ist diese Voraussetzung durch den Einsatz von Wrapper Komponenten zur erf llen Diese bilden dann das geforderte Schnitt stellenverhalten der Umgebung auf die obige Schnittstellendefinition ab Eine konkrete Schnittstelle ist stark implementationsabh ngig und korre liert z B mit den Echtzeiteigenschaften und dem Task Scheduling z B von OSEK Daher erfolgt hier die Konzentration auf die Hauptlogik gem ss der TSG Spezifikation und eine Abstraktion wie beim ASCET Modell Analog zu Abschnitt 7 1 1 m ssen die Konfigurationswerte z B RL oder FCODE_TO vor Inbetriebnahme der Funktionen zun chst ber den CAN Bus eingelesen werden Ein leerer Kanal NoVal wird hier als g ltiger Wert interpretiert um der Zustandsraumexplosion beim Modelchecking entgegenzuwirken Ein leerer Kanal NoVal bedeutet hier dass keine CAN Nachricht anliegt siehe Fussnote 2 85 8 1 2 Aufbau und Funktionsweise Der Aufbau und die Funktionsweise gleichen prinzipiell dem ASCET Modell aus Abschnitt 7 1 2 so dass hier im Wesentlichen die Unterschiede zu dessen Beschreibung hervorgehoben werden Die Funktionen werden auf die Hauptkomponenten Windows DoorLock und Ligh
10. 109 Grund ist der grosse Freiheitsgrad seitens C Eine direkte bijektive Abbil dung einzelner C Konstrukte nach AutoFOCUS w rde zudem den Vorteil der Modellierung zunichte machen Man k nnte dann gleich in C pro grammieren Vorteile der modellbasierten Entwicklung gegen ber der Programmie rung auf Codeebene ergeben sich durch die bessere Verst ndlichkeit Zu sammenh nge k nnen grafisch visualisiert und damit schneller erkannt werden Bei steigender Team und Projektgr sse l sst sich der berblick leichter behalten Die hierarchische Strukturierung des Systems tr gt dazu bei Auch Laien k nnen sich somit schneller in ein existierendes Modell einarbeiten was die sp tere Wartung eines Systems durch Drit te vereinfacht Weiterhin k nnen Standardkomponenten Bibliotheken entnommen werden und per drag amp drop einem System hinzugef gt wer den Systeme wie z B Regelstrecken lassen sich damit einfach zusam menklicken und auf die Schnelle simulieren Allerdings k nnen sich auch bei der Erstellung von Modellen Fehler ein schleichen Als pr ventive Massnahme k nnen z B unternehmensspezi fische Modellierungsrichtlinien wie z B Hua04 dazu dienen Leicht sinnsfehler zu vermeiden Auch deren automatische berpr fung durch entsprechende Werkzeuge ist m glich Trotz der in Abschnitt 2 2 genannten Vorteile der automatischen Code generierung ist der Einsatz in manchen F llen nicht m glich Beispiels weise wenn h
11. 180V BLINK BLINK_Of kein Blinken BLINK_50 0 5 Sekunden lang Blinken BLINK_100 1 Sekunde lang Blinken FHB FHB_Neutral kein Befehl von der Fensterheberbedienung FHB_DownAuto Befehl zum automatischen Herunterfahren des Fensters bis zum Anschlag FHB_DownMan Befehl zum Herunterfahren des Fensters FHB_UpMan Befehl zum Hochfahren des Fensters FHB_UpAuto Befehl zum automatischen Hochfahren des Fensters bis zum Anschlag FZENTR_MOT FZENTR_MOT_Neutral kein Befehl an Fond Verriegelungsmotoren FZENTR_MOT_Open Befeh zum Offnen an Fond Verriegelungsmotoren FZENTR_MOT _Close Befeh zum Schliessen an Fond Verriegelungsmotoren KEY_STATE KEY_STATE_Neutral T rschloss nicht gedreht KEY_STATE_Lock T rschloss aufschliessen KEY_STATE_Unlock T rschloss zuschliessen VERDECK VERDECK_Opened Cabriolet Verdeck ge ffnet VERDECK_Opening Cabriolet Verdeck beim Offnen VERDECK_Closing Cabriolet Verdeck beim Schliessen VERDECK_Closed Cabriolet Verdeck geschlossen 126 WIN_CAN WIN_CAN_Invalid ohne Wirkung WIN_CAN_Move Befehl vom CAN Bus zum Bewegen des Fen sters WIN_CAN_MoveEnd Befehl vom CAN Bus zum Bewegen des Fen sters bis zum Anschlag WIN_MOTOR WIN_MOTOR_Neutral ohne Wirkung WIN_MOTOR_Close Befehl zum ffnen an Fensterhebermotoren WIN_MOTOR_Open Befehl zum Schliessen
12. DoorLock_Out_BLINK BLINK CAN Ausgang periodisches Signa DoorLock_Out_FZENTR_MOT FZENTR_MOT S2 Ausgang kontinuierliches Stellsignal DoorLock_Out_ZENTR_MOT ZENTR_MOT S1 Ausgang kontinuierliches Stellsignal DoorLock_Out_ZV_SCHL_L ZV_SCHL CAN Ausgang periodisches Signa DoorLock_Out_ZV_SCHL_R ZV_SCHL CAN Ausgang periodisches Signa DoorState_In_DOOR_STATE Boolean CAN Eingang periodisches Signa VL DoorState_In_DOOR_STATE Boolean CAN Eingang periodisches Signa VR Signale mit dem Pr fix TSG werden gleichzeitig auf mehrere Module verteilt in ASCET geschieht die Verteilung ber Namensaufl sung 127 DoorState_In_DOOR_STATE HL DoorState_In_DOOR_STATE HR DoorState_In_F_T_OFFEN_V DoorState_In_F_T_OFFEN_H TSG_In_FCODE_T1 TSG_In_LL TSG_In_RL DoorLight_Out_T_LICHT DoorLight_Out_FT LICHT InteriorLight_In_KL InteriorLight_Out_I_LICHT Windows_Back_In_FHB_VL Windows_Back_In_FHB_VR Windows_Back_In_FHB_HL Windows_Back_In_FHB_HR Windows_BackMotor_In_FF _BEWEG Windows_BackMotor_In_FF _OBEN Windows_BackMotor_In_FF _UNTEN Windows_BackMotor_Out_FF _MOTOR Windows_CAN_Back_Out WIN_HL_CL Windows_CAN_Back_Out _WIN_HL_OP Windows_CAN_Back_Out _WIN_HR_CL Windows_CAN_Back_Out _WIN_HR_OP Windows_CAN_Front_Out WIN NL CL Windows CAN Front Out _WIN_VL_OP Windows_CAN_Front_Out _WIN_VR_CL Windows_CAN_Front_Out _WIN_VR_OP Windows_Front_In_F_BEWEG Windows Front In H LOBEN Windows Front In H UNIEN Windows
13. E T E A pUy 4 F r alle Pfade a in T existiert ein i N so dass t M cllk und Yj lt i t M allt A 2 LTL A 2 1 Syntax LTL Formeln ergeben sich durch die rekursive Anwendung der Regel p P pVp p Xp Fp Gp pUp pRp mit P als Aussagenvariable A 2 2 Semantik Die folgenden Bemerkungen gelten f r den Abwicklungsbaum T t M s einer Kripke Struktur M s mit M S R L ber den Aus sagenvariablen mu D p und up stellen hier LTL Formeln dar LTL Formeln werden ber Pfade m interpretiert F r einen Pfad m S0S1 SiSi 1 Sn bezeichnet der Ausdruck ji das Pfadelement s m fi bezeichnet den Pfad der ab der Position i im urspr nglichen Pfad m be ginnt wobei ab 0 indiziert wird Die Menge der nat rlichen Zahlen N enthalte hier die 0 Eine Kripke Struktur M s erf llt eine LTL Formel p gdw alle unendlichen Pfade von t M s die Formel o erf llen Fol gende Beziehungen dr cken aus wann ein Pfad m eine Formel erf llt TE pi gt p L r 0 nFp lt gt TE Ee TE y oder zk zk Ku 1r1T1Fp zk Gu lt gt Mi CENaT ku ak Fo lt gt Z eNafikue 121 zk ein Hi EeN mrTiF y AY Sj lt i gt rT jF o 122 Anhang B Hardware Schnittstelle des T rsteuerger tes Folgende Tabellen geben eine bersicht ber die Zuordnung der An schl sse der peripheren Komponenten zu den Steckerschnittstellen des T rsteuerger ts Weitere Details k nnen PH02 entno
14. Modul Modul 9 u mesglcont 0 inactive B 1 Task20ms active 00 xO mesgleont 1 active START CT calc Modul SS a 2 Taskis active BRD e init Modul Abbildung 6 4 Scheduling in ASCET gehen bei Modulen Eine Klasse stellt eine Art Template dar Dessen Instanzen k nnen in Modulen mehrfach eingesetzt werden Die Prozesse in diesen Modulen k nnen somit auf die Methoden der Klasse zur ckgreifen Der Aufruf ei ner Methode st sst den dazugeh rigen Berechnungsablauf an und liefert ggf ein Ergebnis ber den Ausgabeparameter zur ck Oft wiederver wendete Berechnungen und Strukturen lassen sich damit in Bibliotheken zusammenfassen Mit diesen Modellierungskonstrukten lassen sich diskrete sowie konti 55 nuierliche regelungstechnische Berechnungsabl ufe darstellen Aus den erstellten Modellen kann in ASCET MD Code f r die Entwicklungsplatt form generiert werden Sie lassen sich somit simulieren Details k nnen Gmb03a GmbO3b entnommen werden 6 1 2 ASCET RP Rapid Prototyping mit Hilfe von ASCET RP erm glicht die Validierung eines ASCET MD Modells Daf r bietet ETAS Hardwarel sungen an die sich in ein Fahrzeug einbauen lassen und mit dessen Aktoren bzw Sensoren interagieren k nnen Beim Rapid Prototyping wird typischer weise solch ein Ger t anstelle des eigentlichen Steuerger tes im Regel kreis platziert F r das in ASCET MD erstellte Modell wird anschlies
15. Varianten Versionsverwaltung Anforderungsmanagement Erfassen und Verfolgen von An forderungen Lieferantenmanagement Verwalten der firmen bergreifen den Zusammenarbeit Qualit tssicherung Massnahmen zur Qualit tspr fung und sicherstellung Tabelle 2 2 Unterst tzungsprozesse Die enge Verzahnung der verschiedenen Prozesse untereinander ist an Hand der Qualit tssicherung ersichtlich Neben Richtlinien kommen hier auch Massnahmen zur Anwendung die sich im rechten Ast in Bild 2 1in Form von Tests wiederfinden Kapitel 3 geht nochmals n her darauf ein 19 Einen weiteren wichtigen Schritt zur Beherrschung der steigenden Kom plexit t von elektronischen Ger ten im Automobil stellt die Einf hrung von standardisierten Schnittstellen dar Dazu haben sich namhafte in ternationale Automobilhersteller und Zulieferer zum AUTOSAR Kon sortium zusammengeschlossen AUTb Ziel ist die Erarbeitung einer einheitlichen Software Infrastruktur und von Schnittstellen in Form von Standards Die Software kann dadurch modularer gestaltet werden Bes ser ausgetestete Software Komponenten k nnen somit vermehrt wieder verwendet werden ECU 1 ECU 2 Software Komponente 2 Software Komponente 3 Software Komponente 1 Software Software Software Komponente 1 Komponente Komponente 3 RTE Basis Software ECU Hardware Basis Software ECU Hardware Abbildun
16. bei automatisierten Tests ausgew hlte benutzerspezifische Eigenschaf ten Tabelle 10 1 Testen vs Modelchecking Dar ber hinaus existieren noch weitere vielversprechende Ans tze Tools und Techniken zur Qualit tssicherung auf die im Folgenden nur hinge wiesen wird e Der Symbolic Polyspace Verifier der Firma Polyspace verwen det das statische Verfahren der abstrakten Interpretation um 117 Schwachstellen in einem Programm auszumachen Pol e Einen weiteren Testansatz stellt das evolution re Testen dar sys Dabei werden Testf lle durch iterative Bewertung und Rekombina tion optimiert e Den in AutoFocus betrachteten Systeme liegt ein globaler Sy stemtick und somit eine Diskretisierung der Zeit zu Grunde Syste me k nnen jedoch auch mit Hilfe von Zeitautomaten beschrieben werden Somit lassen sich Echtzeitsysteme in Werkzeugen wie Up paal2k modellieren und berpr fen UPP Die hier angesprochenen und in den vorhergehenden Kapiteln behandel ten Software Qualit tssicherungsmethoden haben ein gemeinsames Ziel Die Erstellung korrekt funktionierender Software Bekannt ist aber auch dass eine Kette nur so stark ist wie ihr schw chstes Glied Daher sollte die Absicherung von Software im Ein klang mit der Hardware stehen Denn nur wenn diese die Annahmen erf llt die z B beim Modelchecking an das Modell gestellt wurden ist ein fehlerfreier Ablauf des Gesamtsystems m glich Ans
17. hrt Der Abgleich des Modells mit dem Sour cecode erfolgt ber einen diversifizierenden Testansatz Hierbei liegen unterschiedliche Versionen des Testobjekts vor die dieselbe Spezifikati on erf llen sollen Alle Testf lle f hren dann im fehlerfreien Fall bei allen Versionen zu identischen Resultaten Auf diese Weise k nnen Codegene ratoren bzw die manuelle Codeerstellung berpr ft werden 5 Eingabe Modell Ausgabe 3 ge Konkretisierung Codegenerierung Konkretisierung zc S konkrete m Ausgabe D S g Get Li konkrete E ingabe aktuelle Ausgabe Abbildung 3 4 Diversifizierender Testansatz Das berpr fte und getestete Modell dient als Referenz Dessen Testeingabe und Testausgabedaten werden als Referenzplots aufgezeich net Die Testeingabedaten auf Modellebene werden in entsprechende Eingabedaten f r die Software Ebene umgesetzt konkretisiert Analog wird mit den Ausgabedaten des Modells verfahren Aus dem Modell kann der Code generiert werden der mit den eben konkretisierten Ein gabedaten ausgef hrt wird Bei einer Abweichung der aktuellen Ausgabe von der konkretisierten Ausgabe kann man auf Fehler schliessen Man nennt dieses Verfahren auch Back to Back Test thier Modell bzw Sourcecode 37 Kapitel 4 Qualit tssicherungsverfahren akademischen Ursprungs Konventionelle Qualit tssicherungsverfahren zielen darauf ab Fehler zu finden Die Fehlerfreih
18. in dem ein verz gerter Alarm eintreffen kann ist dieses Flag gesetzt Bei gesetztem Flag wird ein Timeout Alarm nicht bearbeitet und ist daher wirkungslos Beleuchtung und weitere Teilaufgaben Zu den Komponenten DoorLight InteriorLight und DoorState wird auf die Beschreibung in Abschnitt 5 4 verwiesen 92 8 2 Testverfahren Im Rahmen der konventionellen Qualit tssicherung bietet sich in Au toFocus die Simulationsumgebung SimCenter an Der Ablauf der Be rechnungen der einzelnen SSDs und STDs eines Systems l sst sich hierbei visualisieren ber einen Editor k nnen je Systemtick die Eingabekan le des Modells mit Daten belegt werden Testdaten k nnen somit manuell eingegeben werden um Funktionen gezielt berpr fen zu k nnen An dererseits stellt das AutoFocus Framework mit dem Test Input Ge nerator TIG eine M glichkeit zur Verf gung Testdaten automatisch generieren zu lassen die dann z B f r die Simulation als Eingabedaten zur Verf gung stehen Der TIG analysiert die Schnittstelle des Modells zur Umgebung und gruppiert die Eingangskan le Zu jeder Gruppe wer den alle m glichen Tupel von Eingabewertekombinationen generiert und nacheinander im Test Data Format abgespeichert Die TDF Datei kann dann von SimCenter eingelesen werden Folgende Varianten zur Erzeugung von Testdaten bietet der TIG hierbei an Simple Input Generator Jeder einzelne Eingabekanal wird als Grup pe betrachtet Pair Input Genera
19. korrekt ist liefert der Modelchecker ein Gegenbeispiel Dieses kann als Testsequenz f r die Implementierung verwendet werden Im Gegensatz zum Testen basierend auf Modellen erm glicht der Va lidas Codegenerator auch das Testen auf Codeebene Es k nnen die in 3 2 2 erw hnten Verfahren auf den generierten Code angewandt werden Die Umsetzung der AutoFocus Modelle in Code erfolgt beim Validas Codegenerator hnlich wie beim ASCET Codegenerator auf eine kano nische Weise Daher kann man von Fehlern im Code leicht auf die ent sprechenden Modellteile schliessen um dort die Fehler zu beheben 8 3 Modelchecking Komponenten ab der Gr ssenordnung von Windows oder DoorLock wur den im Rahmen der Diplomarbeit nicht mehr verifiziert Grund war nicht der daf r notwendige Speicheraufwand sondern der Zeitaufwand von SMV Beispielsweise war SMV mit dem Nachweis der in Abschnitt 8 3 1 vorgestellten Eigenschaft f r Windows nach 3 Stunden immer noch nicht fertig mit der 4 Fixpunkt Iteration Im Vergleich dazu ben tigte der Nachweis der Eigenschaft f r die Subkomponente FrontMotor mit ber 400 Iterationen unter 4 Minuten SMV wurde daher vorrangig f r die Verifikation von Eigenschaften von Teilkomponenten mit weniger als 10 STDs verwendet Damit konnten logische Fehler ausgeschlossen bzw leicht ausgemacht werden Beispiel 8 3 1 Um zu berpr fen ob eine Implikation A gt B auch tats chlich zur Anwendung kommen kann kann die Erre
20. r die Kripke Struktur in Beispiel 4 2 1 Hier m ssten als Gegenbeispiel alle m glichen Pfade im Abwicklungsbaum aufgez hlt werden die diese Eigenschaft nicht erf llen wovon es unendlich viele gibt Wie eben angedeutet wurde liegt die Problematik beim Modelchecking in der Anzahl der erreichbaren Zust nde Bei sehr komplexen Syste men steigt diese Anzahl und damit w chst auch der Zustandsraum Das Problem der Zustandsraumexplosion macht sich in der Praxis bei Er reichen von Speicher und Zeitlimits schnell bemerkbar G ngige Model checker unterst tzen daher unterschiedliche Varianten und Erweiterun gen zur Implementierung des Algorithmus um dieser H rde entgegen zuwirken On the fly Modelchecker bauen w hrend des Verifikations LTL Formeln wird implizit ein einziger Pfad Allquantor vorangestellt Dies entspricht dem Vorgehen beim expliziten Modelchecking 43 vorganges nur den Teil des Zustandsraumes auf der ben tigt wird Dies reduziert den Speicheraufwand Symbolische Modelchecker hingegen basieren intern auf einer kompakten Repr sentation des Systems mit dem Ziel den Zeit und Speicheraufwand zu reduzieren 3Mittels Ordered Binary Decision Diagrams werden Kripke Strukturen als bool sche Formeln repr sentiert 44 Kapitel 5 Fallbeispiel T rsteuerger t Die Bewertung der bisher beschriebenen Qua lit tssicherungsmassnahmen erfolgt anhand eines Fallbeispiels aus der Automobili
21. ssen erst die CAN Nachrichten ausgelesen werden wie z B RL um entscheiden zu k nnen ob das Fahrzeug ein Rechts oder Linkslenker ist siehe TSG Spezifikation Dies erfordert eine Wartezeit von minde stens 500ms beim ersten Start da dies das gr sste Zeitintervall ist mit dem periodische CAN Nachrichten auftreten Die Werte k nnen z B im NVRAM abgespeichert werden so dass diese Wartezeit beim n chsten Start entf llt Bei sich ndernden Umst nden ist ein Neustart des Sy stems notwendig um z B neue Konfigurationen einzulesen 7 1 2 Aufbau und Funktionsweise Dieser Abschnitt befasst sich mit der Umsetzung der Spezifikation von Kapitel 5 in ein Projekt in ASCET Es werden die einzelnen ASCET Module vorgestellt T rschloss Das Modul DoorLock_Module ist f r die Zentralverriegelung zust ndig Bei einer Hysteresekurve erfolgt das Erkennen des h her liegenden Spannungspe gels bei einem h heren Schwellenwert als beim Erkennen des niedrigeren Spannungspe gels Dadurch wird ein Hin und Herflattern des Zustands bei kleinen Schwankungen vermieden 69 handelock_In_VERDECK handeLock In FCCDE_TO ERES handelock_In_ERRCR KEY handeLock In BATT handeLock_In_T AIESE handeLock_In FT RIESE handlelsck_In_dalck handleLock handleRequest handetequest_In_Door ignal_VL Word dl Wrdows_In_Lock tarr bse MuliplexSignds_In Lock ESCH Er MutiplexSignals_In_Lock_B_LOW_KEY 8 Muliplersignd
22. tze wie HIL Testverfahren zielen auf solch ein Zusammenspiel von Soft und Hard ware ab Im Bereich Automotive sollte somit der Einsatz von formalen Verifikationstechniken kein Verzicht auf konventionelle Testverfahren be deuten Deutlich wird aber auch dass Testverfahren und formale Verifi kationtechniken komplement re Qualit tssicherungstechniken darstellen die sich gegenseitig erg nzen und in Kombination angewandt einen Syner gieeffekt hervorbringen k nnen Weder die eine noch die andere Technik k nnen als die in allen Belangen Bessere identifiziert werden Das Potential von formalen Verifikationstechniken wie Modelchecking ist noch l ngst nicht ausgereizt so dass zur Zeit auf diesem Gebiet ei ne gewisse Dynamik bei den Werkzeugherstellern herrscht Dies r hrt auch daher dass die modellbasierte Entwicklung in industriellen An wendungen immer mehr Fuss fasst und dabei ebenfalls in Bereiche der Hardware Entwicklung vordringt Ebenso lassen sich die Qua lit tssicherungsverfahren nicht nur im Kontext der Automobilindustrie anwenden Technische Systeme jeglicher Art deren Software gewissen sicherheitskritischen Anforderungen Stand halten muss k nnen aus dem Einsatz von Modelchecking analog zu bisherigen Betrachtungen Vorteile ziehen 118 Einen wichtigen Meilenstein in der Automobilindustrie wird der aufkom mende AUTOSAR Standard darstellen Die Schnittstelle zwischen den einzelnen Software und Hardware Schichten kann al
23. Beim Ad Hoc Ansatz werden die Komponenten in einer zuf lligen Rei henfolge getestet und zusammengef gt Eine nicht inkrementelle Vorgehensweise stellt der Big Bang Ansatz dar Hier werden alle Komponenten erst einzeln getestet Nachdem das gesamte System integriert ist wird abschliessend nochmal getestet ohne dazwischenliegende Integrationsschritte 3 2 3 Testverfahren im Bereich Automotive Die oben besprochenen Verfahren sind im Laufe der Jahre im Kontext von IT Softwaresystemen entstanden Mit dem zunehmenden Anteil von Software im Automobil hat das Thema Software Testen auch hier an Relevanz gewonnen Allerdings kommen dabei dedizierte Testverfahren zur Anwendung die die Software in den Kontext eines Steuerger tes ein beziehen Der Zusammenhang zur Anwendungsdom ne und den anderen technischen Fachdisziplinen wird auch hier deutlich sichtbar Zum Beispiel fliessen im Kontext der Motorsteuerung Erfahrungen aus dem Maschinenbau und der Elektrotechnik ein In einem grafischen Tool siehe Kapitel 6 erstellt der Spezialist der Anwendungsdom ne ein rege lungstechnisches Funktionsmodell das die Z ndung ansteuert das Gas gemischt korrekt einstellt etc Stabilit tsbetrachtungen im Zusammen hang mit der Regelstrecke stehen hier im Vordergrund Dieses Modell wird dann an die Software Entwickler weitergereicht welche wiederum die technischen Anpassungen an die Hardware Umgebung und die Um setzung in Code manuell oder pe
24. Front Out _MOTOR Windows_Out_B_LOW_WIN Windows_Out_ERROR_WIN Windows_Request_Back_In _FFHB_HL Windows_Request_Back_In _FFHB_HR Windows_Request_Back_In _WIN_HL_CL Windows_Request_Back_In _WIN_HL_OP Windows_Request_Back_In AWIN HR CL Boolean Boolean Boolean Boolean Boolean Boolean Boolean Boolean Boolean Boolean Boolean FHB FHB FHB FHB Boolean Boolean Boolean WIN_MOTOR WIN_CAN WIN_CAN WIN_CAN WIN_CAN WIN_CAN WIN_CAN WIN_CAN WIN_CAN Boolean Boolean Boolean Boolean Boolean Boolean FHB FHB WIN_CAN WIN_CAN WIN_CAN CAN Eingang CAN Eingang CAN Eingang CAN Eingang CAN Eingang CAN Eingang CAN Eingang S1 Ausgang S2 Ausgang CAN Eingang CAN Ausgang S1 Eingang S1 Eingang S1 Eingang S1 Eingang S2 Eingang S2 Eingang S2 Eingang S2 Ausgang CAN Ausgang CAN Ausgang CAN Ausgang CAN Ausgang CAN Ausgang CAN Ausgang CAN Ausgang CAN Ausgang S1 Eingang S1 Eingang S1 Eingang S1 Ausgang CAN Ausgang CAN Ausgang S2 Eingang S2 Eingang CAN Eingang CAN Eingang CAN Eingang periodisches Signa periodisches Signa periodisches Signa periodisches Signa periodisches Signa periodisches Signa periodisches Signa kontinuierliches Stellsignal kontinuierliches Stellsignal periodisches Signa periodisches Signa kontinuierliches Sensorsigna kontinuierliches Sensorsigna kontinuierliches Sensorsigna kontinui
25. Model 86 DoorLock Komponente in Autobocug 2 87 Windows Komponente in AutoFOCUS 89 Front Motor in AutoFOCUS das rer 91 DispatchCommand in AutoFOCUS 2 2 2 2 92 Modellbasiertes Testen mit AutoFOCUS 94 Modularer Verifikationsansatz 2 2 2222 100 Beispielautomat zur Demonstration der Codeerzeugung 108 Code Einbindung in ACHT 109 131 Tabellenverzeichnis 2 1 2 2 3 1 3 2 3 3 3 4 3 5 7 1 8 1 9 1 9 2 9 3 10 1 C 1 C 2 Zuordnung von Funktionen zu Subsystemen 18 U nterst tzungspr zesse 2 02 SU FE a8 Dis 19 Einfache Bedingungs berdeckung 29 Mehrfachbedingungs berdeckung 30 Minimale Mehrfachbedingungs berdeckung 30 MOIDE pra pa Bu wi ine ee rar 31 Klassifikation der Testsysteme e 36 Schnittstellenkonvention in ASCET 66 Schnittstellenkonvention in AutoFOCUS 85 Zeitlicher Modellierungsaufwand 2 2 107 Anzahl gefundener Fehler 2 2 222220 111 Gefundene Fehler je Zeitaufwand 114 Testen vs Modelchecking 2 22 2000 117 Verwendete Datentypen in ASCET 127 Bedeutung der Nachrichten im ASCET Modell auf Modu lebens 4 282 2 282 8 ma ar Ba Margaret 129 132 Literaturverzeichnis Auta AUTb Bal00 BHS99 BS01 Cad CGA00 Com Est FTWT 05 G o6 AutoFOCUS 2 Website http wwwA4 in tum de
26. R f ri lt r R so 8r S0 SrSr41 S x S Sr Sr41 R L S PPa mit L so s L r Beispiel 4 2 2 Zur Veranschaulichung wird der Abwicklungsbaum t M so f r das oben angegebene Beispiel M so angegeben KN so 5051 5082 505152 508183 805251 50818281 S0S2S152 50828183 5081825182 41 R s0 5051 50 5052 5051 508152 5051 505153 5052 505251 505152 50815251 L so L sos p1 p2 L sos2 pa L s0os182 P2 L sos 53 p2 L 505281 P Pa Got SoS Htp pe SoS2F p2 y y S081S3H p2 508182H p2 5082S1F p p2 Y y SH 508182S1F p1 p2 S0S2S1S2F p2 508251S3H p2 Y Y 4 2 2 Spezifikationsprache Mit Hilfe einer Spezifikationssprache k nnen Eigenschaften die beim Sy stem nachgewiesen werden sollen formuliert werden Es existieren ver schiedene Varianten wobei hier nur auf CTL Computation Tree Logic und LTL Linear Time Temporal Logic eingegangen werden soll Die Syntax und die Semantik von CTL und LTL finden sich im Anhang A Nicht alle Eigenschaften lassen sich mit diesen beiden Sprachen zei gen Zudem existieren f r beide Sprachen Eigenschaften die in der jeweils anderen Sprache nicht formuliert werden k nnen Die Aus drucksm glichkeiten von CTL und LTL bilden nur eine Schnittmenge CTL Abbildung 4 1 Inklusionseigenschaft von Spezifikationssprachen Da man in L
27. Stuttgart 2003 N Hartmann Automation des Tests eingebetteter Systeme am Beispiel der Kraftfahrzeugelektronik PhD thesis Uni versit t Karlsruhe 2001 M Huang BMW Group ASCET SD 4 2 4 Modellierungs richtlinien 2004 Jan J rjens and Guido Wimmel Security Modelling for Electronic Commerce The Common Electronic Purse Spe cifications In Beat Schmid Katarina Stanoevska Slabeva and Volker Tschammer editors Towards the E Society Proceedings of 1st IFIP International Conference on E Commerce E Business and E Government pages 489 506 Kluwer Academic Publishers 2001 R Meinlschmidt BMW Group Modellierungsrichtlinien MATLAB Simulink Stateflow and TargetLink 2005 MISRA Guidelines for the Use of the C Language in Vehicle Based Software 1998 H Mann H Schiffelgen and R Froriep Einf hrung in die Regelungstechnik Hanser 2005 G J Myers Methodisches Testen von Programmen Ol denbourg 2001 B Paech and F Houdek Das T rsteuerger t Eine Bei spielspezifikation Technischer Report IESE Report Nr 002 02 D 2002 in German 134 Pol RCT RJd1CV04 SPHPO2 SPW04 sys SZ04 Tel The UPP Val WDO05 Wimo0 Wimo5 Polyspace Technologies http www polyspace com RCTA Inc http www rtca org B Remp J Jany M de la Cruz and A Vollerthun Leitfa den zur Testfall Erstellung Technical report BMW Group 2004 B Sch tz A Pretschner F Hub
28. Taskaktivierungen kann bei einem Offline Experiment in ASCET durch den Benutzer variiert werden Beim Modelchecking wurde fast die gesamte Zeit f r das Erstellen von Ei genschaften in Anspruch genommen Diese mussten mit der Spezifikation und dem Modell abgeglichen werden siehe oben Die Ausf hrungszeit des Modelcheckers auf den TSG Komponenten der unteren Hierarchie ebenen betrug in diesem Fall im Durchschnitt unter 5 Minuten Vor aussetzung ist ein Modell mit kleinem Zustandsraum vgl Abschnitt 8 3 Im Allgemeinen kann jedoch nicht von solch einer relativ kurzen Zeit ausgegangen werden Je nach Modellgr sse k nnen daf r mehrere Stunden oder Tage aufgewandt werden Es muss dann abh ngig von der Sicherheitsrelevanz ein individueller Kompromiss zwischen Modellgenau igkeit und Zeitaufwand gefunden werden Bei iterativen kleinen Verbesse rungen und anschliessendem Modelchecking summieren sich diese Zeiten zudem auf und ziehen den Prozess in die L nge Allerdings ist der Auf wand durch die Qualit t der damit erzielten Ergebnisse Ausmachen von schwer zu findenden Fehlern gerechtfertigt Wurde die Existenz eines Fehlers im Modell gezeigt so nahm auch des sen Lokalisierung Zeit in Anspruch Ein Gegenbeispiel muss zun chst ausgef hrt und interpretiert werden Auch dies erfordert ein intuitives Vorgehen im Zusammenhang mit der Spezifikation was schwer zu auto matisieren ist Diesen Prozess kann man durch Bounded Model Checking bes
29. Testen auf Modellebene Simulation Basierend auf dem erstellten ASCET Modell der T rsteuerung erfolg te die Anwendung von konventionellen Qualit tssicherungsmassnahmen Die Testverfahren k nnen sowohl auf das Modell als auch auf den daraus generierten C Code angewandt werden F r das Testen auf Modellebene stellt ASCET eine Simulationsumgebung zur Verf gung Bei dem als Offline Experiment bezeichneten Verfahren erfolgt die Ausf hrung des generierten Codes auf dem PC Durch eine entsprechende Einbettung des Codes kann der Programmablauf in der Simulationsumgebung visuali siert werden Damit lassen sich Werte Nachrichten Variablen aktueller Zustand in Automaten etc mit Hilfe von numerischen und grafischen Anzeigen darstellen Denkbar w re auch eine Coverageanalyse der Au tomaten wof r zum jetzigen Zeitpunkt allerdings keine Unterst tzung in ASCET vorliegt Eine berdeckungsanalyse auf Modellebene wird zum Beispiel von Matlab Simulink mit dem Simulink Performance Tool unterst tzt The Auf einen In the Loop Ansatz wurde hier verzichtet da f r die berschaubaren Schnittstellen des TSGs zur Umgebung kein elaborier tes physikalisches Umgebungsmodell wie z B f r ein Fahrwerk erfor derlich war Im vorliegenden Fall wurden haupts chlich Tests auf den ASCET Modulen durchgef hrt Ein Grund daf r ist die weitgehende Unabh ngigkeit der Module untereinander Die Testf lle sind der Spezifikation nach folgendem Schema e
30. af AUTOSAR Website http www autosar org H Balzert Lehrbuch der Software Technik Software Entwicklung Spektrum Akademischer Verlag 2000 M Broy F Huber and B Sch tz AutoFocus Ein Werkzeugprototyp zur Entwicklung eingebetteter Systeme Informatik Forschung und Entwicklung 13 3 121 134 1999 M Broy and K Stolen Specification and Development of Interactive Systems Springer 2001 Cadence SMV http embedded eecs berkeley edu Alumni kenmcmil smv E M Clarke O Grumberg and Peled D A Model Checking MIT Press 2000 International Electrotechnical Commission http www iec ch Esterel Technologies http www esterel technologies com S F rst H Treseler T Woeniger Trausenecker A Buch wieser H Putzer and A Vollerthun BMW Group Stan dard 95014 Embedded Software Entwicklung 2005 M G rtner Efficient Development of Embedded Automoti ve Software with IEC 61508 Objectives using SCADE Drive http www esterel technologies com files EW 2006 133 Gmb Gmb03a Gmbo3b Gmb03c Har01 Hua04 JW01 Mei05 MIS98 MSFO5 Mye0l PHO2 Efficient Development of Embedded A utomotive Software with IEC 61508 Objectives using SCADE Drive pdf 2006 ETAS GmbH http www etas de ETAS GmbH ASCET V5 0 Benutzerhandbuch Stuttgart 2003 ETAS GmbH ASCET V5 0 Referenzhandbuch Stuttgart 2003 ETAS GmbH ASCET V5 0 Schnelleinstieg
31. an Fensterhebermotoren ZENTR_MOT ZENTR_MOT_Neutral kein Befehl an Front Verriegelungsmotoren ZENTR_MOT_Open Befeh zum ffnen an Front Verriegelungsmotoren ZENTR_MOT_Close Befeh zum Schliessen an Front Verriegelungsmotoren ZV SCHL ZV_SCHL_KeepState ohne Wirkung ZV_SCHL_Lock Befehl vom CAN Bus zum Verriegeln ZV_SCHL_Unlock Befehl vom CAN Bus zum Entriegeln Tabelle C 1 Verwendete Datentypen in ASCET C 2 Nachrichten Nachricht Datentyp Schnittstelle Schnittstellentyp TSG_In_BATTT BATT CAN Eingang periodisches Signa DoorLock_In_ERROR_KEY Boolean CAN Eingang spontanes Signal DoorLock_Out_ERROR_KEY Boolean CAN Ausgang spontanes Signal TSG_In_FCODE_TO Boolean CAN Eingang periodisches Signa TSG In FT_OFFEN Boolean S2 Eingang kontinuierliches Sensorsignal DoorLock_In_FT_RIEGEL Boolean S2 Eingang kontinuierliches Sensorsignal DoorLock_In_KEY_STATE KEY_STATE S1 Eingang kontinuierliches Sensorsignal DoorLock_In_KL_START Boolean CAN Eingang periodisches Signa DoorLock_In_MOTOR_LFT Boolean CAN Eingang periodisches Signa TSG_In_T_OFFEN Boolean S1 Eingang kontinuierliches Sensorsignal DoorLock_In_T_RIEGEL Boolean S1 Eingang kontinuierliches Sensorsignal DoorLock_In_VERDECK VERDECK CAN Eingang periodisches Signa DoorLock_In_ZV_SCHL_A ZV_SCHL CAN Eingang periodisches Signa DoorLock_In_ZV_SCHL_L ZV_SCHL CAN Eingang periodisches Signa DoorLock_In_ZV_SCHL_ R ZV_SCHL CAN Eingang periodisches Signa DoorLock_Out_B_LOW_KEY Boolean CAN Ausgang spontanes Signal
32. eine 100 ige Testabdeckung m sste jeder Pfad mindestens einmal durchlaufen werden In der Praxis ist dies fast nie erreichbar da while Schleifen unter Umst nden unendlich oft durchlaufen werden k nnen Daher dient die Cs berdeckung eher als theoretisches Vergleichsmass Eine 100 ige Abdeckung von Pfaden erreicht man unter Umst nden mit Hilfe einer Abschw chung Es werden dann nur Pfade betrachtet deren while Schleifendurchl ufe an eine festgelegte Anzahl gebunden sind Bedingungs berdeckungstests Die obigen berdeckungskriterien waren vorwiegend kontroll flussorientiert Daneben gibt es auch noch bedingungsbasierte berdeckungskriterien Diese betreffen die Bedingungen in einem Programm z B an ifEntscheidungsstellen die den Programmablauf beeinflussen Eine zusammengesetzte Bedingung kann in atomare Ausdr cke zerlegt werden Zum Beispiel besteht die C Bedingung aBool amp amp bInt lt cInt dBool aus den drei atomaren Ausdr cken aBool bInt lt cInt und dBool F r eine 100 ige Abdeckung des Testobjekts existieren damit verschiedene berdeckungskriterien die beim Testen je Bedingung im Programm angewandt werden k nnen 1 Einfache Bedingungs berdeckung branch condition testing Jeder atomare Ausdruck muss mindestens einmal zu wahr bzw falsch aus gewertet worden sein Das Kriterium wird f r oben genannen Beispiel ausdruck erf llt wenn w hrend des Testablaufs folgende Ausw
33. mit Hilfe von Modellen beschreiben SPW04 Vorteile ergeben sich daraus durch die Einschr nkung des Interpretationsspiel raumes Die internen Zusammenh nge eines formalen Modells k nnen iterativ verfeinert d h genauer spezifiziert werden Modelle lassen sich dadurch soweit konkretisieren dass sie als ausf hrbares Programm um gesetzt werden k nnen Sie erlauben somit eine fr hzeitige Validierung gegen ber den eingangs gestellten Anforderungen des Auftraggebers Eine iterative Verfeinerung des Modells bis hin zur Implementierungsebe ne f hrt zu einem ineinandergreifenden bergang der Entwicklungspha sen Unterst tzung hierbei leisten CASE Werkzeuge siehe Kapitel 6 Mit ihrer Hilfe lassen sich Funktionsmodelle zun chst ohne detaillierte Programmierkenntnisse erstellen Experten aus der Anwendungsdom ne k nnen somit das Verhalten spezifizieren ohne sich Gedanken ber kon krete implementationstechnische Einschr nkungen Datentypenkonver tierungen etc machen zu m ssen Zudem k nnen Simulationen und Rapid Prototyping Kapitel 7 4 die Anforderungen absichern Mehr deutigkeiten und fehlende Beschreibungen im Lastenheft k nnen somit ausgemacht werden Dies l sst ein fr hzeitiges Erkennen und Beseitigen von Fehlern zu ohne den gesamten Fehlerbehebungszyklus siehe Kapitel 2 1 nochmals durchlaufen zu m ssen In der Implementierungsphase erfolgt die bersetzung der Modelle in Code Die manuelle Umsetzung der Modelle von
34. nicht so effi zient eingegangen werden wie bei der manuellen Programmierung von Hand Auf lange Sicht kann dieser Nachteil jedoch vernachl ssigt wer den da die Leistung und Ressourcen zuk nftig eingesetzter Hardware tendenziell zunehmen Bei ausreichend vorhandenen Ressourcen wiegen die genannten Vorteile der Codegenerierung auf was einen weiteren Grund f r den Einsatz der modellbasierten Entwicklung darstellt Als konkretes Beispiel f r eine Werkzeugkette das einen modellbasier ten Entwicklungsprozess unterst tzt sei hier die SCADE Suite erw hnt 15 G 06 Die Firma Esterel Technologies Est stellt damit eine mo dellbasierte Entwicklungsumgebung mit zertifiziertem Codegenerator zur Verf gung 2 3 Software Entwicklung im Bereich Au tomotive Randbedingungen wie die eingeschr nkten Ressourcen die hohen Sicherheits und Zuverl ssigkeitsanforderungen erfordern ein anderes Vorgehen bei der Entwicklung von Software f r das Automobil im Ge gensatz zur traditionellen Softwareentwicklung von IT Softwaresystemen Im folgenden soll deswegen auf einige Konzepte und technische Begriffe die in der Automobilindustrie Anwendung finden eingegangen werden Die Regelung und Steuerung von physikalischen Vorg ngen im Kraftfahr zeug erfolgt in zunehmendem Masse durch Steuerger te Ein Steuerger t bzw eine ECU ist ein elektronisches Modul in Form eines eingebette ten Systems dessen Funktionalit t durch die darauf laufende S
35. rsteuerger t bernimmt UnlockSynchronize bzw LockSynchronize CloseWindows st sst bei entsprechender TSG Konfiguration das 87 Schliessen der Fenster an Konflikte bei gleichzeitigen ffnen und Schliessbefehlen werden hier ebenso umgangen indem die Komponente handleLock beim Eintreffen eines ffnenbefehls blockiert wird Zum Zeitpunkt der Erstellung der Diplomarbeit wurden noch keine hierarchischen STD Zust nde von der Modelchecking Anbindung unterst tzt Daher wurden die beiden Modi Blockiert und Unblockiert in Lock auf einen Automaten ohne Unter zust nde abgebildet MultiplexSignals Die von handleLock und handleUnlock erzeugten Signale werden ber MultiplexSignals ausgegeben W hrend einer ffnenaktion werden nur die Signale von handleUnlock weitergeleitet Ansonsten diejenigen von handleLock Fensterheber Die Komponente Windows ist f r den Fensterheber zust ndig siehe Bild 8 3 Dispatcher verteilt die eingehenden Signale an die betreffenden Komponenten CAN Front bzw CAN Back Beide Komponenten funktionieren auf dieselbe Weise wie der entspre chende Teil des ASCET Modells Daher wird an dieser Stelle auf Ab schnitt 7 1 2 verwiesen Request_Front bzw Request_Back Request_Front und Request_Back unterscheiden sich in der Art und An zahl der Eing nge Beide Komponenten verarbeiten Benutzeranweisun gen nach derselben Arbeitsweise wie in Abschnitt 7 1 2 Im ASCET Modell erfolg
36. stemtick zur Verf gung Das zugeh rige SSD kann statt der normalen Ports auch ber sogenannte Immediate Ports an die anderen Komponenten angebunden sein Falls dies der Fall ist stehen die Nachrichten schon im selben Systemtick den anderen Komponenten zum Auslesen zur Verf gung Der Ablauf ist formal durch die Semantik von AutoFocus definiert und kann Wim05 entnommen werden 5 Zahl lt 5 Eingang Zahl 5 Zahl gt 5 Eingang Zahl Priorit t Eingang de Ingang zan R hb ga EES e EE 5 Zahl 5 Eingang Zahl AusganglFalse Abbildung 6 7 Beispiel f r ein STD 6 3 3 Extended Event Traces EET Zur Beschreibung von konkreten Systemabl ufen werden Ereignisdia gramme eingesetzt Der zeitliche Verlauf des Nachrichtenaustausches zwischen mehreren Komponenten kann damit aufgezeichnet werden EETs k nnen zur Darstellung von Gegenbeispielen beim Modelchecking verwendet werden 60 6 3 4 Data Type Definitions DTD Benutzerdefinierte Datentypen k nnen f r lokale STD Variablen oder f r die zu bertragenden Nachrichten verwendet werden Sie befinden sich mit den auf ihnen operierenden Funktionen in Diagrammen f r Daten typdefinitionen DTD Die vier erw hnten Diagrammarten stellen jeweils eine eigene Sicht auf ein konkretes modelliertes System dar SPHPO2 Diesen Beschreibungs techniken liegt als gemeinsamer Nenner ein Metamodell zu Grunde das die Beschreibungselemente der Diagrammarten mite
37. und Aussagekr ftigkeit der Testl ufe Vie le grosse Testf lle im CTE Tool f hren zum Beispiel zu grossen Matri zen was auch nicht gerade zur bersichtlichkeit bei der Interpretation beitr gt Ein automatisiertes Vorgehen ohne menschliche Eingriffe ba sierend und ausgehend von einer formalen Spezifikation wie bei der mo delbasierten Testfallgenerierung k nnte hier Abhilfe schaffen Allerdings k nnen wie schon in Abschnitt 3 2 2 angedeutet alle Pfade durch ein Programm im Allgemeinen praktisch nicht zu 100 ausgetestet werden 114 Die Anzahl der m glichen Testf lle ist dazu zu hoch und die zeitlichen Ressourcen bei der Testplanung beschr nkt hnlich verh lt es sich beim Modelchecking Man kann im Allgemeinen auch hier kein 100 ig korrektes Modell unter allen Umst nden nachwei sen Lediglich die Korrektheit der gestellten Fragen hier der formulier ten Eigenschaften kann nachgewiesen werden Je mehr Eigenschaften nachgewiesen werden desto gr sser wird der Teil des abgedeckten Mo dellverhaltens Im Idealfall wird f r jede Anforderung der Spezifikation die entsprechende Eigenschaft nachgewiesen Folglich ist die Suche nach Fehlern bei komplexen Systemen einfacher als der Nachweis der Fehlerfreiheit eines Produkts Trotz eines Korrektheits nachweises nehmen folgende Fehlerquellen Einfluss auf das resultierende Produkt e Nichterf llung der gestellten Annahmen z B bei Hardware Problemen e Fehlerhafte Spezifik
38. zwischenzeitlich keine weiteren Ereignisse auftreten Eine naive Modellierung w rde z B alle Signal nderungen als neuen Befehl interpretieren und gem ss Spezi fikation diesen dann auch gleich ausf hren Wenn nun der Fahrer seine Taste zuerst loslassen und der Beifahrer seine Taste noch gedr ckt hal ten w rde dann w rde erstere Aktion f lschlicherweise als Stopbefehl f r die Fensterbewegung interpretiert werden Eine Ber cksichtigung dieses Umstandes f hrt zu einem komplexeren Modell Der im Vergleich zu ASCET h here Zeitaufwand resultierte unter ande rem auch aus der restriktiven Notation und der fehlenden M glichkeit zum Kopieren ganzer SSD Hierarchien inklusive dazugeh rigen STDs In AutoFocus 2 wurde dieses Defizit mittlerweile behoben Dieser Auf wand entf llt falls das Modell im Vornherein feststeht und sich nicht mehr im Nachhinein ndert In der Praxis kann diese Annahme jedoch nicht getroffen werden da sich Anforderungen auch w hrend der Ent wicklungphase ndern k nnen Relativiert wird dies durch die Tatsache das die erw hnte Kopierfunktion in AutoFocus 2 zur Verf gung stehen wird Im Rahmen des Modelcheckings wurden weitere Umstrukturierungen in Windows vorgenommen um das Problem der Zustandsexplosion in den Griff zu bekommen vgl Abschnitt 8 3 1 Dieser Eingriff dauerte eine Woche Modellierung in ASCET 106 Dadurch dass bei der Modellierung in AutoFocus die Hauptprobleme bei der Interpret
39. Das Erf llen eines informell spezifizierten Ziel z B Ausfall von mindestens zwei Komponenten oder eine Absch tzung des Anteils noch vorhande ner Fehler k nnen dabei als Testendekriterien dienen RJdICVO4 Ein weiteres oft eingesetztes Testendekriterium ist das Erreichen einer ge wissen berdeckungsgr sse als Mass f r den Grad der Vollst ndigkeit 25 eines Tests siehe Kapitel 3 2 2 Abzusehen ist von zeitlichen Limits als Abbruchkriterien da diese oft nicht mit der Fehlererkennungsrate kor relieren F r den Fall dass der Zeitplan f r das Testen dennoch nicht eingehalten werden kann sieht die Testplanung eine Testpriorisierung vor Wichtigere Tests werden dann bei zeitlichen Engp ssen vorgezogen Dynamische Testverfahren k nnen weiterhin in Black Box Tests und White Box Tests untergliedert werden Black Box Tests Bei der Betrachtung eines Objektes als Black Box ist dessen interne Struktur von aussen nicht sichtbar oder im betrachteten Kontext unbe deutend Bei Black Box Tests betrachtet man folglich nur funktionelle Gesichtspunkte des Testobjekts Zur Erstellung der Testf lle wird kei ne Information ber den inneren Aufbau des Testobjekts herangezogen Man greift hierbei auf die Spezifikation zur ck quivalenzklassentests Ziel dieser Black Box Test Variante ist es eine hohe Fehlerentdeckungs wahrscheinlichkeit mit einer minimalen Anzahl von Testf llen zu errei chen Dabei werden die Wertebe
40. ERROR_WIN Die Einbettung von FrontMotor in den Kontext des eigentlichen TSG Modells kann als Verfeinerung R von R angesehen werden Denn die von Ra gelieferten Eingabedaten In ber Battery_Front und Mo torFront stellen eine Untermenge der von Biz erzeugten chaotischen Eingabedatenmenge In dar Die Eingabe der Kan le Bottom_Front MovingSensor_Front und Top_Front bleibt weiterhin chaotisch da die se Kan le nach wie vor mit der externen TSG Umgebung interagieren und nicht ber Hi bzw Rin an FrontMotor gelangen Rout besteht aus den beiden STDs ResolveError und ResolveBattery die die Ausgabe von FrontMotor nur nach aussen weiterleiten Also ndert sich nichts an der akzeptierten Ausgabe ber den Kanal Front_Motor Out Out Die Ausgabemenge von FrontMotor wird somit nicht durch die Verfeinerung eingeschr nkt Wenn man diese Verfeinerung nun aus Sicht der Komponente FrontMotor 9 x steht f r in bzw out 101 betrachtet so wird beim bergang von R zu R daher nur die Eingabe menge der Kan le Battery_Front und MotorFront eingeschr nkt Wenn die Eigenschaft f r alle m glichen Eingaben korrekt ist dann trifft dies auch f r einen Teil der Eingaben zu Die G ltigkeit der obigen Eigen schaft bleibt damit im Kontext des Gesamtmodells R erhalten 102 Kapitel 9 Evaluierung 9 1 Bewertung der Werkzeuge Beim folgenden Vergleich der beiden Werkzeuge AutoFocus und ASCET sollten ein
41. Hand ist fehlertr chtig und die Absicherung des Codes gegen ber dem Modell zeitintensiv Der ICARE steht f r Computer Aided Requirements Engineering CASE steht f r Computer Aided Software Engineering 14 Einsatz von Codegeneratoren behebt diese Schw che Ein Codegenera tor erzeugt aus einem Modell den entsprechenden Code dessen Kompilat dann auf der Zielmaschine zur Ausf hrung gebracht werden soll Im Ge gensatz zur Entwicklung auf Basis einer textuellen Spezifikation entfallen damit auf Grund der automatisierten Werkzeug Unterst tzung fehler tr chtige manuelle Arbeitsschritte vgl Bild 2 2 Gmb03c Daraus ergibt sich eine erh hte Produktivit t und eine verbesserte Softwarequa lit t Funktions manuelles Codieren Software entwicklung und Respezifizieren entwicklung automatisiert Funktions Software entwicklung entwicklung Zeit Abbildung 2 2 Verteilung des Arbeitsaufwandes Voraussetzung f r ein fehlerfreies Ergebnis ist die korrekte Funktions weise des Codegenerators und Compilers Diversifizierende Testans tze siehe Kapitel 3 2 3 und die Verwendung zertifizierter Codegeneratoren k nnen hierbei die Fehlerwahrscheinlichkeit verringern Ein weiterer wichtiger Gesichtspunkt bei der Codeerzeugung im Umfeld von eingebetteten Systemen ist die Codeoptimierung Auf Grund der kanonischen Umsetzung von Modellen in Code kann auf den Zeit und Speicherverbrauch bei der automatischen Codegenerierung
42. N Signal JI Zeit SE Zeit Beispiel 7 1 6 Spontanes Versenden eines CAN Signals i ee ee ae eit Nachricht 0 Zeit Eine weitere Schnittstellenfestlegung betrifft die Abstraktion der Signale die die Gleichstrommotoren ansteuern An beide Anschl sse eines Motors hier z B f r die Verriegelung kann ber FZENTR_MOTOR1 True FZENTR_MOTOR2 False Nachricht SS n CS n CAN Signal Ma Fa eine Spannung angelegt werden Eine Negation beider Ausdr cke ver tauscht die Polung Um das Modell bersichtlicher zu halten wurden beide Signale zu einer ASCET Nachricht zusammengefasst FZENTR_MOTOR FZENTR_MOTOR_Open bzw FZENTR_MOTOR FZENTR_MOTOR Close Annahmen an die Umgebung Die Systemumgebung muss sicherstellen dass obige Schnittstellenkon ventionen eingehalten werden Dies kann softwarem ssig durch die An passung mit Hilfe von Wrapper Modulen geschehen Andernfalls basieren die Berechnungen ggf auf falschen Werten was zu nicht vorhersehbaren Folgen f hren kann z B beim Einklemmschutz Die Hardware muss daf r sorgen dass die anliegenden Sensorsignale einen definierten Zu stand einnehmen z B durch die Entprellung von Tastern Die Messung von sich kontinuierlich ndernden Werten z B Batteriespannung sollte 68 mit einer Hysterese versehen sein Ebenso ist bei Systemstart eine korrekte Vorinitialisierung der ASCET Nachrichten f r einen reibungslosen Ablauf notwendig Insbesondere m
43. Output True 62 j u 1 u Abbildung 6 9 SSD zur Demonstation der Modelchecking Anbindung 3 Input 2 Output True CG 2 Input 1 Output True gt 1 Input 0 OutputlFalse D Abbildung 6 10 STD zur Demonstration der Modelchecking Anbindung V State Initial next State Any Input 0 next Output False State bezeichnet hierbei den aktuellen Zustand next State den Nachfolgezustand Input den aktuell anliegenden Eingabewert und next Output die Ausgabe beim n chsten Systemtick Die Ber cksichtigung von Priorit ten f hrt auf folgende Formel State Initial A next State Two A Input 2 A next Output True tete ini ner ep Git E N E EEEE T E N E LEERE SEN Input 1 V Input 2 Die aus allen STDs resultierenden Formeln werden im n chsten Schritt zu einer einzigen zusammengefasst Diese repr sentiert alle m glichen parallel ausf hrbaren Berechnungsschritte des Gesamtsystems Ansch liessend wird sie so umcodiert dass benutzerdefinierte Datentypen und Funktionen eliminiert werden und letztendlich eine Boolsche Formel vor liegt Der SMV Modelchecker ist nun im Stande das Modell in Form dieses Ausdrucks einzulesen und damit die spezifizierte Figenschaft zu berpr fen Das Resultat und gegebenenfalls ein Gegenbeispiel werden wieder in das AutoFocus Framework importiert und k nnen dort in Form von EETs visualisiert werden 63 K
44. State Transition Diagram STD Jeder nicht weiter hierarchisch untergliederten Komponente in einem SSD kann ein Zustands bergangsdiagramm STD zugeordnet werden Ein STD spezifiziert das Verhalten einer solchen atomaren Komponente Es besteht aus Zust nden in Form von Ovalen Beschriftete Verbindun gen zwischen diesen stellen Transitionen dar Eine Komponente kann sich zu jedem Zeitpunkt in nur einem Zustand befinden Der bergang in einen anderen Zustand erfolgt ber eine der anliegenden Transitions verbindungen Dazu werden bei jedem Systemtick die Transitionsbe schriftungen bestehend aus Priorit t Vorbedingung Eingabe Ausgabe und internen Aktionen ausgewertet Beim Eintreffen des Systemticks werden in jeder STD Komponente fol gende Schritte durchgef hrt Die aktuell anliegenden Werte an den Nach richteneing ngen werden zun chst ausgelesen und an Variablen gebun den Damit werden dann die pr dikatenlogischen Vorbedingungen ausge wertet Eine Transition kann nur dann schalten falls ihre Vorbedingung 59 erf llt ist Von diesen aktiven Transitionen werden nur diejenigen mit der h chsten Priorit t betrachtet Falls mehrere Transitionen gleichzei tig schalten k nnen wird von diesen nichtdeterministisch eine Transition ausgew hlt Das Schalten dieser Transition geschieht mit der Aktuali sierung von lokalen Variablen und der Ausgabe von Nachrichten Diese Nachrichten stehen dann f r andere Komponenten beim n chsten Sy
45. TL Formeln keine Pfadquantoren wie bei CTL verwenden darf lassen sich LTL Formeln einfacher formulieren Man muss nicht 42 immer die Auswirkung auf den gesamten Abwicklungsbaum wie bei CTL im Hinterkopf behalten sondern betrachtet nur einen Pfad Weiterf hrende Informationen k nnen CGA00 entnommen werden 4 2 3 Verifikationsalgorithmus Mit den bisher besprochenen Mitteln ist es nun m glich ein System in Form einer Kripke Struktur zu modellieren Zudem kann daf r mittels einer Spezifikationssprache eine Eigenschaft formuliert werden Die Ei genschaft liegt somit als CTL oder LTL Formel vor deren Aussagenva riablen den Labeln der Zust nde der Kripke Struktur entsprechen Das Ziel des Modelcheckings ist der Beweis der G ltigkeit dieser Eigen schaft f r das modellierte System F r diesen Verifikationsvorgang wird ein algorithmisches Verfahren ben tigt Dieses exploriert die erreichba ren Zust nde des Systems und berpr ft in jedem Zustand ob die spe zifizierte Eigenschaft erf llt ist Dabei wird der Abwicklungsbaum der betrachteten Kripke Struktur abgegangen Im Falle der Nichterf llung ist es m glich ein Gegenbeispiel in Form eines Pfades durch den Abwick lungsbaum zu generieren Damit k nnen Fehlerstellen im modellierten System ausgemacht werden Nicht immer kann f r eine Eigenschaft ein eindeutiges aussagekr ftiges Gegenbeispiel geliefert werden Ein Beispiel daf r ist die CTL Formel EF pl A p2 f
46. Technische Universit t M nchen Fakult t f r Informatik Diplomarbeit in Informatik Vergleich zwischen konventionellen und formalen Methoden zur Software Qualit tssicherung an einem Beispiel aus dem Bereich Automotive Daniel Rei Technische Universit t M nchen Fakult t f r Informatik Diplomarbeit in Informatik Vergleich zwischen konventionellen und formalen Methoden zur Software Qualit tssicherung an einem Beispiel aus dem Bereich Automotive Diplomand Aufgabensteller Betreuer Abgabe Daniel Rei Prof Dr Manfred Broy Dr Jan J rjens David Trachtenherz 15 Mai 2006 Ich versichere dass ich diese Diplomarbeit selbstst ndig verfasst und nur die angegebenen Quellen und Hilfsmittel verwendet habe Ort Datum Unterschrift Zusammenfassung Der wachsende Anteil von Software in eingebetteten Systemen pr gt die heutige Automobilindustrie Dort erfordern sicherheitskritische Software Anwendungen ein hohes Mass an Zuverl ssigkeit Um dieses Ziel zu erreichen erfolgt ein intensiver Einsatz von Testverfahren Im Rahmen dieser Arbeit werden Software Qualit tssicherungsmethoden bewertet Als Fallstudie dient die Softwarekomponente eines T rsteuerger tes auf die verschiedene Verfahren angewandt werden Inbesondere erfolgt die Evaluierung von Modelchecking als Verifikati onsverfahren akademischen Ursprungs im Vergleich zu konventionellen Qualit tssicherungsmethoden wie Simulation und Whitebo
47. Vorgehensweise und Restriktionen bei der Modellierung w rde seine Freiheitsgrade und somit seine Effizienz einschr nken Daher sollten entsprechend der Forderung nach einer se paraten Testgruppe Verifikationsspezialisten eingesetzt werden die den Testprozess begleiten 116 Kapitel 10 Fazit und Ausblick Ein entscheidendes Defizit der Modelchecking Methode ist das Problem der Zustandsraumexplosion Befindet sich die Entwicklung jedoch noch in einem fr hen Stadium bzw liegt ein event gesteuertes System auf einer h heren Abstraktionsebene vor so sind die Bedingungen f r das Model checking gegeben Damit kann mit Hilfe von Verifikationstechniken die Grundlage f r die folgenden Entwicklungsschritte und Testverfahren ge schaffen werden Beispielsweise k nnen dann basierend auf verifizierten Modellen Testf lle f r Back to Back Tests erstellt werden Folgende Tabelle stellt allgemeine Gesichtspunkte der beiden Qua lit tssicherungsmethoden nochmals gegen ber Testen Modelchecking untersucht ein physikalisches bzw konkretes untersucht ein abstraktes Modell System In The Loop Tests erfolgen in einer Umge bung die dem realen Umfeld nahe kommt billige und fr hzeitige Verifikation ohne kom plexe In The Loop Testumgebung kein Nachweis der Korrektheit von Eigenschaf ten m glich Nachweis der Korrektheit von gefragten Eigen schaften m glich verwendet oft viele oberfl chliche Testdaten z B
48. apitel 7 Modellierung in ASCET Dieses Kapitel besteht aus zwei wesentlichen Teilen Der erste Teil befasst sich mit der Modellierung der T rsteuerger te Software sie he Kapitel 5 in ASCET siehe Abschnitt 6 1 Die nachfolgen den Abschnitte beschreiben die Anwendung von konventionellen Qua lit tssicherungsmassnahmen auf das Resultat vgl Kapitel 3 7 1 Modell des T rsteuerger tes 7 1 1 Rahmenbedingungen Ein Modell stellt im Allgemeinen die Abstraktion eines realen Zusammen hangs dar Ein Grund daf r ist die Konzentration auf das Wesentliche Technische Details sollen damit den Entwicklungsprozess nicht vernebeln F r die technische Realisierung eines solchen Modells sind letztenendes konkretisierende Massnahmen erforderlich Im vorliegenden Fall ist dies zum Beispiel die automatische Codegenerierung Voraussetzung f r einen reibungslosen bergang vom Modell zur Rea lisierung sind definierte Schnittstellen und Rahmenbedingungen die an die Umgebung des Steuerger ts gestellt werden 64 Schnittstellenkonvention Die Stecker S1 S2 und S3 stellen die Schnittstelle des Steuerger tes zur Umgebung dar siehe Anhang B Es werden Signale ber Steckerpins S1 S2 und den CAN Bus S3 bertragen Die Modellierung dieser externen Schnittstellen in ASCET ist in dieser Diplomarbeit durch fol gendes Schema festgelegt worden Externe Signale werden mit Hilfe von ASCET Nachrichten modelliert Abh ngig von der Art des S
49. ation bzw fehlerhafte Interpretation einer tex tuellen Spezifikation e Inkorrektes Beweissystem z B auf Grund von Programmierfeh lern Einsatz von Modelchecking Entgegen der in Abschnitt 3 2 gestellten Forderung nach einer un abh ngigen Testgruppe wurde bei der Durchf hrung der Diplomar beit aus pragmatischen Gr nden darauf verzichtet D h Entwicklung und Tests wurden hier von derselben Person erbracht Dadurch ergab sich als zus tzlicher Gesichtspunkt die Anwendung von Modelchecking w hrend des Entwicklungsprozesses aus der Entwicklersicht statt als unabh ngiger Verifikationsprozess aus Testersicht Als hilfreiches Fea ture von AutoFocus konnten dabei Gegenbeispiele in Form von EETs ber das TDF Zwischenformat in den Simulator geladen und ausgef hrt werden Gefragte Eigenschaften betrafen vor allem die Erreichbarkeit bzw den Ausschluss von Systemzust nden Grosse Komponenten konnten in AutoFocus nicht per Modelchecking berpr ft werden vgl Abschnitt 8 3 1 Man k nnte hier komposi tionelles Modelchecking anwenden was jedoch tiefgreifende Kenntnisse aus der Theorie voraussetzt und somit nicht mehr eine Push Button 115 Verifikationsmethode darstellt In der Praxis ist die Anwendung von Modelchecking durch den Entwickler nicht f r komplexe Projekte geeignet da dieser selbst mit vielen anderen Problemen aus der Anwendungsdom ne z B Regelkreisstabilit t etc konfrontiert ist Eine aufgezwungene
50. ation der TSG Spezifikation schon blossgestellt waren fiel die Umsetzung in ASCET leichter Auch die liberaleren Beschrei bungsmittel trugen dazu bei Somit konnten DoorState Windows und die Beleuchtung DoorLight bzw InteriorLight in der halben Zeit wie bei AutoFocus fertiggestellt werden Die prinzipielle Struktur wurde gr sstenteils bernommen und in eine kompaktere Form gebracht Die Anwendung der Testverfahren f hrte nur zu kleineren nderungen Fairerweise muss erw hnt werden dass die Umsetzung und Interpreta tion der Spezifikation fast die H lfte der Zeit f r die Bearbeitung in AutoFocus ausgemacht hat Bei der Modellierung in ASCET fiel diese Zeit zum Grossteil nicht mehr an da auf die vorher in AutoFOCUS ge sammelte Erfahrung zur ckgegriffen werden konnte Das grundlegende L sungskonzept wurde schon in AutoFocus erarbeitet Somit kann bei beiden Tools von einem quivalenten Zeitaufwand f r die Modellierung ausgegangen werden wenn man von den nachtr glichen Umstrukturie rungen in AutoFocus im Rahmen des Modelcheckings absieht Tabelle 9 1 stellt den zeitlichen Aufwand f r die Modellierung in beiden Tools nochmals gegen ber ASCET AutoFocus und Spezifikation Einarbeitung 1 bis 2 Wochen 1 Tag Modellierung 1 5 Wochen 3 Wochen DoorLock Modellierung 1 5 Wochen 3 Wochen Windows Modellierung 0 5 Wochen 1 Woche Light Tabelle 9 1 Zeitlicher Modellierungsaufwand In AutoFocus wu
51. bis 35 Zeilen 3 bis 8 Das Ansteuern der Motoren erfolgt mindestens f r 6 Systemticks Abstraktion der Startup Zeit Zeile 9 und 10 Das Fenster ist nach der Startup Zeit noch nicht am oberen Anschlag und bewegt sich nicht Zeile 11 Wenn ein Einklemmen erkannt worden ist Zeilen 3 bis 10 dann reagiere darauf Zeilen 12 bis 24 Zeile 12 Die Reaktion erfolgt zeitlich nach dem Einklemmen Zeilen 13 bis 19 Fahre die Schreibe runter Zeile 14 bis Zeile 15 die Scheibe blockiert Zeile 16 oder schon am unteren Anschlag angelangt ist Zeile 18 Zeilen 22 bis 31 oder 10 Systemticks vergangen sind Abstraktion des 3 Sekunden Timeouts Die LTL Formel greift dabei nicht auf Unterkomponenten und interne Kan le von FrontMotor zur ck sondern nur auf die Kan le der Schnitt stelle nach aussen Somit beschreibt die formulierte Eigenschaft das Verhalten von FrontMotor in Form einer Black Box Die Eingabe ei ner Nachricht in die Black Box Komponente hier FrontMotor kann zu internen Berechnungsschritten f hren Dabei k nnen Nachrichten intern eine Pipeline von Unterkomponenten durchlaufen Es werden somit erst einige Systemticks ben tigt bis das Ergebnis am Ausgang vorliegt Beim Aufstellen von Formeln in AutoFocus kommt dieser Pipelining Effekt zum Vorschein Soll eine gew nschte Eigenschaft gezeigt werden z B wenn X gilt dann ergibt sich Y dann ist diese zeitliche Verz gerung zu ber cksichtigen Dieses zeitliche V
52. bwohl der Anschlag am Fensterrand noch nicht erreicht worden ist Der letzte Fall f hrt beim Fensterschliessen zur Aktivierung des Ein klemmschutzes Dabei wird das Fenster ge ffnet ohne auf weitere Auf forderungen des Benutzers zu reagieren 5 4 Beleuchtung Innenraumbeleuchtung Grunds tzlich erlischt die Innenraumbeleuchtung sobald die Mo torz ndung aktiviert wird Ansonsten wird das Licht f r 10 Minuten eingeschaltet wenn eine T r ge ffnet wurde Wurden alle T ren ge schlossen so leuchtet das Licht noch f r 30 Sekunden Die Ansteuerung Das berdr cken der Fensterhebertaste erm glicht automatisches ffnen bzw Schliessen des Fensters bis zum Anschlag Die Taste muss dann nicht weiter gedr ckt gehalten werden wie beim manuellen ffnen bzw Schliessen Auf Grund von techni schen Einschr nkungen kann die Taste vom automatischen in den neutralen Zustand nur ber das Passieren des manuellen Zustands wechseln Damit der automatische Fensterlauf dabei nicht abgebrochen wird soll ein direkter Wechsel vom automati schen in den manuellen Tastenzustand erst nach einer Verz gerung von 0 5 Sekunden erkannt werden 50 per Hand und die berwachung der Batteriespannung wird vom Decken steuerger t bernommen Ausstiegsleuchten Die Ausstiegsleuchte einer ge ffneten T r wird bei entsprechender Bat teriespannung eingeschaltet ol Kapitel 6 Eingesetzte Werkzeuge Wie in Abschnitt 2 2 anged
53. chleuni gen Neben der Ausf hrungszeit des Modelcheckers reduziert sich da durch auch die L nge der Gegenbeispiele 113 In Tabelle 9 3 wird die aufgebrachte Zeit mit der dabei erreichten Feh leranzahl in Beziehung gesetzt Zu beachten ist hierbei dass jeweils in AutoFocus und ASCET der berdeckungsgradanalyse bzw dem Mo delchecking die Simulation vorausging Verfahren Zeitaufwand Fehleranzahl Stunden Experiment ASCET 24 10 Simulation AutoFocus 24 5 Modelchecking 80 5 White Box Testen 56 5 Tabelle 9 3 Gefundene Fehler je Zeitaufwand Die Interpretation der Zahlen besagt dass im Rahmen dieser Fallstu die beim Modelchecking in derselben Zeit wie beim Coverage Testen we niger Fehler gefunden wurden Allerdings muss hinzugef gt werden dass die dabei gefundenen Fehler beim Modelchecking schwerwiegen dere Logik und Synchronisationsfehler waren siehe obiger Abschnitt Fehlerfindung Weiterhin l sst sich der Unterschied durch die Natur des Modelcheckings begr nden Beim Modelchecking erfolgt normalerweise der konstruktive Nachweis von Eigenschaften Das Aufdecken von Fehlern ergibt sich als Nebenprodukt in Form eines Gegenbeispiels Im Gegensatz dazu ist Testen auf das Finden von Fehlern ausgerichtet Effizienz Beim Testen gilt die Devise Je mehr Fehler gefunden wurden desto erfolgreicher waren die Tests Die Wahrscheinlichkeit Fehler zu finden erh ht sich mit der Anzahl
54. d 8 5 angesteuert Nach dem Einschalten des Motors ben tigt das Fenster auf Grund dessen Tr gheit ein wenig Zeit bis es in Bewegung gesetzt wird W hrend dieser Zeit soll das Stehenbleiben der Scheibe jedoch nicht als Einklemmen bzw Blockieren interpretiert werden Dazu wird das Flag StartupMode abgefragt Zu Beginn einer Scheibenbewegung wird das Flag gesetzt Nach Ablauf der Zeitspanne f r das Anlaufen wird StartupMode wieder zur ckgesetzt Die Unterkomponente Timer f hrt zum Abbruch der Scheibenbewegung bei einem Timeout Auf Grund der Semantik von AutoFocus weist die Ubermittlung von Nachrichten ber Kan le einen Pipeline Effekt auf 91 Abbildung 8 5 DispatchCommand in AutoFocus Ein Signalfluss durch mehrere Komponenten steht erst um mehrere Sy stemticks verz gert am Ende an Verzweigt sich der Signalfluss um nach einer parallelen Bearbeitung am Ende wieder zusammengef hrt zu wer den so liegen beide Resultate unter Umst nden nicht mehr zum gleichen Zeitpunkt bei der Zusammenf hrung an Somit kann z B der Fall eintreten dass das bisherige ffnen des Fen sters zu einem Timeout f hrt und gleichzeitig ein neuer Befehl zum Schliessen des Fensters in DispatchCommand eintrifft Der neu begon nene Schliessvorgang wird dann f lschlicherweise durch den verz gerten Timeout Alarm abgebrochen Mit Hilfe des Flags IgnoreTimeout in DispatchCommand wird dies unterbunden W hrend des Zeitintervals
55. de instru mentieren siehe Abschnitt 3 2 3 um berdeckungsanalysen wie die Co oder MC DC berdeckung durchzuf hren Das Resultat eines Testlaufs l sst sich r ckwirkend farbig im Quelltext darstellen Gr n eingef rbte Zeilen haben die Anforderung des ausgew hlten berdeckungskriteriums w hrend des Tests erf llt rote hingegen nicht 6 2 2 CTE XL Ein weiteres Werkzeug das im Zusammenhang mit konventionellen Test verfahren eingesetzt wird ist CTE XL Damit lassen sich Testf lle gra fisch erstellen und festhalten In Form einer Matrix k nnen abh ngig vom Zeitpunkt Werte f r jeden Eingabeparameter des Testobjekts an gegeben werden Diese Testf lle lassen sich dann exportieren und in ein entsprechendes Format f r die Eingabe in das Testobjekt wandeln 97 2 2 2 2 22 2 2 2223 GEEEEEEEEEE Abbildung 6 5 CTE XL Screenshot 6 3 AutoFocus AutoFocus ist ein frei erh ltliches Systementwicklungswerkzeug das an der Technischen Universit t M nchen entwickelt wurde Es basiert auf Konzepten der formalen Beschreibungsmethodik FOCUS B501 FOCUS dient zur formalen Spezifikation und Entwicklung verteilter re aktiver Systeme mit Hilfe von pr zise definierten formalen Darstellungs mitteln Zum Einsatz kommen dabei intuitive entwicklungsorientierte Beschreibungstechniken Ein verteiltes System wird dabei als Verbund
56. den CAN Bus weiter Sie unterscheiden sich dahingehend dass CAN_Front CAN Nachrichten f r das gegen berliegende vordere Fenster generiert w hrend CAN_Back CAN Nachrichten f r das hintere Fenster auf der anderen Seite erzeugt Damit einher geht auch eine unterschiedli che Interpretation der Eingangssignale abh ngig von der Konfiguration der Fahrer und Fahrzeugseite In CAN_Front bzw CAN_Back folgt auf das Einlesen der Eingangssigna le ggf eine Verz gerung um 0 5 Sekunden vgl Fussnote 2 auf Seite 50 Hinzu kommt die Auswertung des Signals von Doorlock_Module dass beim Verriegeln der T ren an Windows_Module bermittelt wird Ei ne entprechende TSG Konfiguration f hrt damit zur Generierung eines Schliessbefehls Am Ende der Signalbearbeitung werden die resultieren den Befehle f r den CAN Treiber aufbereitet Request_Front bzw Request_Back Die Komponenten Request_Front und Request_Back verarbeiten Anwei sungen zur Bewegung der Fensterscheiben auf derselben Fahrzeugseite wie das TSG Request_Front ist f r das vordere Fenster und Request_Back f r das Hintere zust ndig Beide Komponenten arbeiten prinzipiell nach derselben Weise und unterscheiden sich haupts chlich in der Art und Anzahl der Eing nge Request_Front erh lt die Anweisungen vom CAN Bus der vorderen Fensterhebertaste und von der Zentralverriegelungs komponente Doorlock_Module Request_Back hingegen reagiert auf An weisungen vom CAN Bus der hinteren Fenst
57. der Korrekturstelle nochmals durchlaufen Es ergibt sich somit ein Zyklus dessen L nge von der Fehlerstelle abh ngt 12 Je sp ter d h je weiter oben im rechten Ast der Fehler gefunden wurde desto aufwendiger wird dessen Korrektur Oftmals findet die Implemen tierung eines Produkts zudem bei einem Zulieferer statt so dass komple xe Zuliefererstrukturen die Fehlerbehebung zeitlich in die L nge ziehen k nnen Dies wirkt sich negativ auf die Fehlerbehebungskosten aus Gr nde f r Fehler kann man klassifizieren Es ergeben sich unter anderem folgende Fehlerklassen 1 Das Verhalten des Produktes wurde in der Spezifikation nicht ein deutig formuliert Der Interpretationsspielraum hat zur falschen Umsetzung gef hrt 2 Das Verhalten des Produktes wurde in der Spezifikation nicht vollst ndig beschrieben Die Erg nzung des Verhaltens nach ei genen Vorstellungen war fehlerhaft 3 Der Grund f r den Fehler war programmiertechnischer Natur In diesem Zusammenhang soll der Unterschied zwischen den beiden Be griffen Verifikation und Validierung erl utert werden Unter Verifi kation versteht man die berpr fung ob die vorgegebene technische Spezifikation korrekt in das Produkt umgesetzt worden ist Validierung hingegen bezeichnet die berpr fung ob das Produkt die gestellten An forderungen berhaupt erf llt bzw ob es sich f r seinen vorgesehenen Einsatzzweck eignet Man kann dabei funktionale An
58. der Qualit tssicherung vor beugende Massnahmen dar die die Fehlerwahrscheinlichkeit im voraus verringern sollen Unternehmensspezifische Richtlinien existieren unter anderem f r die Entwicklung auf Modellebene mit Hilfe von industri ell eingesetzten Modellierungswerkzeugen Hua04 Mei05 Sie definie ren die Struktur eines Modells um die Qualit t der Modelle und der zu entwickelnden Software hinsichtlich Funktionalit t Zuverl ssigkeit Benutzbarkeit nderbarkeit und Wiederverwendbarkeit sicherzustellen Damit sollen Fl chtigkeitsfehler und typische Fehler verhindert werden Beispiele f r Vorgaben sind e bersichtliche Modellierung durch Einhalten von Grenzen und Abst nden e Verwenden von Namenskonventionen indem aussagekr ftige Be zeichner f r Komponenten gew hlt werden e Initialisierungspflicht f r Variablen Desweiteren gibt es Codierungsrichtlinien zum Verhindern von Fehlern auf Sourcecodeebene Die MISRA C Richtlinie MIS98 ist ein Beispiel daf r Beispielregeln dienen zur Vermeidung von goto Anweisungen oder von Zeigerarithmetik im C Code Auch manche Codegeneratoren vgl 23 Abschnitt 2 2 erzeugen MISRA C konformen Code Est 3 2 Industriell eingesetzte Software Testverfahren 3 2 1 Allgemeine Aspekte des Software Testens Gem ss Mye01 verfolgt man beim Testen folgendes Ziel Testen ist der Prozess ein Testobjekt mit der Absicht zu berpr fen Fehler zu finden Testen stellt somit
59. die Synchronisation und Randbedingungen betrafen wurden mit dem Modelchecker gefunden Beispielsweise wurde so der verz gerte Timeout Alarm in Abschnitt 8 1 2 ausgemacht Ohne den Einsatz des Modelcheckers w ren wesentlich mehr Testl ufe notwendig gewesen um Fehler dieser Art ausfindig zu machen Tabelle 9 2 stellt die Anzahl der gefundenen Fehler in beiden Tools ge gen ber Es werden hier nur Fehler betrachtet die erst nach der Fer tigstellung der Komponenten aufgedeckt worden sind und nicht schon w hrend des schrittweisen Aufbaus der Komponenten Bei den Anga ben muss beachtet werden dass dem Modelchecking und White Box Testen jeweils die Simulation bzw das Experiment vorausging Der Grossteil der Fehler wurde somit schon vor Beginn des Modelcheckings bzw White Box Testens abgefangen ASCET AutoFocus Experiment Simulation 10 5 Modelchecking 5 White Box Testen 5 Tabelle 9 2 Anzahl gefundener Fehler Intellektueller Aufwand Der Hauptaufwand beim Testen in ASCET bestand vor allem in der 111 Interpretation der Testausgaben und dem Abgleich mit den Anforderun gen der Spezifikation Im Allgemeinen l sst sich der Testaufwand mit wachsendem Automatisierungsgrad der Tests reduzieren So existieren auch Ans tze die Anforderungen mit der Testausf hrung zu koppeln Tools wie DOORS von Telelogic stehen daf r zur Verf gung Tell Die Schwierigkeit besteht dabei in der Erfassung von komp
60. e Zustandsraumexplosion Einschr nkungen Eine Begrenzung der Schritte bzw Integerwerte ist notwendig Benutzerdefinierten Datentypen d rfen nicht rekursiv definiert werden ASCET unterst tzt keine rekursiv definierten Datentypen auf der Mo dellebene AutoFocus ist in Kombination mit Modelchecking f r ereignisgesteuerte Systeme ohne zeitliche Bedingungen pr destiniert 9 1 2 Zeitlicher Aufwand bei der Modellierung Einarbeitung Die im Vergleich zu ASCET eingeschr nkte Notation von AutoFoOcus kann innerhalb eines Tages erlernt werden ASCET hingegen bedurfte einer ungleich l ngeren Einarbeitungsphase von ber einer Woche Grund ist die Vielfalt von Ausdrucksm glichkeiten 105 und die Frarbeitung der im Bereich Automotive g ngigen Konzepte In beiden F llen mangelte es nicht an Dokumentation und Ansprechpart nern Modellierung in AutoFocus Die Modellierung der Komponenten DoorLock und Windows erfolgte in jeweils drei Wochen Light wurde in einer Woche erstellt Die Schwie rigkeit lag in der korrekten Interpretation und Umsetzung der textuellen Spezifikation Weiterhin hatten nachtr gliche Korrekturen von logischen Fehlern und das Beheben von Synchronisationsproblemen aufwendige Umstrukturierungen zur Folge Beispiel 9 1 1 Das gleichzeitige manuelle ffnen des Beifahrerfensters durch die Fahrerfensterhebertaste und die Beifahrerfensterhebertaste dau ert solange an bis beide Tasten losgelassen wurden falls
61. e Encoding Die Fraunhofer TSG Spezifikation von Kapitel 5 konnte nicht als Grund lage dienen da die dort gestellten Hardwareanforderungen hier nicht erf llt wurden Beispielsweise basiert der Einklemmschutz in der Fraun hofer Spezifikation auf Sensoren f r den Anschlag der Fensterscheibe am Fensterrand Hier hingegen sind solche Sensoren nicht vorhanden Die Positionsbestimmung musste ber den eben beschriebenen Z hler rea lisiert werden Das hier implementierte Modell h lt sich daher an die vorgegebene Hardware und erf llt dessen Grundfunktionalit ten e Vertikales und horizontales Verstellen der Aussenspiegel mit Ti meout e Verriegeln und Entriegeln des T rschlosses e manuelles bzw automatisches Fensterhoch und Fensterrunterfah ren mit Einklemmschutz Im Vergleich zur Entwicklung von Prototypen auf Basis der Zielplattform kann die Validierung beim Rapid Prototyping ohne R cksichtnahme auf Ressourcen Beschr nkungen erfolgen Auch der Eingriff in das System durch Messungen ist m glich insofern Echtzeiteigenschaften nicht davon betroffen sind In ASCET RP k nnen beim Rapid Prototyping in einem Online Experiment Zustands nderungen des Systems r ckwirkend im Modell auf der Entwicklungsplattform dargestellt werden 83 Kapitel 8 Modellierung in AutoFocUs Dieses Kapitel beschreibt zun chst die Umsetzung der Fraunhofer Spezi fikation des T rsteuerger tes in AutoFocus Im Anschluss daran wird die Verifikatio
62. e Modul definiert ein Integrier Glied mit zwei Prozessen init und calc Die im Block diagramm den Prozessenamen vorangestellten Ziffern legen den Berech nungsablauf je Prozess fest calc f hrt zwei Schritte hintereinander aus Bei jedem Aufruf von calc durch den Scheduler wird die seit dem letzten Aufruf vergangene Zeit AT mit dem Eingangssignal u und einem Parameter K multipliziert und zum bisherigen Wert von y hinzuaddiert Der zweite Schritt besteht in der Ausgabe des aktuell integrierten Wertes Der Prozess init besteht nur aus einem Initialisie rungsschritt Bild 6 4 zeigt die Zuweisung der Prozesse zu den OSEK Tasks Oft wiederverwendete und hierarchisch untergliederte Komponenten in Modulen k nnen mit Hilfe von Klassen deklariert und strukturiert wer den Klassen k nnen mit den selben Beschreibungselementen der Module erstellt werden Allerdings werden Berechnungsabl ufe in Klassen nicht in Prozessen sondern in Methoden mit Ein und Ausgabeparametern zusammengefasst Die Definition von Methoden erfolgt analog zum Vor 54 D self Modul FD val cont Fr K cont BO dT dT d D5 u mesglcor Abbildung 6 3 Definition von Prozessen ZO Graphics Bi 08 amp Formulas amp Impl Type comm IRI Binding Fies KO self Project DES Preemp Levels GE Coop Levels Ia zl Enable Monitoring Application Modes Tasks 3
63. einen destruktiven Prozess dar der psychologisch nicht im Einklang mit der T tigkeit eines Entwicklers steht Denn aus der Sicht eines Testers war der Test erfolgreich falls ein Fehler aufgetre ten ist Einen Entwickler demotiviert diese Einstellungsweise Aus seiner Sicht w rde er damit beabsichtigt seine Arbeit degradieren Damit die Effizienz des Testprozesses davon nicht beeinflusst wird sollte die Auf gabe des Testens nicht von dergleichen Entwicklergruppe sondern einer separaten Testergruppe durchgef hrt werden 3 2 2 Testverfahren in der Softwareentwicklung Traditionelle Software Tests basieren auf statischen und dynamischen Verfahren siehe Bild 3 1 Statische Verfahren berpr fen ein Testobjekt an sich ohne dessen Ausf hrung Darunter fallen unter anderem formale vgl Kapitel 4 und informelle Verfahren die auf den zur Verf gung gestellten Dokumenten z B C Code oder Modell basieren Bei letz teren Verfahren wird der Code in einer Diskussionsrunde besprochen um Fehler aufzudecken was sich nur f r berschaubare Systeme bzw Teile davon eignet Die dynamischen Testverfahren bilden eine weitere Testgruppe Hierbei wird das Testobjekt zur Ausf hrung gebracht Das Testobjekt stellt im vorliegenden Fall eine Funktion oder ein System dar Beim Testen werden Testf lle auf das Testobjekt angewandt und jeweils berpr ft ob bei der Ausf hrung ein Fehler aufgetreten ist Die Testf lle werden von der Spezifikation des Testob
64. eit von Software kann im Allgemeinen jedoch nicht mit traditionellen Testverfahren gezeigt werden Dazu m sste die Korrektheit der Ausgaben zu allen m glichen Eingaben gezeigt werden Praktisch ist dies nicht ohne erheblichen Aufwand durchf hrbar da die 100 ige Pfad berdeckung des Testobjekts durch Testf lle vgl Ab schnitt 3 2 2 oft nicht m glich ist Dieses Defizit kann durch Verfahren akademischen Ursprungs behoben werden 4 1 Verifikationsmethoden Die aus dem akademischen Bereich herr hrenden Verfahren basieren auf der Anwendung formaler Methoden Formale Methoden umfassen Vor gehensweisen zur Beschreibung und Analyse von Systemen die auf ma thematisch logischen Darstellungsmitteln und Verfahren beruhen Bei spielsweise l sst sich der Syntax von Beschreibungsnotationen eine wi derspruchsfreie Semantik zuweisen Die auf dieser Grundlage erstellten formalen Spezifikationen sind somit pr zise definiert und haben eine mathematisch festgelegte Bedeutung Damit k nnen dann bestimmte Eigenschaften mathematisch gezeigt oder widerlegt werden Ein Beispiel f r eine formale Spezifikationstechnik ist FOCUS siehe Abschnitt 6 3 38 Die Verifikation im Sinne der Informatik ist der Nachweis dass ein Sy stem der vorgegebenen Spezifikation entspricht Wird diese berpr fung mit Hilfe eines mathematischen Beweises unter Hinzunahme von formalen Methoden durchgef hrt so spricht man von einer formalen Verifikati on V
65. eiterer sich daraus ergebender Vorteil ist die Allgemeinheit der Me thodik Einsatzgebiete von AutoFOCUS beschr nken sich damit nicht auf eingebettete Systeme in der Automobilindustrie Beispielsweise k nnen ebenso Geldtransfersysteme zur Untersuchung von Sicherheitsl cken mo delliert werden JWO1 Allerdings erschwert dieser allgemeine Ansatz im Gegenzug dazu eine tief gehende Integration in bestehende Konzepte in der Automobilindustrie Die in spezialisierten Werkzeugen wie ASCET integrierten Konzepte sind beispielsweise e Scheduling in OSEK mittels Tasks und Prozesse e Abbildung der Datentypen auf die von der Hardware unterst tzten Datentypen e Unterscheidung von Programm und Datenstand AutoFocus eignet sich somit vor allem f r die Beschreibung der ab strakten Logik einer Funktion Die Einbettung in den darunterliegen Hardware Kontext und die Nachbildung der obigen Konzepte sollte je doch nicht mehr im Rahmen der Modellierung in AutoFocus erfolgen Technische Details einer Verfeinerung des Modells w rden die Gr sse und Komplexit t des Modells auch im Hinblick auf die Zustandsraumexplo sion stark anwachsen lassen Problematisch dabei ist der Pipeline Effekt vgl Abschnitt 8 1 2 und damit verbundene Synchronisationsprobleme bedingt durch die parallele Berechnung des Komponentennetzwerkes In ASCET spielt die Synchronisation der einzelnen Komponenten eben falls eine Rolle Allerdings ist hier eine sequentielle Abarb
66. eitung durch den Prozessablauf und das Task Scheduling vorgegeben vgl Abschnitt 6 1 1 Dies ist ein bedeutender Unterschied zum AutoFOCUS Konzept mit parallel arbeitenden Komponenten deren Berechnungen bei jedem 104 Systemtick synchron voranschreiten Auf der Ebene der Verhaltensbeschreibung von Komponenten setzt sich die Differenzierung fort Die Auswahl von STD Transitionen in Au toFocus erfolgt bei gleicher Priorit t und erf llten Vorbedingungen indeterministisch Der Benutzer von AutoFOCUS muss darauf achten dass die Auswahl der Transitionen durch entsprechende Vorbedingungen und Priorit tenvergabe deterministisch bleibt Ein deterministischer Ab lauf muss somit explizit erzwungen werden In ASCET sind die Berech nungen in Zustandsautomaten hingegen deterministisch unterschiedliche Transitions Priorit ten sind obligatorisch Die Modellierung von zeitgesteuertem Verhalten in AutoFoCus erfordert auf Grund des globalen Systemticks die Diskretisierung der Zeit Timer Komponenten k nnen in AutoFocus mit Hilfe von Integer Variablen rea lisiert werden Die Aufl sung eines Timeout Intervalls wird dann durch eine Anzahl von Ticks bestimmt In ASCET Modellen werden Zeitangaben direkt ohne Diskretisierung im Modell angegeben Die Codegenerierung in ASCET SE befasst sich dann mit der Abbildung auf entsprechende Hardware Timer und deren korrekte Initialisierung Durch das Modelchecking ergeben sich in AutoFocus bedingt durch di
67. em XMotor_In_Command cale CheckBattery retum XMotor_Out_B_LOW_WIN trigger In_Battery In_Command DI ce In_Battery Out Comman lee Command trigger A XMotor_In_Battery cale Chekbatery p ispatchCommand CheckBattery a KE XMotor_In_K_UNTEN cale e trigger DispatchCommand In X Border EE In_Down rrer Besser EE 1 y Border YOO Out xEror Ech Ak H in_DownError In_X_BEWEG H 1 XMotor_Out_ERROR_WIN er D e Out_ERROR_WIN Esseg E mm we BE J In_X_BEwEG In_XErrorstart Out_DownErrorStart in Kaes retumn xMotor_ut_ERROR_WIN DownEror D DownError 1 XMotor_Out_X_MOTOR Out X Motor EG E return XMotor_Out_X_MOTOR ee XMotor_In_XLOBEN cal In_X_Border MT ot M rn Jk 4 In _UpError In_X_BEWEG In_XErrorStart UpError Out UpErrorstart Dpatchcommand Abbildung 7 3 FrontMotor in ASCET Die Motoransteuerungen FrontMotor siehe Bild 7 3 und BackMotor sind identisch implementiert FrontMotor erh lt die Anforderung von Request_Front und steuert den vorderen Fensterscheibenmotor an Bei BackMotor und Request_Back gilt Analoges f r die hintere Fensterschei be Bei ausreichender Batteriespannung wird die Motorbewegung durch das Anlegen der entsprechenden Spannung an die TSG Ausg nge ange stossen Die Scheibenbewegung wird erst wieder gestoppt bzw umge kehrt wenn e eine andere Anforderung von Request_Front bzw Request_Back an liegt e die Scheibe den Anschlag erreicht hat e der 3 Sekunden Timer abgelaufe
68. em eine Be rechung nur in Folge des Eintreffens eines usseren Ereignisses stattfin det existieren im TSG Modell auch zeitliche Abh ngigkeiten Beispiele sind die zahlreichen Timeouts und Countdown Timer Da AutoFocus einen diskreten Systemtick zu Grunde legt k nnen keine kontinuierlichen Zeitwerte betrachtet werden Mittels Integervariablen werden Count downz hler modelliert Die Genauigkeit der Zeitaufl sung wird durch die Anzahl der Z hlschritte bestimmt Zum Beispiel k nnte 1 Sekun de durch 10 Systemticks dargestellt werden Es muss ein Kompromiss zwischen der Genauigkeit der Aufl sung und dem Zeitaufwand f r das Modelchecking getroffen werden 8 3 1 Verifikation des Einklemmschutzes Ein durchg ngiges Beispiel f r den Einsatz von Modelchecking ist der Nachweis der Korrektheit des Einklemmschutzes Wie schon oben erw hnt konnte der Modelchecker das Gesamtmodell nicht auf einmal verarbeiten Daher wurde ein modularer Ansatz gew hlt um die Kor rektheit des Einklemmschutzes f r das Gesamtsystem zu zeigen Die f r den Einklemmschutz bedeutsame Komponente FrontMotor befindet sich innerhalb der Windows Komponente Hier wird die Eigenschaft exem plarisch f r das Vorderfenster gezeigt Ein analoges Vorgehen ergibt sich f r das Hinterfenster Die Schnittstelle dieser Komponente besteht aus den Eing ngen e Bottom_Front registriert ob sich die Fensterscheibe am unteren Anschlag befindet e MovingSensor_Front registrier
69. en den muss der Code instrumentiert werden Dabei werden Z hler und weitere Hilfskonstrukte in den Code eingef gt Bei der Ausf hrung des Kompilats mit bestimmten Testdaten werden die instrumentierten Stel len teilweise durchlaufen Die Z hlerst nde geben am Ende Aufschluss ber die Anzahl der Durchl ufe Durch das Instrumentieren ver ndert sich jedoch das Laufzeit und Ressourcenverhalten des Testobjekts was zu anderen Ergebnissen als bei MIL oder SIL f hren kann 4 Hardware in the loop HIL Der Code wird f r die Zielplattform generiert und in das Steuerger t geladen Die Kopplung an den Rechner mit der Umgebungssimulation erfolgt ber spezielle Hardware Schnittstellen Diese nehmen teilweise selbst die R ckkopplung vor wenn eine reaktionsschnelle Signalverar beitung gefordert ist Auch eine Lastsimulation liegt daher in ihrem Aufgabengebiet Bei den eben beschriebenen X in the loop Systemen wird eine nicht exi stierende Umgebung simuliert Falls eine reale Umgebung zur Verf gung steht l sst sich das Testobjekt darin einbetten Einen popul ren Ansatz auf der Modellebene stellt das Rapid Prototyping dar Ziel ist das fr hzeitige Validieren von Funktionen am realen System Das Modell wird mit Hilfe spezieller Rapid Prototyping Hardware die an die Umge bung angebunden ist ausgef hrt Voraussetzung ist das Vorliegen eines ausf hrbaren Modells vgl Abschnitt 2 2 In Abschnitt 7 4 wird n her darau
70. en Befehle vom CAN Bus der aktuelle T rzustand und der Zustand des T rschlosses eingelesen und ausgewer tet Abh ngig von den anliegenden Signalen wird beim Eintreten von entsprechenden Bedingungen gem ss Abschnitt 5 2 der entsprechende Befehl weitergeleitet handleUnlock erh lt einen Befehl zum ffnen falls e ein inkonsistenter T r und Riegelzustand vorliegt e eine T r auf der Fahrzeugseite des TSGs ge ffnet wird e das T rschloss aufgedreht wird oder e cine CAN Nachricht mit der Anweisung zum ffnen eintrifft 70 handleLock erh lt einen Befehl zum Schliessen falls alle T ren geschlos sen sind und e eine CAN Nachricht mit der Anweisung zum Schliessen eintrifft oder e das T rschloss zugedreht wird handleUnlock Das Eintreffen eines ffnen Befehls veranlasst handleUnlock den Entrie gelungsvorgang gem ss Abschnitt 5 2 2 ab dem Pr fen der Batteriespan nung durchzuf hren Dabei werden die Riegelmotoren nur gestartet falls die Riegel nicht schon ge ffnet sind handleLock Mit einem Schliess Befehl von handleLock wird der Verriegelungsvorgang ab der berpr fung der Batteriespannung gem ss Abschnitt 5 2 2 an gestossen Wie bei handleUnlock wird nur dann eine Spannung an die Riegelmotoren gelegt wenn die Endposition noch nicht erreicht worden ist W hrend des Bearbeitungsvorganges eines Befehls kann unter Umst nden ein weiterer Befehl eintreffen der den entgegengesetz ten Verriegelungs
71. enten ber folgende Schnittstellen angeschlossen Sensoren und Aktoren die sich in der Vordert r befinden sind dem Stecker S1 zuge ordnet Sensoren und Aktoren auf der gleichen Fahrzeugseite die nicht in der Vordert r platziert sind sind ber Stecker S2 mit dem Steuer ger t verbunden Dazu geh ren zum Beispiel Elemente im Aussenspiegel und in der Hintert r Stecker S3 ist f r die Anbindung an den CAN Bus zust ndig Eine detaillierte Zuordnung von in dieser Diplomarbeit relevanten peripheren Komponenten zu den Steckern ist im Anhang B zu finden Im Folgenden wird die grunds tzliche Funktionsweise der in dieser Diplomarbeit betrachteten Komponenten erl utert Dies sind das T rschloss der Fensterheber und die Beleuchtung Die restlichen Kom ponenten sowie die Fehlersicherung und Diagnose sind nicht mehr Ge genstand dieser Arbeit Details sind PH02 zu entnehmen 47 5 2 T rschloss Die T rschloss Funktion ist verantwortlich f r die Zentralverriegelung des Fahrzeugs Betroffen sind alle T ren wobei bzgl der T renanzahl zwischen den Fahrzeugtypen Cabriolet Coupe und Limousine unterschie den wird Jedes T rsteuerger t interagiert mit den Aktoren und Sensoren der T r en der eigenen Fahrzeugseite und stimmt sich ber den CAN Bus mit dem anderen Steuerger t ab 5 2 1 Verriegeln Ein Verriegeln Signal ber den CAN Bus oder das Zusperren des T rschlosses an der Vordert r fasst das TSG als Auff
72. er Fensterend positionssensor Fensterheber taster Fensterheber motoren Fensterposition Spiegelheizung Spiegelmotoren Spiegelposition Spiegelwahl schalter Abbildung 5 1 Funktionen des T rsteuerger tes Die Funktionen f r die Sitzeinstellung sind zust ndig f r das Verstellen von Lehnenwinkel Sitzposition Sitzh he und Schalung des zugeordne ten Vordersitzes Das Speichern von Einstellungen des Fahrersitzes und der Aussenspiegel erfolgt im Benutzermanagement F r die Aussenspie geleinstellung ist eine eigene Funktionsgruppe zust ndig Der Funktio nalit t f r das T rschloss die Fensterheber und die Beleuchtung sind eigene Abschnitte gewidmet Diese Diplomarbeit beschr nkt sich in ih rer Betrachtung auf die drei zuletzt genannten Komponenten 46 5 1 2 Hardwareeigenschaften Fahrerseite Beifahrerseite ge eege EE Fensterhebertaster Fensterhebertaster f r alle T ren rechtes TSG EI linkes TSG 5 Griff und 5 Griff und 4 T rschloss gt T rschloss Fensterhebertaster Ba Kindersicherung Kindersicherung H Bez Ki Griff Es Abbildung 5 2 Position der T rsteuerger te und Bedienelemente Beide Steuerger te sind an den CAN Bus angebunden und k nnen somit miteinander und mit anderen Komponenten des Fahrzeugs kommunizie ren Zudem sind je T rsteuerger t auf dessen Fahrzeugseite periphere Kompon
73. er and J Philipps Model Based Development of Embedded Systems In Advances in Object Oriented Information Systems Lecture Notes in Computer Science volume 2426 pages 298 311 Springer Verlag 2002 B Sch tz M Pister and A Wisspeintner Anforderungs analyse in der modellbasierten Entwicklung am Beispiel von AutoFocus Softwaretechnik Trends 24 1 2004 systematic testing com http www systematic testing com J rg Sch uffele and Thomas Zurawka Automotive Software Engineering Vieweg 2004 Telelogic http www telelogic com The Mathworks Inc http www mathworks com UPPAAL http www uppaal com Validas AG http www validas de M Wolff and H Deiss Neue Testmethodik f r vernetzte Systeme Hanser Automotive 7 2005 Guido Wimmel Specification Based Determination of Test Sequences in Embedded Systems Master s thesis Techni sche Universit t M nchen 2000 G O Wimmel Model Based Development of Security Critical Systems PhD thesis Technische Universit t M nchen 2005 135
74. erden Darauf basierend sollen anschliessend Qualit tssicherungsmassnahmen wie Modelchecking und White Box Tests angewandt bewertet und ge gen bergestellt werden Der Vergleich der Verfahren soll Vor und Nach teile aufzeigen die beim Einsatz von formalen Verfahren im Entwick lungsprozess aufkommen 1 2 Struktur der Diplomarbeit Das zweite Kapitel gibt einen einf hrenden berblick ber den Entwick lungsprozess von Software Die Vorz ge modellbasierter Entwicklung und die Entwicklung von Software in der Automobilindustrie werden dar in erl utert Im dritten Kapitel werden traditionelle Techniken f r das Testen von Software vorgestellt Unterschieden wird hier zwischen Qua lit tssicherungsverfahren f r IT Systeme und Verfahren f r Software in Kraftfahrzeug Steuerger ten Das darauf folgende Kapitel gibt eine kompakte Einf hrung in die Grund lagen von Modelchecking Als Basis f r die Anwendung der beschriebenen Qua lit tssicherungsmethoden dient die Spezifikation des oben genannten T rsteuerger tes Das f nfte Kapitel befasst sich daher mit dessen f r die Diplomarbeit relevanten Teilen Im Anschluss daran beschreibt das n chste Kapitel die eingesetzten Werkzeuge mit denen die Spezifikation des T rsteuerger tes jeweils um gesetzt wurde Schwerpunkte bilden einerseits ASCET als industriell eingesetztes CASE Tool und andererseits AutoFocus als Modellierungs werkzeug akademischen Ursprungs mit einer Modelcheck
75. erhebertaste der Fahrer Fensterhebertaste und von Doorlock_Module Bei den Fensterheberta sten wird dem Signal unter Umst nden eine Verz gerung hinzugef gt vgl Fussnote 2 auf Seite 50 Aus der Aufl sung der vorbereiteten Eingangswerte folgt die resultie rende Anweisung die dann an die Motoransteuerung weitergeleitet wird Dazu werden folgende Schritte zyklisch bei jedem Aufruf durch den Sche duler wiederholt 1 berpr fe ob eine manuelle Fensterbewegung beendet werden soll vgl Fussnote 2 auf Seite 50 73 und keine weitere Anweisung desselben Typs mehr anliegt 2 falls ja dann leite einen Stopbefehl an die Motoransteuerung weiter 3 a ansonsten berpr fe ob es eine neue Anweisung die zur Fenster scheibenbewegung f hren soll gibt z B wenn ein bislang ma nuelles Fensterhochfahren in ein automatisches Fensterhochfahren bergehen soll oder wenn z B statt eines manuellen Fensterhoch fahrens ein manuelles Fensterrunterfahren erw nscht ist 3 b falls ja dann w hle diejenige mit der h chsten Priorit t und leite den entsprechenden Befehl an die Motoransteuerung weiter Auf diese Weise wird nach Ablauf der Schritte immer die zeitlich zuletzt get tigte Benutzeranweisung ausgef hrt Auch f r den Konfliktfall dass mehrere Anforderungen gleichzeitig eintreffen ist durch die Priorisierung in Schritt 3 b gesorgt Diese Schrittreihenfolge verhindert zudem dass der Motor zu fr h abge stellt wird
76. erliches Sensorsigna kontinuierliches Sensorsigna kontinuierliches Sensorsigna kontinuierliches Sensorsigna kontinuierliches Stellsignal periodisches Signa periodisches Signa periodisches Signa periodisches Signa periodisches Signa periodisches Signa periodisches Signa periodisches Signa kontinuierliches Sensorsignal kontinuierliches Sensorsignal kontinuierliches Sensorsignal kontinuierliches Stellsignal spontanes Signal spontanes Signal kontinuierliches Sensorsignal kontinuierliches Sensorsignal periodisches Signal periodisches Signal periodisches Signal 128 Windows_Req _WIN_HR_OP Windows_Req WIN_VL_CL Windows_Req _WIN_VL_OP Windows_Req WIN_VR_CL Windows_Req _WIN_VR_OP uest_Front_In uest_Front_In uest_Front_In uest_Front_In WIN_CAN WIN_CAN WIN_CAN WIN_CAN WIN_CAN CAN Eingang CAN Eingang CAN Eingang CAN Eingang CAN Eingang period period period period period isches Signa isches Signa isches Signa isches Signa isches Signa Tabelle C 2 Bedeutung der Nachrichten im ASCET Modell auf Modulebene 129 Abbildungsverzeichnis 2 1 2 2 2 3 2 4 2 9 2 6 3 1 3 2 3 3 3 4 4 1 5 1 5 2 6 1 6 2 6 3 6 4 6 5 6 6 6 7 6 8 6 9 6 10 7 1 1 2 Phasen der Software Entwicklung 2 2 2 2 Verteilung des Arbeitsaufwandes 2 2 2 2 2
77. ertungen stattfinden aBool bInt lt dBool cInt 0 0 0 1 1 1 Tabelle 3 1 Einfache Bedingungs berdeckung 3jede Zeile entspricht einer Auswertung der gesamten Bedingung 29 2 Mehrfachbedingungs berdeckung branch condition combination testing Jede Kombination von atomaren Ausdrucksauswertungen muss mindestens einmal vorkommen F r das Beispiel m ssen beim Testen also folgende Auswertungen auftreten 3 Minimale Mehrfachbedingungs berdeckung modified branch condition decision testing All diejenigen Kombination von Ausdrucksauswertun gen mit folgender Eigenschaft m ssen mindestens einmal vorkommen Unterscheiden sich zwei Kombinationen im Wahrheitswert eines einzigen atomaren Ausdrucks und zugleich des Gesamtausdrucks so m ssen diese aBool bInt lt dBool cInt 0 0 0 0 0 1 0 1 0 0 1 l 1 0 0 1 0 1 1 1 0 1 1 1 Tabelle 3 2 Mehrfachbedingungs berdeckung Kombinationen w hrend des Testablaufs auftreten aBool bInt lt dBool aBool amp amp bInt lt cInt cInt dBool 0 0 1 0 0 1 0 0 0 1 1 0 1 0 0 0 1 0 1 1 ji 1 0 1 1 1 1 1 Tabelle 3 3 Minimale Mehrfachbedingungs berdeckung 30 Durch einen Vergleich kann man feststellen dass die erste Zeile von Ta belle 3 2 in Tabelle 3 3 fehlt Diese Zeile ist auch nicht mehr erforderlich da sie die hier erforderliche Eigenschaft nic
78. etriebssystem deutlich Einem Projekt k nnen OSEK Tasks zugewiesen werden Entsprechend den Erl uterungen zu OSEK in Abschnitt 2 3 ist jeder Task minde stens ein Prozess zugeordnet Die Reihenfolge der Task und Pro zessausf hrungen kann ber das Scheduling von OSEK in ASCET kon figuriert werden In ASCET MD werden Prozesse innerhalb von Modu len definiert Module bilden damit die Komponenten auf der h chsten Ebene eines hierarchisch strukturierten Projektes Die Kommunikation zwischen mehreren Modulen wird durch den Austausch von Nachrichten modelliert Die Prozesse eines Moduls k nnen auf dessen Nachrichten eing nge und ausg nge zugreifen und darauf basierend Berechnungen durchf hren Dazu k nnen gemischt graphische und textuelle Elemente f r Berechnungen eingesetzt werden Als textuelles Beschreibungsele ment dient die Java hnliche Beschreibungssprache ESDL Embedded Software Description Language ESDL verzichtet dabei auf Vererbung implementierungsabh ngige Konzepte z B Zeiger und beschr nkt sich auf die im Umfeld von eingebetteten Systemen relavanten Konzep te Diese Einschr nkungen erlauben eine semantische berpr fung auf 53 Abbildung 6 2 Projektstruktur Korrektheit Auch C Code kann f r hardwarespezifische Erg nzungen eingef gt werden Blockdiagramme und Zustandsautomaten stellen die graphischen Elemente dar Bild 6 3 illustriert anhand eines Beispiels die Definition von Prozessen Das darin gezeigt
79. eutet wird der modellbasierte Entwicklungs prozess durch den Einsatz von CASE Werkzeugen unterst tzt Sol che Werkzeuge kamen auch bei der Umsetzung der Spezifikation des T rsteuerger tes zur Anwendung Im Folgenden werden daher die in dieser Diplomarbeit verwendeten Tools vorgestellt 6 1 ASCET Werkzeugkette Die ETAS Group Gmb richtet sich mit ihren Produkten und Dienst leistungen an die OEMs und Zulieferer aus der Automobilbran che Dazu stellt sie unter anderem f r die Entwicklung von Steuer ger tesoftware eine Werkzeugkette zur Verf gung die den Entwicklungs prozess durchg ngig unterst tzen soll In Anlehnung an das V Modell zeigt Bild 6 1 welche Aufgabengebiete dabei abgedeckt werden Die ASCET Softwarefamilie adressiert hierbei die Schritte vom Entwurf bis zur Implementierung Sie ist gegliedert in ASCET MD Modeling amp Design ASCET RP Rapid Prototyping und ASCET SE Software Engineering 52 Modellierung und Simulation Messung Kalibrierung und Diagnose Rapid Prototyping Test und Validation ASCET SE Codegenerierung Applikations Software Plattform Software OSEK Steuerger t Abbildung 6 1 ASCET Toolkette 6 1 1 ASCET MD ASCET MD stellt eine Entwicklungsumgebung zur Verf gung in der Sy stemmodelle erstellt werden k nnen Bild 6 2 veranschaulicht die Struk tur eines Projektes in ASCET MD Darin wird die Integration der Ap plikation in das zugrunde liegende OSEK B
80. f hren zur gleichen Bewegungsrichtung des Fen sters Der entsprechende Befehl wird an die Motoransteuerungen FrontMotor bzw BackMotor weitergeleitet Die Priorisierung in Schritt 2 l st Konflikte bei gleichzeitigem Eintref fen von neuen Anweisungen auf Zudem f hrt dieses Vorgehen zum gew nschten Verhalten beim Loslassen von mehreren gedr ckten Tasten in bestimmten F llen Beispiel 8 1 1 In diesem Kontext wird Beispiel 7 1 7 zum Vergleich wie derholt aufgegriffen Der Fahrer auf der linken Fahrzeugseite dr ckt die Taste zum manuellen Runterfahren des Beifahrerfensters Das rechte TSG erh lt ber den CAN Bus die neue Anweisung zum Runterfahren der vorderen rechten Fensterscheibe Schritt 1 Da nur diese einzige Anweisung zu diesem Zeitpunkt anliegt ist dies die resultierende Anwei sung von Schritt 2 dessen Flag in Schritt 3 a dann auch gesetzt wird Sie ist vom Typ manuelle Fensterrunterbewegung vom CAN Eingang Der entsprechende Befehl wird im Schritt 4 an die Motoransteuerung wei tergeleitet und f hrt zur Runterbewegung der Scheibe Danach bet tigt der Beifahrer auf der rechten Seite die Taste zum manuellen Runterfah ren derselben Fensterscheibe Das TSG verarbeitet das Signal Schritt 1 und registriert dieses als einzige neu eintreffende Anweisung Schritt 2 Im 3 a Schritt wird dessen Typ daher gemerkt Typ manuelle Fensterrunterbewegung vom Taster Die bisherige Anweisung von der Fahrerseite hat denselben Ty
81. f Erfahrungswerten des Te sters Hier gibt es keine systematisches Vorgehensweise Die Intuition des Testers im Fehlerfinden basiert auf einer langj hrigen Erfahrung im Testen und im Umgang mit der Anwendungsdom ne Neben den hier erw hnten gibt es noch eine F lle weiterer Black Box Test Verfahren die jedoch im Rahmen der Diplomarbeit nicht weiter betrachtet werden Mye01 White Box Tests Bei der Betrachtung eines Objektes als White Box ist dessen inter ner Aufbau nach aussen hin sichtbar und analysierbar Deswegen kann man im Gegensatz zu den vorgestellten Black Box Testverfahren bei der Testfallermittlung f r White Box Tests auf die innere Struktur des Sy stems zur ckgreifen Der Ablauf von Berechnungen kann unter anderem mit Hilfe eines Kontrollflussgraphen visualisiert werden siehe Abbildung 3 2 Die Berechnungsschritte eines Programms werden dabei den Knoten eines gerichteten Graphen zugeordnet berg nge zwischen Berech nungsschritten Spr nge und Verzweigungen im Programm werden durch Transitionen zwischen den Graphenknoten dargestellt Ausgehend vom Startknoten werden dann entsprechend dem Berechnungsablauf des Pro gramms die verschiedenen Knoten durchlaufen Jeder Testfall entspricht somit einem Pfad durch den Kontrollflussgraphen Dies erm glicht Aussagen ber den Grad der Abdeckung des Testobjektes beim Te sten White Box Tests k nnen somit verwendet werden um Testf lle die durch Black Box Methoden ge
82. f eingegangen Im Gegensatz zum Rapid Prototyping liegt beim Onboard Testsystem ein Prototyp Fahrzeug mit realer Steuerger te Hardware vor so dass die Steuerger te Software darauf getestet werden kann Die Interaktion er folgt ber den Fahrer In folgender Tabelle sind obige Testsysteme nochmals zusammengefasst 35 Umwelt simuliert real Modellebene Model in the loop Rapid Prototyping Softwareebene Software in the loop Testboard Processor in the loop Steuerger t Hardware in the loop Onboard Test Tabelle 3 5 Klassifikation der Testsysteme Folgende Grafik veranschaulicht eine beispielhafte Einordnung der Test verfahren in den zeitlichen Ablauf der Entwicklung von Steuerger te Software im Zusammenspiel mit der Hardware Entwicklung Steuerger te Applikation Onboard Test Hardware in the Loop Processor in the Loop Graphische Modellierung Model in the Loop Rapid Prototyping Software in the Loop Seriencode Generierung Abbildung 3 3 Einordnung der Testsysteme MC Modelchecking Abschnitt 8 3 TIG Modellbasierte Testfallgenerierung Abschnitt 8 2 SIM Simulation Abschnitt 7 2 WBT White Box Tests Abschnitt 7 3 Codegeneratoren nehmen wie schon in Abschnitt 2 2 angesprochenen eine zunehmend wichtigere Rolle bei der Seriencode Generierung ein Al lerdings werden spezifische Anpassungen im Sourcecode teilweise immer 36 noch per Hand durchgef
83. forderungen die auf den Zweck des Systems ausgerichtet sind von nichtfunktionalen Anfor derungen wie Leistung Laufzeit und Speicherverbrauch unterscheiden Verifikation Wurde das Produkt richtig implementiert Validierung Wurde das richtige Produkt implementiert Die Verifikation befasst sich mit Fehlern der Fehlerklasse 3 Die Validie rung adressiert Fehler aus den Fehlerklassen 1 und 2 Somit stellen Verifikation und Validierung z B in Form von Tests qualit tsverbessernde Massnahmen dar Organisatorisch werden diese im Rahmen der Testplanung ber cksichtigt Darin erfolgt die Zutei lung der Ressourcen wie Mitarbeiter und der zeitlichen Einteilung der T tigkeiten Desweiteren wird festgelegt mit welcher Intensit t und Priorit t die einzelnen Systemteile zu testen sind Auch die zu verwen denden Werkzeuge werden hier bestimmt Kapitel 3 geht auf das Testen 13 an sich noch genauer ein 2 2 Modellbasierte Entwicklung Wie oben angedeutet ist ein Grund f r das Entstehen von Fehlern nicht nur eine missverst ndliche bzw unvollst ndige textuelle Spezifikation Dies liegt in der inh renten Mehrdeutigkeit der menschlichen Sprache be gr ndet Verbessern kann man diese Situation durch die Strukturierung der Informationen mit Hilfe von CARE Werkzeugen wie z B Telelogics DOORS Tel Einen weiteren Ausweg bilden formale Beschreibungs techniken die in Kapitel 4 genauer erl utert werden Damit lassen sich Spezifikationen
84. form Abbildung 7 6 Rapid Prototyping Aufbau baute T rsteuerger t wird durch die Rapid Prototyping Hardware emu liert Diese besteht aus dem ES1000 Geh use welches mit verschiedenen Steckkarten den Umweltanforderungen angepasst werden kann Im vor liegenden Fall sind darin die ES1130 3 und ES 1325 Karten verbaut die beide ber den VME Bus miteinander verbunden sind Die ES1130 3 Karte ist zust ndig f r die Kommunikation mit dem dem Entwicklungs host ber eine Ethernet Schnittstelle Auf der Entwicklungsplattform wird mit ASCET RP Code aus dem ASCET Modell cross kompiliert auf die ES1130 geladen und dort ausgef hrt Die Interaktion mit Akto ren und Sensoren erfolgt dann ber die ES1325 Karte Dazu ist diese mit digitalen Ein und Ausg ngen ausgestattet Allerdings werden da mit die Aktoren bzw Sensoren in der T r nicht direkt angesteuert bzw ausgelesen Die Koppelung der Signalpegel erfolgt ber eine separate Zwischenschaltung Teilweise sind in diese Schaltung weitere Funktionen aufgenommen worden die nicht durch die ETAS Hardware nachgebildet oder aus technischen Gr nden nicht in der Fahrzeugt r platziert werden konnten So z B die Taster f r den Fensterheber und die Aussenspie geleinstellung Desweiteren werden die Sensorsignale der Fensterschei benbewegung in dieser Schaltung weiter aufbereitet 81 Die Scheibenbewegung f hrt zur Drehung eines R dchens an dem zwei um 90 Grad gedrehte Hallsensoren angebracht si
85. g 2 5 AUTOSAR Software Architektur Hardwarespezifische Details sollen den Anwendungen verborgen bleiben so dass diese unabh ngig von der Hardware und portabel implementiert werden k nnen Auf individuelle Kundenw nsche auf Applikationsebene kann so leichter eingegangen werden Zum Beispiel l uft die Kommuni kation zwischen Software Komponenten f r diese transparent ber Ports ab so dass sie unabh ngig vom Deployment auf dieselbe Schnittstel le zugreifen Die Implementierung dieses Virtuellen Funktionsbusses VFB erfolgt mit Hilfe des AUTOSAR Runtime Environments RTE welches die Intra und Inter Steuerger tekommunikation verwaltet Das RTE wiederrum setzt auf der Basis Software auf die den Zusammen hang zur Hardware eines Steuerger tes darstellt Als Teil der Basis Software kann ein OSEK kompatibles Betriebssystem zum Einsatz kom men OSEK kompatible Betriebssysteme unterst tzen den ISO 17356 Standard Im folgenden wird daf r stellvertretend der Begriff OSEK verwendet ohne sich auf ein bestimmtes OSEK Derivat zu beschr nken AUTOSAR steht f r AUTomotive Open System ARchitecture 20 Genauso wie bei AUTOSAR muss OSEK zun chst konfiguriert werden bevor es erstellt und eingesetzt werden kann OSEK ist ein statisches Betriebssystem Zur Laufzeit findet zum Beispiel keine dynamische Spei cherallokation statt denn die Anzahl der Anwendungen und eingesetzten Betriebsmittel wird fest vorkonfiguriert
86. g 9 2 Code Einbindung in ASCET Im Vergleich zur Entwicklung mit den beiden Werkzeugen bietet die Pro grammierung auf Codeebene einen gr sseren Freiheitsgrad hinsichtlich der Beschreibungsm glichkeiten Vor allem bei hardwarenahen Funk tionen wird dies deutlich Beispielsweise unterst tzt ASCET RP 5 1 in Verbindung mit der Rapid Prototyping Karte ES 1222 keine Versendung von azyklischen CAN Nachrichten im direct mode mit Hilfe von Modell elementen und Standardeinstellungen ASCET kompensiert dies ber Workarounds durch die M glichkeit die Funktion mit benutzerspezifi schem C Code nachzubilden AutoFocus hat vom Umfang her restriktivere Beschreibungstechniken und damit geringere Freiheitsgrade Letzteres ist allerdings darauf zur ckzuf hren dass AutoFOCUS aus der Idee heraus entstand einge schr nkte Beschreibungsmittel zur Verf gug zu stellen die im Gegenzug dazu dann mit formalen Methoden behandelt werden k nnen vgl Ab schnitt 9 1 1 Hardwarenahe Codeabschnitte k nnen in AutoFocus nach der Codege nerierung von Hand eingef gt werden Allerdings muss dieser Vorgang bei jeder Ab nderung des Modells und nachfolgender Codegenerierung wiederholt werden Eine automatisierte r ckwirkende nderung des Modells nach einer Co de nderung ist sowohl bei AutoFocus als auch bei ASCET momentan nicht gegeben Ohne Einschr nkungen bei der Programmierung mittels Richtlinien ist solch ein Ansatz praktisch auch nur schwer realisierbar
87. gl Ab schnitt 8 3 1 Beispielsweise k nnen durch die Zeitdiskretisierung zeitli che Abst nde mittels Verkettung von Next Operatoren ausgedr ckt wer den Nicht immer lassen sich damit auf Grund von Wechselwirkungen Eigenschaften auf eine intuitive Art und Weise darstellen Die verz gerte Nachrichten bermittlung in AutoFocus bei Verzicht auf immediate ports f hrt zu komplexeren Formeln um die zeitlichen Abh ngigkeiten zu erfassen Mit wachsender Komplexit t der Formel wird es auch zuneh mends schwerer die Korrektheit der Formulierung der Eigenschaft selbst im Hinblick auf die Spezifikation zu zeigen 112 Subjektiv betrachtet stellte dies jedoch im Gegensatz zu den manuel len sysiphusartigen Schritten beim Testen eine herausfordernde Aufga be dar Auch die konstruktive Art Eigenschaften nachzuweisen statt Fehler finden zu m ssen wirkten sich positiv auf die Motivation aus Zeitlicher Aufwand Fast die gesamte Zeit f r das Testen wurde zu gleichen Teilen f r das Aufstellen von Testf llen hinsichtlich eines hohen berdeckungsgrades und die Interpretation der Testlaufergebnisse aufgewandt Wie schon oben erw hnt k nnte dieser Teil durch eine entsprechende Automati sierung hinsichtlich der Anforderungen reduziert werden Die Rechen ausf hrungszeit der Tests selbst gem ss 7 3 kann in ASCET skaliert werden so dass der daf r betriebene Aufwand praktisch irrelevant klein ist Das Zeitintervall zwischen zwei
88. hitektur Funktionsnetzwerk auf die technische Systemarchitektur Steuerger tenetzwerk Dabei werden die einzelnen Funktionen den vorhandenen Steuerger ten zuge ordnet Im Falle der Zentralverriegelung sind die T rsteuerger te davon betroffen siehe Kapitel 5 Nachdem die technische Architektur f r das System feststeht erfolgt dessen Partitionierung in Steuerger tehardware Steuerger tesoftware Sollwertgeber Sensoren Aktuatoren und deren parallele Entwicklung Die vorliegende Diplomarbeit befasst sich vorwie gend mit der Entwicklung der Software von Steuerger ten weswegen nur der Teilast f r die Software Entwicklung im Bild detaillierter dargestellt ist Nach der Implementierung wird das System wieder aus den einzelnen Teilsystemen zusammengesetzt Komponenten Integrations System tests verifizieren das jeweilige Resultat bzgl dessen Spezifikation Eine Validierung gegen ber Benutzeranforderungen findet im Akzeptanztest statt Die nachtr gliche Kalibrierung nach der Integration der System komponenten sorgt f r eine Anpassung regelungstechnischer Parame ter Zum Beispiel k nnen hier die Kennfelder eines Motorsteuerger tes f r einen konkreten Motor individuell eingestellt werden Der Kernprozess wird von Unterst tzungsprozessen begleitet deren Auf gabengebiete in folgender Tabelle zusammengefasst sind S704 Projektmanagement Kosten Termin Organisations planung Risikoanalyse Konfigurationsmanagement
89. ht erf llt Denn bei alleiniger nderung der Auswertung eines einzigen atomaren Ausdrucks entwe der aBool bInt lt cInt oder dBool von 0 auf 1 ndert sich der Gesamtausdruck aBool amp amp bInt lt cInt dBool nicht 4 Modifizierte Bedingungs Entscheidungs berdeckung modified condi tion decisiton coverage bzw MC DC Entspricht der minimalen Mehr fachbedingungs berdeckung mit der Einschr nkung dass f r jede ato mare Aussage auf die die Eigenschaft der minimalen Mehrfachbedin gungs berdeckung zutrifft nur ein Paar von Kombinationen aufzutreten braucht Aus Tabelle 3 3 k nnen f r den Ausdruck aBool die Paare mit den Zeilennummern 1 5 3 7 oder 2 6 in die Tabelle 3 4 bernommen werden Denn auf jedes dieser Zeilenpaare trifft die Eigenschaft aus Punkt 3 zu Hier fiel die Entscheidung zugunsten letzteren Paares Analog wird f r die anderen atomaren Ausdr cke bInt lt cInt und dBool auch ein Zeilenpaar aus Tabelle 3 3 ausgew hlt und zu Tabelle 3 4 hinzugef gt aBool bInt lt dBool aBool amp amp bInt lt cInt cInt dBool 0 1 0 0 1 0 0 0 1 0 1 1 1 d 0 1 Tabelle 3 4 MC DC Weitere Testschritte Ein System l sst sich oft hierarchisch zerlegen Auf der untersten Hierar chieebene befinden sich die Module auf die Tests mit den oben erw hnten Kriterien angewendet werden k nnen Daher werden diese Tests auch als Modulte
90. ichbarkeit von Zust nden abgefragt werden in denen die Pr misse A erf llt ist AG not A liefert ein Gegenbeispiel das die Erreichbarkeit eines Zustands in dem A erf llt wird belegt Allerdings schwankte der zeitliche Aufwand abh ngig von der Komple 95 xit t der Komponenten zwischen 2 bis 10 Minuten Um den zeitlichen Aufwand beim Modelchecking zu verringern wurde der Zustandsraum explosion durch folgende Massnahmen bei der Modellierung entgegenge wirkt e Schnittstellen des TSGs zur Umgebung wurden so modelliert dass ein leerer Kanal NoVal ebenso als Wert interpretiert wird Statt z B einem Kanal den Datentyp Bool mit der Wertemenge False True zuzuweisen wird ein benutzerdefinierter Datentyp Foo mit der Wertemenge Bar verwendet Dadurch reduziert sich die Wertemenge NoVal False True mit der ein Kanal belegt werden kann auf die Wertemenge Noval Bar e Trotz der Definition eines Limits bei der Verwendung von Inte gerwerten MaxInt k nnen mehrere unabh ngig verwendete In tegervariablen den Zustandsraum erheblich vergr ssern Beispiels weise werden in dem TSG Modell Timerkomponenten eingesetzt die nach Ablauf eines Countdownz hlers in Form einer Integerva riablen einen Alarm ausgeben Werden z B 2 solcher Timerkom ponenten eingesetzt und ist MaxInt auf 15 gesetzt so vergr ssert sich der Zustandsraum u U um den Faktor 15 Besteht zwischen beiden Timerkomponenten e
91. ige Aspekte im Hinterkopf behalten werden Der Hintergrund vor dem AutoFocus entwickelt wurde ist ein ande rer als bei ASCET Der AutoFOCUS Ansatz wurde m glichst generisch gew hlt um ein m glichst grosses Spektrum von Anwendungen zu un terst tzen ASCET hingegen war von Anfang an auf die Entwicklung von Steuerger ten und regelungstechnischen Algorithmen ausgerichtet und somit f r den industriellen Einsatz im Bereich Automotive spezialisiert Relativiert wird diese Situation durch die aktuell voranschreitende Ent wicklung von AutoFocus 2 die momentan am Lehrstuhl von Professor Broy an der TU M nchen vorangetrieben wird Auta Vielversprechende innovative Konzepte zur Realisierung eines durchg ngigen Entwicklungs prozesses werden darin integriert Daher konzentrieren sich die folgenden Abschnitte auf den Vergleich der dahinterliegenden Prinzipien und Methoden der beiden Werkzeuge Es wird an dieser Stelle auch betont dass einige Einschr nkungen in Au toFOCUS nur durch das Modelchecking und nicht durch das Werkzeug selbst bedingt sind 103 9 1 1 Modellierung Die einfache intuitive Beschreibungstechnik in AutoFocus basiert auf einer eingeschr nkten Notation im Vergleich zu anderen Modellierungs werkzeugen wie ASCET Daraus resultiert eine kompakte dahinterliegen de Semantik bei AutoFocus die formal festgehalten werden kann und auch f r andere akademische Verifikationsverfahren wie Theorem Proving zug nglich ist Ein w
92. ignals k nnen der zugeh rigen Nachricht ver schiedene Werte zugewiesen werden Dies wird in ASCET mit Hilfe von Datentypen modelliert Dazu stehen Standard Datentypen z B Bool Int zur Verf gung Alternativ k nnen benutzerdefinierte Datentypen definiert werden Anhang C listet die verwendeten benutzerdefinierten Datentypen und die darauf basierenden ASCET Nachrichten auf Kon kreten Signalpegeln auf S1 und S2 wird somit eine Bedeutung zugewiesen Dasselbe gilt f r die CAN Nachrichten die ber S3 bertragen werden Auch das zeitliche Verhalten der Signal bertragung muss festgelegt wer den Dieses richtet sich nach der Art des Signalempf ngers bzw senders und unterliegt der Konvention in Tabelle 7 1 Im Folgenden bezieht sich der alleinstehende Begriff Nachricht auf Nachrichten in ASCET und nicht auf CAN Nachrichten 65 Eing nge Ausg nge Signale ber S1 S2 Sensoren liefern st ndig ein Si gnal an das TSG Nachrichten wert entspricht immer dem ak tuell gelesenen Sensorwert Aktuatoren erhalten st ndig ein Stellsignal vom TSG Nach richtenwert entspricht immer dem aktuellen Stellwert periodische Signale ber CAN Treiber ber den CAN Bus wird an periodischen Zeitpunkten ein Signal empfangen Nachrich tenwert entspricht dem zuletzt bertragenen Signalwert periodisch zu sendendes Si gnal wird dem CAN Treiber bermittelt Nachrichtenwert entspricht dem periodisch zu bert
93. inander verbindet Mit AutoFocus wird eine Plattform f r die Integration von formalen Methoden und zur Anbindung an externe Werkzeuge zur Verf gung ge stellt Ein Beispiel daf r wird im n chsten Abschnitt n her erl utert 6 3 5 Modelchecking Anbindung AutoFocus unterst tzt unter anderem die Anbindung von Verifikati onswerkzeugen wie dem symbolischen Modelchecker SMV Cad Da mit lassen sich Eigenschaften von modellierten Systemen nachweisen Das Haupteinsatzgebiet des Modelcheckers SMV sind synchrone Syste me Auf Grund ihres globalen Systemticks sind AutoFOCUS Systeme gut daf r geeignet Die zu berpr fenden AutoFocus Modelle m ssen zun chst in ein f r den SMV Modelchecker lesbares Format gewandelt werden das einer codierten Kripke Struktur entspricht siehe Bild 6 8 Diesen Schritt bernimmt die Modelchecking Anbindung Das detaillierte bersetzungsschema kann Wim00 entnommen werden Die STDs der atomaren Komponenten werden dabei zun chst jeweils in Formeln aussa genlogischer Art gewandelt Je STD legt die resultierende Formel einer seits den Initialzustand von lokalen Variablen und Nachrichtenausg ngen fest Andererseits sind darin alle m glichen Zustands berg nge codiert Bislang unterst tzte die Modelchecking Anbindung bei der bersetzung von Transitionen keine Priorit ten In SMV wurden somit Transitio nen trotz unterschiedlicher Priorit t als gleichberechtigt angesehen Im Rahmen der Diplomarbeit wu
94. ine Ausschlussbedingung z B wenn auf Grund des Modellverhaltens immer nur ein Countdown Timer aktiv ist so k nnen beide Komponenten zu Einer zusammenge fasst werden Somit reduziert sich der Faktor auf den Wert 15 Eine weitere Verbesserung kann erzielt werden indem der Count downz hler auf einen definierten Wert gesetzt wird z B 1 falls der Z hler gerade nicht verwendet wird Dies verringert ebenfalls die Anzahl der m glichen Werte die der Z hler in Kombination mit den restlichen Systemzust nden annehmen kann Im Sinne von Design for Testability k nnte man hier den Begriff De sign for Modelcheckability ansetzen wo schon bei der Modellierung eines Systems hinsichtlich des Zustandsraumproblems gewissen Empfehlungen Folge geleistet werden k nnte Das Modell des TSGs greift nicht auf Immediate Ports zur ck Somit erfolgen Berechnungsschritte der Komponenten auch nicht in einem un endlich kleinen Zeitintervall Dies gen gt dem Umstand dass ein Berech Dal Abschnitt 8 1 1 96 nungsschritt auf einem Mikroprozessor ebenfalls Zeit ben tigt Als Kon sequenz ergibt sich ein pipeline artiges Verhalten der Berechnungsschrit te was analog zum integrierten Schaltungsentwurf zu Hazards f hren kann vgl Abschnitt 8 1 2 Damit sich die einzelnen Signale nicht berholen k nnen Synchronisationsmassnahmen wie z B Zwischenpuffer dem entgegen wirken Im Unterschied zu einem rein event gesteuerten System bei d
95. ing Anbindung Die Anbindung an weitere Werkzeuge zur Durchf hrung der Tests werden hier ebenfalls behandelt Die folgenden beiden Kapitel dokumentieren die Modellierung und An wendung der Test und Verifikationsverfahren auf das Steuerger t mit Hilfe der vorgestellten Werkzeuge Basierend auf den gesammelten Erkenntnissen erfolgt im neunten Kapitel die Bewertung der eingesetzten Methoden 10 Kapitel 2 Aspekte der Software Entwicklung Schon die in der Einleitung erw hnten Bemerkungen haben deutlich ge macht dass der Software Entwicklungsprozess von IT Systemen nicht oh ne weiteres direkt im Kontext der Automobilindustrie angewendet wer den kann Im Folgenden werden daher zun chst allgemeine Gesichts punkte des klassischen Software Engineering aufgezeigt Moderne Entwicklungsmethoden wie die der modellbasierten Entwick lung haben mittlerweile auch im Bereich Automotive Fuss gefasst Dar auf sowie auf den Software Entwicklungsprozess von Steuerger ten wird im Anschluss eingegangen um den Zusammenhang zum Automotive Software Engineering herzustellen 2 1 Grundlegende Begriffe Software Engineering kann man als die zielorientierte Bereitstellung und systematische Verwendung von Prinzipien Methoden Konzepten Nota tionen und Werkzeugen f r die arbeitsteilige ingenieurm ssige Entwick lung und Anwendung von umfangreichen Software Systemen auffassen Bal00l Darunter f llt auch die Beschreibung von Vorgehensm
96. interscheibe FF_MOTOR1 Output 1 Anschluss f r den Fensterhebermo tor der Hinterscheibe FF_MOTOR2 Output 2 Anschluss f r den Fensterhebermo tor der Hinterscheibe FF_UNTEN Input Positionssensor f r hintere Fenster scheibe unten FF_OBEN Input Positionssensor f r hintere Fenster scheibe oben FT_OFFEN Input Zustandssensor der Hintert r 124 FT_GRIFF Input Zustandssensor des T rgriffs der Hin tert r FKIND SICH Input Zustand der Kindersicherung der Hin tert r FT LICHT Output Ansteuerung der Ausstiegsleuchte der Hintert r FT RIEGEL Input Zustandssensor f r hintere T rverriegelung FZENTR_MOTI Output 1 Anschluss f r den Verriegelungsmo tor der Hintert r FZENTR_MOT2 Output 2 Anschluss f r den Verriegelungsmo tor der Hintert r 125 Anhang C Modellierung in ASCET C 1 Benutzerdefinierte Datentypen Datentyp Wert Bedeutung AUTO_CLOSE AUTO_CLOSE_Disabled TSG Konfigurationswert keine Wirkung AUTO_CLOSE_Roof TSG Konfigurationswert Schliessen der Fen ster beim Abschliessen wenn Cabriolet Verdeck geschlossen ist AUTO_CLOSE_Always TSG Konfigurationswert Beim Abschliessen werden Fenster immer geschlossen BATT BATT_ge0lt90 OV lt Batteriespannung lt 90V BATT_ge901t100 90 lt Batteriespannung lt 100V BATT ge100le105 100 lt Batteriespannung lt 105V BATT gt105le180 105 lt Batteriespannung lt
97. jekts abgeleitet 24 Verifikationsmethoden dynamisch Black Box Tests White Box Tests Modelchecking quivalenzklassen Anweisungs berdeckung Theorem Proving Walkthrough Zweig berdeckung Pfad berdeckung Bedingungs berdeckung Abbildung 3 1 berblick ber g ngige Testmethoden informell Fehlererwartung Ist das Testobjekt eine berechnende Funktion so besteht ein Testfall aus konkreten Argumenten f r die Funktion als Fingabe und der erwarteten Ausgabe Ein Fehler tritt zum Beispiel auf wenn die erwartete Ausgabe der Funktion nicht mit der aktuellen Ausgabe bereinstimmt Im Gegensatz zu einer Funktion erfolgt bei einem kompletten Software system im Allgemeinen nicht nur eine einmalige Auswertung von Einga bedaten vgl Abschnitt 8 2 Hier besteht ein Testfall aus einer Sequenz von Eingabewerten und den zugeh rigen erwarteten Ausgabewerten Beim Testvorgang werden mehrere Testl ufe nacheinander ausgef hrt Dabei wird je Testlauf ein Testfall auf das Testobjekt angewandt und die dabei entstandene Ausgabe mit der erwarteten Ausgabe verglichen Wenn beide Ausgabewerte voneinander abweichen deutet die Inkonsi stenz auf einen Fehler im Testfall oder im Testobjekt hin Die 100 ige Abdeckung des Testobjekts durch alle m glichen und er denkbaren Testf lle ist im Allgemeinen unm glich Daher erfolgt das Testen nur solange bis eine vorher festgelegte Bedingung eintritt
98. kennzeichnet an denen der bearbeitende Prozess vom Dispatcher auf gerufen wird Der Pfeil zwischen den Beschriftungen verdeutlicht die Abh ngigkeit des ASCET Nachrichtenwertes vom aktuellen Signalwert Die Nachrichtenwerte 0 und 1 werden als Sensorwerte interpretiert Beispiel 7 1 2 Ausgeben eines Stellwertes 1 Signal p DB i 0 e Zeit 1 Zn Zeg ie VE i Nachricht 0 Zeit Hier h ngt die Signalausgabe von der ASCET Nachricht ab Die Nach richtenwerte 0 und 1 werden als Stellwerte interpretiert Beispiel 7 1 3 Empfangen eines periodischen CAN Signals 1 CAN Signal d H Zeit 1 Nachricht 0 Zeit Nur der Nachrichtenwert 1 wird als g ltiges CAN Signal interpretiert 0 hingegen wird hier verwendet um auszudr cken dass nichts empfangen wurde Zu CAN Signalen muss in ASCET somit als Workaround ein separater Wert definiert werden um eine leere Nachricht auszudr cken In AutoFOCUS hingegen sind per Definition leere Nachrichtenkan le er laubt Das Puffern von eingetroffenen Signalen erfolgt im CAN Treiber Hier wird nur die Schnittstelle definiert auf der das Steuerger t aufsetzt Beispiel 7 1 4 Periodisches Versenden eines CAN Signals 1 CAN Signal Nachricht 0 T Zeit Wie in Beispiel 7 1 3 wird hier 0 verwendet um auszudr cken dass nichts gesendet werden soll Beispiel 7 1 5 Empfangen eines spontanen CAN Signals 67 CA
99. l 48 f hrt zum Entriegeln Der Entriegelungsvorgang wird allerdings nur aus gef hrt wenn die Batteriespannung mindestens 9 Volt betr gt Liegt die Batteriespannung tempor r unter 9 Volt weil der Antriebsmotor gerade gestartet wird so wird gewartet bis der Motor gestartet wurde Liegt die Batteriespannung dann wieder ber 9 Volt so wird der Entriegelungsvor gang wiederholt Der Entriegelungsvorgang besteht aus dem Ansteuern der angeschlossenen Verriegelungsmotoren ber das Verschicken einer entsprechenden Nachricht ber den CAN Bus wird das T rsteuerger t auf der gegen berliegenden Seite ebenso zum Entriegeln aufgefordert Nach mindestens zwei Sekunden werden die Verriegelungsmotoren ge stoppt falls bis dahin die Riegel schon ge ffnet wurden Wenn die Riegel nach drei Sekunden noch immer geschlossen sind wird der Entriege lungsvorgang abgebrochen und eine Fehlermeldung ber den CAN Bus verschickt Das T rsteuerger t auf der linken Fahrzeugseite wartet nach erfolgreicher Verriegelung eine Sekunde lang auf eine eventuelle Fehler meldung des rechten T rsteuerger tes Nach Ablauf der Sekunde ohne Fehlermeldung wird abschliessend einmal geblinkt Prinzipiell sollen sich alle T rriegel nach Beendigung der Aktionen im gleichen Zustand befinden Dies setzt eine Synchronisation beider T rsteuerger te ber den CAN Bus voraus Ein Konflikt bei gleichzeiti ger Aufforderung zum Ver und Entriegeln wird durch eine h here Prio
100. lexen Zu sammenh ngen und Abh ngigkeiten Das Vorliegen einer Spezifikation auf formaler Basis w rde diesen Prozess sehr unterst tzen Im Rahmen der Diplomarbeit musste jedoch auf eine Spezifikation in textueller Pro saform zur ckgegriffen werden Schritte mit Interpretationst tigkeiten z B Vergleichen der Ausgabe mit den Anforderungen in der Spezifika tion liessen sich damit nicht maschinell durchf hren und erwiesen sich als langwieriger Prozess Modelchecking in AutoFocus wurde zun chst eingesetzt um Teilkom ponenten auf lokale Eigenschaften hin zu berpr fen Da Kenntnis se ber den internen Aufbau der Komponenten vorlagen White Box konnten mit geringem Aufwand w hrend der Entwicklung gezielt Eigen schaften z B Abwesenheit von Deadlocks formuliert und berpr ft wer den Ein Fehler deutete entweder auf eine inkorrekte Stelle im Modell oder auf eine bzgl der Spezifikation fehlerhaft formulierte Eigenschaft hin Die Schwierigkeit bei der berpr fung mittels Modelchecking be steht zun chst im Aufstellen korrekter Eigenschaften die im Einklang mit der Spezifikation stehen Gezwungenermassen setzt man sich dabei detaillierter mit der Spezifikation auseinander und deckt dadurch unter Umst nden Spezifikationsfehler auf Das nachtr gliche Aufstellen von Eigenschaften ohne Ber cksichtigung der internen Struktur der Komponenten Black Box oder von Kompo nenten einer h heren Hierarchiebene gestaltet sich schwierig v
101. mmen werden B 1 Stecker S1 Anschluss von Elementen der Vordert r Bezeichnung Richtung Bedeutung FHB_VL Input Fensterheber Taste vorne links nur auf Fahrerseite belegt FHB VR Input Fensterheber Taste vorne rechts nur auf Fahrerseite belegt FHB HL Input Fensterheber Taste hinten links nur auf Fahrerseite belegt FHBHR Input Fensterheber Taste hinten rechts nur auf Fahrerseite belegt F_BEWEG Input Bewegungssensor f r die Vorderscheibe T_OFFEN Input Zustandssensor der Vordert r T_GRIFF Input Zustandssensor des T rgriffs der Vor dert r 123 T LICHT Output Ansteuerung der Ausstiegsleuchte der Vordert r F UNTEN Input Positionssensor f r vordere Fenster scheibe unten H OBEN Input Positionssensor f r vordere Fenster scheibe oben T RIEGEL Input Zustandsensor f r vordere T rverriegelung KEY STATE Input Zustandssensor des T rschlosses ZENTR MOT1 Output 1 Anschluss f r den Verriegelungsmo tor der Vordert r ZENTR MOT2 Output 2 Anschluss f r den Verriegelungsmo tor der Vordert r H MOTORI Output 1 Anschluss f r den Fensterhebermo tor der Vorderscheibe F_MOTOR2 Output 2 Anschluss f r den Fensterhebermo tor der Vorderscheibe B 2 Stecker S2 Anschluss von externen Elementen Bezeichnung Richtung Bedeutung FFHB Input Fensterhebertaste der Hintert r FF_BEWEG Input Bewegungssensor f r die H
102. n Be dingungen eintreten Denn auf Grund der Komplexit t der phyikalischen Zusammenh nge kann die simulierte Regelstrecke nur eine Vereinfachung darstellen Die Regelstrecke wird mittels Differentialgleichungen model liert und im Arbeitspunkt linearisiert MSF05 Zudem ist eine Validierung gem ss Kundenw nschen nur in der realen Umwelt m glich da nur dort ein endg ltiger Funktionsnachweis erfol gen kann beispielsweise bei der Erzeugung von authentischem Motoren ger usch oder der Bremspedalr ckwirkung 2 Software in the loop SIL Nach der Umsetzung des Funktionsmodelles in Code kann dieser auf der Entwicklungsplattform zur Ausf hrung gebracht werden Oben bespro chene Testverfahren sind hier ebenfalls anwendbar Auch hier kann die Umgebung durch ein weiteres Software System simuliert werden Da das Gesamtsystem auf einer beliebigen leistungsstarken Hardware simuliert werden kann spielen Echtzeiteigenschaften noch keine Rolle Die Ge schwindigkeit mit der das Funktions und Umgebungsmodell ablaufen kann jeweils beliebig eingestellt werden Analog zu MIL ist SIL frei von zeit und kostenintensiven Versuchen 3 Processor in the loop PIL Hier wird der Code auf einem Testboard auf einem Prozessor ausgef hrt der der Zielplattform entspricht Die Umgebung wird hier auf einem se 34 paraten Rechner im Labor simuliert der mit dem Testboard kommuni ziert Um obige Testverfahren der Code berdeckungsanalyse anzuw
103. n dem mehrere Si gnalbits bertragen werden k nnen Funktionen wie z B die Zentralver riegelung lassen sich durch die Verwendung von Bussystemen r umlich auf die verschiedenen Steuerger te verteilen Der Aufwand f r die Verka belung f llt dadurch weit geringer aus Hinzu kommt die einfachere Er weiterbarkeit und Variantenbildung durch den modularen Aufbau Eine gesteigerte Zuverl ssigkeit und Sicherheit kann durch eine ausfalltoleran te Auslegung und berwachungsrechner erreicht werden Nachteilig ist jedoch das mit der Vernetzung einhergehende Problem der Feature In teraction Eine Feature Interaction ist eine Situation in der sich mehre re Funktionen ungewollt gegenseitig beeinflussen und dabei unerwartete negative Effekte hervorrufen Das gesamte vernetzte System von elektronischen Steuerger ten in einem Fahrzeug l sst sich in mehrere Subsysteme untergliedern Man unter scheidet Antriebsstrang Fahrwerk Multi Media und Karosserie wobei sich letzteres Subsystem in Komfort und passive Sicherheit aufgliedern l sst Beispiele f r die Zuordnung von Funktionen zu Subsystemen 17 Antriebsstrang Motorsteuerung Getriebesteuerung Fahrwerk Anti Blockier System Karosserie Komfort Zentralverriegelung Spiegelverstellung Fensterheber Karosserie passive Sicherheit Airbagsysteme Multi Media Radio Tabelle 2 1 Zuordnung von Funktionen zu Subsystemen Das Zusammenspiel der verschiedenen Kom
104. n ist oder e die Scheibe w hrend der Bewegung blockiert Der letzte Fall aktiviert beim Scheibenhochfahren den Einklemmschutz Die Scheibe wird dann solange wieder runtergefahren bis sie am Anschlag angelangt ist 3 Sekunden abgelaufen sind oder blockiert 75 Bild 7 4 veranschaulicht das Verhalten der Komponente DispatchCom mand In den Zust nden Open und Close wird die Scheibe gem ss obiger Beschreibung Herunter bzw Hochgefahren Jam repr sentiert den Zu stand in dem der Einklemmschutz aktiv ist Init Entry stop motor jam buffer command Static peak error buffer command Jamf Entry start motor timer jam Static countdown Open ER Entry start motor timer jam Static countdown Close Entry start motor timer jam Al Static countdown Abbildung 7 4 DispatchCommand in ASCET Beleuchtung Die beiden Module DoorLight und InteriorLight sind f r die Ausstiegs leuchten bzw die Innenraumbeleuchtung zust ndig Sie setzen die in Abschnitt 5 4 geforderte Funktionalit t um Hilfsmodul Gem ss der TSG Spezifikation bermittelt das TSG auf der Fahrerseite dem gegen berliegenden TSG den aktuellen T rstatus Das Beifahrer TSG kombiniert diesen Status mit dem Zustand der eigenen T ren und 76 sendet das Resultat zur ck Je TSG ist das Modul DoorState daf r zust ndig den kombinierten T rzustand zur Weiterverarbeitung an die Module Doorlock_Module und InteriorLight weiterzuleiten 7 2
105. n mittels Modelchecking als Anwendung eines formalen Ve rifikationsverfahrens erl utert 8 1 Modell des T rsteuerger ts 8 1 1 Rahmenbedingungen Aus denselben Gr nden wie in Abschnitt 7 1 1 werden zun chst die Rah menbedingungen definiert bevor darauf basierend auf das TSG Modell eingegangen wird Schnittstellenkonvention In AutoFocus kommuniziert das T rsteuerger t ber Kan le mit der Umgebung vgl Abschnitt 6 3 1 Den Kan len sind Datentypen zuge ordnet die die Signalwerte repr sentieren Datentypen k nnen Standard datentypen z B Bool oder Int oder benutzerdefinierte Datentypen z B WIN_CAN sein Die kanonische Modellierung der TSG Schnittstelle zur Umgebung basiert auf folgender Konvention 84 Eing nge Ausg nge Signale ber S1 S2 Sensoren liefern bei jedem Sy stemtick ein Signal Kanalwert entspricht immer dem aktuell gelesenen Sensorwert Aktuatoren erhalten bei jedem Systemtick ein Stellsignal vom TSG Kanalwert entspricht im mer dem aktuellen Stellwert periodische Signale ber CAN Treiber wenn bei einem Systemtick eine CAN Nachricht anliegt erh lt entsprechender Kanal diesen Wert CAN Treiber versendet CAN Nachrichten in periodischem Zeitraster gem ss Fraunhofer Spezifikation dazu wird letz ter Wert NoVal des ent sprechenden Kanals verwendet f r einen Systemtick liegt ent sprechender Wert am Kanal an spontane Signale ber CAN Treiber
106. nd siehe Bild 7 7 Hallsensor 1 D Hallsensor 2 a i Abbildung 7 7 Hallsensoren zur Einklemmschutzerkennung Dadurch werden bei der Bewegung der Scheibe zwei um 90 Grad ver schobene Sinuskurven erzeugt Die oben genannte Schaltung wandelt diese mit Hilfe von Schmitt Triggern in zwei um 90 Grad verschobene Rechteckkurven um siehe Bild 7 8 Hallsensor 1 Ln amam g Hallsensor 2 n z Rechteck 1 Rechteck 2 Abbildung 7 8 Signalverl ufe der Sensoren Diese Rechteckkurven gelangen an die Eing nge der ES 1325 und k nnen dann von der ES1130 weiter verarbeitet werden Der zeitliche Abstand zwischen den Flanken der beiden Rechteckkurven deutet auf die Um drehungsgeschwindigkeit des R dchens und somit auf die Bewegungsge schwindigkeit der Fensterscheibe hin berschreitet der Abstand zwi schen zwei Flanken eine gewisse Schwelle obwohl die Motoren einge schaltet sind und sich die Fensterscheibe beim Hochfahren noch nicht am Anschlag befindet so wird dies als Einklemmen interpretiert Die Scheibe wird dann an den unteren Anschlag gefahren Weiterhin kann man aus den Rechteckkurven die Fensterbewegungsrichtung ablesen und somit einen relativen Z hler implementieren siehe Bild 7 9 82 Hallsensor 1 high Hallsensor 2 high Z hler 1 Hallsensor 1 low Hallsensor 2 high Hallsensor 1 high Hallsensor 2 low Z hler 1 Hallsensor 1 low Abbildung 7 9 Zustandsbasiertes Quadratur
107. ndustrie Dazu dient eine im Rahmen eines Projektes am Fraunhofer Institut erstellte Spezifikation PH02 In Form eines Lastenheftes sind darin die Funktionen des Steuerger tes im Automobil beschrieben die das T rmodul und den Fahrzeuginnenraum betreffen Die Systemkomplexit t und Beschreibungstiefe der Spezifikation ist vergleichbar mit denen einfacher Steuerger te im Fahrzeuginnenraum Die Kapitel 7 und 8 befassen sich dann mit der Umsetzung dieser textuell verfassten Spezifikation in ein ausf hrbares Modell Die Umsetzung erfolgte anhand ausgew hlter Komponenten des T rsteuerger tes 5 1 Einsatz des T rsteuerger tes im Auto mobil 5 1 1 Funktionen des T rsteuerger tes Die Spezifikation sieht je Fahrert r ein T rsteuerger t TSG vor Fol gendes Bild veranschaulicht die Funktionsgruppen des Steuerger tes und die mit ihnen interagierenden peripheren Komponenten 45 Benutzermanag menttaster Kindersicher ungsschalter Griffleisten sensor Schlossnuss schalter T r Offen Sensor Zentralver riegelungsmotor T rverriege lungssensor Ausstiegs leuchte Sitzposition Sitzverstell taster Sitzmotoren T rsteuerger t Sitzeinstellung Fensterheber Benutzer management Innenraum beleuchtung T rschloss Bon MAN Aussenspiegel einstellung Bedien beleuchtung CAN Bus Innenraum Spiegeltast
108. nlichkeit dar mit der ein Sicherheitssystem die geforderten Sicherheitsfunktionen in nerhalb eines Zeitraumes erf llen kann SIL 4 stellt die h chste Stufe mit geringer zul ssiger Ausfallswahrscheinlichkeit dar und SIL1 die niedrigste ISIL steht f r Safety Integrity Level 22 Stufe mit h herer zul ssiger Ausfallswahrscheinlichkeit Unter anderem basieren unternehmensspezifische Standards auf dem ge nerischen IEC 61508 Standard Dabei werden oft eigene Abstufungen verwendet wie z B der Automotive Sicherheits Integrit tslevel ASIL statt SIL Abh ngig vom ASIL eines betrachteten Testobjekts eignen sich die verschiedenen Qualit tssicherungsverfahren siehe Abschnitt 3 2 un terschiedlich gut In einem unternehmensspezifischen Standard kann so mit abh ngig vom konkreten ASIL eine Auswahl von Testmethoden f r den Einsatz im eigenen Projekt vorgegeben werden FTWT 05 Da neben ber cksichtigen Standards oft organisatorische Massnahmen und spezifizieren somit die Vorgehensweise f r einen systematischen Testa blauf und die Testplanung Im Allgemeinen geben Standards den Rahmen aber nicht Details f r die Vorgehensweise vor Dies erlaubt eine individuelle Anpassung an das jeweils eigene Projekt Unternehmensspezifische Leitlinien bieten sich hier als Entscheidungs und Orientierungshilfen bei der technischen Um setzung an Im Gegensatz dazu geben Richtlinien einzuhaltende Regeln und Vorgaben an Sie stellen im Kontext
109. ntnommen worden 1 _Extrahiere eine Anforderung aus der Spezifikation z B Licht leuch tet nur 30 Sekunden wenn alle T ren geschlossen worden sind und die Z ndung aus ist 2 Generiere einen Eingabesequenzpr fix der zu dem Systemzustand f hrt ab dem diese Anforderung erf llt werden kann z B Schlies sen aller T ren und Ausschalten der Z ndung 77 3 Vervollst ndige die Sequenz mit Eingaben mit denen die Anforde rung erf llt wird z B Aufrechterhalten des Zustands der geschlos senen T ren und der ausgeschalteten Z ndung f r 30 Sekunden Dabei wurde ber cksichtigt dass der in Schritt 2 erreichte Systemzustand unter Umst nden nicht eindeutig ist z B Fahrzeugtyp ist entweder ein Zweit rer oder ein Viert rer Solche Mehrdeutigkeiten wurden durch zus tzliche Testf lle abgedeckt Ebenso wurden negative Testf lle unter sucht die absichtlich nicht den Anforderungen entsprechen 7 3 Testen auf Codeebene Auch die in Abschnitt 3 2 2 besprochenen Verfahren lassen sich auf den von ASCET generierten Code anwenden Insbesondere wurde hierbei das White Box Testen auf Basis von berdeckungskriterien herangezogen Um grosse Testdatenmengen zu bew ltigen ist der Einsatz von Werk zeugen die die berdeckungsanalyse durchf hren erforderlich ASCET unterst tzt von Haus aus keine Code Coverageanalyse so dass technische Eingriffe f r die Anbindung von externen Coverage Tools notwendig sind Im Rahmen der Diploma
110. ochoptimierter Code f r den Einsatz in zeitkritischen oder speicherarmen Umgebungen n tig ist Weiterhin gibt es kein Werkzeug das alle Einsatzgebiete abdeckt und zu gleich einen effizienten durchg ngigen Entwicklungsprozess unterst tzt ASCET ist beispielsweise auf letzteres im Bereich der Entwicklung f r Steuerger te Software und regelungstechnische Algorithmen ausgerich tet Multimedia Anwendungen oder Anwendungen abseits des Bereichs Automotive werden hingegen nicht betrachtet 9 2 Bewertung der Qualit tssicherungs methoden Fehlerfindung 110 Unstimmigkeiten mit der TSG Spezifikation wurden in ASCET mit Offline Experimenten ausgemacht siehe Abschnitt 7 2 Unter den gefundenen Fehlern befanden sich z B Deadlocks oder fehlerhafte Tran sitionsvorbedingungen die zu einer falschen Priorisierung gef hrt haben Die Tests liefen Hand in Hand mit der Modellierung der einzelnen Kom ponenten Das fertige ASCET Modell wurde im Nachhinein modulwei se mit der in Abschnitt 7 3 vorgestellten Methode auf Codeebene gete stet Es wurden hierbei kleinere Leichtsinns Fehler z B bertragung eines falschen Nachrichtenwertes nicht erreichbare Stellen im Modell und falsche Ablaufsequenzen in ASCET gefunden In AutoFocus war der Simulator recht hilfreich um unmittelbar nach dem Erstellen einer Teilkomponente logische Fehler z B falsche Priori sierung von Transitionen zu entlarven Schwer auffindbare Fehler die vor allem
111. odellen mit deren Hilfe man den Herstellungsprozess eines Softwareproduktes strukturieren kann Der Entwicklungsprozess l sst sich dabei in mehrere grundlegende Aktivit ten zerlegen 11 Anforderungen an das Endprodukt werden zun chst in der Analysephase ber cksichtigt Anschliessend erfolgt in der Entwurfsphase und in der Im plementierungsphase die Umsetzung Die Testphase die Inbetriebnahme und die Wartung runden die Vorgehensweise ab Abh ngig vom gew hlten Vorgehensmodell f llt die Einteilung in diese Phasen und die Beziehungen zwischen ihnen unterschiedlich aus Ein Beispiel f r ein konkretes Vorgehensmodell stellt das V Modell dar Anhand dessen f r die Software Erstellung zust ndigen Teil werden die Beziehungen zwischen den einzelnen Phasen veranschaulicht Software Implementierung Abbildung 2 1 Phasen der Software Entwicklung In Form eines textuell verfassten Lastenheftes werden die Anforderungen auf informelle Art und Weise aus der Sicht des Auftraggebers formu liert Die Umsetzung in einen Entwurf und die Implementierung erfolgt auf dem linken Ast in Bild 2 1 Dabei werden grosse Systemen zur bes seren Beherrschbarkeit hierarchisch in Subsysteme zerlegt Das Testen der Komponenten und des zusammengesetzten Systems erfolgt auf dem rechten Ast Falls beim Testen im rechten Ast Fehler gefunden wurden erfolgt die Korrektur r ckwirkend an der entsprechenden Stelle im linken Ast Die Phasen werden dann ab
112. oftware bestimmt ist ber die Anbindung an Sensoren und Aktuatoren kann das Steuerger t als Teil eines Regelkreises bestehend aus Sollwertgeber Regler Aktuatoren Strecke und Sensoren betrachtet werden Steuerger t Regler St rgr sse Belastung Pulsweitenmodulierter Stromrichter Stellglied Aktuator Gleichstrommotor Regelstrecke Sollwert Vorgabe de Drehgeschwindigkeit UUL ch Inkrementalgeber zur Drehzahlerfassung Messglied Sensor Abbildung 2 3 Das Steuerger t als Teil eines Regelkreises 3ECU steht f r Electronic Control Unit 16 Ein Beispiel f r einen Sollwertgeber ist die Vorrichtung zur bermittlung der Fahrpedalstellung Beispiele f r Sensoren sind Drehzahlmesser und Spannungsmesser Aktoren k nnen unter anderem Motoren oder Ventile sein Die Strecke stellt den zu regelnden physikalischen Vorgang dar z B Umdrehungsgeschwindigkeit Das Steuerger t nimmt als Regler seinen Platz im Regelkreis ein Durch die Verwendung von Steuerger ten lassen sich oft mehrere Steuer und Regelungsfunktionen in einem Ger t vereinen was zu Kosteneinsparungen f hrt Eine weitere Betrachtungsweise von Steuerger ten ergibt sich bei Ber cksichtigung der Vernetzung der Steuerger te untereinander Die Kommunikation zwischen den Steuerger ten erfolgt dabei ber ein Bus systeme wie den CAN Bus Der CAN Bus ist ein nachrichtenorientiertes Bussystem Eine Nachricht beinhaltet ein Datenfeld i
113. or FrontLowWin ji Front Out ERRORC WIN Battery_Front Motor_Front Abbildung 8 7 Modularer Verifikationsansatz 100 Die Kan le Bottom_Front MovingSensor_Front Ton Front und Front_Motor interagieren direkt mit der TSG Umgebung Sie sind somit nicht vom restlichen TSG Modell abh ngig Die Eingangskan le Bat tery_Front und MotorFront hingegen erhalten Nachrichten von anderen TSG Komponenten Nachrichten ber die Ausgangskan le FrontLow Win und Front_Out_ERROR_WIN gelangen ebenfalls nur ber andere TSG Komponenten an die TSG Umgebung Allerdings sind Ausgaben ber FrontLowWin und Front_Out_ERROR_WIN nicht TSG intern ber Battery_Front und MotorFront r ckgekoppelt Dadurch ergeben sich f r die Komponente FrontMotor keine internen R ckkoppelungen zwischen Teilkomponenten des TSGs In AutoFocus werden beim Abgehen des Zustandsraumes w hrend des Modelcheckings alle Eingangskan le der zu berpr fenden Komponente jeweils mit allen m glichen Werten belegt F r die Komponente Front Motor wird mit dieser chaotischen Eingabemenge die Korrektheit obi ger Eigenschaft nachgewiesen Im Kontext des TSG Modells kann man daher die anderen TSG Komponenten als zwei Komponenten R in und Bai auffassen Ab straktion Rin liefert dann nichtdeterministisch Eingabewerte In an FrontMotor ber Battery_Front und MotorFront Rout akzeptiert be liebige Ausgabewerte Out von FrontMotor ber FrontLowWin und Front_Out_
114. or so stellt der TIG ein wirkungsvolles Instrument dar um ohne gros sen Aufwand Testdaten aus dem Testobjekt zu generieren Die erzeugten Testdaten liegen in sequentieller Form vor und k nnen nacheinander in das Testobjekt eingegeben werden Jeder Schritt entspricht einem Test lauf Schwieriger gestaltet sich die Lage bei reaktiven Systemen Hier h ngt die Ausgabe von der vorher get tigten Eingabe und vom bisherigen Zu stand ab Ein Testlauf ist hier nicht eine einmalige Eingabe sondern eine aus praktischen Gr nden beschr nkte Sequenz von Eingabedaten Die Schwierigkeit liegt darin eine inhaltlich zusammenh ngende Testsequenz zu erzeugen die m glichst viele Systemzust nde abdeckt vgl Abschnitt 3 2 2 Eine willk rliche Testdateneingabe f hrt in endlicher Zeit mit ge ringer Wahrscheinlichkeit zu aussagekr ftigen Testdatensequenzen Was durch den Einsatz des TIG somit nicht automatisiert wird ist das Erstel len von GCF Testspezifikationen die dem Ablauf eines reaktiven Systems eine Richtung vorgeben 94 Eine andere M glichkeit Testsequenzen f r reaktive Systeme zu erstellen bietet sich mit dem Modelchecker an Um Beispielsweise eine Eingabe sequenz zu erhalten die das System in einen definierten Zustand bringt kann eine entsprechend negierte Formel dem Modelchecker bergeben werden Zielzustand kann nie erreicht werden Da der erw nschte Zu stand jedoch erreicht werden kann insofern das Modell diesbez glich
115. orausblicken ussert sich in einer nderung der Formel wenn X gilt dann ergibt sich Y nach 2 System 99 ticks Die resultierende Formel nimmt durch diese technischen Details ggf eine unintuitive und aufgeblasene Form an Zudem k nnen kleine Verbesserungen des AutoFocus Modells zu starken nderungen an der Formel f hren Von der anderen Seite her betrachtet m sste man das AutoFocUus Modell anpassen um eine einfache und klare Formel zu erhalten die die gew nschte Eigenschaft ausdr ckt Ein Mittel dazu w re das Ent fernen der Nachrichten Pipelines ber Immediate Ports Eine andere M glichkeit ist das Zusammenfassen eines Komponentennetzwerkes zu einer SSD Komponente In der zugeh rigen STD k nnen dann mehrere sequentielle Berechnungsschritte unter Umst nden zu einem Schritt zu sammengefasst werden Wie schon eben angedeutet f hrt das Ab ndern eines AutoFocus Modells jedoch wiederum zu einer anderen Formel Auf diese Weise bauen FrontMotor und obige LTL Formel aufeinander auf im Sinne von Design for Modelcheckability Dass die Einklemmschutzeigenschaft auch im Kontext des gesamten TSG Modells korrekt ist zeigt die folgende berlegung TSG Front_Motor Top_Front Bpttom_Front MovingSensor_Front S FrontMotor R Im Battery_Front ze Motor Front FrontLowWin 2 Front_Out_ERRORZWIN S Verfeinerung Verfeinerung Top_Front B Front_Motor FrontMot
116. oraussetzung ist das Vorliegen einer formalen Beschreibung des Systems und der Anforderungen Zwei Verifikationsmethoden haben sich im Laufe der Zeit herauskristal lisiert Einerseits gibt es das Theorem Proving Mathematische Be hauptungen die die Eigenschaften eines Systems betreffen werden dabei schrittweise ber die formale Semantik des Systems hergeleitet Teil schritte der Herleitung k nnen mit Hilfe von interaktiven Theorembewei sern automatisiert werden An manchen Stellen ist jedoch der Eingriff des Benutzers notwendig um bei der Herleitung eine Richtung vorzugeben Dieser Schritt ist oft unintuitiv und erfordert detaillierte Kenntnisse im Theorem Proving Folglich ist diese Methode nicht f r den allt glichen Gebrauch durch Entwickler geeignet die eher mit den Problemen ihrer Anwendungsdom ne besch ftigt sind F r die Verifikation von sicher heitskritischen Komponenten ist der Aufwand jedoch gerechtfertigt in sofern Verifikationsexperten hinzugezogen werden Eine andere Verifikationsmethode stellt das Modelchecking dar dessen Gr ndz ge im Folgenden beschrieben werden sollen Die vorliegende Diplomarbeit konzentriert sich auf diese Methode 4 2 Modelchecking Systeme k nnen unterschiedlich ausgepr gt sein Transformationelle Systeme berechnen eine Funktion Zun chst werden die Eingabewer te eingelesen die Berechnung durchgef hrt und dann die Ausgabewerte geliefert Transformationelle Systeme interagie
117. orderung zum Verriegeln auf Die Verriegelung kann allerdings nur dann stattfinden falls alle T ren geschlossen sind und die Batteriespannung mindestens 9 Volt betr gt Der Verriegelungsvorgang besteht aus dem Ansteuern der Verriegelungsmotoren und dem Senden einer CAN Nachricht an das gegen berliegende TSG mit der Aufforderung zum Verriegeln Abh ngig von der Konfiguration des Steuerger tes erh lt auch die Fensterheber komponente ber eine interne Verbindung die Aufforderung zum Schlies sen der Fenster Das Steuerger t kann bei Einbau in ein Cabriolet so konfiguriert werden dass auch das Verdeck geschlossen wird Nach min destens zwei Sekunden werden die Verriegelungsmotoren gestoppt falls bis dahin die Riegel schon geschlossen wurden Wenn die Riegel nach drei Sekunden noch immer ge ffnet sind wird der Verriegelungsvorgang abgebrochen und eine Fehlermeldung ber den CAN Bus verschickt Das T rsteuerger t auf der linken Fahrzeugseite wartet nach erfolgreicher Verriegelung eine Sekunde lang auf eine eventuelle Fehlermeldung des rechten T rsteuerger tes Nach Ablauf der Sekunde ohne Fehlermeldung wird abschliessend zweimal geblinkt 5 2 2 Entriegeln Das mechanische ffnen einer T r z B mittels Griff ein Entriegeln Signal ber den CAN Bus oder das Aufschliessen des T rschlosses an der Vordert r werden als Aufforderung zum Entriegeln aufgefasst Auch der inkonsistente Zustand einer ge ffneten T r mit vorgeschobenem Riege
118. p und liegt immer noch an Daher bleibt dessen Flag weitherhin gesetzt Im Schritt 4 werden beide Anweisungen aufgel st und erzeugen den Befehl f r die Motoransteuerung zum Run terfahren W hrend sich die Scheibe noch in Bewegung befindet l sst der Fahrer nun die Taste los ber den CAN Bus gelangt das Signal Neu tralstellung an das Beifahrer TSG und l scht das entsprechende Flag Schritt 3 b Da der Beifahrer aber noch die eigene Fensterhebertaste gedr ckt h lt bleibt das Flag der anderen bisher vermerkten Anforderung vom Beifahrer weiterhin vermerkt Das Fenster wird weiter runterge fahren Schritt 4 Erst wenn der Beifahrer seine Taste losl sst sind nach Schritt 3 b keine Flags mehr gesetzt und der Motoransteuerungs befehl wird auf Neutralstellung gesetzt 90 Front Motor bzw BackMotor Motorf rontWyIN_MOTOR SeperateEdge FilteredComrtand WIN_MO E Buffer_BATT o lt FrontLowWin B_LOW_WIN BatteryStatus BATT ES Battery_Front BATT CheckBattery c WI MOTO e SE I DispatchCommand H ZZ A A TimerCommand Bool Top_FrontF_OBEN Alarm TIMER_INFO Bottom_Froht F UNTEN Front_Out_ERROR_WIN ER MovingSensof_FrontF_BEW ROR_WIN EG Timer Abbildung 8 4 FrontMotor in AutoFocus Beide Komponenten sind quivalent aufgebaut Beim Eintreffen eines Befehls von Request_Front siehe Bild 8 4 bzw Request Back wird der Motor durch die Unterkomponente DispatchCommand siehe Bil
119. ponenten und der verschiede nen Fachdisziplinen spiegelt sich in der Vorgehensweise bei der Entwick lung von elektronischen Systemen im Fahrzeug wieder Hinzu kommt die firmen bergreifende Zusammenarbeit zwischen Automobilherstellern und Zulieferern Die Entwicklung von elektronischen Systemen und Soft ware gliedert sich in einen Kernprozess und Unterst tzungsprozesse Folgendes Bild veranschaulicht den Kernprozess SZO4 Analyse der Benutzeranforderungen und Akzeptanztest und Systemtest Spezifikation der logischen Systemarchitektur Analyse der logischen Systemarchitektur und Spezifikation der technischen Systemarchitektur Fahrzeugentwicklung Analyse der Software Anforderungen und Spezifikation der Software Architektur EEE TER EEE EE OE Test der Software Komponenten Entwurf und Implementierung der Software Komponenten Subsystementwicklung ECU Software Entwicklung Aktuator Entwicklung hier dargestellt Sensor Sollwertgeber Entwicklung ECU Hardware Entwicklung Abbildung 2 4 Kernprozess der Steuerger te Entwicklung Ausgehend von der Analyse der Benutzeranforderungen wird die logi sche Systemarchitektur spezifiziert Diese legt die einzelnen Funktionen 18 deren Schnittstellen und die Kommunikation untereinander fest Ein kon kretes Beispiel f r eine Funktion ist die Zentralverriegelung Danach er folgt die Abbildung der logischen Systemarc
120. r Codegenerator vornehmen Beispiels weise erfolgt hier die Anpassung an unterst tzte Datentypen etc Durch die entsprechende Unterst tzung durch CASE Tools l sst sich dieser Pro zess beschleunigen und die Umsetzung in Code automatisieren vgl Ka pitel 2 2 Zum Testen eines solchen Systems sind daher angepasste Verfahren not wendig die auch den restlichen Kontext des Regelkreises miteinbeziehen um ein korrektes Zusammenspiel zu gew hrleisten Das Testobjekt wird 33 in die entsprechende Umgebung eingebettet und dort getestet Falls die Umgebung noch nicht existiert bzw das Testobjekt noch nicht eingesetzt werden kann k nnen X in the loop Systeme die fehlende Umgebung ersetzen Abh ngig vom aktuellen Stand der Entwicklung eines Systems hat X in the loop eine andere Auspr gung Da 1 Model in the loop MIL Bei Vorliegen des Funktionsmodells in einem CASE Tool kann dieses si muliert werden Die Umgebung wird ebenfalls modelliert und an das Funktionsmodell angebunden um die Testdaten zur Verf gung zu stel len und die R ckkoppelung zu simulieren Oben besprochene Test verfahren sind hier anwendbar insofern die grafische Notation eine berdeckungsanalyse zul sst Als Vorteile der Simulation sind die schnell reproduzierbaren Ergebnisse zu nennen Die Entwicklung und das Te sten im Labor sparen damit Zeit und Kosten ein Als Nachteil ergibt sich dass manche Fehler unentdeckt bleiben da sie nur unter reale
121. ragenden Signalwert spontane Signale ber CAN ein spontanes Signal wird ein spontanes Signal wird Treiber in Form eines Impulses als Impuls dem CAN Treiber vom CAN Treiber weiter bermittelt Nachrichten gereicht Nachrichtenwert wert wird vom Modul in wird als Impuls dem Modul Impulsform ausgegeben bermittelt Tabelle 7 1 Schnittstellenkonvention in ASCET Die Anbindung an den CAN Treiber ist kontextspezifisch Daher wurde in dieser Arbeit diese generische Schnittstelle gew hlt Die Einbettung in eine konkrete Umgebung erfolgt dann mit Hilfe von separaten Wrapper Modulen die die Ein und Ausgabe den Bed rfnissen entsprechend an passen Beispiele sollen die eben eingef hrte Schnittstellenkonvention verdeutli chen Beispiel 7 1 1 Auslesen eines Sensorsignals 2 BE N Signal 0 Zeit i 1 8 Nachricht 0 Zeit Auf den Zeitachsen sind in periodischen Abst nden die Zeitpunkte ge Das Anliegen eines kontinuierlichen Signals wird letztenendes durch die Hardware realisiert Denn der Prozess der den aktuellen Ausgabewert berechnet ist bedingt durch das Task Scheduling nicht andauernd aktiv 3 Ein Impuls wird in ASCET erzeugt indem eine Nachricht in einem Prozess auf den zu bertragenden Wert gesetzt wird Derselbe Prozess setzt diese Nachricht bei seinem n chsten Aufruf wieder zur ck Somit entsteht ein Impuls der L nge einer Schedulingrunde 66
122. rbeit wurde dazu IBM Rational Test RealTime verwendet Weiterhin wurde auf CTE XL zur ckgegriffen um Testda ten grafisch zu erstellen Bild 7 5 veranschaulicht die Werkzeugkette die zum Einsatz kam Wie beim Testen auf der Modellebene wurden hier ASCET Module be trachtet Mittels CTE XL werden die Eingabesequenzen f r die Modul eing nge erstellt Dazu wird in der CTE Matrix jedem Eingang zu jedem betrachteten Zeitpunkt ein Wert zugewiesen Die exportierte Eingabe sequenz kann dann mit Hilfe eines Skriptes in ein f r ASCET lesbares ASCII Format gewandelt werden Bevor ein Test mit diesen Testdaten ausgef hrt werden kann muss zun chst der Code aus dem zu testenden ASCET Modell generiert wer den Dieser kann dann f r eigene Zwecke auch unabh ngig von der ASCET Toolkette extern weiterverarbeitet werden Der in ASCET MD ASCET RP und ASCET SE generierte Code unterscheidet sich jeweils hinsichtlich der Schnittstelle zur Hardware siehe unten Der Teil f r die Funktionslogik ist identisch 78 Bi C Code kann f r externe Weiterverabeitung entnommen werden Codes U o 1 eege ee Generierung amp gcpp Pr prozessor Expandieren De a R attolcc1 Hilfstool pt siehe Text Instrumentieren C Code Coverage Viewer TestRealtime Ausf hrung des Testfall im Matlab Format Testfall im ASCII Format Simulation Kompil Pr gt pilats a
123. rde die Modelchecking Anbindung um die 61 AutoFOCUS SMV Anbindung Abbildung 6 8 Modelchecking in AutoFocus Unterst tzung von Transitionspriorit ten erweitert Dies soll im folgen den erl utert werden Gem ss Abschnitt 6 3 2 erfolgt die Auswertung der Priorit t einer Tran sition bei der Wahl der zun chst schaltenden aktiven Transition Ei ne Transition wird als aktiv eingestuft falls ihre Vorbedingung erf llt ist Dies ist der Fall wenn die dieser Transition zugeh rige bersetzte pr dikatenlogische Formel im aktuellen Systemzustand als wahr ausge wertet wird Ausschlaggebend ist der Teil der Formel der die Vorbe dingung der Transition repr sentiert Die Erweiterung um Priorit ten entspricht dem Hinzuf gen einer weiteren Vorbedingung f r diese Tran sition Die Nichterf llung der Vorbedingungen aller Transitionen h herer Priorit t Damit ist sichergestellt dass Transitionen niedrigerer Priorit t nicht schalten k nnen wenn h herpriorisierte Transitionen aktiv sind Anhand eines Beispiels wird dieser Vorgang veranschaulicht Das zum Beispiel SSD in Bild 6 9 geh rige STD ist in Bild 6 10 dargestellt Ohne Unterst tzung von Priorit ten w rde die resultierende Formel f r die Beschreibung der drei Transitions berg nge informell folgende Form annehmen State Initial A next State Two A Input 2 A next Output True V State Initial next State One Input 1 next
124. rde hierbei schon Vorarbeit geleistet siehe Text 107 9 1 3 Zusammenhang zwischen Modell und Code Die Umsetzung der Modelle in C Code erfolgt in AutoFocus und ASCET auf eine kanonische Weise Beispielsweise wird in beiden Tools f r einen Zustandsautomaten jeweils eine C Funktion erzeugt Sie be steht im Grossen und Ganzen aus einem einzigen switch Statement das den aktuellen Zustand des Automaten pr ft Bei jedem Aufruf der Funk tion wird das switch Statement einmal durchlaufen In AutoFOCUS ge schieht dies bei jedem Systemtick und in ASCET in jeder Scheduling Runde Vorbedingung_Al Aktion_Al Vorbedingung_A2 Aktion_A2 Zustand_B Vorbedingung_B1 Aktion_Bl Abbildung 9 1 Beispielautomat zur Demonstration der Codeerzeugung Pseudocode zum Automaten von Bild 9 1 void Funktionsberechnung switch aktuellerZustand case Zustand_A if Vorbedingung_A1 Aktion_A1 aktuellerZustand Zustand_B else if Vorbedingung_A2 Aktion_A2 aktuellerZustand Zustand_B case Zustand_B if Vorbedingung_B1 Aktion_B1 aktuellerZustand Zustand A 108 ASCET erlaubt dem Benutzer zus tzlich noch das Hinzuf gen von im plementationsabh ngigem C Code vgl Bild 9 2 Uber Makros kann darin auf die Modellelemente zugegriffen werden Zustands ESDL BDE automaten Modellebene Implementierungsebene Eigener Generierter i C Code C Code Abbildun
125. reiche der Eingabeparameter jeweils in quivalenzklassen unterteilt Alle Elemente einer quivalenzklasse f hren zum gleichen Verhalten des Testobjektes d h man kann anneh men dass Fehler die mit einem Repr sentanten der Klasse gefunden werden ebenso mit allen anderen Elementen der Klasse gefunden wer den k nnen quivalenzklassen sollten zur Repr sentation von g ltigen sowie von ung ltigen Werten je Eingabeparameter erstellt werden Das Erstellen von Testdaten erfolgt durch die Auswahl eines Repr sentanten je Eingabeparameter Durch die Verwendung von Repr sentanten von quivalenzklassen je Eingabeparameter statt allen Elementen des ge samten Eingabewertebereichs kann man die Anzahl der Testf lle erheb lich einschr nken Zeit und Kosteneinsparungen im Testablauf sind die Folge Grenzwertanalyse Bei der Grenzwertanalyse werden gezielt die Randbereiche der Werte heliebiges Element aus der quivalenzklasse 26 bereiche der Eingabeparameter untersucht um dort Fehler aufzudecken Man erhofft sich dadurch wirkungsvollere Testf lle Die Grenzwertanaly se findet oft Anwendung in Kombination mit dem quivalenzklassentest Als Eingabewert dient dann ein Repr sentant aus dem Randbereich der zugeh rigen quivalenzklasse Intuitive Testfallermittlung Fehlererwartung error guessing Ziel dieser Art von Testfallerstellung ist die qualitative Verbesserung und Erg nzung bisheriger Testf lle basierend au
126. ren nur an vordefinierten Stellen mit der Umgebung Reaktive Systeme hingegen interagieren st ndig mit ihrer Umgebung Ein reaktives System besteht aus mehreren Komponenten die parallel zueinander arbeiten ber den Austausch von Nachrichten kommuni zieren sie miteinander und mit der Umgebung Typischerweise ist ihre Laufzeit unbegrenzt Unter anderem geh ren eingebette Systeme zur Klasse der reaktiven Systeme 39 Die f r solche Systeme geltenden Eigenschaften lassen sich klassifizie ren Mit Sicherheitseigenschaften kann man ausdr cken dass gewisse unerw nschte Zust nde nie angenommen werden Lebendigkeitseigen schaften hingegen dr cken aus dass das System irgendwann schliesslich die gew nschte Eigenschaft haben wird Modelchecking ist eine modellbasierte Verifikationstechnik zum Nachweis solcher Eigenschaften f r ein formal spezifiziertes System Im Gegensatz zum interaktiven Theorembeweisen ist Modelchecking eine automatisier te Verifikationstechnik die w hrend der berpr fung kein Eingreifen des Benutzers erfordert Im Folgenden wird auf Konzepte eingegangen die zur Anwendung dieser Technik erforderlich sind 4 2 1 Modellierungssprache Die Beschreibung des zu verifizierenden reaktiven Systems erfolgt mit Hilfe einer Modellierungssprache Abh ngig vom eingesetzten Werkzeug f llt die Darstellung unterschiedlich aus Das grundlegende Prinzip ist jedoch allen gemeinsam Daher wird hier stellvert
127. retend die allgemei ne Beschreibungsnotation einer Kripke Struktur eingef hrt mit der das System modelliert werden kann Definition 4 2 1 Transitionsgraph Ein beschrifteter Transistionsgraph ber Aussagenvariablen p Pn hat die Form M S R L wobei S R ein gerichteter Graph mit der Knotenmenge S und der Transi tionsmenge R ist und L 9 201P eine Labelfunktion ist L s ist die Menge der p die in s gelten Definition 4 2 2 Kripke Struktur Das Tupel M s mit dem Transitionsgraphen M S R L und dem Anfangsknoten s S ist eine Kripke Struktur ber p Pn 40 Beispiel 4 2 1 S FHfp p2 S3F p2 S2F p2 In der hier verwendeten Notation bedeutet s z y dass im Knoten s die Aussagenvariablen x und y erf llt sind Der Graph stellt eine Kripke Struktur M so dar mit M S R L wobei E 5 Jan 51 92 S3 R s0 51 50 52 en 52 S1 83 82 all L so 0 L s p1 p2 L s2 pa L s3 p2 Ausgehend vom Anfangsknoten einer Kripke Struktur k nnen verschie dene Pfade abgegangen werden Dies f hrt zur Definition des Abwick lungsbaumes Definition 4 2 3 Abwicklungsbaum F r eine Kripke Struktur M s ber den Aussagenvariablen p Pn mit M S R L ergibt sich als Abwicklungsbaum wiederum eine Kripke Struktur t M sl R L mit 5 Menge der Folgen so s mit s S So s und si 5 41
128. richtet werden k nnen Bei Steuerger ten ist diese Wiederholbarkeit gegeben Nachdem alle Module getestet wurden k nnen diese zu gr sseren Teil systemen zusammengesetzt werden Der anschliessende Integrationstest befasst sich mit dem Finden von Fehlern beim Zusammenspiel der ein zelnen Komponenten und bei den Schnittstellen zwischen den Kompo nenten Der Aufwand der f r Integrationstests betrieben wird ussert sich z B in der hohen Anzahl von Testf llen Beim funktionalen Test von Fahrwerkssystemen von Mittelklasse PKWs liegt deren Anzahl schon bei 200000 WD05 Automatisierte Testabl ufe sind daher eine Vorausset zung um diese Menge von Daten innerhalb einer beschr nkten Zeit zu bew ltigen Abschliessend erfolgt auf der obersten Hierarchieebene der Systemtest Hier erfolgt die Validierung gegen ber den Systemanforde rungen Gleiches gilt f r den Abnahmetest der jedoch vom Auftraggeber durchgef hrt wird Die eben aufgef hrten Schritte finden sich in Bild 2 1 auf Seite 12 auf dem rechten Ast wieder Trotz der parallelen Vorgehensweise bei der Systemintegration im Entwicklungsprozess und im Testprozess sollten diese beiden Prozesse unterschieden werden Denn kontr r zur oben be 32 schriebenen Bottom Up Strategie kann ein System zun chst in seiner Gesamtheit getestet werden bevor rekursiv die Teilsysteme getestet wer den Top Down Nichtexistente Teilsysteme werden hierbei mit Hilfe von Stubs emuliert
129. rit t der Entriegelung gel st 5 3 Fensterheber Die Systemfunktion des Fensterhebers ist f r das ffnen und Schlies sen der Fenster zust ndig Abh ngig vom Fahrzeugtyp Limousine Ca briolet oder Coupe und der Position des T rsteuerger tes linke bzw rechte Fahrzeugseite reagiert die Fensterheberkomponente auf Anwei sungen von bestimmten Eingangsquellen Quellen k nnen der CAN Bus die vorderen bzw hinteren Fensterhebertasten und das T rschloss sein Die Aufforderungen werden entweder an das gegen berliegende T rsteuerger t weitergeleitet oder selbst weiterverarbeitet abh ngig davon ob sich die betroffene Fensterscheibe auf derselben oder ge gen berliegenden Fahrzeugseite wie das TSG befindet Mit einer Anweisung ist die Aufforderung zum ffnen bzw Schliessen einer be stimmten Fensterscheibe gemeint 49 5 3 1 Fenster ffnen bzw schliessen Sind die eingehenden Aufforderungen f r dieselbe Fahrzeugseite wie die des T rsteuerger tes bestimmt so wird zun chst die Batteriespannung auf einen Wert von mindestens 10 Volt berpr ft Ist diese Voraussetzung erf llt wird der Fensterhebermotor entsprechend angesteuert Folgende Bedingungen f hren dazu dass der Fensterhebermotor gestoppt wird e Loslassen der Fensterhebertaste bei manueller Ansteuerung e Eintreffen eines anderen Befehls e Erreichen des Anschlags am Fensterrand e Erreichen des Timeouts von drei Sekunden e Stoppen der Scheibe o
130. s Grundlage f r An nahmen dienen die z B beim Modelchecking getroffen werden k nnen Verifikationstechniken k nnen somit ebenso von diesem modularen Vor gehen profitieren Werkzeuge die das AUTOSAR Konzept unterst tzen werden in der Au tomobilindustrie Zukunft haben Man darf also gespannt sein wie sich die Lage weiterentwickeln wird 119 Anhang A Spezifikationssprachen A 1 CTL A 1 1 Syntax CTL Formeln ergeben sich durch die rekursive Anwendung der Regel p P pVp p AXp EXp AFp EFp AGp EGp ApUp EPpUp mit P als Aussagenvariable A 1 2 Semantik Die folgenden Beziehungen gelten f r den Abwicklungsbaum T t M s einer Kripke Struktur M s mit M S R L ber den Aussagenvaria blen p1 Pn p und Y stellen dabei OTL Formeln dar F r eine Folge T 8951 Sj8j41 Sn bezeichnet der Ausdruck il das Folgenglied s T E pi p Lis T E wg lt gt JE TEV lt gt TE yode TE TFEXp z Es gibt einen Nachfolger s von s mit t M s E TE Ak gt F r alle Nachfolger s von s gilt t M s E op T E EF gt Es gibt einen Pfad m in T mit Ji N t M alte 120 T E He gt Es gibt einen Pfad m in T mit Vi N t M alte T F AF gt F r alle Pfade 7 in T gilt Ji N t M z it T F Ae gt F r alle Pfade 7 in T gilt Vi N t M z it T E E pUy gt Es existiert ein Pfad m in T und ein i N so dass t M cllk und Yj lt i t M Tli
131. s In Lock ZENTR MOT MultiplexSignats_In Leni Pn MOT MuliplexSignds_In Lock ZW_SCHL hendeLsck_In_BlsckLock _MulkplexSigras_In_Lock_BLINK MultiplexSignals DEER Mitplessgnak_In_Lack_B_LOW_KEY Vue Ar Lech Zus NOT MitplexSignels_In_Lock_FZENTR_MOT MulipexSionele MiltpkesSgnab_in_Lock_ZV_SCHL Muliplessigrde Su VSH MuplesSgnas Out ZU SCHLR MitpeSigas Out BLINK handertequest_In_ Door ignal_ur Miipesigas In Lock BLINK egener eneo PE E handerequest In_Doorsigna HR MultplexSiena _QuLB_ LOW KEY MitpesSinels_In_Unlack_FZENTR_MOT handerequest_In_KEY_STATE handerequest In ZU_SCHLL Milena OU ZENTRMOT handtequest In zu sch M Lutsch e Unlock FENTR_MOT handeRequest In ZV_SCHLA MiitpksSignals_In_Unlock_2V_S0HL handeRequest In _T_OFFEN MtiolesSirisk_In Unlock B LOW KEY handeequest In FT_OFFEN June uek Out FZENTR_MOT Mipan rbl BLINK handeRequest_In_T_RIESE PE ENEE E PENET une Mutolessgna _In_Unsck_ERROR_KEY Mutblessgnab_Our ERROR KEY handleUnlock handleUnock_In_doUrlock handeuriock_Out_BlockLock IhandeUnisck_In_FT RIEGEL ha pa E ech FS Ap Ierzen TRIESEL tege hn dek ZENTRMOT bech In bar VW MuliplexSignds In Unlock ZU SCHL handeUniock In ERROR KEY MultilexSignals_In_Urlock_B_LOW_KEY MuliplexSignas_Ir ec BLINK MuplexSignds_Iin Unlock besch KEY handeUnbek_In_KL_START handeUnbck_In MOTOR LET Abbildung 7 1 DoorLock_Module in ASCET handleRequest In dieser Komponente werd
132. sts bezeichnet Im Sinne des IEC 61508 Standards kann eine C Funktion eines C Programmes als Modul aufgefasst werden Oftmals m ssen dabei mehrere Module miteinander interagieren z B durch den 31 Aufruf einer anderen C Funktion Da der Testprozess zeitlich so fr h wie m glich beginnen soll liegen nicht immer alle Komponenten f r einen reibungslosen Testablauf vor Dann k nnen eigens daf r entwickelte Testtreiber und stubs die fehlenden Komponenten ersetzen Testtrei ber ersetzen die Schnittstelle zum dar berliegenden Teilsystem in dem sich die betrachteten Komponenten befinden Dies w re z B eine main Funktion die die zu testende C Funktion mit Eingabedaten speist Mit Teststubs werden die fehlenden Komponenten hier die aufgerufenen Funktionen emuliert Durch diese Isolierung von Modulen lassen sich diesen explizite Eingabewerte bergeben die sie im integrierten System sonst nicht erhalten h tten Damit l sst sich auch deren Verhalten bei undefinierten Eingabewerten testen Wenn sich w hrend der Entwicklung nderungen am Testobjekt ergeben muss dieses nochmals berpr ft werden Dies erfolgt in den sogenannten Regressionstests Daher ist es notwendig bisher erstellte Testf lle auf zuzeichnen um bei der erneuten Testfallermittlung Zeit zu sparen Sy steme deren Anfangszust nde einfach wieder hergestellt werden k nnen eignen sich f r Regressionstests da f r jeden Testlauf die Anfangsbedin gungen erneut einge
133. t die Aufl sung der Anweisungen mittels ESDL Code siehe Abschnitt 6 1 1 Dieses Beschreibungsmittel steht in AutoFoOCUs nicht zur Verf gung so dass das gleiche Verhalten mit Hilfe eines Komponen tennetzwerkes nachgebildet wird Die Verarbeitung erfolgt in Form einer Pipeline Neue Signale durchlaufen dabei folgende Schritte 1 Eingehende Signale werden abh ngig von der TSG Konfiguration 88 FrontMotor ResolveError Dispatcher f pmnan BackMotor Abbildung 8 3 Windows Komponente in AutoFocus ausgefiltert und aufbereitet 2 Von neu eingetroffenen Anweisungen wird in der Unterkomponente DispatchRequest diejenige mit der h chsten Priorit t ausgew hlt 3 Underscheidung der resultierenden Anweisung aus Schritt 2 a Anweisung zur Fensterbewegung Es wird das Flag f r den Typ dieser Anweisung gesetzt Bisherig gesetzte Flags von anderen Anweisungstypen bleiben nur dann weiterhin gesetzt wenn sie die gleiche manuelle Fensterbewegung darstellen d h manuelles Fensterhochfahren bzw manuelles Fensterrunter fahren und die dazugeh rigen Anweisungen immer noch am TSG Eingang anliegen b Anweisung zur Neutralstellung Das Flag f r den Typ der Anweisung wird nur zur ckgesetzt falls der Typ eine manuelle Fensterbewegung darstellt vgl Fussnote 2 auf Seite 50 vgl Fussnote 7 auf Seite 74 89 4 Die gesetzten Flags
134. t die Fensterscheibenbewegung e TopFront registriert ob sich die Fensterscheibe am oberen An schlag befindet 97 e Battery_Front registriert die aktuelle Batteriespannung e MotorFront registriert einen Befehl von der Komponente Re quest_Front und den Ausg ngen e Front Motor legt die Spannung an den Fensterhebermotor an e Front_Out_ERROR_WIN signalisiert einen Fehler e FrontLowWin signalisiert eine zu niedrige Batteriespannung Die Komponente FrontMotor verh lt sich so wie in den Abschnitten 7 1 2 und 8 1 2 beschrieben wurde Mittels Modelchecking konnte f r FrontMotor gem ss der TSG Spezifikation folgende Eigenschaft nachgewiesen werden F r alle Systemzust nde soll gelten Wenn der Motor mindestens f r die L nge der Startup Zeit eingeschaltet ist und nach Ablauf dieser Zeit ein Einklemmen registriert wird dann fahre die Fensterscheibe wieder runter bis e der untere Anschlag erreicht worden ist e der 3 Sekunden Timeout abgelaufen ist oder e die Fensterbewegung blockiert wird z B wegen einer mechanischen Fehlfunktion Als LTL Formel ausgedr ckt lautet diese Eigenschaft 1 DC 2 LU 3 Val MC_FrontMotor Front_Motor F_MOTOR_Up 4 amp amp O Val MC_FrontMotor Front_Motor F_MOTOR_Up 5 amp amp OO Val MC_FrontMotor Front_Motor F_MOTOR_UPp 6 amp amp OCOCO Val MC_FrontMotor Front_Motor F_MOTOR_UP 7 amp amp OCOCOCO Val MC_FrontMotor Front_Motor F_MOTOR_Up
135. t verteilt Light Dispatcher Windows gt D e D o ber j 7 ATEAN et ch DoorState D Abbildung 8 1 berblick ber das AutoFocus Modell T rschloss Die Komponente DoorLock ist f r die Zentralverriegelung zust ndig sie he Bild 8 2 SignalDispatcher verteilt die eingehenden Signale an die anderen Komponenten von DoorLock handleRequest Befehle vom CAN Bus der aktuelle T rzustand und der Zustand des T rschlosses werden hier eingelesen und ausgewertet Die Unterkompo 86 SignalDispatcher ae handel och MultiplexSignals handleUnlock kene Abbildung 8 2 DoorLock Komponente in AutoFocus nenten RequestLock und Request Unlock l sen die Anforderungen auf und leiten den Befehl dann an handleLock bzw handleUnlock weiter handleUnlock bzw handleLock Die Beschreibung von Abschnitt 7 1 2 trifft hier ebenfalls zu Im Un terschied zum ASCET Modell werden jedoch parallel ausgef hrte Akti vit ten in eigene Subkomponenten ausgelagert Fehlernachrichten die vom gegen berliegenden TSG ber den CAN Bus verschickt werden werden in ErrorBufferUnlock bzw ErrorBufferLock gepuffert Die Countdown Uhr f r den Timeout wird in UnlockTimer bzw Lock Timer ausgelagert Die Ansteuerung der Motoren befindet sich in Unlock Back UnlockFront bzw LockBack LockFront Die Synchronisation mit dem Nachbart
136. tor Jede Paarkombination von zwei Eingabe kan len wird hier einmal als Gruppe betrachtet Connected Input Generator Die Eingangskan le von Komponen ten die mit dem lt lt connected gt gt Attribut gekennzeichnet sind werden jeweils zu einer Gruppe zusammengefasst All Input Generator Hiermit werden alle m glichen Eingabewerte kombinationen getestet Configurable Input Generator Mit Hilfe des Group Configuration Formats GCF kann man die Testdaten individuell spezifizieren Der TIG erzeugt daraus die TDF Datei Mit Hilfe des Codegenerators der Firma Validas Val l sst sich aus dem zu testenden AutoFOCUS Modell C Code erzeugen Das daraus erstellte Programm kann mit den TIG Testdaten ausgef hrt werden Ausgabe und Eingabe zusammen bilden dann Testf lle Bei der modellbasierten Entwicklung k nnen diese Testf lle dann auf Verfeinerungen bzw Implementierungen des AutoFocus Modells ange 93 wandt werden Dazu m ssen die Testf lle vorher an das neue Modell angepasst bzw konkretisiert werden Bild 8 6 stellt diesen Vorgang des modellbasierten Testens dar l aa Konkretisieren Abbildung 8 6 Modellbasiertes Testen mit AutoFocus Bei Back to Back Tests werden die Ausgaben miteinander verglichen um bei Abweichungen Fehler feststellen zu k nnen Voraussetzung f r einen effizienten Ablauf ist ein automatisierter Ansatz Liegt als Testobjekt ein transformationelles System vgl Abschnitt 4 2 v
137. treffenden Komponente handleLock oder handleUnlock an den TSG Ausgang weiter Fensterheber Das Modul Windows_Module ist f r den Fensterheber zust ndig NER EES ANKER oz CAN_X_Dut_WIN_RL_CL CNN nl DEER CAN X Out WINOROP CAN v Io Loch tartieee CAN X Out WIN XR_CL FrontMotor CAN Front idem In 3 EWEG Zort OC BLOW_WIN x Motor_In X UI Montee Request_Front a beten AE maer Out BROR N Request_Front_In_WIN_YR_OP Request Front S i Request Front In WIN_YL_CL main ET bett ben bi ere homme motorin Commana Amber Out X MOTOR Request Front In PHBR Request Front In FHB ML Regest penk In Lockstatclose CAN X_n HBX CES Cut WIN XL_OP sine ie CNX ENEE cannu on BEEN CAN X In LodSincese ank out wine a BackMotor CAN Back Mer In KBENES vue Erem XMotor IN XLNTEN ie Request Ban WIN HLCP Wee XMotor_In 3 DEEN 8 too Dt ERROR WIN Request Sech J P cL Request Back ep In Battery Request Ze Ain CL Raguest Back_In_ FHB HL D BackMater_In_Command XMotor In Command XMotor Cut MOTO Request Back_In_FHB_HR Request Sech Du FTHEHL Request Sech Doft EI Request Back Deet ech Jr LockStariuss Abbildung 7 2 Windows Module in ASCET CAN Front bzw CAN Back Die Implementierungen von CAN_Front und CAN Bock sind identisch 12 Beide registrieren eingehende Anweisungen des Fahrers zur Bewegung der Fenster auf der gegen berliegenden Fahrzeugseite und leiten diese ber
138. uf Rapid Prototyping der Rapid Prototyping Testen mit CTE und Instrumentierung Hardware Abbildung 7 5 Testen mit ASCET Im Falle des Testens wird der Code zus tzlich mit Hilfstools expandiert instrumentiert und kompiliert Abh ngig vom ASCET Werkzeug werden unterschiedliche Compiler ein gesetzt ASCET MD F r die Simulation und das Testen auf dem PC wird der Borland C Compiler verwendet ASCET RP F r die Ausf hrung des Codes auf der Rapid Prototyping Hardware wird der Code f r den PowerPC cross kompiliert ASCET SE F r die Seriencodegenerierung stehen je nach Zielplatt form u a Infineon C16x und TriCore Motorola MPC5xx und 8 attolcc1 setzt C Code voraus in dem Makros expandiert und include Dateien eingebunden sind 79 M68HC12 TI TMS470 NEC V85x Hitachi SH7055F unterschied liche Compiler zur Verf gung Im Rahmen des Testens wird die Simulationsumgebung Messeinstel lungen Mappen der Testdaten auf die Moduleing nge je Komponente einmal aufgesetzt und kann dann f r weitere Testf lle wiederverwendet werden Die Ausf hrung der Simulation geschieht auf Knopfdruck ohne weiteren Eingriff des Benutzers Auf Grund der frei einstellbaren Zeitska lierung k nnen die Simulationsberechnungen in kurzer Zeit durchgef hrt werden Die dabei entstehenden Ausgabedaten werden aufgezeichnet und k nnen somit im Nachhinein analysiert werden bzw stehen f r Regressions und Back to Back Tests zur Verf gung
139. von Komponenten modelliert ber Kan le sind diese miteinander ver bunden und tauschen dar ber Nachrichten aus In AutoFocus findet sich ein Teil dieser Konzepte in Form von graphi schen Beschreibungsmitteln wieder BHS99 Dem gesamten System in AutoFocus liegt ein globaler periodischer Systemtakt zu Grunde Je Sy stemtick f hren alle Komponenten gleichzeitig jeweils einen Berechnungs schritt aus Nachrichten k nnen somit bei jedem Systemtick empfangen und gesendet werden Zur Modellierung eines Systems bietet AutoFOCUS mehrere Diagram marten an Folgende Abschnitte gehen darauf ein 58 6 3 1 System Structure Diagram SSD Ein Systemstrukturdiagramm SSD beschreibt den inneren Aufbau ei ner Komponente Diese kann aus mehreren Unterkomponenten bestehen die im SSD in Form von Bl cken dargestellt werden Nachrichten k nnen ber Kan le zwischen den einzelnen Komponenten ausgetauscht werden Dazu dienen Verbindungslinien zwischen den einzelnen Bl cken die ber Ports angebunden werden Unterkomponenten k nnen wiederum rekur siv in weitere Unterkomponenten zerlegt werden F r jede hierarchisch untergliederte Komponente existiert ein eigenes SSD Port zur n chsth heren Nachrichtenkanal Hierarchieebene Komponente Stoergrdesseilnt Stellgroesse int Regelgroesse nt ERBE Regeifehler int nn Fuehrungsgroesseilnt u gt Int lt Rueckfuehrgroesse h p Abbildung 6 6 Beispiel f r ein SSD 6 3 2
140. wonnen wurden zu erg nzen Folgende Varianten von White Box Testverfahren unterscheiden sich in der Definition ihrer Uberdeckungskriterien als Mass f r die Abdeckung 27 1 int power int base int n Dt 3 inti p 4 p l 5 for i 1 i lt n i 6 p base 7 return p 8 Abbildung 3 2 Beispiel f r einen Kontrollflussgraphen durch Testf lle Anweisungs berdeckungstests Bei diesem Testverfahren wird als berdeckungskriterium folgendes Mass definiert i _ Anzahl durchlaufener Anweisungen Co Uberdeckung zu Gesamtzahl der Anweisungen 100 F r die 100 ige Abdeckung eine Programms gem ss dem eben definier ten Mass m ssen alle Anweisungen des Programms mindestens einmal ausgef hrt werden Zweig berdeckungstests An Verzweigungsstellen in einem Programm teilt sich der Kontrollfluss in mehrere Zweige auf Hier versucht man alle Alternativen an den Ver zweigungsstellen durch Testf lle abzudecken _ Anzahl durchlaufener Zweige C1 Uberdeckung m Gesamtzahl der Zweige 100 Bei einer 100 igen Testabdeckung wird jeder Zweig an jeder Verzwei gungsstelle mindestens einmal durchlaufen Pfad berdeckungstests Bei der Ausf hrung eines Testfalles wird ein gesamter Pfad durch den Kontrollflussgraphen verfolgt Das Uberdeckungskriterium wird hier 28 demzufolge definiert als S _ Anzahl durchlaufener Pfade Co berdeckung g Gesamtzahl der Pfade 100 F r
141. x Tests mit berdeckungsgradanalyse Die dabei gewonnenen Erkenntnisse werden gegen bergestellt um Aussagen ber den zuk nftigen Einsatz der jewei ligen Verfahren treffen zu k nnen Die Ergebnisse lassen sich auch auf die Qualit tssicherung von Software f r technische Systeme abseits der Automobilindustrie bertragen Inhaltsverzeichnis Inhaltsverzeichnis 1 Einleitung 1 1 Aufgabenstellung 43 A 2 LA Bin en 1 2 Struktur der Diplomarbeit 1 242 2 2244 Zr ba Aspekte der Software Entwicklung 2 1 Grundlegende Begriffe 2 2 Modellbasierte Entwicklung 2 2 2 2 2 3 Software Entwicklung im Bereich Automotive Konventionelle Qualit tssicherungsverfahren 3 1 Qualit tssicherungsrichtlinien und standards im Unter Ee EE EES 3 2 Industriell eingesetzte Software Testverfahren 3 2 1 Allgemeine Aspekte des Software Testens 3 2 2 Testverfahren in der Softwareentwicklung 3 2 3 Testverfahren im Bereich Automotive Qualit tssicherungsverfahren akademischen Ursprungs 4 1 Verifikationsmethoden Aere NR a 3a 2 a ra 4 2 Modelchecking 4 Aaf ue 82 alas a aa ala 4 2 1 Modellierungssprache 2 2 22 2 2020 4 2 2 Spezifikationsprache 22 2 2 4 2 3 Verifikationsalgorithmus 2 22 2220 Fallbeispiel T rsteuerger t 5 1 Einsatz des T rsteuerger tes im Automobil 5 1 1 Funktionen des T rsteuerger tes 11 11 14 16 22
142. zeichnet ist Der st ndig wachsende Anteil die kurzen Entwick lungszyklen und die steigende Komplexit t von Software im Automobil stellen hohe Herausforderungen an die Automobilhersteller dar Diese Umst nde werden durch den hohen Kostendruck und die zur Verf gung stehenden beschr nkten Rechnerressourcen nicht gemildert Fehler in der Software sicherheitskritischer Anwendungen k nnen zu Funktionsausf llen und somit zu hohen Kosten f hren Durch den inten siven Einsatz von Qualit tssicherungsmassnahmen versucht man dieses Risiko zu minimieren um ein h heres Mass an Zuverl ssigkeit Sicherheit und Qualit t zu gew hrleisten Moderne Entwicklungsverfahren wie die Modellierung mit grafischen Be schreibungsmitteln und die automatische Codegenerierung sollen eben falls zu dem gew nschten Ergebnis beitragen 1 1 Aufgabenstellung Ziel ist die Anwendung und der Vergleich von konventionellen Software Qualit tssicherungsverfahren mit Modelchecking Andere Verifikations verfahren akademischen Ursprungs werden im Rahmen dieser Diplomar beit nicht n her betrachtet Der Vergleich erfolgt im Kontext der Au tomobilindustrie Als Fallstudie dient eine textuell verfasste ffentlich zug ngliche Spezifikation eines T rsteuerger tes PH02 Die darin beschriebenen Komponenten f r das T rschloss die Fensterheberan steuerung und die Lichtansteuerung sollen mit Hilfe der beiden CASE Werkezeuge ASCET und AutoFocus in Modelle umgesetzt w
143. zustand wie der bisherige Befehl zum Ziel hat handleLock und handleUnlock w rden gleichzeitig die Motoren in verschiedene Richtungen drehen lassen Dieser Konflikt wird aufgel st indem das Entriegeln Vorrang vor dem Verriegeln erh lt Als Vorkeh rungsmassnahme zur Konfliktaufl sung wird handleLock f r die Zeit des Entriegelns blockiert und kann dabei keine Aktionen ausf hren Beim Eintreffen eines ffnen Befehls in handleUnlock wird handleLock dar ber in Kenntnis gesetzt handleLock wird durch einen hierarchischen Automaten mit zwei Oberzust nden implementiert Die Logik f r die normale Ausf hrung befindet sich in einem dieser beiden Zust nde Das Blockieren durch handleUnlock veranlasst den Wechsel in den anderen Zustand Der Kontrolllluss kehrt erst nach Beendigung der Entriegelungsaktion in handleUnlock wieder in den ersten Oberzustand und darin in den urspr nglichen Startzustand zur ck Ein in der Mitte abgebrochener Verriegelungsvorgang wird nicht mehr nachgeholt und muss neu angestossen werden Mit dieser Vorgehensweise werden inkonsistente T rzust nde auf bei 71 den Fahrzeugseiten auf Grund von Synchronisationsproblemen vermie den Sobald die T ren auf einer Seite ge ffnet werden erh lt das ge gen berliegende TSG ber den CAN Bus ebenfalls die Anweisung zum ffnen MultiplexSignals Abh ngig von der aktuell ausgef hrten Aktion Verriegeln oder Entrie geln leitet MultiplexSignals nur Signale der be

Vergleich zwischen konventionellen und formalen

Contents

Download Pdf Manuals

Related Search

Related Contents