An ASM-based Characterization of Starvation-free Systems

TL;DR

This paper introduces an ASM-based framework to characterize and analyze starvation-free properties in systems, enriching the formalism with practical tools for identifying starvation issues.

Contribution

It provides the first ASM-based formalization of starvation-freedom, including a necessary condition and the concept of vulnerable rules for operational analysis.

Findings

Formalization of starvation as a necessary ASM condition

Introduction of vulnerable rules for analysis

Enhanced ASM framework for starvation detection

Abstract

Abstract State Machines (ASMs) have been successfully applied for modeling critical and complex systems in a wide range of application domains. However, unlike other well-known formalisms, e.g. Petri nets, ASMs lack inherent, domain-independent characterisations of computationally important properties. Here, we provide an ASM-based characterisation of the starvation-free property. The classic, informal notion of starvation, usually provided in literature, is analysed and expressed as a necessary condition in terms of ASMs. Thus, we enrich the ASM framework with the notion of vulnerable rule as a practical tool for analysing starvation issues in an operational fashion