Real-time systems. Scheduling, analysis and verification

Описание

PREFACE xv
• Integrated status assessment expert system (ISA) (chapters 10, 11, 12)
• Seat assignment (chapter 11)
• Analysis of 2D line-drawing representation of 3D objects (chapter 11)
• Space Shuttle Orbital Maneuvering and Reaction Control Systems’ Valve and
Switch Classification Expert System (OMS) (chapter 11)
TEXT OUTLINE
Common to every chapter is a description of the available design, analysis, and verification tools; a section on historical perspective and related work; a summary; and
a set of exercises.
Chapter 1 introduces real-time systems, defines the notion of time and how to
measure it, and provides a synopsis of several analysis techniques, including simulation, testing, verification, and run-time monitoring. It also gives pointers to useful
resources in the study and design of real-time systems.
Chapter 2 describes the analysis and verification of non-real-time systems using
symbolic logic and automata-theoretic approaches. It covers topics in propositional
logic, proving satisfiability using the resolution procedure, predicate logic, prenex
normal forms, Skolem standard forms, proving unsatisfiability of a clause set with
Herbrand’s procedure and the resolution procedure, languages and their representations, finite automata, and the specification and verification of untimed systems.
Chapter 3 presents real-time scheduling and schedulability analysis, covering topics in computation time prediction, uniprocessor scheduling, scheduling preemptable and independent tasks, fixed-priority schedulers, rate-monotonic and deadlinemonotonic algorithms, dynamic-priority schedulers, earliest-deadline-first (EDF) algorithm, least-laxity-first (LL) algorithm, scheduling nonpreemptable sporadic tasks,
nonpreemptable tasks with precedence constraints, periodic tasks with precedence
constraints, communicating periodic tasks, deterministic rendezvous model, periodic
tasks with critical sections, kernelized monitor model, multiprocessor scheduling,
schedule representations, scheduling game board, sufficient conditions for conflictfree task sets, scheduling periodic tasks on a multiprocessor, PERTS, PerfoRMAx,
TimeWiz, and real-time operating systems (RTOSs).
Chapter 4 describes model checking of finite-state systems. Topics covered include system specification, Clarke–Emerson–Sistla model checker, CTL, complete
CTL model checker in C, symbolic model checking, binary decision diagrams, realtime CTL, minimum and maximum delays, minimum and maximum number of condition occurrences, and state graphs with non-unit transition time.
Chapter 5 presents visual formalism, Statecharts, and Statemate, covering basic Statecharts features, including OR-decomposition, AND-decomposition, delays
and timeouts, condition and selection entrances, and unclustering. It also describes
activity-charts, module-charts, Statechart semantics, and code executions and analysis.
Chapter 6 describes real-time logic (RTL), graph-theoretic analysis, and Modechart, covering specification and safety assertions, event-action model, restricted

Детали