Modeling Embedded Systems and SoCs

Concurrency and Time in Models of Computation

by Axel Jantsch, ISBN 1558609253, Hardback, 375 Pages, Morgan Kaufmann, June 2003.

Slides

• Introductory lecture on Systems and Models and the Rugby Meta-Model.
• Lecture on Finite State Machines.
• Lecture on Petri Nets.
• Lecture on the Untimed Model of Computation.
• Lecture on the Synchronous Model of Computation.
• Lecture on the Timed Model of Computation.
• Lecture on MoC Integration and Process Migration.
• Lecture on Tightly Coupled Process Networks
• Lecture on Nondeterminism and Probability (slides to be made).
• Lecture on Applications (slides to be made).

Errata

• The last sentence in definition 2.19 on page 88 is not correct because it does not allow for vectors with weight 0 on some places. It should read:

  The Petri net is conservative if it is conservative with respect to a weighting vector which has a positive non zero weight for some places and weights of 0 on the other places.

  The following algorithm constructs the coverability tree for the Petri net $N=(P,T,A,w,\Vx_0)$.

• Algorithm 2.2 uses $x$ incorrectly instead of $x'$ at several places in steps 2.2.2 and 2.2.3. Steps 2.2.2 and 2.2.3 should read as follows:
  
• In section 3.1.5.1 on page 164 on Initial Buffer Conditions the schedule given in the first paragraph for initial buffer condisions $[6,0]$ is not correct, because it has one $t_1$ transition too much. A correct schedule is
  $$\phi = [t_2,t_2,t_1,t_1,t_1]$$