Conference proceeding
Verification of quasi-synchronous systems with Uppaal
2014 IEEE/AIAA 33rd Digital Avionics Systems Conference (DASC), pp.8A4-1-8A4-12
10/2014
DOI: 10.1109/DASC.2014.6979532
Abstract
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 systems-engineering 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.
Details
- Title: Subtitle
- Verification of quasi-synchronous systems with Uppaal
- Creators
- S Bhattacharyya - Advanced Technology CenterS Miller - Advanced Technology CenterJ Yang - Stony Brook UniversityS Smolka - Stony Brook UniversityB Meng - University of IowaC Sticksel - University of IowaC Tinelli - University of Iowa
- Resource Type
- Conference proceeding
- Publication Details
- 2014 IEEE/AIAA 33rd Digital Avionics Systems Conference (DASC), pp.8A4-1-8A4-12
- Publisher
- IEEE
- DOI
- 10.1109/DASC.2014.6979532
- ISSN
- 2155-7195
- eISSN
- 2155-7209
- Language
- English
- Date published
- 10/2014
- Academic Unit
- Computer Science
- Record Identifier
- 9984259433702771
Metrics
6 Record Views