Formal verification of integrated modular avionics (IMA) health monitoring using timed automata

The configuration information of Integrated Modular Avionics (IMA) system includes almost all details of whole system architecture, which is used to configure the hardware interfaces, operating system, and interactions among applications to make an IMA system work correctly and reliably. It is very important to ensure the correctness and integrity of the configuration in the IMA system design phase. In this paper, we focus on modelling and verification of configuration information of IMA/ARINC653 system based on MARTE (Modelling and Analysis for Real-time and Embedded Systems). Firstly, we define semantic mapping from key concepts of configuration (such as modules, partitions, memory, process, and communications) to components of MARTE element and propose a method for model transformation between XML-formatted configuration information and MARTE models. Then we present a formal verification framework for ARINC653 system configuration based on theorem proof techniques, including construction of corresponding REAL theorems according to the semantics of those key components of configuration information and formal verification of theorems for the properties of IMA, such as time constraints, spatial isolation, and health monitoring. After that, a special issue of schedulability analysis of ARINC653 system is studied. We design a hierarchical scheduling strategy with consideration of characters of the ARINC653 system, and a scheduling analyzer MAST-2 is used to implement hierarchical schedule analysis. Lastly, we design a prototype tool, called Configuration Checker for ARINC653 (CC653), and two case studies show that the methods proposed in this paper are feasible and efficient.

Download Full-text

A Model-Based Approach to Optimizing Partition Scheduling of Integrated Modular Avionics Systems

Electronics ◽

10.3390/electronics9081281 ◽

2020 ◽

Vol 9 (8) ◽

pp. 1281

Author(s):

Pujie Han ◽

Zhengjun Zhai ◽

Lei Zhang

Keyword(s):

Analytical Methods ◽

Optimization Problem ◽

Timed Automata ◽

System Model ◽

Parallel Genetic Algorithm ◽

Statistical Model Checking ◽

Convex Optimization Problem ◽

Temporal Partitioning ◽

Model Based ◽

Integrated Modular Avionics

The architecture of Integrated Modular Avionics (IMA) provides airborne software with a robust temporal partitioning mechanism, which achieves the reliable fault containment between avionics applications. However, the partition scheduling of an IMA system is a complex nonlinear non-convex optimization problem, making it difficult to solve the optimal temporal allocation for partitions using traditional analytical methods. This paper presents a model-based approach to optimizing the partition scheduling of IMA systems, whose temporal behavior is modeled as a network of timed automata. Given a system model, the optimizer employs a parallel genetic algorithm to search for the optimal partition resource parameters with respect to minimum processor occupancy. For each promising parameter combination, the schedulability constraints and processor occupancy of the system are precisely evaluated by Classical and Statistical Model Checking (i.e., CMC and SMC), respectively. We also apply SMC hypothesis testing to the fast falsification of non-schedulable solutions, thereby speeding up the schedulability verification based on CMC. Two case studies demonstrate that our proposed approach outperforms classical analytical methods on the processor occupancy of typical IMA systems.

Download Full-text

True Concurrency Semantics

International Journal of Embedded and Real-Time Communication Systems ◽

10.4018/ijertcs.2014040103 ◽

2014 ◽

Vol 5 (2) ◽

pp. 22-42 ◽

Cited By ~ 1

Author(s):

Souad Guellati ◽

Ilham Kitouni ◽

Riad Matmat ◽

Djamel-Eddine Saidouni

Keyword(s):

Model Checking ◽

Formal Verification ◽

Timed Automata ◽

Model Data ◽

True Concurrency ◽

New Class ◽

Computation Tree ◽

Interleaving Semantics ◽

Finite State ◽

Validation Technique

The model checking algorithms have been widely studied for timed automata, it's a validation technique for automatically verifying correctness properties of finite-state systems, which are based on interleaving semantics. Therefore the actions are assumed instantaneous. To overcome the hypothesis of temporal and structural atomicity of actions, we use the durational actions timed automata model (daTA). This model is based on the maximality semantics. Properties to be verified are expressed using the Timed Computation Tree Logic (TCTL). For dealing with formal verification, the Maximality-based Region Graph (MRG) is defined and an adaptation of the model checking algorithm is proposed. The use of the maximality semantics based verification provides new class of properties related to simultaneous progress of actions at different states.

Download Full-text

Test Case Generating for Integrated Modular Avionics Software Health Monitoring

Applied Mechanics and Materials ◽

10.4028/www.scientific.net/amm.494-495.873 ◽

2014 ◽

Vol 494-495 ◽

pp. 873-880

Author(s):

Hui Nan Zhang ◽

Shi Hai Wang ◽

Xiao Xu Diao ◽

Bin Liu

Keyword(s):

Embedded System ◽

Health Monitoring ◽

High Reliability ◽

Life Cycle Costs ◽

Test Case ◽

Test Cases ◽

Model Driven ◽

Test Methodology ◽

Maintenance And Inspection ◽

Integrated Modular Avionics

