A Specification Framework for Mixed-Criticality Scheduling Protocols

This article presents a general formal framework for describing the relationship between a criticality-aware scheduler, a set of application jobs that are assigned different criticality levels, and an environment that generates both work and faults that the run-time system must control. The proposed formalism extends the rely-guarantee approach, which facilitates formal reasoning about the functional behaviour of concurrent systems, to address real-time properties. The exposition of the general framework is supplemented by a seven step approach that enables it to be instantiated to deliver the formal specification of any proposed mixed-criticality scheduling protocol. The expressive power of the approach is explored via a non-trivial instantiation.

• Publication year

  2025

• Venue

  ACM Transactions on Embedded Computing Systems

• Publication date

  2025-09-01

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/3765522
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Mixed-Criticality with Integer Multiple WCETs and Dropping Relations: New Scheduling Challenges

  2023cited by this paper
• Extending rely-guarantee thinking to handle real-time scheduling

  2023cited by this paper
• Foundational Response-Time Analysis as Explainable Evidence of Timeliness

  2022cited by this paper
• Abstract Response-Time Analysis: A Formal Foundation for the Busy-Window Principle (Artifact)

  2020cited by this paper
• Justifying the Service Provided to Low Criticality Tasks in a Mixed Criticality System

  2020cited by this paper
• Re-Thinking Mixed-Criticality Architecture for Automotive Industry

  2020cited by this paper
• Deriving Specifications of Control Programs for Cyber Physical Systems

  2019cited by this paper
• A Lazy Bailout Approach for Dual-Criticality Systems on Uniprocessor Platforms

  2019cited by this paper
• AdaptMC: A Control-Theoretic Approach for Achieving Resilience in Mixed-Criticality Systems

  2018cited by this paper
• Mixed Feelings About Mixed Criticality (Invited Paper)

  2018cited by this paper
• A Survey of Research into Mixed Criticality Systems

  2017cited by this paper
• A Guide to Rely/Guarantee Thinking

  2017cited by this paper
• An Enhanced Bailout Protocol for Mixed Criticality Embedded Software

  2017cited by this paper
• PROSA: A Case for Readable Mechanized Schedulability Analysis

  2016cited by this paper
• Mixed Criticality Systems - A History of Misconceptions?

  2016cited by this paper
• How realistic is the mixed-criticality real-time system model?

  2015cited by this paper
• A Bailout Protocol for Mixed Criticality Systems

  2015cited by this paper
• Mixed-Criticality Embedded Systems -- A Balance Ensuring Partitioning and Performance

  2015cited by this paper
• Safety Assurance Driven Problem Formulation for Mixed-Criticality Scheduling

  2013cited by this paper
• Response-Time Analysis for Mixed Criticality Systems

  2011cited by this paper
• A timeband framework for modelling real-time systems

  2010cited by this paper
• Schedulability Analysis for Real-Time Systems with EDF Scheduling

  2009cited by this paper
• Efficient Exact Schedulability Tests for Fixed Priority Real-Time Systems

  2008cited by this paper
• Real-Time Systems: Formal Specification and Automatic Verification

  2008cited by this paper
• Preemptive Scheduling of Multi-criticality Systems with Varying Degrees of Execution Time Assurance

  2007cited by this paper
• Software Abstractions - Logic, Language, and Analysis

  2006cited by this paper
• Real-Time Systems: Scheduling, Analysis, and Verification

  2002cited by this paper
• Concurrency Verification: Introduction to Compositional and Noncompositional Methods

  2001cited by this paper
• On priority assignment in fixed priority scheduling

  2001cited by this paper
• Formal analysis for real-time scheduling

  2000cited by this paper
• Using Z - specification, refinement, and proof

  1996cited by this paper
• The B-book - assigning programs to meanings

  1996cited by this paper
• Applying new scheduling theory to static priority pre-emptive scheduling

  1993cited by this paper
• Preemptively scheduling hard-real-time sporadic tasks on one processor

  1990cited by this paper
• Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment

  1989cited by this paper
• Specification case studies

  1987cited by this paper
• Systematic software development using VDM

  1986cited by this paper
• Finding Response Times in a Real-Time System

  1986cited by this paper
• Tentative steps toward a development method for interfering programs

  1983cited by this paper
• Specification and Design of (Parallel) Programs

  1983cited by this paper
• Developing methods for computer programs including a notion of interference

  1981cited by this paper

• No citing papers are available for this paper.