Completed on 23.10.14 by Andreas Wrasmann.

Synchronisation concepts for application programs, model checking, SAT

The modules " Operating Systems 1 " and " Operating Systems 2 " deal with synchronisation problems that are to be solved using various synchronisation concepts (semaphores, monitors, rendezvous concept, messages). Proving that such a synchronisation problem has been solved correctly is usually very difficult and requires a mathematical proof. Proving that a solution is incorrect, on the other hand, is usually easier, as the construction of a single counterexample is sufficient. Nonetheless, this is sometimes very time-consuming and tedious, especially in tutorials, as a large number of different potential solutions are generated and the tutors first have to familiarise themselves with each attempted solution. Experience in recent years has shown that (unfortunately) most attempted solutions are incorrect and that it is often possible to construct a sequence in which the synchronisation problem is not solved correctly.

The aim is to analyse the extent to which counterexamples as outlined above can be generated automatically in order to demonstrate the errors. Simple, supposed solutions specified in the system programming language used by the department and in the modules are to serve as the basis.

• Prof. Dr.-Ing. Oliver Theel
• Dipl.-Inform. Eike Möhlmann