Echo: Practical Formal Verification by Reverse Synthesis
Xiang Yin · 2012
Safe operation is crucial to safety-critical systems, such as fly-by-wire flight-control systems in aircraft.Software in these systems has to be correct, or, more precisely, the risk of being incorrect has to be reduced to an acceptable level.Ensuring the absence of implementation flaws by testing only is inadequate because it is infeasible to conduct the number of test cases required to establish a very high level of confidence.Thus formal specification and formally verified implementation are desirable.Current approaches to formal verification are powerful but not sufficiently practical.Verification techniques are difficult and time-consuming to apply, tools are of limited capabilities and cannot be integrated, and the process requires high levels of expertise.Current approaches also impose limitations on developers that make it difficult to fit formal verification into the existing development cycle.To address these problems, I develop a practical and effective approach to formal verification of the functional correctness of computer software.My approach, named Echo, relies upon and incorporates a number of powerful existing notations, tools and techniques, and distributes the verification burden over separate levels.At the core of the approach is a process called reverse synthesis in which a high-level abstract specification is extracted from the source code coupled with a low-level, detailed specification of a software system.Formal verification then involves two proofs each of which is either generated automatically or mechanically checked.These proofs are: (1) a proof that the software source code implements the low-level specification correctly; and (2) a proof that the extracted specification implies the original software system specification.The two proofs can be tackled with separate specialized techniques.It is my honor to first thank my advisor, John Knight, for the years of direction and support to my graduate study and research work.John led me into the world of dependable software systems, inspired my on research ideas, and guided me on how to approach research problems and how to write research articles.He has always been there when I needed him.I am grateful to Wes