Extracting high-level system specifications from source code via abstract state machines

Autoren Flavio Ferrarotti
Josef Pichler
Michael Moser
Georg Buchgeher
Editoren Klaus-Dieter Schewe
Neeraj Kumar Singh
Titel Extracting high-level system specifications from source code via abstract state machines
Buchtitel Model and Data Engineering - Proc. MEDI 2019
Typ in Konferenzband
Verlag Springer
Serie Lecture Notes in Computer Science
Band 11815
ISBN 978-3-030-32064-5
DOI 10.1007/978-3-030-32065-2_19
Monat November
Jahr 2019
Seiten 267-283
SCCH ID# 19045
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 describe, in the form of examples, an abstraction process which starts by extracting an initial ground-level ASM specification from Java source code (with the same core functionality), and ends in a high-level ASM specification at the desired level of abstraction. We argue that this process can be done in a (semi) automated way, resulting in a valuable tool to improve the current software engineering practices.