Modelling Task Priority in Symbolic Predictive Analysis for Embedded Software in Ada

Abstract

The concurrent, embedded software in safety-critical systems is complex, and analyzing all possible execution paths of such programs is challenging. Symbolic predictive analysis statically analyses a given concrete execution trace of a concurrent program to determine whether any feasible permutation of the given trace violates specified properties. The existing tools do not consider the priority of threads in their modeling of concurrent systems. In this work, we apply a novel static analysis technique based on symbolic predictive anal- ysis for the formal verification of concurrent programs in embedded systems with pre-defined priorities and schedules for the tasks. We consider the given trace as a total order of events coupled with a partial order for the causal model, including several alternative interleavings. Additionally, we include the constraints for the order of event execution by considering the priority of the tasks. We develop a tool chain customized for Ada code, encode the constraints for priority and use it for verifying the onboard software of an aerospace launch vehicle. We accurately model the execution environment for this concurrent software and verify it, along with other benchmarks like concurrency litmus tests and mutual exclusion algorithms. Our experimental results demonstrate the correctness of our modeling and the suitability of our tool for verification of critical Ada software.