Combining solution reuse and bound tightening for efficient analysis of evolving systems
Combining solution reuse and bound tightening for efficient analysis of evolving systems
复制标题
结合解决方案重用和边界紧缩，以有效分析不断发展的系统
DOI：
10.1145/3533767.3534399
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Bagheri, Hamid
中科院分区：
文献类型：
--
作者：
Stevens, Clay;Bagheri, Hamid
长期以来，软件工程师一直采用形式化验证来确保其系统设计的安全性和有效性。随着系统的变化--通常是通过可预测的、特定于领域的操作--它们的模型也必须变化，这就要求系统设计者在类似的系统模型上重复执行相同的形式化验证。最先进的形式验证技术在规模上可能是昂贵的，其成本会因重复分析而成倍增加。本文提出了一种新的分析技术-在一个名为SoRBoT的工具中实现-它可以自动确定特定于域的优化，可以显着降低重复分析不断发展的系统的成本。与所有先前的方法不同，这些方法专注于收紧分析边界或重用所有或部分先前的解决方案，SoRBoT的特定领域优化的自动化推导结合了解决方案重用和边界收紧的好处，同时避免了每个的主要陷阱。我们通过实验评估SoRBoT对国家的最先进的技术验证不断发展的规范，证明SoRBoT大大超过这些国家的最先进的技术的运行时性能，同时只引入一个可以忽略不计的开销，相比之下，昂贵的额外计算所需的国家的最先进的验证技术。
Software engineers have long employed formal verification to ensure the safety and validity of their system designs. As the system changes---often via predictable, domain-specific operations---their models must also change, requiring system designers to repeatedly execute the same formal verification on similar system models. State-of-the-art formal verification techniques can be expensive at scale, the cost of which is multiplied by repeated analysis. This paper presents a novel analysis technique---implemented in a tool called SoRBoT---which can automatically determine domain-specific optimizations that can dramatically reduce the cost of repeatedly analyzing evolving systems. Different from all prior approaches, which focus on either tightening the bounds for analysis or reusing all or part of prior solutions, SoRBoT's automated derivation of domain-specific optimizations combines the benefits of both solution reuse and bound tightening while avoiding the main pitfalls of each. We experimentally evaluate SoRBoT against state-of-the-art techniques for verifying evolving specifications, demonstrating that SoRBoT substantially exceeds the run-time performance of those state-of-the-art techniques while introducing only a negligible overhead, in contrast to the expensive additional computations required by the state-of-the-art verification techniques.
登录
查看更多内容
基于灵活的 SAT 框架，用于增量有界升级检查
DOI：
--
发表时间：
2017
期刊：
International Journal on Software Tools for Technology Transfer (STTT)
影响因子：
--
作者：
Grigory Fedyukovich;Ondřej Šerý;N. Sharygina
通讯作者：
N. Sharygina
DOI：
10.1007/978-3-030-45234-6_2
发表时间：
2020-03-13
期刊：
Fundamental Approaches to Software Engineering
影响因子：
--
作者：
Zheng G;Bagheri H;Rothermel G;Wang J
通讯作者：
Wang J
Vac - 基于管理角色的访问控制策略的验证器
DOI：
--
发表时间：
2014
期刊：
International Conference on Computer Aided Verification
影响因子：
--
作者：
A. L. Ferrara;P. Madhusudan;Truc L. Nguyen;G. Parlato
通讯作者：
G. Parlato
工业关键系统的正式方法和工具
DOI：
--
发表时间：
2022
期刊：
International Journal on Software Tools for Technology Transfer (STTT)
影响因子：
--
作者：
Maurice H. ter Beek;K. Larsen;D. Ničković;T. Willemse
通讯作者：
T. Willemse
业务工作流程和基于角色的访问控制系统的形式验证
DOI：
--
发表时间：
2007
期刊：
International Conference on Emerging Security Information, Systems and Technologies
影响因子：
--
作者：
A. Dury;S. Boroday;A. Petrenko;V. Lotz
通讯作者：
V. Lotz