Submitted: November 2020
Abstract
Over the years, concurrency has become increasingly important in the area of software development and is by now perhaps even ubiquitous. Since for beginners, the underlying concepts of concurrent programming can be quite hard to grasp, many people have racked their brains over suitable methods of teaching them. An example of success can be found at Saarland Informatics Campus: The academic programming language pseuCo was designed specifically for this purpose and supports students in understanding the main concepts of practical concurrency. A key strength of pseuCo is its simplicity, enabling students to write concurrent programs without worrying about complicated and overwhelming language constructs and features.
PseuCo is integrated into the teaching tool pseuCo.com, which offers students an interactive learning environment featuring a debugger and several more useful tools. However, until now, it was not possible to formally verify the correctness of programs written in pseuCo. This thesis now closes this gap by introducing a tool to compile pseuCo programs to Promela, the modelling language of the popular model checker SPIN. With this approach, it is possible to let SPIN verify the correctness of programs written in pseuCo by checking their translation against specifications expressed in linear temporal logic (LTL). Moreover, with assertions recently being added to the pseuCo language as a new feature, one can even insert correctness claims into the pseuCo program itself that are then checked by SPIN.
In this thesis, a largely exhaustive translation scheme for pseuCo to Promela is developed, which is both formalised using inference rules and put into practice with an implementation.