Beschreibung, z.B. akutellen Link einfügen

+++ The first tutorial is on Monday, April 1, at 12:00 in ITCS 2021. The first lecture is on Wednesday, April 3, at 10:00 in Seminarraum Informatik 5 (Von Neumann) +++

Overview

Software developers spend between 50% and 70% of the time testing and validating code. Testing code can be defined as the examination of a subset of the behaviours of the program or the system under test. The testing part of this course covers the different techniques and approaches to test software.

The main focus lies on computer-assisted unit testing. This field can be roughly separated into black-box testing where you do not have access to the code and white-box testing where test cases can be designed or generated from the code.

Runtime verification is the discipline of computer science that deals with the study, development, and application of those verification techniques that allow checking whether a run of a system under scrutiny (SUS) satisfies or violates a given correctness property. It is being pursued as a lightweight verification technique complementing verification techniques such as model checking and testing and establishes another trade-off point between these forces.

This course treats how white-box testing and especially automated test case generation and runtime verification can be combined to a powerful verification method.

As considered the heart of runtime verification, the main focus of the RV part of the course lies on synthesis procedures yielding monitors from high-level specifications. We outline several monitor synthesis procedures for Linear-time Temporal Logic (LTL). In general, two main approaches can be found for synthesizing monitoring code: Monitors may either be given in terms of an automaton, which is precomputed from a given correctness specification. Alternatively, the correctness specification may be taken directly and rewritten in a tableau-like fashion when monitoring the SUS. We give examples for both approaches.

Topics Covered

  • Definitions of Testen, Verification and Validation
  • Static testing vs. Dynamic Testing
  • Manual vs. Automated Testing
  • Black box vs. White box Testing
  • Coverage Criteria
  • Test case generation
  • Temporal logic and multi-valued semantics
  • Finite (ω-)automata
  • Monitor synthesis
    • Automata constructions and -analysis
    • Formula rewriting
  • Runtime monitoring, monitor integration
  • RV frameworks
  • Conformance Testing


Vorlesung mit Übungen (2V + 2Ü), 6 ECTS


Master Informatik, Basismodul Theoretische Informatik
Master Informatik, Anwendungsfach IT-Sicherheit und Zuverlässigkeit, Wahlpflicht
Master Entrepreneurship in digitalen Technologien, fachspezifisches Wahlmodul
Master Medizinische Informatik, Basismodul Informatik Wahlpflicht
Master Medieninformatik, Wahlpflicht Informatik



Der Vorbesprechungstermin findet am 2.11. um 16:00 Uhr im ISP Besprechungsraum (Haus 64, OG 1, Raum 108) statt.

In dieser Veranstaltung soll eine SmartHome Lösung erarbeitet werden.

Das Praktikum bezieht sich auf die gesamte Kette eines solchen Systems.
D.h. ausgehend von einzelnen Schaltern, etwas komplexeren Sensoren, und Basis-Hardware, die entsprechende Low-Level-Signale verarbeitet, hin zu Systemen, die die Steuerung per Smartphone des entsprechenden intelligenten Hauses erlauben.

Dabei geht es weniger um die konkrete Entwicklung von Software, sondern mehr um die Kombination existierender Softwaresysteme, was einem großen Bereich des Software-Engineerings in der Praxis entspricht.

Dazu ist eine umfangreiche Analyse und Bewertung existierender Softwaresysteme notwendig.
Um proprietäre Hardware einbinden zu können ist auch die Verwendung von FPGAs oder Mikrocontroler mit zu beachten.

Sicherlich wird es auch erforderlich sein, einige Software entsprechend selber zu entwickeln, insbesondere um low-level Funktionen alter Hardware zu steuern.
Low-Level-Signale sollen dann von einem RaspberryPi koordiniert werden, der entsprechend dann leichter von einem Smartphone gesteuert werden kann.


Dieses Bachelor Projekt ist mit reduziertem Umfang für die allgemeinte Informatik, und mit erhöhtem Aufwand für SSE-Studierende konzipiert (Module CS3701-KP05 und CS3060-KP04).