Functional Alloy Modules

Gammaitoni, Loïc; Kelsen, Pierre

Reference : Functional Alloy Modules


	Document type :	Reports : Internal report
	Discipline(s) :	Engineering, computing & technology : Computer science
	To cite this reference:	http://hdl.handle.net/10993/16386

Title :	Functional Alloy Modules
Language :	English
Author, co-author :	Gammaitoni, Loïc [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC) >]
	Kelsen, Pierre [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC) >]
Publication date :	2014
Publisher :	University of Luxembourg
Collection and collection volume :	Lassy Technical Report
Report number :	TR-LASSY-14-02
City :	Luxembourg
Country :	Luxembourg
Keywords :	[en] Alloy ; model transformation ; functional
Abstract :	[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.
Target :	Researchers
Permalink :	http://hdl.handle.net/10993/16386

File(s) associated to this reference

Fulltext file(s):

	File	Commentary	Version	Size	Access
Open access	TR-LASSY-14-02.pdf		Author postprint	360.67 kB	View/Open

All documents in ORBi^lu are protected by a user license.

University of Luxembourg Library | Feedback | Legal notices