Title
Verification of printer datapaths using timed automata
Abstract
In multiprocessor systems with many data-intensive tasks, a bus may be among the most critical resources. Typically, allocation of bandwidth to one (high-priority) task may lead to a reduction of the bandwidth of other tasks, and thereby effectively slow down these tasks. WCET analysis for these types of systems is a major research challenge. In this paper, we show how the dynamic behavior of a memory bus and a USB in a realistic printer application can be faithfully modeled using timed automata. We analyze, using Uppaal, the worst case latency of scan jobs with uncertain arrival times in a setting where the printer is concurrently processing an infinite stream of print jobs.
Year
DOI
Venue
2010
10.1007/978-3-642-16561-0_38
ISoLA
Keywords
Field
DocType
memory bus,multiprocessor system,infinite stream,wcet analysis,print job,dynamic behavior,major research challenge,data-intensive task,realistic printer application,critical resource
Latency (engineering),Computer science,Automaton,Real-time computing,Multiprocessing,Bandwidth (signal processing),Memory bus,Partial order reduction,Design space exploration,Embedded system,USB
Conference
Volume
ISSN
ISBN
6416
0302-9743
3-642-16560-5
Citations 
PageRank 
References 
4
0.45
14
Authors
2
Name
Order
Citations
PageRank
Georgeta Igna1453.91
Frits Vaandrager21571105.12