An Automated Analysis Of Process Interference Verified With LTL Checking

Nick van Beest, Doina Bucur, Johan Wortmann, Alexander Lazovik



Concurrent processes potentially interfere due to mutual dependence on certain data. This has severe consequences: even if these processes properly terminate, they may lead to undesirable outcomes from a business perspective. As the disruptions are primarily visible to external stakeholders, identifying such erroneous situations is complex and organizations are often unaware of these cases. In this paper, a methodology is developed to identify interfering processes. A software tool is developed to automatically identify and analyze the erroneous situations using simulation and LTL checking. The simulation results are validated against the LTL properties of interference, in order to ensure that the identified erroneous paths are a result of process interference. The magnitude of the problem can be analyzed, as interference is investigated for each execution path. This method has been applied at a large energy company and a large telecom company in the Netherlands. The analysis shows that process interference indeed leads to erroneous situations in a significant number of cases (around 10% of the paths lead to faulty results, with exceptions of 70%), including the possibility of wrong invoices, of ordering new products with wrong customer data, etc. The results clearly show the importance and relevance of these business problems.


Duik in de onderzoeksthema's van 'An Automated Analysis Of Process Interference Verified With LTL Checking'. Samen vormen ze een unieke vingerafdruk.

Citeer dit