Title :
Towards an Alloy Formal Model for Flexible Advanced Transactional Model Development
Author :
Gallina, Barbara ; Guelfi, Nicolas ; Kelsen, Pierre
Author_Institution :
Lab. for Adv. Software Syst., Univ. of Luxembourg, Luxembourg
Abstract :
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.
Keywords :
formal languages; formal specification; programming language semantics; software reusability; ACID variants; ACTA framework; SPLACID; alloy analyzer; alloy formal model; flexible advanced transactional model development; formal tool supported semantics; semi formal language; Analytical models; Computational modeling; Concrete; Metals; Semantics; Software; Syntactics; ACID properties; ACTA framework; Alloy language; Relaxed ACID properties; Software Product Line; dependability; formal semantics; reusability;
Conference_Titel :
Software Engineering Workshop (SEW), 2009 33rd Annual IEEE
Conference_Location :
Skovde
Print_ISBN :
978-1-4244-6863-8
Electronic_ISBN :
1550-6215
DOI :
10.1109/SEW.2009.13