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.