Description of the course
The course is an introduction to formal methods applied in Software Engineering. The course builds understanding on how formal methods help produce high quality software. The course further addresses formal modeling and specification languages in general and Alloy® in particular. Students develop knowledge on extracting and documenting formal requirement specifications and how these specifications can be used for validation and verification of different components of a software system during software engineering phases. Focus is also on automated verification of formal specifications to ensure system correctness.
Description of the participants
This is a compulsory course for Software Engineering students and an optional course for Computer Science and Information Technology students. The course is offered in the 4th year of studies in the Department of Computer Science, ISRA University, Hyderabad Pakistan. In the July 2022 semester the course was attended by 35 students.
Description of gamified design thinking activities
Students were asked to develop and verify simple static models of data representations, or instances, in Alloy®. Students were further challenged to identify constraints, to overcome problems in instances and to revisit models for integrating new constraints. Students regenerated and rechecked instances for errors. The process continued incrementally until no errors were identified in the models. Students worked in groups of 3 individuals. Activities were organized in the following steps.
Step 1. Problem discovery.
Students were challenged to reflect on how a simple perfect looking static model can be erroneous. They were asked to design a simple relational model to represent data items in any data structure. Initially, students designed and represented the model in Alloy® format. Subsequently, they were asked to develop test cases for model verification and compare them with Alloy® generated model instances. They were then asked to describe the problems they found in the models they designed.
Step 2. Problem re-definition.
Students were challenged to re-define their model focusing on the problems they identified in the problem discovery phase by defining constraints for every issue they identified. They were asked to re-define their model with formal specifications considering new constraints to ensure correctness.
Step 3. Ideation.
Students were challenged to introduce as many ideas as possible towards defining constraints. They were asked to define constraints in different ways, for example by representing the same constraint in different logical equations supported in Alloy®. They were asked to define the constraints as facts in the model and verify these facts as assertions. They were further challenged to consider different solutions for problems they encountered. Students discussed different constraint definitions and formed equations or formulas. They were finally asked to remove the functionally duplicate constraints for optimization.
Step 4. Prototyping.
Students developed a model prototype by defining it with facts representing constraints in the Alloy® Analyzer environment. They developed formal model definition scripts. Prototype models were static representations of data structures or types in specific software engineering solutions.
