Abstract
Region composition is an operation where transitions of different automaton are woven together according to synchronization constraints. Reasoning about properties across regions is difficult, which is problematic in systems that are assembled by composing a large number of regions. We introduce two transactions constructs to enforce causality properties between transitions of a state machine. We show that transactions can be checked statically and that they support modular reasoning about region composition by preserving liveness properties within the scope of a transaction. © 2012 ACM.
Recommended Citation
T. Cottenier et al., "Modular Reasoning About Region Composition," FOAL'12 - Proceedings of the 11th Workshop on Foundations of Aspect-Oriented Languages, pp. 15 - 19, Association for Computing Machinery (ACM), May 2012.
The definitive version is available at https://doi.org/10.1145/2162010.2162016
Department(s)
Computer Science
Keywords and Phrases
Composition; Liveness; Statecharts
International Standard Book Number (ISBN)
978-145031099-4
Document Type
Article - Conference proceedings
Document Version
Citation
File Type
text
Language(s)
English
Rights
© 2024 Association for Computing Machinery, All rights reserved.
Publication Date
07 May 2012
