Towards a small model theorem for data independent systems in Alloy

Journal article

Alloy is an extension of first-order logic for modelling software systems. Alloy has a fully automatic analyser which attempts to refute Alloy formulae by searching for counterexamples within a finite scope. However, failure to find a counterexample does not prove the formula correct. 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 paper gives a theorem in a language closely related to Alloy, which applies to models of data-independent systems. The theorem calculates for such types T a threshold size. If no counterexamples are found at the threshold, the theorem guarantees that increasing the scope on T beyond the threshold still yields no counterexamples, and can complete the analysis for data-independent systems.

Authors: Momtahan, L

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Elsevier
• Journal: Electronic Notes in Theoretical Computer Science
• Volume: 128
• Issue: 6
• Pages: 37–52
• Publication date: 2005-05-01
• Edition: Publisher's version
• DOI: 10.1016/j.entcs.2005.04.003
• ISSN: 1571-0661
• Language: English
• Keywords: model finding; data independence; Alloy
• Subjects: Computer science (mathematics)