Analytic real-time analysis and timed automata: a hybrid method for analyzing embedded real-time systems

ABSTRACT

This paper advocates a strict compositional and hybrid approach for obtaining key (performance) metrics of embedded systems. At its core the developed methodology abstracts system components by either flow-oriented and purely analytic descriptions or by state-based models in the form of timed automata. The interaction among the heterogeneous components is modeled by streams of discrete activity-triggers. In total this yields a hybrid framework for the compositional analysis of embedded systems. It supplements contemporary techniques for the following reasons: (a) state space explosion as intrinsic to formal verification is limited to the level of isolated components; (b) computed performance metrics such as buffer sizes, delays and utilization rates are not overly pessimistic, because coarse-grained purely analytic models are used for components only which conform to the stateless model of computation. For demonstrating the usefulness of the presented ideas we implemented a corresponding tool-chain and investigated the performance of a two-staged computing system, where one stage exhibits state-dependent behavior only coarsely coverable by a purely analytic and stateless component abstraction.

References

1. R. Alur and D. L. Dill. Automata For Modeling Real-Time Systems. In M. Paterson, editor, Proc. of the 17th International Colloquium on Automata, Languages and Programming (ICALP'90), volume 443 of LNCS, pages 322--335. Springer, 1990.
2. G. Behrmann, A. David, and K. G. Larsen. A tutorial on uppaal. In M. Bernardo and F. Corradini, editors, Formal Methods for the Design of Real-Time Systems: 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004, number 3185 in LNCS, pages 200--236. Springer-Verlag, September 2004.
3. J. Bengtsson and W. Yi. Timed automata: Semantics, algorithms and tools. In Lectures on Concurrency and Petri Nets, volume 3098 of LNCS, pages 87--124. Springer, 2004.
4. J.-Y. L. Boudec and P. Thiran. Network Calculus: A Theory of Deterministic Queuing Systems for the Internet, volume 2050 of LNCS. Springer, 2001.
5. S. Chakraborty, S. Künzli, and L. Thiele. A General Framework for Analyzing System Properties in Platform-Based Embedded System Designs. Design, Automation and Test in Europe Conference and Exhibition, 1, 2003.
6. S. Chakraborty, L. T. X. Phan, and P. S. Thiagarajan. Event count automata: A state-based model for stream processing systems. In Proc. of the 26th IEEE International Real-Time Systems Symposium (RTSS'05), pages 87--98, 2005.
7. H. Dierks, A. Metzner, and I. Stierand. Efficient Model-Checking for Real-Time Task Networks. In Int. Conf. on Embedded Software and Systems 2009, 2009. Accepted for publication.
8. M. González Harbour, J. J. Gutiérrez García, J. C. Palencia Gutiérrez, and J. M. Drake Moyano. Mast: Modeling and analysis suite for real time applications. In Proc. of 13th Euromicro Conference on Real-Time Systems, pages 125--134. IEEE Computer Society, 2001.
9. M. Hendriks and M. Verhoef. Timed automata based analysis of embedded system architectures. In Proc. of the 20th Int. Parallel and Distributed Processing Symposium (IPDPS 2006). IEEE, 2006.
10. R. Henia, A. Hamann, M. Jersak, R. Racu, K. Richter, and R. Ernst. System Level Performance Analysis-The SymTA/S Approach. IEEE Proceedings-Computers and Digital Techniques, 152(2):148--166, 2005.
11. P. Krcal, L. Mokrushin, and W. Yi. A tool for compositional analysis of timed systems by abstraction (extended abstract). In Proc. of NWPT07, the 19th Nordic Workshop on Programming Theory, October 2007.
12. S. Künzli, A. Hamann, R. Ernst, and L. Thiele. Combined Approach to System Level Performance Analysis of Embedded Systems. In Proc. of the 5th Int. Conf. on Hardware/Software Codesign and System Synthesis 2007, pages 63--68, New York, NY, USA, 2007. ACM.
13. Modular Performance Analysis Framework and Matlab Toolbox. www.mpa.ethz.ch.
14. C. Norström, A. Wall, and W. Yi. Timed automata as task models for event-driven systems. In Proc. of the 6th Intl. Conference on Real-Time Computing Systems and Applications, page 182. IEEE Computer Society, 1999.
15. L. Phan, S. Chakraborty, and P. Thiagarajan. A Multi-mode Real-Time Calculus. In Proc. of the 28th IEEE Real-Time Systems Symposium (RTSS 2008), pages 59--69. IEEE Computer Society, 2008.
16. L. T. X. Phan, S. Chakraborty, P. S. Thiagarajan, and L. Thiele. Composing functional and state-based performance models for analyzing heterogeneous real-time systems. In Proc. of the 28th IEEE Real-Time Systems Symposium (RTSS 2007), pages 343--352. IEEE Computer Society, 2007.
17. L. Thiele, S. Chakraborty, and M. Naedele. Real-time calculus for scheduling hard real-time systems. In Proc. Intl. Symposium on Circuits and Systems, volume 4, pages 101--104, 2000.
18. The Uppaal timed model checker. www.uppaal.com.
19. E. Wandeler, L. Thiele, M. Verhoef, and P. Lieverse. System Architecture Evaluation Using Modular Performance Analysis: A Case Study. International Journal on Software Tools for Technology Transfer (STTT), 8(6):649--667, 2006.

Index Terms

• Computing methodologies

  • Modeling and simulation

    • Model development and analysis

      • Modeling methodologies