SBRDL: A System Behavioral Requirements Description Language for Aerospace Embedded Control Software

Embedded control software is the core of aerospace systems, executing mission-critical functions under stringent real-time constraints. Ensuring the quality of such software is paramount, as failures can lead to catastrophic consequences. While precise requirement specification is recognized as the cornerstone of software quality, specifying temporal behavioral requirements remains a significant challenge. Existing general-purpose specification languages often lack direct support for domain-specific timing and behavioral patterns, such as exclusive waits or periodic execution. Consequently, specifications become overly verbose and difficult for industry practitioners to comprehend. To address these limitations, this paper proposes System Behavioral Requirements Description Language (SBRDL), a novel specification language derived from a systematic analysis of temporal behavioral knowledge in the aerospace domain. SBRDL is function-centric and defines rigorous formal semantics. It supports rich temporal constraints (e.g. run-time limits, release triggers) and compositional operators (e.g. parallelism, periodic execution and interrupt-driven preemption), enabling the concise construction of complex behaviors. To facilitate usability, we provide tool support for specification authoring based on the Xtext framework and specification validation via UPPAAL. The approach is validated using a Sun Search System case study, where the SBRDL specification is transformed into UPPAAL Timed Automata (TA). This transformation allows for the formal verification of critical properties, ensuring the correctness and consistency of the temporal behavioral requirements.