E. Börger, Klaus-Dieter Schewe, Qing Wang,
"Serialisable multi-level transaction control: A specification and verification"
, in Science of Computer Programming, Vol. 131, Elsevier, Seite(n) 42 - 58, 2016, ISSN: 0167-6423
Original Titel:
Serialisable multi-level transaction control: A specification and verification
Sprache des Titels:
Englisch
Original Kurzfassung:
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 behaviour. We prove the correctness property that concurrent runs under the transaction controller are serialisable, assuming an Inverse Operation Postulate to guarantee recoverability. 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.
Sprache der Kurzfassung:
Englisch
Journal:
Science of Computer Programming
Veröffentlicher:
Elsevier
Volume:
131
Seitenreferenz:
42 - 58
Erscheinungsjahr:
2016
ISSN:
0167-6423
Anzahl der Seiten:
17
Notiz zur Publikation:
Abstract State Machines, Alloy, B, TLA, \VDM\ and Z (ABZ 2014)Selected and extended papers from \ABZ\ 2014