COURSE · DF2

Mission-Critical Real-Time Systems

מערכות זמן-אמת קריטיות למשימה

real-time scheduling, dependability, and certification of safety-critical embedded software

Build a certifiable real-time safety-critical control system

Year 313 weeks2h lecture + 2h practiceProject-based

About this course

Engineer software that must be correct and on time: real-time scheduling, safety-critical design, fault tolerance, and the reliability and certification practices defense systems demand.

Course format. Thirteen weeks, four contact hours each: a two-hour lecture (concepts and theory) and a two-hour practice session. The course is project-based; teams carry one running project end to end and present it three times, in weeks 5, 8, and 13.
What you will build

Built a mission-critical real-time control system on FreeRTOS and an ARM Cortex-M target, implementing rate-monotonic scheduling with proven schedulability, priority-inheritance synchronization, triple-modular redundancy with voting, and a DO-178C-style requirements traceability and structural-coverage evidence package.

Expected outcomes

  • Develop and integrate hard real-time tasks on FreeRTOS and Zephyr, perform schedulability analysis with the Rate Monotonic utilization bound n(2^(1/n)-1) and EDF optimality, and validate timing behavior with Tracealyzer kernel-aware trace visualization on STM32 or Raspberry Pi Pico hardware.
  • Implement inter-task communication via bounded lock-free ring buffers and POSIX priority-inheritance mutexes, identify and bound priority inversion scenarios using the Priority Ceiling Protocol, and write ISR-safe device driver routines with deferred task notifications.
  • Profile worst-case execution time on target hardware with logic analyzer timing instrumentation and GDB with JTAG; verify task-set schedulability and jitter bounds using QEMU simulation before hardware deployment.
  • Model and verify the two-task system in UPPAAL timed automata to prove deadline satisfaction and freedom from deadlock; apply SPIN Promela model checking to verify deadlock freedom of the ring buffer and mutex synchronization protocol.
  • Define safety requirements with FMEA and FTA for IEC 61508 SIL and DO-178C DAL integrity levels, review code against MISRA C guidelines using PC-lint or Polyspace, and produce a requirements traceability matrix with structural coverage evidence.
  • Design a Time-Triggered Architecture schedule for deterministic inter-task communication and evaluate the trade-offs among RM, EDF, and TT-Ethernet for mission-critical real-time deployments.

Key topics

  • Real-time scheduling
  • Safety-critical software
  • Fault tolerance & reliability
  • Certification standards

Theoretical foundations

The concepts and results this course rests on.

  • hard vs soft real-time semantics: deadline miss consequences, determinism requirements, and jitter budget analysis
  • worst-case execution time (WCET) analysis: control-flow analysis, cache effects, pipeline hazards, and WCET measurement methods
  • Rate Monotonic Scheduling: fixed-priority assignment, Liu and Layland utilization bound n(2^(1/n)-1), and the schedulability test
  • Earliest Deadline First scheduling: dynamic priority assignment, hyperperiod computation, and EDF optimality on uniprocessors
  • priority inversion and the priority ceiling protocol: unbounded inversion scenario, PIP, PCP, and POSIX priority-inheritance mutex
  • inter-task communication patterns: message queues, shared memory with mutex/semaphore, event flags, and zero-copy IPC
  • interrupt latency and ISR design: non-blocking ISR contract, deferred work via task notifications, and interrupt nesting
  • Time-Triggered Architecture and TT-Ethernet: offline schedule tables, time-slot allocation, TDMA, and deterministic communication
  • safety integrity levels and certification: IEC 61508 SIL 1-4, DO-178C DAL A-E, safety case structure, FMEA, and FTA
  • formal verification with model checking: LTL/CTL temporal logic specifications, state-space explosion countermeasures, and timed automata model checkers for real-time scheduling

Prerequisites

This is a Year-3 course. It assumes the mandatory CS core: data structures and algorithms, operating systems, computer networks, databases, software engineering, and the core mathematics (linear algebra, probability and statistics, calculus, discrete mathematics). It additionally requires the specific prior courses listed below.

Course-specific prerequisites:

  • Operating systems
  • Embedded or systems programming
  • Software engineering

Weekly schedule 13 weeks · lecture + practice

