Towards an Alloy Formal Model for Flexible Advanced Transactional Model Development

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.