Formal Aspects of Software Engineering

• establish a formal specification from an informal problem description
• use distinguished specification styles and techniques to achieve models at an appropriation level of abstract
• stepwise refine a specification
• establish verification obligations (e.g. refinement conditions and required system properties)
• verify simple verification obligations
• translate a specification into an executable program
• apply selected tools relating to formal methods
• explain what can be achieved by using formal methods
• communicate results in a clear and precise manner
• solve problems as a group while keeping individual responsibility

Formal specification using one or more typical examples of specification languages. Various specification techniques and styles for constructing models at different levels of abstraction. Stepwise development and verification by means of a series of models of decreasing level of abstraction. Implementation relation(s). Application of computer based specification tools.

01017/01019/01904/02100/02101/02157/02141/02156/02158, i.e. (1) mastering discrete mathematics: sets, functions, logical expressions in predicate logic, (2) mastering imperative programming (e.g. in Java) and functional programming (e.g. in F#), and (4) knowledge about software modelling.

Lectures, exercises and project work.