Proving absence of starvation by means of abstract interpretation and model checking

Abstract

The Avionics Application Software Standard Interface ARINC 653 is meant to increase predictability of safety-critical software systems. It allows to coordinate multiple tasks by means of priorities, semaphores, setting and waiting for events as well as by sending suspend and resume signals. Thus, it is a major challenge to verify that no such tightly coupled task gets ultimately stuck, e.g., by infinitely waiting for an event or a resume signal by another task. We explain how abstract interpretation together with model checking may nicely cooperate to guarantee absence of such concurrency flaws and report on practical experiments.