Publication Type

Report

Version

publishedVersion

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.

Keywords

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

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

5th Asian Symposium on Programming Languages and Systems (APLAS) (Poster Track), November 29 - December 1

First Page

1

Last Page

2

City or Country

Singapore

Copyright Owner and License

Authors

Additional URL

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

Download

Share

COinS