使用 SPARK Ada 验证用户界面：以 T34 注射驱动器为案例研究

安全与关键系统的增加改善了医疗保健。由于存在伤害风险，此类系统需遵循严格的指南与合规要求。这些安全措施确保了无缝体验，并降低了对最终用户的风险。美国食品药品监督管理局和英国国家医疗服务体系等机构分别制定了国际标准和能力框架，以确保行业符合这些安全关切。医疗设备制造主要关注标准。因此，这些标准现在提倡在医疗设备的用户交互中考虑更好的人为因素。这迫使制造商在开发过程中依赖大量的测试和审查来覆盖许多此类因素。遗憾的是，许多人因风险直到在现实中进行适当测试时才会被发现，这对于像 T34 输液泵这样的移动设备来说可能是灾难性的。因此，在形式化方法研究上的努力可能会提出新的解决方案，在开发早期阶段预测这些错误，甚至基于标准通用模型的使用来减少其发生。这些通用开发的模型将为行业中的安全集成提供一个通用框架，并可能通过形式化验证数学证明来得到证明。本研究使用 SPARK Ada 的形式化验证工具，针对 T34 输液驱动器的行为模型进行验证。探索并实现了一个通用输液泵模型在 SPARK Ada 中的细化。作为 Ada 语言的一个子集，最终原型的验证级别使用 SPARK 进行评估。在探索潜在限制时，定义了在 SPARK Ada 中考虑用户界面设计的抽象和组件时，所提出模型的实现责任。