SMAVE RV

动态对象关系验证

围绕运行过程中不断变化的对象集合建立量化约束，表达对象间安全距离、协同行为和异常关系，帮助工程人员在系统执行期间持续检查复杂动态场景中的安全属性。

有界历史状态分析

通过 last、prev、history 等历史访问机制引用信号历史值，并由存储分析计算所需历史深度，在满足时序属性验证需求的同时控制长时间运行中的内存开销。