Reference : Functional Alloy Modules |
Reports : Internal report | |||
Engineering, computing & technology : Computer science | |||
http://hdl.handle.net/10993/16386 | |||
Functional Alloy Modules | |
English | |
Gammaitoni, Loïc ![]() | |
Kelsen, Pierre ![]() | |
2014 | |
University of Luxembourg | |
Lassy Technical Report | |
TR-LASSY-14-02 | |
Luxembourg | |
Luxembourg | |
[en] Alloy ; model transformation ; functional | |
[en] The Alloy language was developed as a lightweight modelling language that allows fully automatic analysis of software design models
via SAT solving. The practical application of this type of analysis is hampered by two limitations: first, the analysis itself can become quite time consuming when the scopes become even moderately large; second, determining minimal scopes for the entity types (limiting the number of entities of each type) to achieve better running times is itself a non-trivial problem. In this paper we show that for the special case of Alloy modules specifying transformations we may be able to circumvent these limitations. We define the corresponding notion of functional module and define precise conditions under which such functional modules can be efficiently interpreted rather than analysed via SAT solving and we also explain how interpretation of functional Alloy modules can be seamlessly integrated with the SAT-based analysis of other modules. We provide evidence that for complex transformations interpreting functional modules may result in significant time savings. | |
Researchers | |
http://hdl.handle.net/10993/16386 |
File(s) associated to this reference | ||||||||||||||
Fulltext file(s):
| ||||||||||||||
All documents in ORBilu are protected by a user license.