Paper Info
Title
Alloy: A New Technology for Software Modelling
Abstract
Alloy is a lightweight language for software modelling. It's designed to be flexible and expressive, and yet amenable to fully automatic simulation and checking. At its core, Alloy is a simple first order logic extended withrelational operators. A simple structuring mechanism allows Alloy to be used in a variety of idioms, and supports incremental construction of models. Alloy is analyzed by translation to SAT. The current version of the tool uses the Chaff and Berkmin solvers; these are powerful enoughto handle a searchspace of 2100 or more. Alloy has been applied to problems from very different domains, from checking the conventions of Microsoft COM to debugging the design of a name server. Most recently, we have used it to check distributed algorithms that are designed for arbitrary topologies. We are also investigating the use of Alloy to analyze object-oriented code.
Year
DOI
Venue
2002
10.1007/3-540-46002-0_2
TACAS
Keywords
Field
DocType
new technology,automatic simulation,lightweight language,software modelling,berkmin solvers,simple structuring mechanism,incremental construction,arbitrary topology,object-oriented code,current version,name server,different domain,object oriented,first order logic,distributed algorithm
Programming language,Computer science,Alloy Analyzer,Modeling language,Network topology,Theoretical computer science,Distributed algorithm,First-order logic,Structuring,Name server,Debugging
Conference
ISBN
Citations 
PageRank 
3-540-43419-4
20
0.73
References 
Authors
1
1
Name
Order
Citations
PageRank
Daniel Jackson1464.25