Mechanization of the Ravenscar Profile in Coq

Abstract

The Ada Ravenscar profile [1] is a subset of Ada concurrency to implement deterministic real-time systems: - mono-core systems- periodic or sporadic tasks - communication through protected objects with Immediate Ceiling Priority Protocol, ICPP - Absolute delays.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 15, 2023
Accession Number
AD1204973

Entities

People

  • Jérôme Hugues

Organizations

  • Carnegie Mellon University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Department Of Defense
  • Engineering
  • Guarantees
  • Language
  • Materials
  • Scheduling (Production)
  • Semantics
  • Simulations
  • Simulators
  • Software Development
  • Universities

Readers

  • Database Systems and Applications
  • Mathematical Modeling and Probability Theory.
  • Theoretical Analysis.