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

As safety-critical systems become increasingly more complex, statutory certification organizations are increasingly mandating that formal techniques be used to prove that such systems meet their specifications. Techniques from real-time scheduling theory are commonly applied during this proof process to demonstrate compliance with temporal specifications. This project focuses 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. The objective is to identify several such principles and establish that scheduling techniques complying with these principles are more likely to yield error-free real-time systems. We will seek methods of deriving scheduling techniques that are compliant with these principles. Using these techniques, the project seeks to provide theoretical foundations for the analysis of timing constraints in such systems, and obtain new methodologies for obtaining system designs that are provably correct by construction (thereby concurrently obtaining both correct designs and their formal proofs of correctness). Broader impacts include joint research with industry colleagues, building on strong expressions of interest from system designers in the topics and possible outcomes of this research. All tools and development platforms implemented as part of this project are being made public, and can be used by other institutions for research and teaching purposes.