Verification of recovered software architectures

A common technique employed by software developers is the use of log files to generate traces of observed software behavior. As a resource for reverse engineering, a log file has the advantage of being an accurate account of software behavior. Model checking approaches work by using exploration to determine whether certain safety and liveness conditions are satisfied by a finite-state model. In this paper we describe an approach that combines the use of model checking and log file analysis to facilitate verification of recovered models.