Timing Analysis of Synchronous Programs using WCRT Algebra: Scalability through Abstraction

Abstract

Synchronous languages are ideal for designing safety-critical systems. Static Worst-Case Reaction Time (WCRT) analysis is an essential component in the design flow that ensures the real-time requirements are met. There are a few approaches for WCRT analysis, and the most versatile of all is explicit path enumeration. However, as synchronous programs are highly concurrent, techniques based on this approach, such as model checking, suffer from state explosion as the number of threads increases. One observation on this problem is that these existing techniques analyse the program by enumerating a functionally equivalent automaton while WCRT is a non-functional property. This mismatch potentially causes algorithm-induced state explosion. In this paper, we propose a WCRT analysis technique based on the notion of timing equivalence, expressed using WCRT algebra. WCRT algebra can effectively capture the timing behaviour of a synchronous program by converting its intermediate representation Timed Concurrent Control Flow Graph (TCCFG) into a Tick Cost Automaton (TCA), a minimal automaton that is timing equivalent to the original program. Then the WCRT is computed over the TCA. We have implemented our approach and benchmarked it against state-of-the-art WCRT analysis techniques. The results show that the WCRT algebra is 3.5 times faster on average than the fastest published technique.

References

1. 2016. Gurobi optimiser. (Nov. 2016). http://www.gurobi.com.
2. 2016. UPPAAL model checker. (Nov. 2016). http://www.uppaal.org.
3. J. Aguado, M. Mendler, J. J. Wang, B. Bodin, and P. Roop. 2017. Compositional timing-aware semantics for synchronous programming. In Forum on Specification and Design Languages (FDL’2017). Verona, Italy.
4. Sidharta Andalam, Partha S. Roop, and Alain Girault. 2011. Pruning infeasible paths for tight WCRT analysis of synchronous programs. In Design, Automation Test in Europe Conference Exhibition (DATE). 1--6.
5. Sidharta Andalam, Partha S. Roop, Alain Girault, and Claus Traulsen. 2014. A predictable framework for safety-critical embedded systems. IEEE Trans. Comput. 63, 7 (July 2014), 1600--1612.
6. Marian Boldt, Claus Traulsen, and Reinhard von Hanxleden. 2008. Compilation and worst-case reaction time analysis for multithreaded esterel processing. EURASIP Journal on Embedded Systems (2008), 594129.
7. Reinhold Heckmann and Christian Ferdinand. 2005. Verifying safety-critical timing and memory-usage properties of embedded software by abstract interpretation. In Proceedings of the Design, Automation Test in Europe Conference Exhibition (DATE). 618--619.
8. Lei Ju, Bach Khoa Huynh, Samarjit Chakraborty, and Abhik Roychoudhury. 2009. Context-sensitive timing analysis of esterel programs. In Proceedings of the Design Automation Conference (DAC). 870--873.
9. Lei Ju, Bach Khoa Huynh, Abhik Roychoudhury, and Samarjit Chakraborty. 2012. Performance debugging of esterel specifications. Real-Time System 48, 5 (Sept. 2012), 570--600.
10. Matthew Kuo, Roopak Sinha, and Partha S. Roop. 2011. Efficient WCRT analysis of synchronous programs using reachability. In Proceedings of the Design Automation Conference (DAC). 480--485.
11. Yau-Tsun Steven Li and Sharad Malik. 1995. Performance analysis of embedded software using implicit path enumeration. In Proceedings of Languages, Compilers and Tools for Real-time Systems (LCTES), Vol. 30. ACM, 88--98.
12. Michael Mendler, Partha S. Roop, and Bruno Bodin. 2016. A novel WCET semantics of synchronous programs. In International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS). Springer, 195--210.
13. Pascal Raymond, Claire Maiza, Catherine Parent-Vigouroux, Fabienne Carrier, and Mihail Asavoae. 2015. Timing analysis enhancement for synchronous program. Real-Time Systems 51, 2 (2015), 192--220.
14. Partha S. Roop, Sidharta Andalam, Reinhard von Hanxleden, Simon Yuan, and Claus Traulsen. 2009. Tight WCRT analysis of synchronous C programs. In Compilers, Architecture, and Synthesis for Embedded Systems (CASES). 205--214.
15. Reinhard von Hanxleden, Björn Duderstadt, Christian Motika, Steven Smyth, Michael Mendler, Joaquín Aguado, Stephen Mercer, and Owen O’Brien. 2014. SCCharts: Sequentially constructive statecharts for safety-critical applications: HW/SW-synthesis for a conservative extension of synchronous statecharts. In Programming Language Design and Implementation (PLDI). ACM, 372--383.
16. Jia Jie Wang, Partha S. Roop, and Sidharta Andalam. 2013. ILPc: A novel approach for scalable timing analysis of synchronous programs. In Compilers, Architecture, and Synthesis for Embedded Systems (CASES). 1--10.
17. Li Hsien Yoong, Partha S. Roop, and Zoran Salcic. 2013. Implementing constrained cyber-physical systems with IEC 61499. In ACM Transactions on Embedded Computing Systems (TECS). Number 1. ACM.
18. Li Hsien Yoong and Gareth D. Shaw. 2010. Auckland Function Block Benchmark.University of Auckland. (2010). pretzel.ece.auckland.ac.nz/files/iec61499-benchmarks.zip.

Index Terms

• Computer systems organization

  • Embedded and cyber-physical systems

    • Embedded systems

      • Embedded software

  • Real-time systems