面向医疗器械软件产品家族的形式化开发与验证

Each user has particular medical conditions and evolves in a different environment than another. Therefore, medical device manufacturers need to produce families of similar products that have common features but present variability to fit classes of users. Hence, instead of developing a single product they develop a family of similar products. Both regulators and manufacturers eagerly need a technique to guarantee the quality of the product family of medical device software. However, current formal methods cannot fully meet this requirement...This project intends to propose a refinement-based methodology for developing product family of medical device software. It covers requirements, implementation, to testing. We will also study the composition and reconstruction methodology of features, and the specification generation technique of product families, in order to reuse features in the process of development. Moreover, the technique of generating test cases from formal specification of product families will be studied, for the purpose that regulators can use them to test the product families that are produced by various manufacturers. Finally, the complementary approach of theorem proving, model checking, and constraint solving will be studied to improve the verification capabilities.

考虑到用户的差异性和环境的演化性，医疗器械软件的开发通常包括一系列既有共同功能又有差异功能的产品家族，而非单个软件产品。虽然监管者与生产者都迫切的希望医疗器械软件的质量能够得到保障，但是当前的形式化开发方法并不能为产品家族的开发提供足够的技术支持。..本项目拟提出一个面向产品家族精化开发方法的开发框架，覆盖需求、实现、测试等不同阶段，使其能适用于医疗器械软件领域；基于该框架，研究形式化产品家族的组合、重构，及相应的规格说明生成方法，以实现产品家族开发过程中的功能重用；基于形式化的规格说明模型，研究产品家族测试用例生成方法，使监管者可以对各产商所生产的产品家族进行检测；研究验证过程中的定理证明、模型检查、约束求解的互补方法，以提高验证的处理能力。

医疗器械软件的开发通常包括一系列既有共同功能，又有差异功能的产品家族，而非单个软件产品。本项目面向产品家族开发方法，提出形式化产品家族的精化、组合等方法，以实现产品家族开发过程中的功能重用；本项目提出混合系统的时间约束建模方法，适用于医疗器械软开发。在理论的基础上，我们为以上的方法提供了工具原型。