FormalZ

FormalZ is a browser-based education game that teachers can use to break the typical monotony in a class on formal method by allowing students to have some fun playing the game, while also learning the basic of writing formal specifications. Unlike existing software engineering themed education games, FormalZ takes a deeper gamification approach, where ’playing’ is given a more central role. After all, what makes games so engaging is not merely the awarded scores and badges, but primarily the experience of playing them. The ultimate research question that intrigues us is whether such an approach will actually make a difference towards the game’s ultimate learning goal. This is still on-going work. Currently, we have a fully functional implementation of FormalZ, but polishing the user interface is still future work. 

Papers and publication

  • I. S. W. B. Prasetya, Template for Game Based Exercises in Formal Structures a Small Take Away from FormalZ, under review at “ICSE’s Joint Track on Software Engineering Education and Training” 2021 (PDF)
    Abstract: Computer science students often find doing exercises in writing formal structures to be boring, and yet this is a useful skill to have, both academically and practically. Providing some of the exercises as a game may help in making the learning process more engaging, while in addition is also useful as an automated trainer. However, developing an education game is quite an endeavour. Additionally, after the development we also have to maintain the system. This paper presents a template that can be instantiated for a given target formal system to give a minimalistic set of game concepts to turn formalization exercises in this formal system into game based exercises. The template is derived from a game called FormalZ, as we observe that its core game concepts are actually general and can be reapplied to other use cases. Along with the template this paper also proposes a light weight architecture that would allow game based exercises to be developed maintained with less effort.
  • I. S. W. B. Prasetya, C. Q. H. D. Leek, R. Oosenbrug, P. Kostic and M. d. Vries, “Can Learning Formal Specification Be Fun? —Experience and Perspective,” 2020 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW), Porto, Portugal, 2020, pp. 437-440, doi: 10.1109/ICSTW50294.2020.00078. (PDF)

    Abstract: Writing formal specifications is a useful skill for students to develop and to grow a positive mindset towards it. Unfortunately this is hampered by the stereotyping of formal method as dry and boring. In this short paper we discuss our experience in using of a computer game called FormalZ as an attempt to introduce some fun in teaching the skill. Two setups are discussed: as an embedded part of a course, and as a loose tutorial, afterwhich we will conclude with the lessons learned. Index Terms—teaching formal method, gamification in teaching formal method, gamification in teaching software engineering

  • Paper: Having Fun in Learning Formal Specifications, by I.S.W.B. Prasetya , Craig Q.H.D. Leek , Orestis Melkonian , Joris ten Tusscher , Jan van Bergen , J.M. Everink, Thomas van der Klis , Rick Meijerink , Roan Oosenbrug , Jelle J. Oostveen , Tijmen van den Pol , Wink M. van Zon. Presented at the 41st International Conference on Software Engineering (ICSE): Software Engineering Education and Training (SEET), 2019.
    Abstract: There are many benefits in providing formal specifications for our software. However, teaching students to do this is not always easy as courses on formal methods are often experienced as dry by students. This paper presents a game called FormalZ that teachers can use to introduce some variation in their class. Students can have some fun in playing the game and, while doing so, also learn the basics of writing formal specifications in the form of pre- and post-conditions. Unlike existing software engineering themed education games such as Pex and Code Defenders, FormalZ takes the deep gamification approach where playing gets a more central role in order to generate more engagement. This short paper presents our work in progress: the first implementation of FormalZ along with the result of a preliminary users’ evaluation. This implementation is functionally complete and tested, but the polishing of its user interface is still future work.
  • FormalZ backend analytics is presented in: IMPRESS: Improving Engagement in Software Engineering Courses Through Gamification, by Tanja EJ Vos, I.S.W.B. Prasetya, Gordon Fraser, Ivan Martinez-Ortiz, Ivan Perez-Colado, Rui Prada, José Rocha, António Rito Silva. Presented at the International Conference on Product-Focused Software Process Improvement (PROFES) 2019.

    Abstract: Software Engineering courses play an important role for preparing students with the right knowledge and attitude for software development in practice. The implication is far reaching, as the quality of the software that we use ultimately depends on the quality of the people that make them. Educating Software Engineering, however, is quite challenging, as the subject is not considered as most exciting by students, while teachers often have to deal with exploding number of students. The EU project IMPRESS seeks to explore the use of gamification in educating software engineering at the university level to improve students’ engagement and hence their appreciation for the taught subjects. This paper presents the project, its objectives, and its current progress.

Teaching how to write formal specifications with FormalZ.

Technology

FormalZ is a browser-based game written in JavaScript. However, to be able to be used as a teaching tool it needs to be supported by some backend services, e.g. to allow users to register, to allow teachers to upload “problems”, and to organize users in “class-rooms”. The picture above shows the top-level architecture of FormalZ. The Haskell backend is used to check whether formulas built by users are semantically equivalent to the ones expected by the teacher. In turn, this backend uses the theorem prover Z3 to do the checking.

More on the architecture and various design decisions behind FormalZ can be found in its Design Document , 2018.

Getting it

FormalZ is Free and Open Source. Installer and dockers:

Source code:

  • You can get it from its Github.This will show two repositories: one for the FormalZ game itself, and the other is for its formula checker backend (the Haskell backend in the above picture).
  • UCM’s fork, adapted to ease analytics, integration, and deployment.

Demos

First FormalZ, with comentary
Latest FormalZ, no commentary