Advanced Symbolic Analysis Tools for Fault-Tolerant Integrated Distributed Systems

[摘要] The project aims to develop advanced model-checking algorithms and tools to automate the verification of fault-tolerant distributed systems for avionics. We present a new method called Property-Directed K-Induction (PD-KIND) for synthesizing K-inductive invariants of state-transition systems. PD-KIND builds upon Satifiability Modulo Theories (SMT) to generalize Bradley's IC3 method and its variants. This method is implemented in a new tool called SALLY. Case studies show that PD-KIND can automatically verify fault-tolerant algorithms under a variety of fault models and that SALLY is competitive with other SMT-based model checkers.

[发布日期] 2018-05-01

[学科分类] 计算机系统及组成

[关键词] FAULT TOLERANCE;SYSTEMS INTEGRATION;AVIONICS