Using Simulation Games in Teaching Formal Methods for Software Development

Introduction

We live in the era of massification of higher education. We encounter not only highly motivated and interested students but also average ones, where didactic methods, usually used on lower types of schools become relevant. All kinds of subjects in university curricula are affected by this situation but maybe the most suffering ones are those closely related to the field of mathematics. And formal methods courses definitely belong to this group.

Formal methods (FM) are rigorous mathematically based techniques for the specification, analysis, development and verification of software and hardware. Rigorous means that a formal method provides a formal language with unambiguously defined syntax and semantics and mathematically based means that some mathematical apparatus (formal logic, set theory, etc.) is used to define the language. But as Cerone, Roggenbach, Schlingloff, Schneider and Shaikh (2013) note, a language is not enough to constitute a formal method. To call it a method, procedures that allow doing something with specifications written in the language have to be present, too. An example of a well-known FM are regular expressions (Cerone et al., 2013): Syntax of its language can be specified by a context-free grammar. For the semantics there are several ways how to define it, for example by specifying corresponding sets of words or constructing a finite automaton that recognizes words satisfying given expression. A procedure can, for example, be a replacement of every word that satisfies given expression by another word. There are many ways how to classify FM and one, especially interesting from the educational point of view, is a taxonomy based on automation of their procedures and on how easy it is to use them. This taxonomy distinguishes between lightweight and heavyweight formal methods. Lightweight formal methods usually do not require deep expertise. The heavyweight ones are more complex, less automatic, but also more finely grained and powerful (Almeida, Frade, Pinto, & de Sousa, 2011). We can say that for a lightweight FM it is enough to learn its language and know what button to hit in corresponding software tool to do this or that. Often it is not even necessary to learn formal semantics of its language, an explanation in a natural language is sufficient. The aforementioned regular expressions are a lightweight FM. To use them for a text search or replacement in a text editor one just has to read few lines in the editor user’s manual, write an expression to an appropriate text field and press a button next to it. On the other hand, significant examples of heavyweight FM are those involving theorem proving as a method of software correctness verification. In principle, the theorem proving cannot be fully automated because underlying theories are usually not decidable. So, to prove assertions about a system a human assistance is often required and to be able to assist one has to possess knowledge about the syntax and formal semantics of the language of given FM and operation of its prover. This means a lot of effort but as Harrison (2008) points out, theorem proving brings substantial benefits over other, highly automated, verification methods (e.g. model checking). Provided that properties of a system are correctly specified, its formal verification can ensure that the properties will hold in any state of the system. In an ideal world all software should be like this – 100% verified before its delivery to users. But in reality we use to get faulty software, be it games, operating systems or firmware, and faults are fixed afterwards by means of updates.