Abstract
We show how a parallel composition of action systems can be refined by refining the components separately, and checking non-interference against invariants and guarantee conditions, which are abstract and stable. The guarantee condition can be thought of as a very abstract specification of how a system affects the global state, and it allows us to show that an action system refinement is valid in a given environment, even if we do not know any of the details of that environment. The paper extends the traditional notion of action systems slightly, and it makes use of a generalisation of the attribute model for program variables.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Back, R., Wright, J. Compositional Action System Refinement. Formal Aspects of Computing 15, 103–117 (2003). https://doi.org/10.1007/s00165-003-0005-6
Issue Date:
DOI: https://doi.org/10.1007/s00165-003-0005-6