RealTime Systems: Scheduling, Analysis, and Verification (Google eBook)The first book to provide a comprehensive overview of the subject rather than a collection of papers.

What people are saying  Write a review
Review: RealTime Systems: Scheduling, Analysis, and Verification
User Review  Scott  GoodreadsThis was for a real time systems graduate class Read full review
Contents
1  
10  
3 REALTIME SCHEDULING AND SCHEDULABILITY ANALYSIS  41 
4 MODEL CHECKING OF FINITESTATE SYSTEMS  86 
5 VISUAL FORMALISM STATECHARTS AND STATEMATE  134 
6 REALTIME LOGIC GRAPHTHEORETIC ANALYSIS AND MODECHART  148 
7 VERIFICATION USING TIMED AUTOMATA  187 
8 TIMED PETRI NETS  212 
Common terms and phrases
ACSR actions algorithm analyze assigned automata automaton BDDs behavior bisimulation Boolean checking Cheng clause clock computation condition element constraints corresponding cycle deadline denote described determine edge enabling condition EQL program EQL(B equivalent Estella example execution exists expert system false firstorder logic fixed point function GPIp implementation initial input integer labeled language matching WMEs maximal number Modechart model checker modify mutually exclusive node number of rule operator OPS5 program optimization periodic tasks Petri nets predicate logic process algebra propositional logic reach a fixed reachable realtime systems responsetime Rete network rule firings rulebased program rulebased systems safety assertion satisfy semantic semantic tree sensor sequence set of rules special form specification sporadic tasks statespace graph Statecharts subrule subset symbol task set techniques temporal logic termination tokens transition relation transition table true upper bound values variables verification vertex WMEs writeln(stdout
Popular passages
Page 11  A literal is an atomic formula or the negation of an atomic formula, and we refer to these as being positive or negative, respectively.
Page 472  The Infeasibility of Quantifying the Reliability of LifeCritical RealTime Software," IEEE Transactions on Software Engineering, Vol.
Page 501  W. Zhao, K. Ramamritham, and J. Stankovic, "Scheduling Tasks with Resource Requirements in Hard RealTime Systems," IEEE Transactions on Software Engineering, May 1987.
Page 493  CY Park and AC Shaw, Experiments with a Program Timing Tool Based on SourceLevel Timing Schema, IEEE Computer, May 1991, 4856.
Page 19  ML are defined recursively as follows: 1. An atom is a formula. 2. If G is a formula, then so are ~G and G*.