research-article

Enabling parametric feasibility analysis in real-time calculus driven performance evaluation

Authors:

Alena Simalatsar,

Simon Perathoner,

Roberto Passerone,

Lothar ThieleAuthors Info & Claims

CASES '11: Proceedings of the 14th international conference on Compilers, architectures and synthesis for embedded systems

Pages 155 - 164

https://doi.org/10.1145/2038698.2038723

Published: 09 October 2011 Publication History

Abstract

This paper advocates a rigorously formal and compositional style for obtaining key performance and/or interface metrics of systems with real-time constraints. We propose a hierarchical approach that couples the independent and different by nature frameworks of Modular Performance Analysis with Real-time Calculus (MPA-RTC) and Parametric Feasibility Analysis (PFA). Recent work on Real-time Calculus (RTC) has established an embedding of state-based component models into RTC-driven performance analysis for dealing with more expressive component models. However, with the obtained analysis infrastructure it is possible to analyze components only for a fixed set of parameters, e.g., fixed CPU speeds, fixed buffer sizes etc., such that a big space of parameters remains unstudied. In this paper, we overcome this limitation by integrating the method of parametric feasibility analysis in an RTC-based modeling environment. Using the PFA tool-flow, we are able to find regions for component parameters that maintain feasibility and worst-case properties. As a result, the proposed analysis infrastructure produces a broader range of valid design candidates, and allows the designer to reason about the system robustness.

References

[1]

R. Alur and D. L. Dill. Automata For Modeling Real-Time Systems. In M. Paterson, editor, ICALP'90, LNCS 443, pages 322--335. Springer, 1990.

Digital Library

[2]

R. Alur, T. A. Henzinger, and M. Y. Vardi. Parametric real-time reasoning. In STOC'93, pages 592--601, New York, NY, USA, 1993. ACM.

Digital Library

[3]

E. André, T. Chatain, L. Fribourg, and E. Encrenaz. An Inverse Method for Parametric Timed Automata. Electron. Notes Theor. Comput. Sci., 223:29--46, December 2008.

Digital Library

[4]

A. Basu, M. Bozga, and J. Sifakis. Modeling Heterogeneous Real-time Components in BIP. In Proc. of the Fourth IEEE Intl. Conference on Software Engineering and Formal Methods, pages 3--12, Washington, DC, USA, 2006. IEEE Computer Society.

Digital Library

[5]

G. Behrmann, R. David, and K. G. Larsen. A tutorial on Uppaal. In Formal Methods for the Design of Real-Time Systems: 4th Intl. School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004, pages 200--236. Springer, 2004.

[6]

E. Bini and G. C. Buttazzo. Schedulability Analysis of Periodic Fixed Priority Systems. IEEE Trans. Comput., 53(11):1462--1473, 2004.

Digital Library

[7]

M. Büker, A. Metzner, and I. Stierand. Testing real-time task networks with functional extensions using model-checking. In Proc. of the 14th IEEE int. conference on Emerging technologies & factory automation, ETFA'09, pages 564--573, Piscataway, NJ, USA, 2009. IEEE Press.

Digital Library

[8]

G. C. Buttazzo. Hard Real-Time Computing Systems: Predictable Scheduling Algorithms and Applications. Kluwer Academic Publishers, Norwell, MA, USA, 1997.

Digital Library

[9]

S. Chakraborty, L. T. X. Phan, and P. S. Thiagarajan. Event Count Automata: A State-Based Model for Stream Processing Systems. In RTSS'05, pages 87--98, 2005.

Digital Library

[10]

A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: A New Symbolic Model Verifier. In N. Halbwachs and D. Peled, editors, CAV'99, volume 1633 of Lecture Notes in Computer Science, pages 495--499. Springer, 1999.

Digital Library

[11]

A. Cimatti, L. Palopoli, and Y. Ramadian. Symbolic Computation of Schedulability Regions Using Parametric Timed Automata. RTSS'08, 0:80--89, 2008.

Digital Library

[12]

A. Cimatti, L. Palopoli, and Y. Ramadian. Symbolic Computation of Schedulability Regions Using Parametric Timed Automata. In RTSS'08, Nov. 30 - Dec. 3 2008.

Digital Library

[13]

H. Dierks, A. Metzner, and I. Stierand. Efficient Model-Checking for Real-Time Task Networks. In Proc. of the 2009 Intl. Conference on Embedded Software and Systems, pages 11--18, Washington, DC, USA, 2009.

Digital Library

[14]

L. Doyen, T. A. Henzinger, A. Legay, and D. Nickovic. Robustness of Sequential Circuits. In ACSD'10, pages 77--84, 2010.

Digital Library

[15]

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.

Digital Library

[16]

R. Henia, A. Hamann, M. Jersak, R. Racu, K. Richter, and R. Ernst. System Level Performance Analysis-The SymTA/S Approach. IEEE Proc.-Computers and Digital Techniques, 152(2):148--166, 2005.

