The hardware and software in modern aircraft control systems are good candidates for verification using formal methods: they are complex, safety-critical, and challenge the capabilities of test-based verification strategies. We have previously reported on our use of model checking to verify the time partitioning property of the Deos/spl trade/ real-time operating system for embedded avionics. The size and complexity of this system have limited us to analyzing only one configuration at a time. To overcome this limit and generalize our analysis to arbitrary configurations we have turned to theorem proving. This paper describes our use of the PVS theorem prover to analyze the Deos scheduler. In addition to our inductive proof of the time partitioning invariant, we present a feature-based technique for modeling state-transition systems and formulating inductive invariants. This technique facilitates an incremental approach to theorem proving that scales well to models of increasing complexity, and has the potential to be applicable to a wide range of problems.

This paper describes our work modeling key portions of the safety-critical software infrastructure in an integrated modular avionics (IMA) platform in an effort to analytically establish correctness of important aspects of its design. In particular, we use model checking to verify timing properties of the Deos/spl trade/ real-time operating system in the presence of various advanced scheduling features. We focus here on the addition of scheduler overhead processing time to the Deos model and analyzing its effect on the time partitioning property and the internal assertions (function preconditions) in the model. Our model includes advanced scheduling features (dynamic threads, slack recovery, aperiodic interrupts) and explicitly models the scheduler operations at the same level of detail as the source code. Our findings support the use of formal methods to verify key properties of safety-critical systems that would be difficult or impossible to establish otherwise.

As systems become increasingly complex and existing methodologies become insufficient to handle the complexity, the design community is beginning to look at formal methods for a possible solution. Techniques involving a limited use of formal techniques (such as semi-formal methods and equivalence checking) have given a glimpse of what full usage of formal techniques can achieve. For the use of formal methods to be a widely accepted methodology among designers, it must provide the designers with the capabilities of structuring specifications in a manner similar to the structuring they are used to using with programming languages. In this paper, we provide a description of the structuring capabilities of VSPEC (VHDL SPECification), a requirements specification language for VHDL. These capabilities include the use of multiple pre- and post-condition pairs within a single specification and combination of specifications using common Boolean operators.