Specification Engineering
Modern programs and software-intensive systems are increasingly finding their way into everyday life. Be it the car control or the train safety system, the control of the home automation or the financial program. A failure or the malfunction of such programs usually tries high costs and can lead to damage to life and limb. Therefore, such critical systems have to be specified particularly precisely and the error-free implementation has to be verified resiliently.
In the lecture Specification Engineering, basic mathematical methods and applications for the specification of software and software-intensive systems are introduced. In addition, modern verification algorithms and tools are introduced, which can also be used to verify compliance with the specifications.
In addition, leading tools from the field of formal verification are introduced and practically tested in the exercises.
Details
Learning Objectives
- Familiarity with methods of formal specification
- Ability to assess for which software artifacts the use of formal specification makes sense
- Knowledge of potentials and limitations of formal methods
Lecture Contents
- Formal versus informal specification
- Specification, validation, verification, generation
- Specification of abstract data types
- Specification of temporal sequences and processes, application example: protocol specification
- Concrete specification languages and tools
- Motivation and basic concepts
- Specification of abstract data types
- Dynamic and temporal logic