Skip to main content
Article
Model Checking in the Absence of Code, Model and Properties
5th Asian Symposium on Programming Languages and Systems (APLAS) (Poster Track)
  • David LO, Singapore Management University
  • Siau-Cheng Khoo, National University of Singapore
Publication Type
Report
Publication Date
11-2007
Abstract
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.
City or Country
Singapore
Additional URL
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.100.3425
Citation Information
David LO and Siau-Cheng Khoo. "Model Checking in the Absence of Code, Model and Properties" 5th Asian Symposium on Programming Languages and Systems (APLAS) (Poster Track) (2007)
Available at: http://works.bepress.com/david_lo/53/