Approximations, anomalies and "the proof of correctness wars"
Leona F. Fass · ACM SIGSOFT Software Engineering Notes · 2004
We discuss approaches to establishing "correctness" and describe the usefulness of logic-based model checkers for producing better practical system designs. While we could develop techniques for "constructing correctness" in our theoretical behavioral-modeling research, when applied to Real World processes such as software development only approximate correctness might be established and anomalous behaviors subsequently found. This we view as a positive outcome since resultant adaptation, or flaw detection and correction, may lead to improved development and designs. We find researchers employing model checking as a formal methods tool to develop empirical techniques have reached similar conclusions. Thus we cite some applications of model checking to generate tests and detect defects in such Real World processes as aviation system development, fault-detection systems, and security.