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

CSR-EHCS (EHS)，SM：实时系统分析的形式基础：原理和潜在陷阱

• 批准号: 0834270
• 负责人: Sanjoy Baruah
• 金额: $ 27万
• 依托单位: University of North Carolina at Chapel Hill
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2008
• 资助国家: 美国
• 起止时间: 2008-09-01 至 2011-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0834270&HistoricalAwards=false
• 关键词: CSR; EHCS; EHS; SM; Formal

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.

随着安全关键系统变得越来越复杂，法定认证组织越来越多地要求使用正式技术来证明此类系统符合其规范。在这个证明过程中，通常应用实时调度理论中的技术来证明对时间规范的遵从性。本项目重点研究元实时调度理论这一新兴领域。元调度理论试图理解那些导致某些调度理论技术在设计和实现实时系统时比其他技术更成功的特性，并寻求这些成功技术的通用原则。目标是确定几个这样的原则，并确定遵循这些原则的调度技术更有可能产生无错误的实时系统。我们将寻求获得符合这些原则的调度技术的方法。使用这些技术，该项目寻求为分析此类系统中的时间约束提供理论基础，并获得通过构造获得可证明正确的系统设计的新方法（从而同时获得正确的设计及其正确性的正式证明）。更广泛的影响包括与行业同事的联合研究，建立在系统设计师对该研究的主题和可能结果的强烈兴趣的基础上。作为该项目的一部分实施的所有工具和开发平台都是公开的，可供其他机构用于研究和教学目的。