Formal Modeling and Scheduling of Datapaths of Digital Document Printers

Abstract. 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 stateof-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.

• Type: Conference
• Year: 2008
• Where: FORMATS
• Authors: Georgeta Igna, Venkatesh Kannan, Yang Yang, Twan Basten, Marc Geilen, Frits W. Vaandrager, Marc Voorhoeve, Sebastian de Smet, Lou J. Somers
• Keywords: Challenging Industrial Case, Formal Methods, FORMATS 2008, Image Processing Pipeline, Synchronous Data Flow