Model Checking in the Absence of Code, Model and Properties

• Main Authors: LO, David, KHOO, Siau-Cheng
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2007
• Subjects: preliminary study; model checking; formal property; model checking tool; execution trace; software correctness; available input; binary version; temporal property; commercial off-the-shelf; automatic way; enable execution trace; instrumentation tool; widespread industrial adoption; major approach; third party vendor; Software Engineering
• Online Access: https://ink.library.smu.edu.sg/sis_research/1279; https://ink.library.smu.edu.sg/context/sis_research/article/2278/viewcontent/ModelChecking_AbCode_2007.pdf
• Institution: Singapore Management University

Model checking is a major approach in ensuring software correctness. It verifies a model converted from code against some formal properties. However, difficulties and programmers ’ reluctance to formalize formal properties have been some hurdles to its widespread industrial adoption. Also, with the advent of commercial off-the-shelf (COTS) components provided by third party vendors, model checking is further challenged as often only a binary version of the code is provided by vendors. Interestingly, latest instrumentation tools like PIN and Valgrind have enable execution traces to be collected dynamically from a running program. In this preliminary study, we investigate what can be done with model checking tools when code, model and properties are not available and the only available input is execution traces. Specifically, we combine studies on learning automata from traces and learning temporal properties from traces. The preliminary study suggests an automatic way to discover bugs using model checking tools when only execution traces are available.