Verification of quasi-synchronous systems with Uppaal

扫码查看

原文链接

NETL

外文摘要：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。

外文关键词：

ClocksJitterModelingProtocolsReal-time systemsSwitchesSynchronizationAADLPilot Flying systemUppaalmodel checkingquasi-synchronousverification

作者：

Bhattacharyya, S.、Miller, S.、Yang, J.、Smolka, S.、Meng, B.、Sticksel, C.、Tinelli, C.

展开 >

作者单位：

Rockwell Collins, Advanced Technology Center, Cedar Rapids, IA

会议名称：

IEEE/AIAA Digital avionics systems conference

会议地点：

Colorado Springs, CO(US)

会议母体文献：

2014 IEEE/AIAA 33rd Digital avionics systems conference: Designing an Air Transportation System with Multi-Level Resilience

页码：

8A4-1-8A4-12

出版时间：

2014

DOI：

10.1109/DASC.2014.6979532