Stepwise abstraction of high-level system specifications from source code

Abstract We are interested in specifications which provide a consistent high-level view of systems. They should abstract irrelevant details and provide a precise and complete description of the behaviour of the system. This view of software specification can naturally be expressed by means of Gurevich’s Abstract State Machines (ASMs). There are many known benefits of such an approach to system specifications for software engineering and testing. In practice however, such specifications are rarely generated and/or maintained during software development. Addressing this problem, we present an exploratory study on (semi-)automated extraction of high-level software specifications by means of ASMs. We devise a method consisting in two phases. In the first phase we propose fully automated transformations from source code to base-level ASM specifications with the same core functionality. We present a prototype of an implementation of this phase which transforms Java code into base-level ASM specifications. The second phase consists in incrementally applying sound semi-automated abstraction procedures for ASMs to derive higher-level specifications, starting from the base-level ASM specification obtained in the first phase. This is by no means a trivial task. It opens up new and interesting research questions. We discuss possible methodologies to approach this task and provide a proof of concept in the form of elaborated and detailed examples. We argue that this process can be done in a (semi-)automated way and thus result in a valuable tool to improve the current software engineering practices.