Small model theorems for data independent systems in Alloy

Thesis

A system is data independent in a type T if the only operations allowed on variables of type T are input, output, assignment and equality testing. This property can be exploited to give procedures for the automatic verification of such systems independently of the instance of the type T. Alloy is an extension of first-order logic for modelling software systems. Alloy has a fully automatic analyzer which attempts to refute Alloy formulas by searching for counterexamples within a finite scope. However, failure to find a counterexample does not prove the formula correct. A small model theorem is a theorem which shows that if a formula has a model then it has a model within some finite scope. The contribution of this thesis is to give a small model theorem which applies when modelling data-independent systems in Alloy. The theorem allows one to detect automatically whether an Alloy formula is data independent in some type T and then calculate a threshold scope for T, thereby completing the analysis of the automatic analyzer with respect to the type T. We derive the small model theorem using a model-theoretic approach. We build on the standard semantics of the Alloy language and introduce a more abstract interpretation of formulas, by way of a Galois insertion. This more abstract interpretation gives the same truth value as the original interpretation for many formulas. Indeed we show that this property holds for any formula built with a limited set of language constructors which we call data-independent constructors. The more abstract interpretation is designed so that it often lies within a finite scope and we can calculate whether this is the case and exactly how big the finite scope need be from the types of the free variables in the formula. In this way we can show that if a formula has any instance or counterexample at all then it has one within a threshold scope, the size of which we can calculate.

Authors: Momtahan, L

• Publication date: 2007
• DOI: 10.5287/ora-d5dj1oogj
• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Language: English
• Keywords: Alloy; data independence; Automated verification
• Subjects: Computer science (mathematics)