This paper proposes a new methodology for early validation of high-level requirements on cyber-physical systems with the aim of improving their quality and, thus, lowering chances of specification errors propagating into later stages of development where it is much more expensive to fix them. The paper presents a transformation of a real-world requirements specification of a medical device$-$a PCA pump$-$into an Event Calculus model that is then evaluated using answer set programming and the s(CASP) system. The evaluation under s(CASP) allowed deductive as well as abductive reasoning about the specified functionality of the PCA pump on the conceptual level with minimal implementation or design dependent influences, and led to fully-automatically detected nuanced violations of critical safety properties. Further, the paper discusses scalability and non-termination challenges that had to be faced in the evaluation and techniques proposed to (partially) solve them. Finally, ideas for improving s(CASP) to overcome its evaluation limitations that still persist as well as to increase its expressiveness are presented.

翻译：本文提出一种用于信息物理系统高层需求早期验证的新方法，旨在提升需求质量，从而降低规格错误蔓延至开发后期阶段的可能性——在后期阶段修复错误的成本将显著增加。本文通过将真实医疗设备（患者自控镇痛泵）的需求规格转化为事件演算模型，并利用答案集编程及s(CASP)系统进行评估验证。在s(CASP)框架下的评估支持对PCA泵概念层功能规范的演绎与溯因推理，且最大程度减少了实现或设计依赖的影响，最终实现了对关键安全属性细微违规情形的全自动检测。此外，本文探讨了评估过程中面临的可扩展性与非终止性挑战，并提出了（部分）解决这些挑战的技术方案。最后，针对s(CASP)系统当前仍存在的评估局限性及表达能力不足的问题，提出了相应的改进思路。