Abstraction Modulo Stability

The analysis of legacy systems requires the automated extraction of high-level specifications. We propose a framework, called Abstraction Modulo Stability, for the analysis of transition systems operating in stable states, and responding with run-to-completion transactions to external stimuli. The a...

Full description

Saved in:
Bibliographic Details
Published in:Formal methods in system design 2024-09
Main Authors: Becchi, Anna, Cimatti, Alessandro
Format: Article
Language:English
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The analysis of legacy systems requires the automated extraction of high-level specifications. We propose a framework, called Abstraction Modulo Stability, for the analysis of transition systems operating in stable states, and responding with run-to-completion transactions to external stimuli. The abstraction captures, in the form of a finite state machine, the effects of external stimuli on the system state. This approach is parametric on a set of predicates of interest and on the definition of stability. We consider some possible stability definitions, which yield different practically relevant abstractions, and propose parametric algorithms for abstraction computation. The framework is evaluated in terms of expressivity and adequacy within an industrial project with the Italian Railway Network, on reverse engineering of relay-based interlocking circuits to extract specifications for a computer-based reimplementation.
ISSN:0925-9856
1572-8102
DOI:10.1007/s10703-024-00461-2