Extracting High-Level System Specifications from Source Code via Abstract State Machines

Flavio Ferrarotti, Josef Pichler, Michael Moser, Georg Buchgeher

Research output: Chapter in Book/Report/Conference proceedingsConference contributionpeer-review

1 Citation (Scopus)


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.

Original languageEnglish
Title of host publicationModel and Data Engineering- 9th International Conference, MEDI 2019, Proceedings
EditorsKlaus-Dieter Schewe, Neeraj Kumar Singh
Number of pages17
ISBN (Print)9783030320645
Publication statusPublished - 2019
EventMEDI 2019 - Tuolouse, France, France
Duration: 28 Oct 201931 Oct 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11815 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceMEDI 2019
CityTuolouse, France
Internet address


Dive into the research topics of 'Extracting High-Level System Specifications from Source Code via Abstract State Machines'. Together they form a unique fingerprint.

Cite this