Real-Time Systems: Scheduling, Analysis, and Verification
Albert M. K. Cheng
John Wiley & Sons, Inc.
August 2002



Junior/Senior-Level Semester Course Covering Scheduling and Analysis/Verification

Week 1: Chapter 1 - Introduction
Week 2: Chapter 3, sections 3.1, 3.2, 3.2.1 - rate-monotonic scheduling
Week 3: Chapter 3, section 3.2.1 - earliest-deadline-first scheduling, least-laxity-first scheduling, premptable sporadic tasks
Week 4: Chapter 3, section 3.2.2 - Nonpremptable sporadic tasks,section 3.2.3 - Nonpremptable tasks with precedence constraints
Week 5: Chapter 3, section 3.2.4 - Communicating periodic tasks, section 3.2.5 - Periodic tasks with critical sections
Week 6: Chapter 3, section 3.3 - Multiprocessor scheduling
Week 7: Chapter 3, section 3.4 - Scheduling tools, Exam 1
Week 8: Chapter 2 - Review of logic, automata, and languages
Week 9: Chapter 4 - sections 4.1, 4.2 - Model checking
Week 10: Chapter 4 - sections 4.3-4.5 - Implementation, section 4.6 - Symbolic model checking
Week 11: Chapter 4 - sections 4.7, 4.8 - Real-time CTL and tools
Week 12: Chapter 5 - Statecharts
Week 13: Chapter 6 - sections 6.1-6.4 - Real-Time Logic
Week 14: Chapter 6 - sections 6.5-6.10 - Checking unsatisfiability, Modecharts, tools
Week 15: Chapter 7, 8, or 9 - selected sections
Week 16: Chapter 10 - selected sections, Exam 2


Junior/Senior-Level Semester Course Covering Analysis/Verification but no Scheduling

Week 1: Chapter 1 - Introduction
Week 2: Chapter 2 - Review of logic, automata, and languages
Week 3: Chapter 4 - sections 4.1, 4.2 - Model checking
Week 4: Chapter 4 - sections 4.3-4.5 - Implementation, section 4.6 - Symbolic model checking
Week 5: Chapter 4 - sections 4.7, 4.8 - Real-time CTL and tools
Week 6: Chapter 5 - Statecharts
Week 7: Chapter 6 - sections 6.1-6.4 - Real-Time Logic
Week 8 Chapter 6 - sections 6.5-6.10 - Checking unsatisfiability, Modecharts, tools, Exam 1
Week 9: Chapter 7 - section 7.1 - Lunch-Vaandrager automata
Week 10: Chapter 7 - section 7.2-7.4 - Alur-Dill automata, tools
Week 11: Chapter 8 - sections 8.1-8.3 - Untimed and timed Petri nets, section 8.7 - tools
Week 12: Chapter 9 - sections 9.1-9.7 - Untimed and timed process algebras, tools
Week 13: Chapter 10 - selected sections - Rule-based systems
Week 14: Chapter 10 - selected sections - Rule-based systems
Week 15: Chapter 12 - selected sections - Optimizatin of Rule-based systems
Week 16: Chapter 12 - selected sections - Optimizatin of Rule-based systems, Exam 2


First-Year Graduate-Level Semester Course Covering Scheduling and Analysis/Verification

Week 1: Chapter 1 - Introduction, Chapter 3, sections 3.1, 3.2, 3.2.1 - rate-monotonic scheduling
Week 2: Chapter 3, section 3.2.1 - earliest-deadline-first scheduling, least-laxity-first scheduling, premptable sporadic tasks
Week 3: Chapter 3, section 3.2.2 - Nonpremptable sporadic tasks,section 3.2.3 - Nonpremptable tasks with precedence constraints
Week 4: Chapter 3, section 3.2.4 - Communicating periodic tasks, section 3.2.5 - Periodic tasks with critical sections
Week 5: Chapter 3, section 3.3 - Multiprocessor scheduling, tools
Week 6: Chapter 2 - Review of logic and automata, Chapter 4 - sections 4.1-4.6 - Model checking, implementation
Week 7: Chapter 4 - sections 4.6-4.8 - Symbolic model checking, real-time CTL, Exam 1
Week 8: Chapter 5 - Statecharts
Week 9: Chapter 6 - sections 6.1-6.4 - Real-Time Logic
Week 10: Chapter 6 - sections 6.5-6.10 - Checking unsatisfiability, Modecharts, tools
Week 11: Chapter 7 - section 7.1 - Lynch-Vaandrager automata, Alur-Dill automata, tools
Week 12: Chapter 8 - sections 8.1-8.3 - Untimed and timed Petri nets, section 8.7 - tools
Week 13: Chapter 9 - sections 9.1-9.7 - Untimed and timed process algebras, tools
Week 14: Chapter 10 - selected sections - Rule-based systems
Week 15: Chapter 11 - selected sections - Rule-based systems
Week 16: Chapter 12 - selected sections - Optimization of Rule-based systems, Exam 2


First-Year Graduate-Level Semester Course Covering Analysis/Verification but no Scheduling

Week 1: Chapter 1 - Introduction, Chapter 3 - Review of logic and automata
Week 2: Chapter 4 - sections 4.1-4.6 - Model checking, implementation
Week 3: Chapter 4 - sections 4.6-4.8 - Symbolic model checking, real-time CTL, Exam 1
Week 4: Chapter 5 - Statecharts
Week 5: Chapter 6 - sections 6.1-6.4 - Real-Time Logic
Week 6: Chapter 6 - sections 6.5-6.10 - Checking unsatisfiability, Modecharts, tools
Week 7: Chapter 7 - section 7.1 - Lynch-Vaandrager automata, Alur-Dill automata, tools, Exam 1
Week 8: Chapter 8 - sections 8.1-8.3 - Untimed and timed Petri nets, section 8.7 - tools
Week 9: Chapter 9 - sections 9.1-9.7 - Untimed and timed process algebras, tools
Week 10: Chapter 10 - Propositional-logic rule-based systems
Week 11: Chapter 10 - Propositional-logic rule-based systems
Week 12: Chapter 10 - Predicate-logic rule-based systems
Week 13: Chapter 11 - Predicate-logic rule-based systems
Week 14: Chapter 11 - Predicate-logic rule-based systems
Week 15: Chapter 12 - Optimization of Rule-based systems
Week 16: Chapter 12 - Optimization of Rule-based systems, Exam 2




Last updated: September 15, 2002