Title

Model Checking in the Absence of Code, Model and Properties

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.

Discipline

Software Engineering

Research Areas

Software Systems

Publication

5th Asian Symposium on Programming Languages and Systems (APLAS) (Poster Track)

City or Country

Singapore

Additional URL

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.100.3425