Model-based Verification - Fundamentals and Industrial Practice

Lec­tur­ers	Thomas Kropf Jürgen Ruf
In­struc­tors	Jürgen Ruf Se­bas­t­ian Burg AlumniSe­bas­t­ian Burg Hanno Eichel­berger Ste­fan Hus­ter Jo Laufen­berg Re­searcherJo Laufen­berg
Tu­to­r­ial	15.04.2014, 17:00 Uhr, A104
Amount	2 SWS / 4 LP
Entry in course cat­a­log	Cam­pus

Beschrei­bung

Re­li­a­bil­ity, se­cu­rity, ac­cu­racy, and ro­bust­ness of soft­ware be­come more and more im­por­tant. Mis­takes in sys­tem de­vel­op­ment are made, in­clud­ing crit­i­cal ones, due to men­tal-logic er­rors in the spec­i­fi­ca­tion and/or dur­ing im­ple­men­ta­tion of the soft­ware it­self. Thereby, com­pil­ers and used pro­gram­ming lan­guages play an im­por­tant role. To avoid er­rors, the used pro­gram­ming lan­guages are often lim­ited to spe­cific lan­guage con­structs. This is done to avoid dy­namic mal­func­tion (mem­ory over­flows, mem­ory leaks etc.). An­other rea­son for that is to sim­plify the analy­sis and ver­i­fi­ca­tion process of these soft­ware com­po­nents. The ver­i­fi­ca­tion tech­niques range from sta­tic code analy­sis of pro­grams and their spec­i­fi­ca­tions to com­bi­na­tions of au­to­mated proof sys­tems and model-check­ers. Be­sides error pre­ven­tion and fault de­tec­tion, error tol­er­ance (e.g. due to re­dun­dancy) in soft­ware is an in­ter­est­ing ap­proach to in­crease re­li­a­bil­ity of safety crit­i­cal sys­tems. To do so, tech­niques such as test­ing, run­time ver­i­fi­ca­tion, pro­gram ob­ser­va­tion, mon­i­tor­ing, and con­sis­tency check­ing come into ac­tion. An­other as­pect is qual­ity as­sur­ance of soft­ware. An ex­am­ple would be the cer­ti­fi­ca­tion of safety-re­lated sys­tems that re­lies on the com­pli­ance of soft­ware and its spec­i­fied prop­er­ties re­gard­ing safety stan­dards like ISO 26262 and IEC 61508. In this con­text, li­braries, tools, com­pil­ers, sys­tem com­po­nents and third-party soft­ware play an im­por­tant role. The aim of this sem­i­nar is to pro­vide an in­sight into the the­ory of soft­ware ver­i­fi­ca­tion and the cor­re­spond­ing re­search top­ics and tools. A sec­ond goal is to in­ves­ti­gate on meth­ods that are cur­rently used in in­dus­trial soft­ware de­vel­op­ment units. The lec­tur­ers have rel­e­vant ex­pe­ri­ence in the de­sign and ver­i­fi­ca­tion of sys­tems in in­dus­trial en­vi­ron­ments.

The­men

Unter an­derem: Soft­ware Ver­i­fi­ca­tion in in­ter­na­tionalen Teams: Soft­ware­pro­jekte wer­den immer größer und auch die Ver­i­fika­tion dieser Soft­ware wird immer wichtiger um Schaden zu ver­mei­den und die Rep­u­ta­tion einer Firma zu er­hal­ten. Ins­beson­dere in großen Fir­men wer­den die Auf­gaben des Soft­ware-tests auf große, örtlich verteilte Teams aufgeteilt oder als ganzes an ein ex­ternes Team aus­ge­lagert. In diesem Kon­text wer­den Kom­mu­nika­tion und kul­turelle Kom­pe­ten­zen immer wichtiger. De­shalb sollen in diesem Sem­i­nar­beitrag die Schwierigkeiten von in­ter­na­tional agieren­den Teams un­ter­sucht wer­den und da­raus bes­timmte Ver­hal­tensweisen abgeleitet wer­den um die Kom­mu­nika­tion zu op­ti­mieren und in­terku­turelle Prob­leme möglichst frühzeitig zu erken­nen und wenn möglich zu ver­mei­den. Ex­em­plar­isch sollen die Prob­leme und Lösungsvorschläge an­hand einer frem­den Kul­tur aufgezeigt wer­den (z.B. In­dien, Japan, China, …)

