Keywords

1 Introduction

Current practices of developing software include its testing. However, from a formal point of view, it is not feasible to cover every possible piece of software functionality with tests. Especially this concern relates to safety or mission critical software, such as software for medical machines and satellites.

Formal methods in software engineering address this problem by utilizing mathematical frameworks of reasoning about programs, which is hard to understand for the majority of students. Courses that involve formal methods become the most unpopular.

To the best knowledge of the author, there exists no systematic literature review that addresses challenges of teaching formal methods. One of the notable works that addresses challenges of teaching formal methods is the survey by Spichkova and Zamansky [24]. However, this survey is not comprehensive as it lacks the papers from the conferences on teaching formal methods. Thus, there is a need for systematic synthesis of the literature on the practices of teaching formal methods.

Despite the importance of formal methods for testing and verification of critical software, universities fail in teaching this aspect of computer science to students. This systematic literature review will categorize and systematize the existing experience of teaching formal methods to students at the university level.

2 Review Questions

To carry out this systematic literature review a number of activities, including database search, quality assessment as well as data extraction and synthesis, were conducted to formulate a conclusion.

The objective of this study is to identify the struggles that educators encounter during teaching formal methods in the higher education. A particular interest is strategies that used to overcome the struggles.

So, to achieve the objective the following research questions were formulated:

  • RQ1. What are the challenges of teaching formal methods in the universities?

  • RQ2. What are the strategies used to deal with these challenges?

3 Review Methods

According to Kitchenham and Charters [11], the following review components should be present to establish replicability of the review:

  • Study search strategy

  • Study selection criteria

  • Study quality assessment

  • Data extraction strategy

3.1 Study Search Strategy

Based on the objective of the paper, the following search query was used for the search: “teaching” AND “formal methods”. The terms were matched to titles, abstracts and keywords.

The following databases were used for search:

Fig. 1.
figure 1

A flowchart that represents research protocol

Full size image

The author has decided to include papers from conference proceedings. Proceedings of the following conferences were included:

  • TFM 2009

  • FMET 2008

  • TFM 2006

  • FMED 2006

As can be seen in Fig. 1, the primary search have found 151 studies.

3.2 Study Selection Criteria

After the initial review of the queries, some keywords were identified as irrelevant to the study. Here is the list of excluded keywords: statistic, statistics, Grammar, Second Language Learning, formal methods of estimation, Economics education, Law students, Physical education, Physicians, Emergency Medicine Education. Other criteria for selection are papers should be published not later than 2001 and be written in English language. Number of studies at this stage is 53.

After keywords exclusion, all papers were reviewed by the author to perform third stage of selection. During this stage we filtered papers based on their relevance to the research questions.

Then, papers were filtered based on title and abstract. During this filtering process studies that claimed to teach formal methods outside of universities, presented formal methods in other contexts were excluded. For example, title of [25] states about experience in middle school and [7] about formal methods in electronic government. At this stage the number of papers was reduced to 43.

3.3 Study Quality Assessment

In this stage rest of the papers were read and assessed on how they answer at least one of the research questions. At this stage, primary targets for filtering out were papers that have not neither evidence nor opinion regarding how challenges of teaching formal methods or what strategies were used improve experience of the students that participate in the course. Examples of the filtered out papers are [18] and [15]. The former paper mostly consists of anecdotes that are aimed to motivate anyone, who reads them, to use formal methods. The latter paper is the one, which focused more on the tool, rather then how the tool solves the problem of students. The final number of papers used to answer research questions is 22.

3.4 Data Extraction Strategy

The resulting set of the papers is a mixture of teaching experience that was recorded either through a session or within a certain period, when course was offered. Other papers demonstrate the use of software or teaching approaches to solve general or a particular problem along with student’s feedback.

Due to the nature of the “raw” material, structured data extraction becomes either very difficult or impossible to conduct in the objective manner. So the author used a word processor to identify some of the themes presented in the studies, grouping them as necessary.

4 Results

In this section we report findings about research questions. The purpose is to provide themes discovered in the studies.

4.1 What Are the Challenges of Teaching Formal Methods?

We found 17 studies that identified 3 main themes that answer this question: students scepticism, difficulties with auxiliary software and challenges with materials.

Students’ Scepticism. This is one of the biggest challenges identified by majority of researchers. Throughout the literature there were two prominent problems that are related: student’s scepticism about formal methods as well as isolation of formal methods from application in other courses.

Students Are Skeptical About the Usefulness of Formal Methods. This is the major problem identified in 8 studies [2,3,4, 6, 9, 17, 19, 26]. Blanco et al. [2] discusses how program verification is viewed by students as a “an additional burden”. Brakman et al. [4] perceives that students see little practicality in use of formal methods.

Isolation of Formal Methods from Application in Other Courses. Boute [3] observes often such behavior is motivated by little exposure to formal methods across curriculum. Supporting, Sekerinski [22], reporting his experience of teaching a course on software design with formal methods, identifies an isolated use of formal methods as a main obstacle that prevents its flourishing.

Difficulties with Auxiliary Software. Another theme that was identified throughout review is difficulties with tools that are used to teach formal methods. Steep learning curve and bad user experience are major challenges that support the theme.

Steep Learning Curve for Tools. Lipaczewski and Ortmeier [13] recognized a steep learning curve as one of the failures of tools that use formal methods. Schreiner [21] supports them adding that teaching time is too scarce to consider teaching how to use this “difficult to learn and/or inconvenient to use” software.

Tools Give Little Feedback. In their course Bayley, Lightfoot and Martin [1] avoid using software tools, because tools can “produce a fairly cryptic and discouraging response”. Gopalakrishnan [9] observed that most tools lack a good user experience and failing do not provide insight at why they fail.

