Model checking as support for inspecting compliance to rules in flexible processes. (June 2015)

• Record Type: Journal Article
• Authors: Letia, Ioan Alfred; Goron, Anca
• Is Part Of: Journal of visual languages & computing. Volume 28(2015)
• Page Start: 100
• Page End: 121
• Publication Date: 2015-06
• Subjects: Flexible processes -- Compliance to rules -- Dynamic condition response graph -- Clinical guidelines -- Hybrid logics -- Description logics; Visual programming languages (Computer science) -- Periodicals; Visual programming (Computer science) -- Periodicals; Programming languages (Electronic computers) -- Semantics -- Periodicals; Langages de programmation visuelle -- Périodiques; Programmation visuelle -- Périodiques; Langages de programmation -- Sémantique -- Périodiques; Programming languages (Electronic computers) -- Semantics; Visual programming (Computer science); Visual programming languages (Computer science); Periodicals; Electronic journals; 005
• DOI: 10.1016/j.jvlc.2014.12.008
• Languages: English
• ISSNs: 1045-926X

Abstract

Abstract: Context : In backing business processes with information technology, a difficult trade-off appears between the desire to control processes for avoiding undesirable executions, and the flexibility that users need in order to attain their higher level goals. While this is a general trend in general business processes, it is even more acute in specific domains like the medical area, where the clinical guidelines are expected to contribute to the optimization of medical assistance. Objective : We study model checking as support for understanding and solving the inconsistencies between the process models and their corresponding execution. The aim is to provide various human users with output in controlled English for the checking of properties about the execution of such processes, and perhaps input in controlled English for properties of interest from the point of view of the user. Method : For the conformance checking of such complex situations, we use an extended version of a Hybrid Logics model checking tool, for the verification of various properties within an abstract representation model. The extension with Description Logics helps to exploit a more refined representation of the entities involved in the execution of processes. The advantages of using the model checker in visualizing and verbalizing connections of the properties checked with their dependencies over time are shown on a sore throat running scenario, relative to its corresponding clinical guidelines. Results : With new data for an alternative run of the execution, our method can update the abstract model to enable the user to see what might happen or might have happened in such runs of the process model. The new updated abstract model corresponding to the new real situations is then used to analyze whether the overall state is acceptable or should further actions be considered to arrive at an acceptable state of the world. Conclusion : Our results show how the combination of Hybrid Logic and Description Logic can provide the necessary abstraction for the checking to be carried out at a level understandable by the human user when the properties of interest can be translated by a controlled English language interface. Abstract : Highlights: Conformance checking of flexible processes with verbalization for human users. Properties verified can be expressed straightforwardly in controlled English. Update of abstract model to new real world situations. Hybrid Logic, to describe dynamics, and Description Logics, for concepts. Abstractions used by human users are shown in significant decisions.