Foundations
Wk 1
Hard vs soft real-time semantics and jitter analysis
LectureDefine hard vs soft real-time semantics: deadline miss consequences, determinism requirements, and jitter budget analysis; the periodic task model with periods, deadlines, and WCET (P1).
PracticeSet up FreeRTOS on STM32 or Raspberry Pi Pico; simulate initial periodic tasks with QEMU before flashing; observe task timing and scheduling behavior.
ProjectRepository, target platform (STM32 or Raspberry Pi Pico), and periodic tasks running on FreeRTOS.
Scheduling
Wk 2
Rate Monotonic Scheduling
LectureRate Monotonic fixed-priority assignment, the Liu and Layland utilization bound n(2^(1/n)-1), and the schedulability test for a task set (P3).
PracticeImplement a Rate Monotonic task set on FreeRTOS; use Tracealyzer to visualize kernel scheduling events and verify deadline compliance.
ProjectRate Monotonic task set running on FreeRTOS with proven schedulability.
Wk 3
Earliest Deadline First scheduling
LectureEDF dynamic priority assignment, hyperperiod computation, and EDF optimality on uniprocessors; comparison with RM under overload (P4).
PracticeImplement EDF scheduling on Zephyr RTOS; compare RM and EDF behavior under the same task set using QEMU simulation.
ProjectSchedulability analysis report comparing RM and EDF for the two-task project design.
Wk 4
Priority inversion and synchronization protocols
LectureUnbounded priority inversion scenario, Priority Inheritance Protocol (PIP), Priority Ceiling Protocol (PCP), and the POSIX priority-inheritance mutex (P5).
PracticeReproduce a priority inversion on FreeRTOS; apply a POSIX priority-inheritance mutex; debug and measure bounded blocking using GDB with JTAG.
ProjectInter-task synchronization with bounded blocking documented and measured on target.
Milestone
Wk 5
Specification presentationPresentation
LectureScoping a two-task hard real-time system: sensor-acquisition and control-law tasks, lock-free ring buffer specification, RM schedulability argument, and WCET measurement plan.
PracticeTeam presentation: each team presents system concept, task periods and deadlines, RM schedulability analysis, safety requirements, and IEC 61508 / DO-178C certification target.
ProjectApproved specification with requirements, timing model, and schedulability argument.
WCET and IPC
Wk 6
Worst-case execution time analysis
LectureWCET analysis: control-flow analysis, cache effects, pipeline hazards, and measurement-based WCET estimation methods (P2).
PracticeInstrument the sensor-acquisition and control-law tasks with logic analyzer timing on STM32 or Raspberry Pi Pico; compute WCET bounds from hardware measurements.
ProjectWCET bounds for both tasks feeding the RM schedulability argument.
Wk 7
ISR design and inter-task communication
LectureMessage queues, shared memory with mutex/semaphore, event flags, and zero-copy IPC (P6); non-blocking ISR contract, deferred work via task notifications, and interrupt nesting (P7).
PracticeImplement the lock-free ring buffer between sensor-acquisition and control-law tasks in FreeRTOS; validate ISR-safe operations and deferred task notification using GDB with JTAG.
ProjectLock-free ring buffer connecting sensor-acquisition and control-law tasks on target.
Milestone
Wk 8
Interim demo presentationPresentation
LectureTime-Triggered Architecture and TT-Ethernet: offline schedule tables, time-slot allocation, TDMA, and deterministic communication for distributed real-time (P8).
PracticeTeam presentation: demo the two-task system with RM scheduling and lock-free ring buffer running on target; show WCET bounds from logic analyzer and deadline compliance in Tracealyzer.
ProjectWorking two-task system with RM scheduling, lock-free ring buffer, and measured WCET bounds demonstrated on hardware.
Formal verification
Wk 9
Formal verification with timed automata
LectureLTL/CTL temporal logic specifications, state-space explosion countermeasures, and timed automata model checkers for verifying real-time scheduling properties (P10).
PracticeModel the two-task system in UPPAAL timed automata; verify deadline satisfaction and absence of timing violations across the hyperperiod.
ProjectUPPAAL timed automata model verifying deadline satisfaction for the two-task design.
Wk 10
Model checking for deadlock freedom
LectureSPIN Promela model checker: encoding concurrency, state-space search, deadlock freedom, and liveness properties (P10 continued).
PracticeEncode the ring buffer and mutex synchronization protocol in SPIN Promela; verify deadlock freedom and ring buffer invariants with QEMU-assisted state exploration.
ProjectSPIN deadlock-freedom certificate for the task communication model.
Certification
Wk 11
Safety integrity levels and DO-178C
LectureIEC 61508 SIL 1-4, DO-178C DAL A-E, safety case structure, FMEA, and FTA; tool qualification and MISRA C guidelines (P9).
PracticeRun MISRA C checker (PC-lint or Polyspace) on the project code; build a requirements traceability matrix and measure structural coverage on the critical control path.
ProjectMISRA C compliance report, FMEA, and requirements traceability matrix taking shape.
Wk 12
Verification, time-triggered communication, and safety case
LectureVerification strategy, TT-Ethernet time-slot scheduling, safety case assurance argument, and configuration management for certified workflows.
PracticeImplement a time-triggered message schedule in Zephyr RTOS; assemble the safety case evidence package with UPPAAL and SPIN certificates, WCET measurements, and MISRA C report.
ProjectComplete verification evidence package: UPPAAL deadlock-freedom certificate, SPIN proof, WCET bounds, MISRA C report, requirements traceability matrix, and structural coverage report.
Milestone
Wk 13
Final demo and oral defensePresentation
LectureCourse synthesis: from Rate Monotonic analysis and WCET measurement through lock-free ring buffer, UPPAAL verification, and IEC 61508 / DO-178C evidence.
PracticeTeam presentation: final demo of the complete two-task system on target hardware; walk through RM schedulability proof, WCET measurements, UPPAAL deadlock-freedom certificate, SPIN proof, and MISRA C findings; oral defense.
ProjectComplete real-time system: RM scheduling, lock-free ring buffer, WCET instrumentation, UPPAAL and SPIN verification, and IEC 61508/DO-178C certification evidence.
AI tools in this course.