[17]

T. Hune, J. Romijn, M. Stoelinga, and F. W. Vaandrager. Linear Parametric Model Checking of Timed Automata. In TACAS'01, pages 189--203, London, UK, 2001. Springer-Verlag.

Digital Library

[18]

K. Keutzer, S. Malik, A. R. Newton, J. Rabaey, and A. Sangiovanni-Vincentelli. System Level Design: Orthogonolization of Concerns and Platform-Based Design. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 19(12), December 2000.

Digital Library

[19]

P. Krcal, L. Mokrushin, and W. Yi. A tool for compositional analysis of timed systems by abstraction (extended abstract). In Proc. of 19th Nordic Workshop on Programming Theory (NWPT07), October 2007.

[20]

K. Lampka, S. Perathoner, and L. Thiele. Analytic Real-Time Analysis and Timed Automata: A Hybrid Method for Analyzing Embedded Real-Time Systems. In EMSOFT'09: Proc. of the 7th ACM int. conference on Embedded software, pages 107--116, New York, NY, USA, 2009. ACM.

Digital Library

[21]

K. Lampka, S. Perathoner, and L. Thiele. Analytic Real-Time Analysis and Timed Automata: A Hybrid Methodology for the Performance Analysis of Embedded Real-Time Systems. Design Automation for Embedded Systems, 14(3):193--227, 2010.

Digital Library

[22]

C. Lu, J. A. Stankovic, T. F. Abdelzaher, G. Tao, S. H. Son, and M. Marley. Performance Specifications and Metrics for Adaptive Real-Time Systems. In RTSS'00. IEEE Computer Society, 2000.

Digital Library

[23]

M. Lv, G. Nan, W. Yi, and G. Yu. Combining Abstract Interpretation with Model Checking for Timing Analysis of Multicore Software. In RTSS'10, pages 339--349, Washington, DC, USA, 2010. IEEE Computer Society.

Digital Library

[24]

C. Norström, A. Wall, and W. Yi. Timed Automata as Task Models for Event-Driven Systems. In RTCSA '99, page 182, Washington, DC, USA, 1999. IEEE Computer Society.

Digital Library

[25]

S. Perathoner, E. Wandeler, L. Thiele, A. Hamann, S. Schliecker, R. Henia, R. Racu, R. Ernst, and M. G. Harbour. Influence of different system abstractions on the performance analysis of distributed real-time systems. In Proc. of the 7th ACM & IEEE int. conference on Embedded software, EMSOFT '07, pages 193--202, New York, NY, USA, 2007. ACM.

Digital Library

[26]

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 RTSS'07, pages 343--352, Washington, DC, USA, 2007. IEEE Computer Society.

Digital Library

[27]

A. L. Sangiovanni-Vincentelli. Quo Vadis, SLD? Reasoning About the Trends and Challenges of System Level Design. Proc. of the IEEE, 95(3):467--506, March 2007.

[28]

K. Sen, M. Viswanathan, and G. Agha. Statistical Model Checking of Black-Box Probabilistic Systems. In CAV'04, LNCS 3114, pages 202--215. Springer, 2004.

[29]

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.

[30]

E. Wandeler, L. Thiele, M. Verhoef, and P. Lieverse. System Architecture Evaluation Using Modular Performance Analysis: A Case Study. STTT, 8(6):649--667, 2006.

Digital Library

[31]

E. Wandeler, L. Thiele, M. Verhoef, and P. Lieverse. System Architecture Evaluation Using Modular Performance Analysis: A Case Study. STTT, 8(6):649--667, 2006.

Digital Library

[32]

S. Yovine. Model Checking Timed Automata. In G. Rozenberg and F. W. Vaandrager, editors, European Educational Forum: School on Embedded Systems, volume 1494 of Lecture Notes in Computer Science, pages 114--152. Springer, 1996.

Digital Library

[33]

D. Zhang and R. Cleaveland. Fast On-the-Fly Parametric Real-Time Model Checking. In RTSS'05, pages 157--166, Washington, DC, USA, 2005. IEEE Computer Society.

Digital Library

Cited By

Lampka KLackorzynski A(2019)Using Hypervisor Technology for Safe and Secure Deployment of High-Performance Multicore Platforms in Future Vehicles2019 26th IEEE International Conference on Electronics, Circuits and Systems (ICECS)10.1109/ICECS46596.2019.8964912(783-786)Online publication date: Nov-2019
https://doi.org/10.1109/ICECS46596.2019.8964912
Lampka KGiannopoulou GPellizzoni RWu ZStoimenov N(2018)A formal approach to the WCRT analysis of multicore systems with memory contention under phase-structured task setsReal-Time Systems10.1007/s11241-014-9211-y50:5-6(736-773)Online publication date: 28-Dec-2018
https://dl.acm.org/doi/10.1007/s11241-014-9211-y
Altisen KMoy M(2016)Causality problem in real-time calculusFormal Methods in System Design10.1007/s10703-016-0250-y48:1-2(1-45)Online publication date: 1-Apr-2016
https://dl.acm.org/doi/10.1007/s10703-016-0250-y
Show More Cited By

