Creating models of interactive systems with the support of lightweight reverse-engineering tools

Creating formal models of interactive systems is an important step in the development process, particularly for safety-critical interactive systems. Such models can be used for a variety of software engineering purposes such as model-checking, verification, testing, refinement etc. While the use of such models at the beginning of the implementation cycle is important, it is often the case that we are interested in performing many of the same activities (particularly safety verification and testing) on systems which have been built without the use of formal methods or modelling. In order to do this we need to somehow reverse-engineer the system to generate the models post-implementation. In this paper we describe an approach we have developed to support the reverse-engineering of interactive systems and tools which support this. The tools perform partial reverse-engineering and act as a guide to the developer of the models rather than providing a fully automated solution. We motivate this by discussing the importance of what we describe as 'light-weight' tools in the engineering process.