时序需求的正式验证
时序需求的正式验证
提问于 2012-11-20 13:43:09
我知道不同的正式验证工具用于验证程序的属性(例如，SPIN模型检查器)。在实时嵌入式系统中，有没有通用的工具/方法来验证时序需求？例如：“此算法必须始终在50ms内终止”。这种类型的验证通常是如何完成的？
回答 2
Stack Overflow用户
回答已采纳
发布于 2012-11-21 00:09:21
在给定所有任务的激活延迟和截止日期的情况下，速率单调分析在确定系统是否可调度时非常有用。有一些软件包可以为您处理数字，但我认为其中涉及的数学运算并不超出电子表格的范围。
除此之外，您提到的技术需求类型可能很难验证。即使您有可见性来测量算法处于活动状态的时间量，通常也不可能测试所有可能的场景来验证从未超过截止日期。
我在心脏起搏器和航空电子设备等关键应用中所做的是设计算法，使其不会超过所需的截止日期。这可以通过限制它在一次激活中可以处理的数据量来完成，或者让函数自己计时并在超过截止日期时提前终止(并返回错误)。我希望这能帮到你。
Stack Overflow用户
发布于 2014-05-03 14:41:09
如果工具集用于执行定时系统的模型检查，则有UPPAAL工具。它基于时间自动机的理论。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/13467240
复制相关文章
相似问题
腾讯云开发者