Avionics software is safe-critical embedded system and its architecture is evolving from traditional federated architecture to Integrated Modular Avionics (IMA) to improve resource usability. As an architecture widely employed in the avionics industry, supports partitioning concepts. To insure the development of the avionics software constructed on IMA operating system with high reliability and efficiency Health Monitoring (HM) has been shown to be a key step in reducing the life cycle costs for structural maintenance and inspection. In this paper , we propose a model-driven test methodology using Architecture Analysis &Design Language (AADL). It proposes modeling patterns of IMA errors to support the test case generating mechanisms of the HM module, proposing 3 kinds of test cases that can be injected in the HM to stimulate these kinds of errors, and we present the preliminary results that can meet the satisfactory from a ongoing project based on IMA system.

Download Full-text

Formal Verification of Heuristic Autonomous Intersection Management Using Statistical Model Checking

Sensors ◽

10.3390/s20164506 ◽

2020 ◽

Vol 20 (16) ◽

pp. 4506

Author(s):

Aaditya Prakash Chouhan ◽

Gourinath Banda

Keyword(s):

Model Checking ◽

Statistical Model ◽

Formal Verification ◽

Autonomous Vehicles ◽

Timed Automata ◽

Autonomous Systems ◽

Statistical Model Checking ◽

Stage Of Development ◽

Verification Techniques ◽

Intersection Management

Autonomous vehicles are gaining popularity throughout the world among researchers and consumers. However, their popularity has not yet reached the level where it is widely accepted as a fully developed technology as a large portion of the consumer base feels skeptical about it. Proving the correctness of this technology will help in establishing faith in it. That is easier said than done because of the fact that the formal verification techniques has not attained the level of development and application that it is ought to. In this work, we present Statistical Model Checking (SMC) as a possible solution for verifying the safety of autonomous systems and algorithms. We apply it on Heuristic Autonomous Intersection Management (HAIM) algorithm. The presented verification routine can be adopted for other conflict point based autonomous intersection management algorithms as well. Along with verifying the HAIM, we also demonstrate the modeling and verification applied at each stage of development to verify the inherent behavior of the algorithm. The HAIM scheme is formally modeled using a variant of the language of Timed Automata. The model consists of automata that encode the behavior of vehicles, intersection manager (IM) and collision checkers. To verify the complete nature of the heuristic and ensure correct modeling of the system, we model it in layers and verify each layer separately for their expected behavior. Along with that, we perform implementation verification and error injection testing to ensure faithful modeling of the system. Results show with high confidence the freedom from collisions of the intersection controlled by the HAIM algorithm.

Download Full-text

Wavlet Decomposition based Diagnostic for Structural Health Monitoring on Metallic Aircrafts: Case of Crack Triangulation and Corrosion Detection

International Journal of Prognostics and Health Management ◽

10.36001/ijphm.2013.v4i1.1438 ◽

2020 ◽

Vol 4 (1) ◽

Author(s):

Hamza Boukabache ◽

Christophe Escriba ◽

Sabeha Zedek ◽

Jean-Yves Fourniols

Keyword(s):

Structural Health Monitoring ◽

Frequency Analysis ◽

Health Monitoring ◽

Control Method ◽

Temporal Frequency ◽

Time Frequency ◽

Structural Health ◽

Acoustic Signatures ◽

Integrated Modular Avionics ◽

Pulse Echo

This work focus on the structural health monitoring of aircrafts parts specimen structures made of 2024 Aluminum alloys using a reliable Joint Time Frequency Analysis calculation (Joint Temporal Frequency Analysis). In this paper we demonstrate the feasibility of a new non destructive control method capable to probe very large structures within a short time. The method we developed is based through a wide piezoelectric sensors network on a smart comparison between two acoustic signatures: the healthy structure response captured before the commissioning of the plane and “an after flight” response. The sensors network exploits the capability of piezoelectric patches to generate/measure specific Lamb wave’s modes. The system is therefore dynamically configured to localize mechanicals flaws using a triangulation algorithm that operates using different techniques like pitch-catch and pulse-echo. The aim of this paper is to highlight a methodology that is currently being integrated into reconfigurable qualified and certified hardware architecture. The idea behind is to interface the airplane's structure to an integrated modular avionics calculator (IMA).An analytic study is performed and tests to prove the proposed method feasibility on corroded and damaged structures specimens are provided at the end of this paper.

Download Full-text

Simulation and Formal Verification for Improving Safety of PLC Programs

Recent Innovations in Mechatronics ◽

10.17667/riim.2016.1-2/9. ◽

2016 ◽

Vol 3 (1-2.) ◽

Author(s):

Joel Galvão ◽

José Machado

Keyword(s):

Formal Verification ◽

Timed Automata ◽

Programmable Logic ◽

Programmable Logic Controllers ◽

Mechatronic Systems ◽

Analysis Techniques ◽

Function Blocks ◽

Complementary Techniques ◽

Modeling Formalism

The use of analysis techniques for improving quality of software for industrial controllers is widely used. Mainly Simulation and Formal Verification can be used as complementary techniques improving dependability of mechatronic systems behavior. In this paper there are used Simulation and Formal Verification for guaranteeing safe software for Programmable Logic Controllers, mainly related with using Function blocks of IEC 61131-3 standard. For studying, simulating and verifying behavior of those blocks are used timed automata, as modeling formalism, and UPPAAL, as tool for simulation and Formal Verification purposes.

Download Full-text