printlogo
ETH Zuerich - Homepage
Computer Engineering and Networks Laboratory (TIK)
 

Publication Details for Inproceedings "Timed Model Checking with Abstractions: Towards Worst-Case Response Time Analysis in Resource-Sharing Manycore Systems"

 

 Back

 New Search

 

Authors: Georgia Giannopoulou, Kai Lampka, Nikolay Stoimenov, Lothar Thiele
Group: Computer Engineering
Type: Inproceedings
Title: Timed Model Checking with Abstractions: Towards Worst-Case Response Time Analysis in Resource-Sharing Manycore Systems
Year: 2012
Month: October
Pub-Key: glst2012a
Book Titel: Proc. International Conference on Embedded Software (EMSOFT)
Pages: 63-72
Keywords: ESD, MPA
Publisher: ACM
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 re- source 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.
Location: Tampere, Finland
Resources: [BibTeX] [ External LINK ] [Paper as PDF]

 

 Back

 New Search