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

Authors Flavio Ferrarotti
Josef Pichler
Michael Moser
Georg Buchgeher
Editors Klaus-Dieter Schewe
Neeraj Kumar Singh
Title Extracting high-level system specifications from source code via abstract state machines
Booktitle Model and Data Engineering - Proc. MEDI 2019
Type in proceedings
Publisher Springer
Series Lecture Notes in Computer Science
Volume 11815
ISBN 978-3-030-32064-5
DOI 10.1007/978-3-030-32065-2_19
Month November
Year 2019
Pages 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.