Hoch, R. (2019). Connecting process models, object life cycles and context-dependent conditions through semantic specifications [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2019.67744
Process models; object life cycles; semantic specification; semantic task specification; formal verification; model checking; fluent calculus
en
Abstract:
Conceptual models of process-centric software can be taskor artefact-centric. These approaches are mostly used in isolation and no formal connection exists. Tasks in (business) processes may be executed by services and operate on business objects (artefacts). In general, there is no formal definition of the actions a task performs and how this has effects on business objects. In essence, there is no connection between a task, its executing service(s) and business object(s). Moreover, business objects may not change their status arbitrarily but only in a well-defined order according to their object life cycle. Since there exists no defined connection between the models, they are often not consistent with each other, e.g., a process may perform an action that does not fit the object life cycle. Thus, formally verifying consistency of process models and object life cycles is desirable. This thesis presents an approach to formally connect tasks in process models and object life cycles through semantic specifications. We declaratively specify the actions that a task performs, via preand post-conditions, and relate them to attributes of object life cycles, i.e., we ground them in the object life cycle. This establishes a well-defined connection between the conceptual models of processes and business objects and enables checking their consistency. An additional complication is that in different contexts, defined by business rules, a task may have different conditions that have to be fulfilled for its execution, i.e., tasks are context-dependent. Thus, we propose semantically specified context-dependent conditions. The semantic specifications of tasks in processes are enriched with context information and their preand post-conditions are adapted accordingly. This allows checking the consistency of process models against object life cycles in a specific context. In order to guarantee that the same (software) services can be reused for implementing tasks in different contexts, the specifications of the former must be in subtyping relationships with the specifications of the latter. Even a recursive application of this approach on different levels of abstractions is possible. On a higher abstraction level, a composition of tasks may be viewed as a single step in the process as long as the subtyping relationship is enforced. In conclusion, the proposed approach enables to formally connect process models, object life cycles and context-dependent conditions and to verify if they are procedurally and logically consistent.