Serialisable multi-level transaction control: A specification and verification

Autoren Egon Börger
Klaus-Dieter Schewe
Qing Wang
Editoren
Titel Serialisable multi-level transaction control: A specification and verification
Typ Artikel
Journal Science of Computer Programming
DOI 10.1016/j.scico.2016.03.008
Monat April
Jahr 2016
Seiten online 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.