Enhancing the Alloy Analyzer with Patterns of Analysis

TL;DR

This paper introduces Loy, a lightweight language for object-oriented specifications, and patterns of analysis to improve Alloy Analyzer's usability and accuracy in verifying program correctness.

Contribution

It presents Loy, a new specification language, and analysis patterns that enhance Alloy Analyzer's effectiveness for software correctness verification.

Findings

Loy can be effectively encoded into Alloy for automated analysis.

Analysis patterns guide developers to better understand specifications.

The approach improves Alloy's usability for software verification tasks.

Abstract

Formal techniques have been shown to be useful in the development of correct software. But the level of expertise required of practitioners of these techniques prohibits their widespread adoption. Formal techniques need to be tailored to the commercial software developer. Alloy is a lightweight specification language supported by the Alloy Analyzer (AA), a tool based on off-the-shelf SAT technology. The tool allows a user to check interactively whether given properties are consistent or valid with respect to a high-level specification, providing an environment in which the correctness of such a specification may be established. However, Alloy is not particularly suited to expressing program specifications and the feedback provided by AA can be misleading where the specification under analysis or the property being checked contains inconsistencies. In this paper, we address these two shortcomings. Firstly, we present a lightweight language called "Loy", tailored to the specification of object-oriented programs. An encoding of Loy into Alloy is provided so that AA can be used for automated analysis of Loy program specifications. Secondly, we present some "patterns of analysis" that guide a developer through the analysis of a Loy specification in order to establish its correctness before implementation.