An Educational Module for Temporal Features in Alloy 6

As software systems have become increasingly important, teaching Software Engineering students how to develop high-quality software is essential. In this regard, formal modeling and verification are important educational tools that help students in getting an in-depth understanding of software. Nonetheless, formal languages are not straightforward to teach and, therefore, carefully designed materials are needed to convey them. In this paper we focus on Alloy, which is an easy-to-learn formal language equipped with a usable analyser, and we present a complete teaching module that can be used by teachers to support students in learning the temporal constructs defined in its latest version, Alloy 6. The module is designed exploiting active learning methods and is supported by multimedia content. It is openly available and can be reused and tailored to the need of specific courses.