Students use AI assistants and vibe-coding to write and refactor RTOS task code for FreeRTOS or Zephyr, generate scheduling and synchronization scaffolding, and translate response-time and utilization analysis into checkable code. They interact with toolchains and analyzers through assistants and MCP servers that expose the build, the target board, schedulability tools, and coverage tools, asking the model to set up a task set or instrument timing measurements. AI generates requirements-based tests, fault-injection scenarios, and traceability scaffolding for a DO-178C-style evidence package, and helps analyze structural coverage and timing results. Because the code is safety-critical, students rigorously review and independently verify every AI suggestion against timing budgets, schedulability proofs, and the safety requirements.

Student project

Teams design and implement a two-task hard real-time control system on an RTOS-capable hardware target (STM32 or Raspberry Pi Pico with FreeRTOS or Zephyr): a high-frequency sensor-acquisition task and a lower-frequency control-law task communicating through a lock-free ring buffer, scheduled with Rate Monotonic assignment, instrumented for WCET measurement with logic analyzer and GDB with JTAG, and formally verified for deadlock freedom using UPPAAL timed automata and SPIN model checking.

Requirements

  • Build a working system, not a set of disconnected exercises.
  • Be original: a new system that solves a real problem, not a re-implementation of a tutorial or course demo.
  • Show real depth: real data, real users or realistic load, and engineering trade-offs that are measured rather than assumed.
  • Carry one running project from specification to a deployed, defensible result across the whole term.
  • Work in a team of three or four and defend the design at each of the three presentations (weeks 5, 8, and 13).

Example projects

Flight-control loop for a small fixed-wing UAVEngine or motor controller with redundant sensingRailway signaling interlock prototypeMedical infusion-pump controllerTriple-redundant attitude estimation nodeAutomotive brake-by-wire control loopTime-triggered distributed sensor network

Assessment & grading

Grading is project-based, with no written exam. Teams of three or four present one running project three times.

ComponentWhat it coversWeight
Project · SpecificationPresentation 1 (week 5): problem, objectives, and architecture20%
Project · InterimPresentation 2 (week 8): the working system demonstrated live30%
Project · FinalPresentation 3 (week 13): end-to-end demo with oral defense50%

Tools & platforms

  • FreeRTOS: open-source real-time kernel for embedded targets
  • Zephyr RTOS: scalable real-time OS for embedded systems
  • Ada and SPARK: language and toolset for high-integrity software
  • Cheddar: open-source real-time scheduling analysis tool
  • STM32 or similar ARM Cortex-M target board
  • GNAT and the Ada toolchain for certified development
  • AbsInt aiT: static worst-case execution time analysis
  • LDRA or VectorCAST: structural coverage and unit testing for DO-178C
  • GoogleTest: unit testing of critical components
  • Git and a configuration-management workflow for traceability
  • Logic analyzer and oscilloscope for timing measurement
  • Wireshark with time-triggered protocols for network analysis

Free online courses

Existing free, video-based courses this course can build on, for self-study or as a teaching basis.

Primary literature

Seminal works for advanced study.

References

Books and resources link to an online or publisher page.

Role in each concentration

ConcentrationRole
Intelligent Software SystemsElective
Networking & Cyber SecurityElective
AI & RoboticsElective
AI and Quantum Computing for FinanceElective
Immersive Systems & Game DevelopmentElective
Defense Technologies & Autonomous SystemsCore · Semester 2