You are here

PROCESS & DATA VERIFICATION

The need to extend business process languages with the capability to model complex data objects along with the control flow perspective has lead to significant practical and theoretical advances in the field of Business Process Modeling (BPM). On the practical side, there are several suites for control flow and data modeling; nonetheless, when it comes to formal verification, the data perspective is abstracted away due to the intrinsic difficulty of handling unbounded data. On the theoretical side, there is significant literature providing decidability results for expressive data-aware processes. However, they struggle to produce a concrete impact as being far from real BPM architectures and, most of all, not providing actual verification tools.  Our research aims at bridging such a gap: we provide concrete frameworks close to the widely used BPM suites grounded on solid formal basis which allow to perform formal verification tasks.

Activities

The growing adoption of IT-systems for modeling and executing (business) processes or services has thrust the investigation towards techniques and tools which support complex forms of process analysis. Many of them, such as conformance checking, process alignment, mining and enhancement, rely on complete observation of past (tracked and logged) executions. In many real cases, however, the lack of human or IT-support on all the steps of process execution, as well as information hiding and abstraction of model and data, result in incomplete log information of both data and activities. This research activity tackles the issue of automatically completing traces with missing information by notably considering not only activities but also data manipulated by them. Our techniques rely on authomated reasoning techniues such as abduction or planning to return solutions.

Projects

While BPM is a mature field for what concerns modeling and enactment of business processes, it is still lacking in the proper support and analysis of the active process executions. The main goal of the KAOS project is to overcome such issues by empowering OS with domain knowledge. In particular, KAOS will develop a foundational framework of concepts covering organizations, processes, participants, and information as relevant for Knowledge-empowered OS. It will then exploit this framework as the basis for the development of a new generation of OS techniques truly flexible and able to support domain experts and business analysts in the effective execution of business processes.

Resource

FLLOAT (From LTLf and LDLf tO Automata) is a Java library for translating Linear-time Temporal Logic (LTL) and Linear Dynamic Logic (LDL) formulas with finite-trace semantics to automata, so as to perform satisfiability and validity reasoning tasks in the finite-trace setting. The tool also allows for exporting automata in the graphviz format as well as providing the traditional automata operations through the jautomata library (determinization, intersection, negation, trimming and so on).

LTLf/LDLf-synthesis is based on FLLOAT and performs the automated synthesis of LTL and LDL formulas with finite-trace semantics, that is finding all strategies/plans (that are temporal assignments to variables we can control) satisfying a specific goal formula.