TY - GEN
T1 - UTP Semantics for Shared-State, Concurrent, Context-Sensitive Process Models
AU - Butterfield, Andrew
AU - Mjeda, Anila
AU - Noll, John
N1 - Publisher Copyright:
© 2016 IEEE.
PY - 2016/8/10
Y1 - 2016/8/10
N2 - Process Modelling Language (PML) is a notationfor describing software development and business processes. It takes the form of a shared-state concurrent imperative language describing tasks asactivities that require resources to startand provide resources when they complete. Its syntax covers sequential composition, parallelism, iteration and choice, but without explicit iteration and choice conditions. It is intended to support a range of context-sensitive interpretations, from a rough guide for intended behaviour, to being very prescriptive about the order in which tasks must occur. We are using Unifying Theories of Programming (UTP) to modelthis range of semantic interpretations, with formal links between them, typically of the nature of a refinement. We address a number of challenges that arise when trying to developa compositional semantics for PML and its shared-state concurrent underpinnings, most notably in how UTP observations need to distinguishbetween dynamic state-changes and static context parameters. The formal semantics are intended as the basis for tool support for process analysis, with applicationsin the healthcare domain, covering such areas as healthcare pathwaysand software development and certification processesfor medical device software.
AB - Process Modelling Language (PML) is a notationfor describing software development and business processes. It takes the form of a shared-state concurrent imperative language describing tasks asactivities that require resources to startand provide resources when they complete. Its syntax covers sequential composition, parallelism, iteration and choice, but without explicit iteration and choice conditions. It is intended to support a range of context-sensitive interpretations, from a rough guide for intended behaviour, to being very prescriptive about the order in which tasks must occur. We are using Unifying Theories of Programming (UTP) to modelthis range of semantic interpretations, with formal links between them, typically of the nature of a refinement. We address a number of challenges that arise when trying to developa compositional semantics for PML and its shared-state concurrent underpinnings, most notably in how UTP observations need to distinguishbetween dynamic state-changes and static context parameters. The formal semantics are intended as the basis for tool support for process analysis, with applicationsin the healthcare domain, covering such areas as healthcare pathwaysand software development and certification processesfor medical device software.
KW - Concurrency
KW - Process Modelling Language
KW - Shared-State
KW - Unifying Theories of Programming
UR - http://www.scopus.com/inward/record.url?scp=84988014413&partnerID=8YFLogxK
U2 - 10.1109/TASE.2016.22
DO - 10.1109/TASE.2016.22
M3 - Conference contribution
AN - SCOPUS:84988014413
T3 - Proceedings - 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016
SP - 93
EP - 100
BT - Proceedings - 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016
Y2 - 17 July 2016 through 19 July 2016
ER -