We employ formal methods for modelling, verifying and deploying healthcare workflows. Our methodology consists of four main phases, as illustrated in Figure 1.
Figure 1: Our methodology
Following a standard process modelling approach, an initially underspecified, possibly “fuzzy” concept, such as a policy, practice, or system is analysed and decomposed to smaller, independent, loosely specified processes. This includes identifying typical tasks, actors and resources involved in the studied system. This stage is usually performed in close collaboration with domain experts and practitioners who can provide the necessary domain knowledge. We can employ different methods for collecting data, such as interviews, contextual inquiry and focus groups.
The identified processes are formally modelled at this stage. We, thus, develop a formal, well-defined, logic-based model for each of the smaller processes. This is achieved with the use of our visual tool (see Figure 2), which allows the user to graphically specify processes along with their inputs and outputs, while automatically producing their logical definition in the background. The end result is a set of visually defined processes, accompanied by their formal specification in Classic Linear Logic in the underlying theorem proving engine based on HOL Light.
Figure 2: Our visual tool for formal process modelling and rigorous workflow composition
The specified processes are then rigorously composed to form a well-defined workflow for the original complex system. This stage is fully supported by our diagrammatic tool, which allows the user to visually compose the workflow by matching the inputs and outputs of different processes. More importantly, mathematical proofs are seamlessly and automatically run in the background, enabled through the underlying connection of the visual tool with the theorem proving engine HOL Light. This means that the composition is rigorously verified and the constructed workflow can be trusted to be correct.
The composed workflow is deployed as an executable solution that can be readily used by healthcare practitioners. We provide a systematic, automated procedure that translates the modelled workflow into a deployed solution of an appropriate form, such as a web-based information system or electronic checklists. This automated procedure allows design properties of the modelled workflow to persist in its deployment and minimises the required human effort in order to maximise deployment speed and maintainability.
D5 Creation | Powered by: WordPress