LTL-based Verification of Reconfigurable Workflows

TL;DR

This paper demonstrates how Linear Temporal Logic (LTL) and model checking can verify properties of reconfigurable workflows, addressing the challenges of modern dynamic systems.

Contribution

It introduces a method to verify reconfigurable workflows using LTL and model checking, filling a gap in existing formal verification approaches for adaptable systems.

Findings

Workflow reconfiguration termination is proven using LTL and Zot.

Demonstrates feasibility of formal verification for dynamic workflows.

Provides a proof of concept for future research in reconfigurable system verification.

Abstract

Logics and model-checking have been successfully used in the last decades for modeling and verification of various types of hardware (and software) systems. While most languages and techniques emerged in a context of monolithic systems with a limited self-adaptability, modern systems require approaches able to cope with dynamically changing requirements and emergent behaviors. The emphasis on system reconfigurability has not been followed by an adequate research effort, and the current state of the art lacks logics and model checking paradigms that can describe and analyze complex modern systems in a comprehensive way. This paper describes a case study involving the dynamic reconfiguration of an office workflow. We state the requirements on a system implementing the workflow and its reconfiguration and we prove workflow reconfiguration termination by providing a compilation of generic workflows into LTL, using the Bound model checker Zot. The objective of this paper is demonstrating how temporal logics and model checking are effective in proving properties of dynamic, reconfigurable and adaptable systems. This simple case study is just a "proof of concept" to demonstrate the feasibility of our ideas.