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.
%0 Journal Article
%1 momtahan_05_towards
%A Momtahan, Lee
%B Proceedings of the Fouth International Workshop on Automated Verification of Critical Systems (AVoCS 2004)
%D 2005
%J Electronic Notes in Theoretical Computer Science
%K _hardcopy 2005 alloy data_independence small_model _folder_1
%N 6
%P 37--52
%R 10.1016/j.entcs.2005.04.003
%T Towards a Small Model Theorem for Data Independent Systems in Alloy
%U http://dx.doi.org/10.1016/j.entcs.2005.04.003
%V 128
%X 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.
@article{momtahan_05_towards,
abstract = {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.},
added-at = {2009-02-11T21:03:27.000+0100},
author = {Momtahan, Lee},
biburl = {https://www.bibsonomy.org/bibtex/2cc4b4190913a1e61336ceaca2c4c72ce/leonardo},
booktitle = {Proceedings of the Fouth International Workshop on Automated Verification of Critical Systems (AVoCS 2004)},
citeulike-article-id = {3180243},
doi = {10.1016/j.entcs.2005.04.003},
interhash = {76166542f6c0255c84180479c83c898b},
intrahash = {cc4b4190913a1e61336ceaca2c4c72ce},
journal = {Electronic Notes in Theoretical Computer Science},
keywords = {_hardcopy 2005 alloy data_independence small_model _folder_1},
month = May,
number = 6,
pages = {37--52},
posted-at = {2008-09-01 23:28:45},
priority = {4},
timestamp = {2009-02-11T21:03:27.000+0100},
title = {Towards a Small Model Theorem for Data Independent Systems in Alloy},
url = {http://dx.doi.org/10.1016/j.entcs.2005.04.003},
volume = 128,
year = 2005
}