Journal
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING
Volume 48, Issue 10, Pages 4041-4059Publisher
IEEE COMPUTER SOC
DOI: 10.1109/TSE.2021.3110191
Keywords
Unified modeling language; Semantics; Business; Model checking; Context modeling; Software; Task analysis; Process models; object life cycles; semantic specifications; formal consistency verification; model checking
Funding
- ProREUSE Project of the Austrian FFG [834167]
- FeatureOpt Project of the Austrian FFG [849928]
- VerASoS Project of the Austrian FFG [861210]
Ask authors/readers for more resources
This paper presents a new approach for verifying consistency between process models, object life cycles, and context-dependent semantic action specifications. By involving declarative specifications of all the actions of a process and enforcing a subtyping relation for reuse, this formal consistency verification ensures that all involved specifications fit together procedurally and logically.
Process models in general, and those specifying process-oriented software in particular, should be formally verified. While activity-oriented process models have been verified against object life cycles, formally specified semantic specifications of actions were not involved. Hence, previous approaches for the verification of process models did not make use of declaratively represented knowledge of actions. This paper presents a new approach for verification of consistency between process models, object life cycles, and context-dependent semantic action specifications. This approach involves declarative specifications of all the actions of a process, which also depend on the context of use of the actions. These context-dependent specifications define the 'logic' of the process flow, which is grounded in (extended) object life cycles. Since a subtyping relation is enforced, reuse is facilitated through substitutability. Our extension of object life cycles makes them applicable to processes including non-monotonicity, and even to model communication based on physical interaction in cyber-physical systems. As a consequence, this formal consistency verification ensures that all the involved specifications 'fit together', both procedurally and logically.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available