基于语义的概念性工作产品模型用于复杂交互系统的形式化验证
软件工程
2020-08-05 v1 机器学习
摘要
许多临床工作流依赖于交互式计算机系统来处理高度技术性的概念性工作产品，例如诊断、治疗计划、护理协调和病例管理。我们描述了一种自动逻辑推理器，用于验证这些对护理至关重要但抽象的高度技术性工作产品的客观规范。概念性工作产品规范作为基本输出需求，必须表述清晰、正确且可解。此类规范具有战略重要性，因为反过来它们使得系统模型检测能够验证机器功能与用户规程相结合确实能够实现这些抽象产品。我们选取多发性硬化症（MS）门诊病例管理作为用例，因其具有挑战性的复杂性。作为第一步，我们展示了如何与领域专家共同开发并评审来自 UML 的图形化类图与状态图，以作为病例管理概念性工作产品的规范。一个关键特征是规范必须是声明式的，从而独立于任何过程或技术。我们需要借助语义网工具的领域本体（Work Domain Ontology）来翻译 UML 类图与状态图，以通过自动推理验证可解性。可解模型随后将准备好用于人机规程与机器功能的系统模型检测。我们使用富有表达力的规则语言 SPARQL Inferencing Notation (SPIN) 来开发 UML 类图、状态机及其交互的形式化表示。利用 SPIN，我们证明了静态与动态概念交互的一致性。我们讨论了如何将新的 SPIN 规则引擎整合进对象管理组（OMG）本体定义元模型（ODM）。
引用
@article{arxiv.2008.01623,
title = {Semantic based model of Conceptual Work Products for formal verification of complex interactive systems},
author = {Mohcine Madkour and Keith Butler and Eric Mercer and Ali Bahrami and Cui Tao},
journal= {arXiv preprint arXiv:2008.01623},
year = {2020}
}