fm4se-alloy-sigs-checker

This project and worksheet is part of the lecture Formal Methods for Software Engineering. We are using the light-weight formal methods tool Alloy Analyzer.

Usually we use formal methods to analyze software designs by translating analysis problems to formal methods tools. Now we will treat the quality of formal methods specifications as a software analysis problem. In this task we will implement a tool that analyzes properties of Alloy models (using Alloy itself).

Project Setup

📼 see the project setup video

1. Install OpenJDK/JDK
2. Clone the repository
3. Open in any IDE of your choice (e.g. Eclipse, VS Code, etc.)
4. Run and inspect src/main/java/de/buw/fm4se/ExampleUsingTheCompiler.java
5. Run and inspect src/main/java/de/buw/fm4se/ExampleUsingTheAPI.java

Task 1

Implement a the body of method findDeadSignatures in class AlloyChecker to determine a list of dead signatures of an Alloy model, i.e., list all signatures that do not have atoms in any instance.

• Use the first command in the Alloy file. To see how to parse Alloy models and how to access commands see, e.g., lines 57 and 65 in class ExampleUsingTheCompiler.
• You may update the predicate a command cmd checks to expression e by using the returned Command of cmd.change(e).
• To see how you can create formulas from signatures and other formulas see, e.g., line 90 in class ExampleUsingTheAPI.

Task 2

Implement a method findCoreSignatures in class AlloyChecker to determine a list of core signatures of an Alloy model, i.e., list all signatures that always have atoms except in the empty instance.

• Again, use the first command in the Alloy file.

Task 3

Implement a method findMinScope in class AlloyChecker to determine the minimum scope for each signature in an Alloy model, i.e., map each signature name to an integer scope for which the model is still satisfiable.

• Again, use the first command in the Alloy file.
• You may update the scope of a signature sig in a command cmd to integer i by using the returned Command of cmd.change(sig, false, i).
• Computing a maximal scope is a bit tricky and done for you in method getMaxScope.

📼 see the code walk-through and explanation of tasks 1-3