Serialisable multi-level transaction control: A specification and verification

Autoren Egon Börger
Klaus-Dieter Schewe
Qing Wang
Editoren
TitelSerialisable multi-level transaction control: A specification and verification
TypArtikel
JournalScience of Computer Programming
DOI10.1016/j.scico.2016.03.008
MonatApril
Jahr2016
Seitenonline fist
SCCH ID#1537
Abstract

We define a programming language independent controller TaCtl for multi-level transactions and an operator TA, which when applied to concurrent programs with multi-level shared locations containing hierarchically structured complex values, turns their behavior with respect to some abstract termination criterion into a transactional behavior. We prove the correctness property that concurrent runs under the transaction controller are serialisable. For its applicability to a wide range of programs we specify the transaction controller TaCtl and the operator TA in terms of Abstract State Machines (ASMs). This allows us to model concurrent updates at different levels of nested locations in a precise yet simple manner, namely in terms of partial ASM updates. It also provides the possibility to use the controller TaCtl and the operator TA as a plug-in when specifying concurrent system components in terms of sequential ASMs.