Paper Info
Title
Timed model checking with abstractions: towards worst-case response time analysis in resource-sharing manycore systems
Abstract
Multicore architectures are increasingly used nowadays in embedded real-time systems. Parallel execution of tasks feigns the possibility of a massive increase in performance. However, this is usually not achieved because of contention on shared resources. Concurrently executing tasks mutually block their accesses to the shared resource, causing non-deterministic delays. Timing analysis of tasks in such systems is then far from trivial. Recently, several analytic methods have been proposed for this purpose, however, they cannot model complex arbitration schemes such as FlexRay which is a common bus arbitration protocol in the automotive industry. This paper considers real-time tasks composed of superblocks, i.e., sequences of computation and resource accessing phases. Resource accesses such as accesses to memories and caches are synchronous, i.e., they cause execution on the processing core to stall until the access is served. For such systems, the paper presents a state-based modeling and analysis approach based on Timed Automata which can model accurately arbitration schemes of any complexity. Based on it, we compute safe bounds on the worst-case response times of tasks. The scalability of the approach is increased significantly by abstracting several cores and their tasks with one arrival curve, which represents their resource accesses and computation times. This curve is then incorporated into the Timed Automata model of the system. The accuracy and scalability of the approach are evaluated with a real-world application from the automotive industry and benchmark applications.
Year
DOI
Venue
2012
10.1145/2380356.2380372
EMSOFT
Keywords
Field
DocType
arbitration scheme,worst-case response time analysis,timed automata,manycore system,shared resource,model complex arbitration scheme,resource access,arrival curve,timed model checking,automotive industry,timed automata model,analysis approach,common bus arbitration protocol,embedded systems
FlexRay,Model checking,Computer science,Parallel computing,Automaton,Real-time computing,Arbitration,Shared resource,Multi-core processor,Distributed computing,Scalability,Automotive industry
Conference
Citations 
PageRank 
References 
22
0.78
19
Authors
4
Name
Order
Citations
PageRank
Georgia Giannopoulou119410.43
Kai Lampka222814.45
Nikolay Stoimenov332216.77
Lothar Thiele414025957.82