• Tu­to­r­ial for As­pectJ As­pect-ori­ented pro­gram­ming (AOP) can re­place the event-han­dling in ob­ject-ori­ented lan­guages. It can watch events when ob­ject meth­ods are called or vari­able val­ues change. The AOP con­cepts can be used for the mon­i­tor­ing of the soft­ware as well, es­pe­cially in the area of Run­time Ver­i­fi­ca­tion. A pop­u­lar as­pect-ori­ented lan­guage is As­pectJ. This topic re­quires the pre­sen­ta­tion of basic con­cepts of As­pectJ and the ap­pli­ca­tion of As­pectJ to some small soft­ware ex­am­ples. The pre­sen­ta­tion can in­clude a live demon­stra­tion of the frame­work.
• Sur­vey about Re­play De­bug­ging Re­play De­bug­ging is an ap­proach which records the ex­e­cu­tion of a soft­ware dur­ing op­er­a­tion until a fail­ure oc­curs and re­plays the ex­e­cu­tion in order to debug the fail­ure in the lab­o­ra­tory. The state-of-the-art in this area in­cludes dif­fer­ent con­cepts, e.g. in­struc­tion-based record­ing, hard­ware-based record­ing or event cap­tur­ing. For this topic sev­eral up-to-date pa­pers in the area of re­play de­bug­ging should be ex­am­ined and their con­cepts should be pre­sented. The pre­sen­ta­tion can in­clude a com­par­i­son be­tween some of the cur­rent ap­proaches.
• Fuzz Test­ing Fuzz test­ing, or fuzzing is one method for soft­ware test, in which an at­tempt is made to trig­ger a fault due feed­ing the sut with in­valid or semi­valid input. Based on a paper about cov­er­age cri­te­ria for fuzz test­ing, an overview about fuzzing meth­ods and the tenor from that paper should be pre­sented.
• Sur­vey about ver­i­fi­ca­tion meth­ods A sur­vey about ex­ist­ing meth­ods for model-based soft­ware ver­i­fi­ca­tion, their lim­i­ta­tions, ideas, ap­pli­ca­tion areas, ben­e­fits and dis­ad­van­tages is the task of this pre­sen­ta­tion.
• The Frac­tal Di­men­sion of SAT For­mu­las Struc­tures of in­dus­trial SAT For­mu­las.
• Thread-Based Multi-En­gine Model Check­ing for Mul­ti­core Plat­forms Model Check­ing in Mul­ti­core Plat­forms.

Be­merkung

Vorbe­sprechung

15.4., um 17Uhr, A104 Folien aus der Vorbe­sprechung

Vor­trag­ster­min

24.7., um 15 Uhr in B226

An­melde­modalitäten

Down­load In­foblatt An­melde­modalitäten

Randbe­din­gun­gen fürs Sem­i­nar

Von den Teil­nehmerin­nen und Teil­nehm­n­ern wird eine weit­ge­hend selb­stständige Er­ar­beitung des jew­eili­gen The­menge­bi­ets incl. Lit­er­aturbeschaf­fung und -recherche er­wartet. Lit­er­aturhin­weise wer­den natürlich gegeben, eine be­darf­s­ges­teuerte Be­treu­ung ist sichergestellt.

Vor­trags­dauer und The­me­nauf­bau

Der Vor­trag soll einen Dauer von 25 Minuten haben und fol­gen­den Auf­bau be­sitzen:

• Ein­leitung mit Mo­ti­va­tion (ca. 5 Minuten im Vor­trag)
• The­o­rie zum jew­eili­gen Thema (ca. 10-15 Minuten im Vor­trag)
• Prak­tis­che An­wen­dung / Fall­beispiele (restliche Zeit, mind. 5. Minuten)
• Zusam­men­fas­sung (2 Minuten im Vor­trag)
• Vor­trag muss in en­glis­cher Sprache gehal­ten wer­den

Be­din­gun­gen für den Sem­i­narschein / Beno­tung

Um den Schein zu er­hal­ten muss

• eine Vor­trags­gliederung 4 Wochen vor dem Vor­trag­ster­min mit dem Be­treuer durchge­sprochen sein
• eine erste Vor­tragsver­sion 2 Wochen vor dem Vor­trag­ster­min mit dem Be­treuer durchge­sprochen sein (vorzugsweise Pow­er­Point oder PDF)
• ein Vor­trag (25 Minuten + Diskus­sion) in en­glis­cher Sprache gehal­ten wer­den
• eine schriftliche Ausar­beitung in en­glis­cher Sprache abgegeben wer­den (6-8 Seiten in Post­Script- oder PDF-For­mat)
• bei allen Sem­i­narter­mi­nen an­we­send sein Die Sem­i­narleis­tung wird nach fol­gen­den Kri­te­rien benotet:* Ein­hal­tung der Ter­mine
• Qualität der durchgeführten Lit­er­atur­recherche
• In­haltliche Qualität des Vor­trags
• Qualität der Präes­nta­tion incl. Zeit­ein­hal­tung
• Qualität der Ausar­beitung
• Grad der Seb­stständigkeit (davon unberührt sind natürlich Diskus­sio­nen mit dem Be­treuer über Auswahl der zu präsen­tieren­den The­men, Eig­nung zur Präsen­ta­tion etc. - solche Diskus­sio­nen sind sogar ex­plizit erwünscht)