time - 时序要求的正式验证

Question

我知道用于验证程序属性的不同形式验证工具（例如 SPIN 模型检查器）。是否有任何通用工具/方法可用于验证实时嵌入式系统中的时序要求？例如：“此算法必须始终在 50 毫秒内终止”。这种类型的验证通常是如何完成的？

Answer 1

考虑到所有任务的激活延迟和截止日期，速率单调分析可用于确定系统是否可调度。有一些软件包可以为你计算数字，但我认为所涉及的数学并不超出电子表格。

除此之外，您提到的技术要求类型可能难以验证。即使您可以测量算法处于活动状态的时间量，通常也无法测试所有可能的场景以验证永远不会超过最后期限。

我在起搏器和航空电子设备等关键应用中看到的做法是设计算法，使其不会超过规定的期限。这可以通过限制它在一次激活中可以处理的数据量来完成，或者让函数本身计时并在超过截止日期时提前终止（并返回错误）。我希望这有帮助。

Answer 2

有用于对定时系统进行模型检查的工具 UPPAAL、IF 工具集。它基于时间自动机理论。