Formal Engineering of Digital and Hybrid Systems

Formal Engineering of Digital and Hybrid Systems

Audience

This advanced course addresses Bachelor and Master students in Computer Science, Bioinformatics, CuK or Computerlinguistics. Background in the module Verification are of advantage but not mandatory.

Topic

The main topic of this lecture is to show how verification techniques can be applied to real-world systems. The main challenge is hereby to cope with the state space explosion problem: The size of the state space typically grows exponentially in the number of components. For instance, a circuit with 64 flipflops can contain up to 2⁶⁴ =18446744073709551616 states. If all these states have to be traversed only once during verification and visiting a single state takes 1 ns, the traversal still needs more than 500 years! This severely limits all algorithms relying on an explicit state space representation (i.e. a representation which lists all states and transitions of the system) to rather small state spaces.

Symbolic methods, in contrast, represent states and transitions as solutions of formulas or as paths in a directed graph. This has the advantage that the size of the representation can be smaller by orders of magnitude than the represented state space. However, this requires dedicated algorithms which can directly work on such symbolic representations and whose running time only depends on the size of the representation and not on the size of the represented state space.

In this lecture, we will look into different symbolic data structures and algorithms like ordered binary decision diagrams, (linear) and-inverter graphs, SAT and QBF formulas, difference bound matrices, ... and show how they can be used to verify not only digital circuits, but also timed automata and linear hybrid systems.

Credits: 

6 ECTS points (3 hours of lecture, 1 hour of tutorials, and some exercises every week).

Time and location:

Tuesday 14-16 and Thursday 10-12 in the seminar room 015 in building E1 3