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....

Expand abstract

Authors: Momtahan, L

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