《面向醫療器械軟體產品家族的形式化開發與驗證》是依託上海大學，由蘇雯擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：面向醫療器械軟體產品家族的形式化開發與驗證
- 項目類別：青年科學基金項目
- 項目負責人：蘇雯
- 依託單位：上海大學
中文摘要,結題摘要,
中文摘要
考慮到用戶的差異性和環境的演化性，醫療器械軟體的開發通常包括一系列既有共同功能又有差異功能的產品家族，而非單個軟體產品。雖然監管者與生產者都迫切的希望醫療器械軟體的質量能夠得到保障，但是當前的形式化開發方法並不能為產品家族的開發提供足夠的技術支持。..本項目擬提出一個面向產品家族精化開發方法的開發框架，覆蓋需求、實現、測試等不同階段，使其能適用於醫療器械軟體領域；基於該框架，研究形式化產品家族的組合、重構，及相應的規格說明生成方法，以實現產品家族開發過程中的功能重用；基於形式化的規格說明模型，研究產品家族測試用例生成方法，使監管者可以對各產商所生產的產品家族進行檢測；研究驗證過程中的定理證明、模型檢查、約束求解的互補方法，以提高驗證的處理能力。
結題摘要
醫療器械軟體的開發通常包括一系列既有共同功能，又有差異功能的產品家族，而非單個軟體產品。本項目面向產品家族開發方法，提出形式化產品家族的精化、組合等方法，以實現產品家族開發過程中的功能重用；本項目提出混合系統的時間約束建模方法，適用於醫療器械軟開發。在理論的基礎上，我們為以上的方法提供了工具原型。
