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 and other types of systems. 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 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.
- Paper for FMTea 2024: PDF Document
- Research Project Presentation: PDF Document
- Teaching Guidelines: PDF Slides
| Activity | Description | Duration | Material |
|---|---|---|---|
| First Theoretical Lecture | In the first theoretical lecture, the focus is on comparing how time-varying systems are handled in Alloy 5 vs. Alloy 6. The aim is to demonstrate the enhanced effectiveness of Alloy 6 in this regard, thanks to the introduction of new logic operators and keywords. By the end of this lesson, students should grasp how Alloy 5 addresses dynamic modeling, recognize its limitations and understand why the new features in Alloy 6 are necessary. | 45 minutes | PDF Slides \ Quizzes and Solutions |
| Flipped Lecture | Video watching and self-studying help students learn the topics related to temporal operators introduced in Alloy 6. | 15 minutes | PDF Slides \ Video |
| Second Theoretical Lecture | In the second lesson, the objectives are two-fold: firstly, through the flipped class approach, to assess students' understanding of the material covered in the first lesson and in the video; secondly, to continue exploring the new temporal features introduced in Alloy. | 45 minutes | PDF Slides \ Quizzes and Solutions |
| Exercise Lecture | The exercise lecture consists of a review of the main features of Alloy 6, explained through three exercises | 90 minutes | PDF Slides \ Code Snippets |
| Challenge | The challenge consists of a complex, real and actual problem that should be solved by students, on their own or divided into groups | 2 weeks | PDF Slides |
- Luca Padalino (luca.padalino@mail.polimi.it)
- Francesca Pia Panaccione (francescapia.panaccione@mail.polimi.it)
- Francesco Santambrogio (francesco2.santambrogio@mail.polimi.it)