Challenges with Course Materials. The third theme that was common to a number of studies is challenges with course materials. Such challenges include dryness of the course, diversity of materials, lack of comprehensive textbook and course require students to have better mathematical knowledge than they have.

Dryness of the Course. Two studies, [4] and [19] identified dryness of the course as a problem of teaching formal methods. In particular, Brakman et al. [4] reports that “lack of visualization” is the primary reason of ineffectiveness of teaching formal methods.

Diversity of Materials. Gopalakrishnan [9] notes that there are a variety of tools that use formal methods; however, there are few initiatives to adopt them. These tools “face the uphill battle of vying for attention and commitment from teachers” [9]. In other word, there are plenty of resources on formal methods that are yet to be adopted by educators.

No Comprehensive Textbook.  While there exists a diversity of materials, some authors find it difficult to navigate through them. In particular, Kofroň, Parízek and Šerý [12] report that they were not satisfied with comprehensiveness of one of the textbooks used for one of their courses.

Inadequate Background in Mathematics.  Several authors [8, 14, 16, 23] report students that take courses in formal methods often do not know a certain concepts that are used in the course. Consequently, such inadequacy requires inclusion of additional materials into the course.

4.2 What Are the Strategies Used to Deal with These Challenges?

We have found 15 papers and 4 major themes that answer this question that are formulated as a form of advice: practice, engage students, avoid isolation of formal methods and simplify material.

Practice. This advice was formulated because several authors attributed the success of the formal methods courses they ran to the extensive practice. They provided a large number of examples to the students to facilitate the ingestion of theoretical and practical components of formal methods.

Use a Lot of Examples. Aceto et al. [6] report that they avoid presenting general theory, preferring investigation of particular instances. They declare that examples play “primary role” in their practice.

Real-life Examples and Projects. Some practitioners [4, 5, 20] make stronger claims by saying that examples should involve “real-life”, not artificial instances of the problem. For instance, Brakman et al. [4] discusses how presenting verification of Bluetooth protocol as a course project helped their students to increase understanding of formal methods.

Engage Students. This strategy was devised to describe several reported practices that increased engagement and motivation of the students with formal methods. Gamify. Prasetya et al. [19] presents a game, FormalZ, that presents concepts of formal methods in fun and engaging manner. It also introduces a competitive environment by introducing a leaderboard, a ranking list. Their preliminary results show positive feedback from students. Use Electronic Voting systems. Miller and Cutts [16] introduce an electronic voting system (EVS) to help students to actively participate. EVS often consists of a several buttons that represent answer choices and a display that presents a question. Often EVS are anonymous and are instruments to increase student engagement rather than test of the knowledge. Miller and Cutts [16] report use of EVS increased confidence of student to “to answer questions within the class”.

Avoid Isolation of Formal Methods. This direction came from several studies that report an underrepresentation of the formal methods across curricula. Such situation leads to formal methods looking esoteric, decreasing student’s motivation [3, 22].

Start Early in Introductory Course. Blanco et al. [2] reports that the course on introductory programming that was based on formal methods was helpful for students to learn appreciation of formal methods. They report that the course had lasting effect based on “the optional courses they choose later on in the programmes, and the topics they choose for their final projects” [2].

Use a Combination of Formal Techniques. Some educators claim that they achieve best results when they explain several formal techniques. Hallerstede and Leuschel [10] utilize combination of “formal proof, model-checking, and animation” to improve accuracy of a formal model.

Juxtapose of Taught Formal Methods with Other Methodologies. To overcome students’ scepticism about formal methods Catano and Rueda [6] ask students throughout the course to reflect upon pros and cons of the formal methods compared to the already learned traditional approaches.

Simplify Material. This strategy is intended to simplify not formal methods, but the material used to deliver the lesson. While it is difficult, or impossible to make formal methods accessible for everyone, some educators have found ways of making their delivery friendlier to the listeners.

Use Another, Simpler Tool. Some studies [13, 21] suggest that to overcome challenges associated with software, which uses formal methods, it is the best to use other, simpler tools. For example, Lipaczewski and Ortmeier [13] propose SAML with its plugins for IDE and web-based user interface. SAML is intended as tool for building models that are more friendly to the user than existing alternatives.

Use Common Languages that Have Built-in Expressivity. Another study avoids specialized formal methods software and languages. Instead, Gopalakrishnan [9] uses a general purpose language, like Python, for “Models of Computation” course. It has features, like list comprehension that helps writing definitions with mathematical notation.

Use Less Formal Testing as a Medium for Teaching Some of the Formal Methods. Utting and Reeves [26] suggest that interweaving of traditional testing approach and elements of formal methods helped their students to have a better satisfaction with using formal methods.

5 Discussion

This systematic review have demonstrated that there is a number of challenges, like students’ scepticism, difficulties with computer-aided assistants and challenges with the course materials. There are a few practices that can help to overcome these challenges, like use of examples, gamification, teaching of combination of formal methods and simplification of the delivery. The author believes that some of the discovered challenges are valid and hope that provided strategies will help to overcome them.

5.1 Limitations

Even though this literature review attempts to be objective, there is no ideal, objective criteria that would quantify success or failure of the provided solutions. Most of the researchers relied on the students feedback, course enrollment number or their own senses to draw a conclusion about usefulness of certain techniques.

6 Conclusion

A systematic literature review was performed on 22 papers that report practices of teaching formal methods in universities. The aim of this review was to identify the struggles that educators encounter while teaching formal methods, as well as exploring strategies that are used to deal with these struggles. The findings allowed to formulate 8 themes of challenges that were further grouped into 3. We have found 11 themes of strategies that were grouped into 4.