An algebra of synchronous atomic steps

Hayes, Ian J., Colvin, Robert J., Meinicke, Larissa A., Winter, Kirsten and Velykis, Andrius (2016). An algebra of synchronous atomic steps. In: John Fitzgerald, Constance Heitmeyer, Stefania Gnesi and Anna Philippou, FM 2016: Formal Methods - 21st International Symposium, Proceedings. 21st International Symposium on Formal Methods, FM 2016, Limassol, Cyprus, (352-369). 9-11 November 2016. doi:10.1007/978-3-319-48989-6_22

Author Hayes, Ian J.
Colvin, Robert J.
Meinicke, Larissa A.
Winter, Kirsten
Velykis, Andrius
Title of paper An algebra of synchronous atomic steps
Conference name 21st International Symposium on Formal Methods, FM 2016
Conference location Limassol, Cyprus
Conference dates 9-11 November 2016
Proceedings title FM 2016: Formal Methods - 21st International Symposium, Proceedings   Check publisher's open access policy
Journal name Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)   Check publisher's open access policy
Place of Publication Heidelberg, Germany
Publisher Springer
Publication Year 2016
Sub-type Fully published paper
DOI 10.1007/978-3-319-48989-6_22
Open Access Status Not yet assessed
ISBN 9783319489889
ISSN 1611-3349
Editor John Fitzgerald
Constance Heitmeyer
Stefania Gnesi
Anna Philippou
Volume 9995
Start page 352
End page 369
Total pages 18
Language eng
Formatted Abstract/Summary
This research started with an algebra for reasoning about rely/guarantee concurrency for a shared memory model. The approach taken led to a more abstract algebra of atomic steps, in which atomic steps synchronise (rather than interleave) when composed in parallel. The algebra of rely/guarantee concurrency then becomes an interpretation of the more abstract algebra. Many of the core properties needed for rely/guarantee reasoning can be shown to hold in the abstract algebra where their proofs are simpler and hence allow a higher degree of automation. Moreover, the realisation that the synchronisation mechanisms of standard process algebras, such as CSP and CCS/SCCS, can be interpreted in our abstract algebra gives evidence of its unifying power. The algebra has been encoded in Isabelle/HOL to provide a basis for tool support.
Subjects 2614 Theoretical Computer Science
1700 Computer Science
Q-Index Code E1
Q-Index Status Provisional Code
Institutional Status UQ

Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 0 times in Thomson Reuters Web of Science Article
Scopus Citation Count Cited 0 times in Scopus Article
Google Scholar Search Google Scholar
Created: Sun, 08 Jan 2017, 10:19:47 EST by System User on behalf of Learning and Research Services (UQ Library)