Reference : Towards an Alloy Formal Model for Flexible Advanced Transactional Model Development

	Document type :	Scientific congresses, symposiums and conference proceedings : Paper published in a journal
	Discipline(s) :	Engineering, computing & technology : Computer science
	To cite this reference:	http://hdl.handle.net/10993/23633

Title :	Towards an Alloy Formal Model for Flexible Advanced Transactional Model Development
Language :	English
Author, co-author :	Gallina, Barbara [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC) >]
	Guelfi, Nicolas [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 :	2009
Journal title :	Abstract book of 33rd Annual IEEE Software Engineering Workshop 2009 (SEW-33)
Publisher :	IEEE
Peer reviewed :	Yes
Audience :	International
ISSN :	1550-6215
Event name :	IEEE Software Engineering Workshop 2009
Event date :	from 13-10-2009 to 14-10-2009
Keywords :	[en] transactional ; acid ; semantics
Abstract :	[en] SPLACID is a semi-formal language conceived for the specification and synthesis of (advanced) transactional models from basic features, such as transaction types and (relaxed) ACID variants. SPLACID is an improvement of the ACTA framework offering a well-structured and formal syntax. Neither ACTA nor SPLACID, however, benefit from a formal tool-supported semantics. This paper presents the first step for having a full formal semantics of SPLACID by translation to Alloy. In particular, we present the translation of the SPLACID concepts into Alloy concepts focusing on those concepts pertaining to the structure of a Transactional Model and those characterizing the isolation variant. The Alloy specification obtained by this translation preserve the SPLACID main key-properties, namely, modularity, flexibility and reusability. To support this claim we show how flexible, modular and reusable structures and isolation variants can be obtained in Alloy. Finally, we analyze the flat and nested transactional model structures and the serializability-based isolation variant using the Alloy Analyzer.
Permalink :	http://hdl.handle.net/10993/23633

	File(s) associated to this reference
	Fulltext file(s): File Commentary Version Size Access Open access 2009-SEW-Gallina-Guelfi-Kelsen.pdf Publisher postprint 574.75 kB View/Open

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

 

University of Luxembourg Library |  Feedback |  Legal notices Site Map