Algebraic System Derivation

Formal methods serve to construct hardware and software systems which provably satisfy the specified requirements. For this, there exist two essential approaches:

• transforming a (frequently non-executable) formal specification by semantics-preserving rules into a (by construction) correct implementation (transformational approach);
• Straight formulation of an implementation with subsequent proof of its correctness with respect to the specification (verification approach).

Both of these approaches, in particular the transformational one, can for realistic systems be carried out fully formally only if algebraic techniques are employed at a large scale; then many small steps in pure logic can be compacted into large steps of (in)equational reasoning. The task is to find suitable algebraic structures and modelling tools.