Seminar: Techniques for the Verification of Probabilistic or Timed Automata - Sommersemester 2011

Übersicht

Beschreibung

Kommentar

Integration of electronic devices is a practice that is turning more and more common in the design of every-day's devices (e.g. smartphones, consoles, dishwashers...) and, on the other hand, of safety-critical systems. If in the former case errors in the design usually can lead to ``just'' a loss of money, in the second one we can imagine much worse scenarios. Examples range from failures in the communication protocol between a train and the
railway infrastructure, which must be able to exchange messages no matter how fast they run, to the fuel injection controller of a car, that should never ``freeze''.

These concepts are pretty clear when we deal with closed systems. We may be asked to verify that a task is executed within a specified amount of time. However, in most cases (trains included) we have to
take into account also external events, which are not predictable and may affect the reliability of communication channels. Here the question turns into finding how large is the probability that the system is anyway able to perform its task.

These systems can be verified using model checking techniques, which aim to certify that a design fulfils its specifications. This subject is exploited in this seminar, seen from the point of
view of the modelling and the application of model checking techniques, and from that of core techniques for speeding-up and improving its efficiency.