Hybrid SynchAADL: Modeling and Formal Analysis of Virtually Synchronous CPSs in AADL
Jaehun Lee, Sharon Kim, Kyungmin Bae, Peter Csaba Ölveczky
Abstract
Abstract We present the $$\textsc {Hybrid}\textsc {Synch}\textsc {AADL}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mrow><mml:mi>H</mml:mi><mml:mstyle><mml:mi>Y</mml:mi><mml:mi>B</mml:mi><mml:mi>R</mml:mi><mml:mi>I</mml:mi><mml:mi>D</mml:mi></mml:mstyle><mml:mi>S</mml:mi><mml:mstyle><mml:mi>Y</mml:mi><mml:mi>N</mml:mi><mml:mi>C</mml:mi><mml:mi>H</mml:mi></mml:mstyle><mml:mi>AADL</mml:mi></mml:mrow></mml:math> modeling language and formal analysis tool for virtually synchronous cyber-physical systems with complex control programs, continuous behaviors, bounded clock skews, network delays, and execution times. We leverage the Hybrid PALS equivalence, so that it is sufficient to model and verify the simpler underlying synchronous designs. We define the $$\textsc {Hybrid}\textsc {Synch}\textsc {AADL}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mrow><mml:mi>H</mml:mi><mml:mstyle><mml:mi>Y</mml:mi><mml:mi>B</mml:mi><mml:mi>R</mml:mi><mml:mi>I</mml:mi><mml:mi>D</mml:mi></mml:mstyle><mml:mi>S</mml:mi><mml:mstyle><mml:mi>Y</mml:mi><mml:mi>N</mml:mi><mml:mi>C</mml:mi><mml:mi>H</mml:mi></mml:mstyle><mml:mi>AADL</mml:mi></mml:mrow></mml:math> language as a sublanguage of the avionics modeling standard AADL for modeling such designs in AADL, and demonstrate the effectiveness of $$\textsc {Hybrid}\textsc {Synch}\textsc {AADL}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mrow><mml:mi>H</mml:mi><mml:mstyle><mml:mi>Y</mml:mi><mml:mi>B</mml:mi><mml:mi>R</mml:mi><mml:mi>I</mml:mi><mml:mi>D</mml:mi></mml:mstyle><mml:mi>S</mml:mi><mml:mstyle><mml:mi>Y</mml:mi><mml:mi>N</mml:mi><mml:mi>C</mml:mi><mml:mi>H</mml:mi></mml:mstyle><mml:mi>AADL</mml:mi></mml:mrow></mml:math> on a number of applications.