Modern defense systems are complex distributed software systems implemented over heterogeneous and constantly evolving hardware and software platforms. Distributed agreement protocols are often developed exploiting the fact that their systems are quasi-synchronous, where even though the clocks of the different nodes are not synchronized, they all run at the same rate, or multiples of the same rate, modulo their drift and jitter. This paper describes an effort to provide systems designers and engineers with an intuitive modeling environment that allows them to specify the highlevel architecture and synchronization logic of quasi-synchronous systems using widely available systemsengineering notations and tools. To this end, a translator was developed that translates system architectural models specified in a subset of SysML into the Architectural Analysis and Description Language (AADL). Translators were also developed that translate the AADL models into the input language of the Uppaal and Kind model checkers. The Uppaal model checker. supports the modeling, verification, and validation of real-time systems modeled as a network of timed automata. This paper focuses on the challenges encountered in translating from AADL to Uppaal, and illustrates the overall approach with a common avionics example: the Pilot Flying System.
Verification of quasi-synchronous systems with Uppaal
01.10.2014
477721 byte
Aufsatz (Konferenz)
Elektronische Ressource
Englisch
Online and Proactive Vehicle Rerouting with Uppaal Stratego
Transportation Research Record | 2021
|Schedulability Analysis of Distributed Multicore Avionics Systems with UPPAAL
AIAA | 2019
|Introducing Liveness into Multi-lane Spatial Logic lane change controllers using UPPAAL
DOAJ | 2018
|Introducing Liveness into Multi-lane Spatial Logic lane change controllers using UPPAAL
ArXiv | 2018
|