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

Primary Classification:
  C. Computer Systems Organization
  C.4 PERFORMANCE OF SYSTEMS
      Subjects: Modeling techniques

General Terms:
Design, Performance, Verification

Keywords:
hard real-time systems, performance analysis, real-time calculus, timed automata