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 mailto [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC) >]
Kelsen, Pierre mailto [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC) >]
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):

FileCommentaryVersionSizeAccess
Open access
TR-LASSY-14-02.pdfAuthor postprint360.67 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.