Model-based Verification - Fundamentals and Industrial Practice

Dozenten	Thomas Kropf Jürgen Ruf
Übungsleitung	Jürgen Ruf Sebastian Burg AlumniSebastian Burg Hanno Eichelberger Stefan Huster Jo Laufenberg ResearcherJo Laufenberg
Übungsgruppe	15.04.2014, 17:00 Uhr, A104
Umfang	2 SWS / 4 LP
Eintrag im Kurskatalog	Campus

Beschreibung

Reliability, security, accuracy, and robustness of software become more and more important. Mistakes in system development are made, including critical ones, due to mental-logic errors in the specification and/or during implementation of the software itself. Thereby, compilers and used programming languages play an important role. To avoid errors, the used programming languages are often limited to specific language constructs. This is done to avoid dynamic malfunction (memory overflows, memory leaks etc.). Another reason for that is to simplify the analysis and verification process of these software components. The verification techniques range from static code analysis of programs and their specifications to combinations of automated proof systems and model-checkers. Besides error prevention and fault detection, error tolerance (e.g. due to redundancy) in software is an interesting approach to increase reliability of safety critical systems. To do so, techniques such as testing, runtime verification, program observation, monitoring, and consistency checking come into action. Another aspect is quality assurance of software. An example would be the certification of safety-related systems that relies on the compliance of software and its specified properties regarding safety standards like ISO 26262 and IEC 61508. In this context, libraries, tools, compilers, system components and third-party software play an important role. The aim of this seminar is to provide an insight into the theory of software verification and the corresponding research topics and tools. A second goal is to investigate on methods that are currently used in industrial software development units. The lecturers have relevant experience in the design and verification of systems in industrial environments.

Themen

Unter anderem: Software Verification in internationalen Teams: Softwareprojekte werden immer größer und auch die Verifikation dieser Software wird immer wichtiger um Schaden zu vermeiden und die Reputation einer Firma zu erhalten. Insbesondere in großen Firmen werden die Aufgaben des Software-tests auf große, örtlich verteilte Teams aufgeteilt oder als ganzes an ein externes Team ausgelagert. In diesem Kontext werden Kommunikation und kulturelle Kompetenzen immer wichtiger. Deshalb sollen in diesem Seminarbeitrag die Schwierigkeiten von international agierenden Teams untersucht werden und daraus bestimmte Verhaltensweisen abgeleitet werden um die Kommunikation zu optimieren und interkuturelle Probleme möglichst frühzeitig zu erkennen und wenn möglich zu vermeiden. Exemplarisch sollen die Probleme und Lösungsvorschläge anhand einer fremden Kultur aufgezeigt werden (z.B. Indien, Japan, China, …)

• Tutorial for AspectJ Aspect-oriented programming (AOP) can replace the event-handling in object-oriented languages. It can watch events when object methods are called or variable values change. The AOP concepts can be used for the monitoring of the software as well, especially in the area of Runtime Verification. A popular aspect-oriented language is AspectJ. This topic requires the presentation of basic concepts of AspectJ and the application of AspectJ to some small software examples. The presentation can include a live demonstration of the framework.
• Survey about Replay Debugging Replay Debugging is an approach which records the execution of a software during operation until a failure occurs and replays the execution in order to debug the failure in the laboratory. The state-of-the-art in this area includes different concepts, e.g. instruction-based recording, hardware-based recording or event capturing. For this topic several up-to-date papers in the area of replay debugging should be examined and their concepts should be presented. The presentation can include a comparison between some of the current approaches.
• Fuzz Testing Fuzz testing, or fuzzing is one method for software test, in which an attempt is made to trigger a fault due feeding the sut with invalid or semivalid input. Based on a paper about coverage criteria for fuzz testing, an overview about fuzzing methods and the tenor from that paper should be presented.
• Survey about verification methods A survey about existing methods for model-based software verification, their limitations, ideas, application areas, benefits and disadvantages is the task of this presentation.
• The Fractal Dimension of SAT Formulas Structures of industrial SAT Formulas.
• Thread-Based Multi-Engine Model Checking for Multicore Platforms Model Checking in Multicore Platforms.

Bemerkung

Vorbesprechung

15.4., um 17Uhr, A104 Folien aus der Vorbesprechung

Vortragstermin

24.7., um 15 Uhr in B226

Anmeldemodalitäten

Download Infoblatt Anmeldemodalitäten

Randbedingungen fürs Seminar

Von den Teilnehmerinnen und Teilnehmnern wird eine weitgehend selbstständige Erarbeitung des jeweiligen Themengebiets incl. Literaturbeschaffung und -recherche erwartet. Literaturhinweise werden natürlich gegeben, eine bedarfsgesteuerte Betreuung ist sichergestellt.

Vortragsdauer und Themenaufbau

Der Vortrag soll einen Dauer von 25 Minuten haben und folgenden Aufbau besitzen:

• Einleitung mit Motivation (ca. 5 Minuten im Vortrag)
• Theorie zum jeweiligen Thema (ca. 10-15 Minuten im Vortrag)
• Praktische Anwendung / Fallbeispiele (restliche Zeit, mind. 5. Minuten)
• Zusammenfassung (2 Minuten im Vortrag)
• Vortrag muss in englischer Sprache gehalten werden

Bedingungen für den Seminarschein / Benotung

Um den Schein zu erhalten muss

• eine Vortragsgliederung 4 Wochen vor dem Vortragstermin mit dem Betreuer durchgesprochen sein
• eine erste Vortragsversion 2 Wochen vor dem Vortragstermin mit dem Betreuer durchgesprochen sein (vorzugsweise PowerPoint oder PDF)
• ein Vortrag (25 Minuten + Diskussion) in englischer Sprache gehalten werden
• eine schriftliche Ausarbeitung in englischer Sprache abgegeben werden (6-8 Seiten in PostScript- oder PDF-Format)
• bei allen Seminarterminen anwesend sein Die Seminarleistung wird nach folgenden Kriterien benotet:* Einhaltung der Termine
• Qualität der durchgeführten Literaturrecherche
• Inhaltliche Qualität des Vortrags
• Qualität der Präesntation incl. Zeiteinhaltung
• Qualität der Ausarbeitung
• Grad der Sebstständigkeit (davon unberührt sind natürlich Diskussionen mit dem Betreuer über Auswahl der zu präsentierenden Themen, Eignung zur Präsentation etc. - solche Diskussionen sind sogar explizit erwünscht)