A topological formal treatment for scenario-based software specification of concurrent real-time systems

TL;DR

This paper introduces a topological approach to formalize scenario-based specifications for concurrent real-time systems, aiming to detect deadlocks early in the development process using a prototype that integrates topology with message sequence scenarios.

Contribution

It presents a novel integration of topological methods with scenario-based requirements to improve deadlock detection in real-time systems.

Findings

Prototype successfully detects deadlocks in specified scenarios.

Topological methods enhance early verification of real-time requirements.

Integration of topology with message sequence charts is feasible and effective.

Abstract

Real-time systems are computing systems in which the meeting of their requirements is vital for their correctness. Consequently, if the real-time requirements of these systems are poorly understood and verified, the results can be disastrous and lead to irremediable project failures at the early phases of development. The present work addresses the problem of detecting deadlock situations early in the requirements specification phase of a concurrent real time system, proposing a simple proof-of-concepts prototype that joins scenario-based requirements specifications and techniques based on topology. The efforts are concentrated in the integration of the formal representation of Message Sequence Chart scenarios into the deadlock detection algorithm of Fajstrup et al., based on geometric and algebraic topology.