复杂交互系统形式化验证的概念工作产品语义模型
Semantic based model of Conceptual Work Products for formal verification of complex interactive systems
摘要：
许多临床工作流程依赖于交互式计算机系统，用于高技术性、概念性的工作产品，例如诊断、治疗计划、护理协调和病例管理。我们描述了一个自动逻辑推理机来验证这些高度技术性的，但抽象的，工作产品是必不可少的照顾客观规范。概念性的工作产品规格作为一个基本的输出要求，必须清楚地陈述，正确和可解决的。这种规范具有战略重要性，因为反过来，它们使系统模型检验能够验证用户过程所采用的机器功能实际上能够实现这些抽象产品。我们选择多发性硬化症（MS）门诊患者的病例管理作为我们的用例，因为它具有挑战性的复杂性。作为第一步，我们说明了如何从UML的图形类和状态图可以开发和批评与主题专家作为规范的概念工作产品的情况下管理。一个关键特性是规范必须是声明性的，因此独立于任何过程或技术。我们的工作领域本体与语义网的工具，需要翻译UML类和状态图的自动推理的可解性验证。然后，可解模型将准备好用于随后对人类程序和机器功能的系统进行模型检验。我们使用了表达规则语言SPARQL推理符号（SPIN）来开发UML类图、状态机及其交互的形式化表示。利用SPIN证明了静态概念和动态概念相互作用的一致性。我们讨论了如何将新的SPIN规则引擎合并到对象管理组（OMG）本体定义元模型（ODM）中
英文摘要：
Many clinical workflows depend on interactive computer systems for highly technical, conceptual work products, such as diagnoses, treatment plans, care coordination, and case management. We describe an automatic logic reasoner to verify objective specifications for these highly technical, but abstract, work products that are essential to care. The conceptual work products specifications serve as a fundamental output requirement, which must be clearly stated, correct and solvable. There is strategic importance for such specifications because, in turn, they enable system model checking to verify that machine functions taken with user procedures are actually able to achieve these abstract products. We chose case management of Multiple Sclerosis (MS) outpatients as our use case for its challenging complexity. As a first step, we illustrate how graphical class and state diagrams from UML can be developed and critiqued with subject matter experts to serve as specifications of the conceptual work product of case management. A key feature is that the specification must be declarative and thus independent of any process or technology. Our Work Domain Ontology with tools from Semantic Web is needed to translate UML class and state diagrams for verification of solvability with automatic reasoning. The solvable model will then be ready for subsequent use with model checking on the system of human procedures and machine functions. We used the expressive rule language SPARQL Inferencing Notation (SPIN) to develop formal representations of the UML class diagram, the state machine, and their interactions. Using SPIN, we proved the consistency of the interactions of static and dynamic concepts. We discussed how the new SPIN rule engine could be incorporated in the Object Management Group (OMG) Ontology Definition Metamodel (ODM)
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
