A Test Generation Framework for Distributed Fault-Tolerant Algorithms
Alwyn E. Goodloe, David H. Bushnell, Paul S. Miner, Corina S. Păsăreanu · NASA Technical Reports Server (NASA) · 2009
Heavyweight formal methods such as theorem proving have been successfully applied to the analysis of safety critical fault-tolerant systems. Typically, the models and proofs performed during such analysis do not inform the testing process of actual implementations. We propose a framework for generating test vectors from specifications written in the Prototype Verification System (PVS). The methodology uses a translator to produce a Java prototype from a PVS specification. Symbolic (Java) PathFinder is then employed to generate a collection of test cases. A small example is employed to illustrate how the framework can be used in practice.