Recommendations

Performance analysis of AADL models using real-time calculus
Monterey'08: Proceedings of the 15th Monterey conference on Foundations of Computer Software: future Trends and Techniques for Development

Architecture Analysis and Design Language (AADL) captures both platform and software architectures of embedded systems in a component-oriented fashion. Properties embedded in an AADL model enable several high-level analysis techniques. In this work, we ...
Finitary Real-Time Calculus: Efficient Performance Analysis of Distributed Embedded Systems
RTSS '13: Proceedings of the 2013 IEEE 34th Real-Time Systems Symposium

Real-Time Calculus (RTC) is a powerful framework to analyze real-time performance of distributed embedded systems. However, RTC may run into serious analysis efficiency problems when applied to systems of large scale and/or with complex timing parameter ...
A Survey of WCET Analysis of Real-Time Operating Systems
ICESS '09: Proceedings of the 2009 International Conference on Embedded Software and Systems

Timing correctness of hard real-time systems is guaranteed by schedulability analysis and worst-case execution time (WCET) analysis of programs. Traditional WCET analysis mainly deals with application programs and has achieved success in industry. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CASES '11: Proceedings of the 14th international conference on Compilers, architectures and synthesis for embedded systems

October 2011

250 pages

ISBN:9781450307130

DOI:10.1145/2038698

Program Chairs:
Rajesh Gupta
University of California at San Diego
,
Vincent Mooney
Georgia Tech. & Nanyang Tech. U.

Copyright © 2011 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 October 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ESWeek '11

Sponsor:

ESWeek '11: Seventh Embedded Systems Week

October 9 - 14, 2011

Taipei, Taiwan

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
140
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Lampka KLackorzynski A(2019)Using Hypervisor Technology for Safe and Secure Deployment of High-Performance Multicore Platforms in Future Vehicles2019 26th IEEE International Conference on Electronics, Circuits and Systems (ICECS)10.1109/ICECS46596.2019.8964912(783-786)Online publication date: Nov-2019
https://doi.org/10.1109/ICECS46596.2019.8964912
Lampka KGiannopoulou GPellizzoni RWu ZStoimenov N(2018)A formal approach to the WCRT analysis of multicore systems with memory contention under phase-structured task setsReal-Time Systems10.1007/s11241-014-9211-y50:5-6(736-773)Online publication date: 28-Dec-2018
https://dl.acm.org/doi/10.1007/s11241-014-9211-y
Altisen KMoy M(2016)Causality problem in real-time calculusFormal Methods in System Design10.1007/s10703-016-0250-y48:1-2(1-45)Online publication date: 1-Apr-2016
https://dl.acm.org/doi/10.1007/s10703-016-0250-y
Simalatsar ABornet RYou WThoma YMicheli G(2014)Safe Implementation of Embedded Software for a Portable Device Supporting Drug AdministrationProceedings of the 2014 IEEE International Conference on Bioinformatics and Bioengineering10.1109/BIBE.2014.55(257-264)Online publication date: 10-Nov-2014
https://dl.acm.org/doi/10.1109/BIBE.2014.55
Neukirchner MLampka KQuinton SErnst RMarculescu RPanda P(2013)Multi-mode monitoring for mixed-criticality real-time systemsProceedings of the Ninth IEEE/ACM/IFIP International Conference on Hardware/Software Codesign and System Synthesis10.5555/2555692.2555726(1-10)Online publication date: 29-Sep-2013
https://dl.acm.org/doi/10.5555/2555692.2555726
Neukirchner MLampka KQuinton SErnst R(2013)Multi-mode monitoring for mixed-criticality real-time systems2013 International Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS)10.1109/CODES-ISSS.2013.6659021(1-10)Online publication date: Sep-2013
https://doi.org/10.1109/CODES-ISSS.2013.6659021
Houben FIgna GVaandrager F(2013)Modeling task systems using parameterized partial ordersInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-012-0264-815:3(269-286)Online publication date: 1-Jun-2013
https://dl.acm.org/doi/10.1007/s10009-012-0264-8
Lampka KPerathoner SThiele L(2013)Component-based system designInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-012-0257-715:3(155-170)Online publication date: 1-Jun-2013
https://dl.acm.org/doi/10.1007/s10009-012-0257-7
Simalatsar A(2012)Integration of correct-by-construction BIP models into the MetroII design space exploration flowProceedings of the 2012 IEEE 30th International Conference on Computer Design (ICCD 2012)10.1109/ICCD.2012.6378688(490-491)Online publication date: 30-Sep-2012
https://dl.acm.org/doi/10.1109/ICCD.2012.6378688

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten