APSEC 2022
Tue 6 - Fri 9 December 2022
Wed 7 Dec 2022 14:30 - 14:50 at Room2 - Model Checking 2 Chair(s): Hideto Ogawa

Avionics embedded systems are subjected to stringent timing requirements to be verified. Evaluating if messages meet their timing requirements, such as the latency constraint, is of the highest importance from the design stage of avionics systems. End-to-end latency of messages is an important design parameter that needs to be within specified bounds for the correct functioning of avionics systems. In this paper, we define the “SysML Flow Model Efor the first time. Subsequently, we propose an approach to transfer the SysML Flow Model to a timed automaton, to perform schedulability and end-to-end latency verification. This fills an important gap in the method toolbox of the safety-critical domain engineer. The definition has a profound potential to broaden the use of Model-Driven Architecture and its well-known advantages in safety-critical avionics applications. Finally, we apply this technique to an industrial case of a flight management system.

Wed 7 Dec

Displayed time zone: Osaka, Sapporo, Tokyo change

14:30 - 15:40
Model Checking 2Technical Track at Room2
Chair(s): Hideto Ogawa Hitachi Ltd.
14:30
20m
Paper
SysML Flow Model
Technical Track
Guohuan Ding East China Normal University, Jing Liu East China Normal University
14:50
20m
Paper
Tuning SAT solvers for LTL Model Checking
Technical Track
Anissa Kheireddine LRDE, Etienne Renault LRDE, Souheib Baarir Université Paris Ouest Nanterre La Défense/LIP6
15:10
20m
Paper
Bounded Model Checking of Synchronous Reactive Models in Ptolemy II
Technical Track
Xiaozhen Zhang Dalian University of Technology, Zhaoming Yang Dalian University of Technology, Hui Kong Huawei Technologies Co., Ltd., Weiqiang Kong Dalian University of Technology