Combining abstract interpretation with model checking for timing analysis of multicore software

Mingsong Lv, Wang Yi, Nan Guan, Ge Yu

Research output: Chapter in book / Conference proceedingConference article published in proceeding or bookAcademic researchpeer-review

80 Citations (Scopus)


It is predicted that multicores will be increasingly used in future embedded real-time systems for high performance and low energy consumption. The major obstacle is that we may not predict and provide any guarantee on real-time properties of software on such platforms. The shared memory bus is among the most critical resources, which severely degrade the timing predictability of multicore software due to the access contention between cores. In this paper, we study a multicore architecture where each core has a local L1 cache and all cores use a shared bus to access the off-chip memory. We use Abstract Interpretation (AI) to analyze the local cache behavior of a program running on a dedicated core. Based on the cache analysis, we construct a Timed Automaton (TA) to model when the programs access the memory bus. Then we model the shared bus also using timed automata. The TA models for the bus and programs will be explored using the UPPAAL model checker to find the WECTs for the respective programs. Based on the presented techniques, we have developed a tool for multi-core timing analysis, which allows automatic generation of the TA models from binary code and WCET estimation for any given TA model of the shared bus. Extensive experiments have been conducted, showing that the combined approach can significantly tighten the estimations. As examples, we have studied the TDMA and FCFS buses, of which the WCET bounds can be tightened by up to 240% and 82% respectively, compared with the worst-case bounds estimated based on worst-case bus access delay.
Original languageEnglish
Title of host publicationProceedings - 31st IEEE Real-Time Systems Symposium, RTSS 2010
Number of pages11
Publication statusPublished - 1 Dec 2010
Externally publishedYes
Event31st IEEE Real-Time Systems Symposium, RTSS 2010 - San Diego, CA, United States
Duration: 30 Nov 20103 Dec 2010


Conference31st IEEE Real-Time Systems Symposium, RTSS 2010
Country/TerritoryUnited States
CitySan Diego, CA

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture
  • Computer Networks and Communications


Dive into the research topics of 'Combining abstract interpretation with model checking for timing analysis of multicore software'. Together they form a unique fingerprint.

Cite this