EHCS (EHS), SM: Formal Foundations of Real-Time Systems Analysis: Principles and Potential Pitfalls

Principal Investigator: Sanjoy K. Baruah, James H. Anderson
Funding Agency: National Science Foundation
Agency Number: CNS-0834270

Abstract
As safety-critical real-time application systems become increasingly more complex, national and international statutory certification organizations are increasingly demanding that formal techniques be used to demonstrate that such systems meet their specifications. In many safety-critical domains such as avionics, the automotive industry, and space, obtaining such a formal proof of correctness of a new design often constitutes a very significant fraction of the total cost and effort invested in the design. Techniques from real-time scheduling theory are commonly applied during this proof process, particularly to demonstrate compliance with temporal specifications. In this proposal, we focus on the emerging field of meta-real-time scheduling theory. Meta-scheduling theory attempts to understand those properties that cause certain scheduling-theoretic techniques to be more successful than others in designing and implementing real-time systems, and seeks general principles that are common to such successful techniques. We identify several such principles and argue that scheduling techniques that comply with these principles are far more likely to facilitate the design and implementation of real-time application systems that are free of temporal errors. We propose to seek methods of deriving scheduling and resource-allocation techniques that are compliant with these principles. We will build on our prior preliminary research exploring these principles, in order to enhance our understanding of the behavior of complex, multiprocessor, real-time systems. From the perspective of these design principles, we propose to provide a firm theoretical foundation for the analysis of timing constraints in such systems, and obtain new tools, techniques, and methodologies for obtaining system designs that are provably correct by construction (thereby concurrently obtaining both correct designs and their formal proofs of correctness).