Department of Mathematics and Computer Science, University of La Rioja, La Rioja, Spain.
J Biomed Inform. 2010 Aug;43(4):520-36. doi: 10.1016/j.jbi.2010.02.009. Epub 2010 Mar 4.
The goal of this research is to provide a framework to enable authoring and verification of clinical guidelines. The framework is part of a larger research project aimed at improving the representation, quality and application of clinical guidelines in daily clinical practice.
The verification process of a guideline is based on (1) model checking techniques to verify guidelines against semantic errors and inconsistencies in their definition, (2) combined with Model Driven Development (MDD) techniques, which enable us to automatically process manually created guideline specifications and temporal-logic statements to be checked and verified regarding these specifications, making the verification process faster and cost-effective. Particularly, we use UML statecharts to represent the dynamics of guidelines and, based on this manually defined guideline specifications, we use a MDD-based tool chain to automatically process them to generate the input model of a model checker. The model checker takes the resulted model together with the specific guideline requirements, and verifies whether the guideline fulfils such properties.
The overall framework has been implemented as an Eclipse plug-in named GBDSSGenerator which, particularly, starting from the UML statechart representing a guideline, allows the verification of the guideline against specific requirements. Additionally, we have established a pattern-based approach for defining commonly occurring types of requirements in guidelines. We have successfully validated our overall approach by verifying properties in different clinical guidelines resulting in the detection of some inconsistencies in their definition.
The proposed framework allows (1) the authoring and (2) the verification of clinical guidelines against specific requirements defined based on a set of property specification patterns, enabling non-experts to easily write formal specifications and thus easing the verification process.
本研究旨在提供一个框架，以支持临床指南的编写和验证。该框架是一个更大的研究项目的一部分，旨在改善临床指南在日常临床实践中的表示、质量和应用。
指南的验证过程基于（1）模型检查技术，以验证指南在其定义中的语义错误和不一致性，（2）结合模型驱动开发（MDD）技术，使我们能够自动处理手动创建的指南规范和时间逻辑语句，以检查和验证这些规范，使验证过程更快且具有成本效益。特别是，我们使用 UML 状态图来表示指南的动态，并基于此手动定义的指南规范，使用基于 MDD 的工具链自动处理它们，以生成模型检查器的输入模型。模型检查器将生成的模型与特定的指南要求一起使用，并验证指南是否满足这些属性。
整个框架已实现为一个名为 GBDSSGenerator 的 Eclipse 插件，特别是从表示指南的 UML 状态图开始，允许根据特定要求验证指南。此外，我们已经建立了一种基于模式的方法来定义指南中常见类型的要求。我们已经通过验证不同临床指南中的属性成功验证了我们的整体方法，从而在其定义中检测到一些不一致。
所提出的框架允许（1）编写和（2）根据一组属性规范模式验证临床指南是否符合特定要求，使非专家能够轻松编写正式规范，从而简化验证过程。
