一般来说,这种验证的问题出现,因为应用程序很大,导致一个扩展的问题。应用程序是如此巨大,以至于使验证过程非常复杂。因此,验证在很长一段时间,更精确地超过24小时。
这么大的应用程序的第一个建议是使用错误发现者。因为错误发现者并不试图证明的东西,它的工作更容易,所以它可以使用巨大的应用。即使你计划使用验证的代码,我们建议使用错误仪之前,因为它将帮助你识别将检测后的运行时错误代码验证:最好不要以来运行时错误在这段代码的代码都被验证,更方便的找到他们之前的错误发现者。修复运行时错误早些时候会节省你的时间。
如果你想继续使用验证的代码,那么我们建议验证拆分成几个部分:更少的代码一个验证意味着更少的复杂性,因此更少的规模问题。
额外的建议与代码验证是使用缩放选项,即选项减少复杂性和应该帮助绕过规模问题。这些选项有:
•“优化大型静态初始化器”(-no-fold)
•如果您使用任务:“减少任务复杂性”(-lightweight-thread-model)
•验证内部结构的“深度”(-k-limiting)。使用值2。
•“精度水平”(o)。使用值0。
它可以被视为一个缩放行为Polyspace代码验证。也请阅读文档附加到MATLAB回答:当面临扩展行为Polyspace代码验证?MATLAB的答案——MATLAB中央(mathworks.com)
