Event-triggered environments for verification of real-time systems

The growing complexity and the safety-critical requirements of the embedded software in avionics systems present many challenges to current test-based verification technology. The use of formal verification methods can increase design assurance by exploring a larger range of system behaviors and fault conditions than can feasibly be covered by testing or simulation. However, one of the most challenging tasks faced in any formal verification activity is the construction of an adequate model for the environment with which the analyzed system interacts. For real-time systems where the timing characteristics are critical to correct performance this task is even more difficult. In this paper we discuss how an event-triggered model of time (as found in discrete event simulations) can be used as the basis for the environment needed to verify real-time avionics software.