Issue No. 04 - April (2014 vol. 40)
Christophe Damas , Department of Computing, Icteam Institute, Université Catholique de Louvain, Louvain-La-Neuve, Belgium
Bernard Lambeau , Department of Computing, Icteam Institute, Université Catholique de Louvain, Louvain-La-Neuve, Belgium
Axel van Lamsweerde , Department of Computing, Icteam Institute, Université Catholique de Louvain, Louvain-La-Neuve, Belgium
Decision-based processes are composed of tasks whose application may depend on explicit decisions relying on the state of the process environment. In specific domains such as healthcare, decision-based processes are often complex and critical in terms of timing and resources. The paper presents a variety of tool-supported techniques for analyzing models of such processes. The analyses allow a variety of errors to be detected early and incrementally on partial models, notably: inadequate decisions resulting from inaccurate or outdated information about the environment state; incomplete decisions; non-deterministic task selections; unreachable tasks along process paths; and violations of non-functional process requirements involving time, resources or costs. The proposed techniques are based on different instantiations of the same generic algorithm that propagates decorations iteratively through the process model. This algorithm in particular allows event-based models to be automatically decorated with state-based invariants. A formal language supporting both event-based and state-based specifications is introduced as a process modeling language to enable such analyses. This language mimics the informal flowcharts commonly used by process stakeholders. It extends High-Level Message Sequence Charts with guards on task-related and environment-related variables. The language provides constructs for specifying task compositions, task refinements, decision trees, multi-agent communication scenarios, and time and resource constraints. The proposed techniques are demonstrated on the incremental building and analysis of a complex model of a real protocol for cancer therapy.
Analytical models, Unified modeling language, Algorithm design and analysis, Semantics, Blood, Flowcharts, Medical treatment,formal specification, Process modeling, process analysis, model verification, decision errors, safety-critical workflows, non-functional requirements, domain-specific languages
Christophe Damas, Bernard Lambeau, Axel van Lamsweerde, "Analyzing Critical Decision-Based Processes", IEEE Transactions on Software Engineering, vol. 40, no. , pp. 338-365, April 2014, doi:10.1109/TSE.2014.2312954