Formal Modeling and Scheduling of Data Paths of Digital Document Printers
We apply three different modeling frameworks -- timed automata (Uppaal), colored Petri nets and synchronous data flow -- to
model a challenging industrial case study that involves an existing state-of-the-art image processing pipeline. Each of the resulting models is used
to derive schedules for multiple concurrent jobs in the presence of limited resources (processing units, memory, USB bandwidth,..). The three
models and corresponding analysis results are compared.
-
Formal Modeling and Scheduling of Data Paths of Digital Document Printers
G. Igna, V. Kannan, Y. Yang, T. Basten, M.C.W. Geilen, F.W. Vaandrager, M. Voorhoeve, S. de Smet, and L.J. Somers.
In F. Cassez and C. Jard, editors, Formal Modelling and Analysis of Timed Systems, 6th International Conference, FORMATS 2008, Proceedings, pages 170-187. Saint-Malo, France, 15-17 September, 2008. Lecture Notes in Computer Science 5215. Springer, Berlin, Germany, 2008. (abstract, pdf).
|
