Aims and Scope

Embedded systems engage into an ongoing, hardly foreseeable, interaction with their asynchronously evolving environment. This fact contributes to the intrinsic complexity of their design and validation. To alleviate this problem, a variety of closed-form models for various aspects -e.g., reaction time, resource usage, possible system dynamics- of embedded systems have been proposed. Within their range of applicability, such models permit the derivation of reliable certificates which are true of all possible interaction sequences of the embedded system with its environment - a degree of coverage that cannot be achieved with testing and related methods. In the lectures, we will introduce a comprehensive set of state-based models as well as automatic procedures for their analysis. The exercise classes will complement this by providing hands-on experience with appropriate verification tools. Furthermore, there will be an opportunity for building such a keypress verification tool yourself within a guided process.

Réalisation Axome - Création de sites Internet