Early Validation of High-level System Requirements with Event Calculus and Answer Set Programming

本论文提出了一种新的方法，用于早期验证物理系统的高级需求，旨在提高其质量，从而降低规范错误传播到开发后期的机会，因为在后期修复它们的代价更高。本文将医疗设备（PCA泵）的真实需求规范转化为事件演算模型，然后使用答案集编程和s(CASP)系统进行评估。在s(CASP)的评估下，可以对PCA泵的指定功能进行演绎和诱导推理，最终自动检测到关键安全属性的微妙违规。此外，本文还讨论了评估中所面临的可扩展性和非终止挑战以及提出的部分解决方案。最后，本文提出了改进s(CASP)以克服其评估限制并增加其表达能力的想法。

本文旨在提出一种新的方法来早期验证物理系统的高级需求，以提高其质量并降低规范错误传播到后期开发阶段的可能性。

本文提出了将实际需求规范转化为事件演算模型，并使用答案集编程和s(CASP)系统进行评估的方法。这种方法可以在概念层面上进行演绎和缺省推理，从而发现关键安全属性的微妙违规。

本文讨论了评估中所面临的可扩展性和非终止挑战，并提出了解决方案。实验设计合理，使用了真实数据集，结果表明该方法可以自动检测到关键安全属性的微妙违规。本文还提出了改进s(CASP)系统以增加其表现力和克服其评估限制的想法。

最近的相关研究包括使用模型检查器验证物理系统和使用形式化方法验证软件系统。