Incremental Verification and Coverage Analysis of Strongly Distributed Systems
Elena V. Ravve, Zeev Volkovich · 2018
This chapter utilizes both software and hardware hierarchical systems as logical structures. It expresses the properties to be tested in different extensions of first-order logic. Coverage analysis is aimed to guarantee that the runs of the tests fully capture the functionality of the system. The chapter proposes a method to analyze quantitative coverage metrics, using the corresponding labeled weighted tree as a representation of the runs of the tests, as well as weighted monadic second-order logic to express the coverage metrics, and weighted tree automata as an effective tool to compute the value of the metric on the tree. It introduces the notion of strongly distributed systems and presents a uniform logical approach to incremental automated verification of such systems. The approach is based on systematic use of two logical reduction techniques: Feferman–Vaught reductions and syntactically defined translation schemes.