Model-Based Performance Analysis Framework for Embedded Systems
Author:
Affiliation:

Fund Project:

National High-Tech R&D Program of China (863) (2015AA015304); National Natural Science Foundation of China (61472052); Chongqing High-Tech Research Program (cstc2014yykfB40007)

  • Article
  • | |
  • Metrics
  • |
  • Reference [23]
  • |
  • Related
  • | | |
  • Comments
    Abstract:

    System performance becomes more and more important in modern embedded systems. Traditionally, system performance is measured after the system has been implemented. When it fails to meet the requirement due to the design of the application at this stage, the cost of fixing them would be high. This paper presents a framework of formal method-based performance analysis (FMPA), whose goal is to detect potential performance problems at the early stage of the model-based procedure of system development. FMPA is aimed to analyse multiple performance criteria. It provides unified input models (UML-MARTE) and various formal models as analysis models. The feasibility of FMPA is illustrated by throughput and response time analysis with real-time model checking, by system reliability prediction using probabilistic model checking, and is further confirmed by the implementation of its support tool FMPAer.

    Reference
    [1] Smith CU, Williams LG. Performance engineering of software systems. In:Lavagno L, Martin G, Selic B, eds. UML for Real:Design of Embedded Real-Time Systems. Dordrecht:Kluwer Academic Publishers, 2003. 343-365.
    [2] Balsamo S, Marco AD, Inverardi P, Simeoni M. Model-Based performance prediction in software development:A survey. IEEE Trans. on Software Engineering, 2004,30(5):295-310.
    [3] Becker S, Koziolek H, Reussner R. Model-Based performance prediction with the palladio component model. In:Proc. of the 6th Int'l Workshop on Software and Performance. ACM, 2007. 54-65.
    [4] Balsamo S, Personè VDN, Inverardi P. A review on queueing network models with finite capacity queues for software architectures performance prediction. Performance Evaluation, 2003,51(2-4):269-288.
    [5] UML Profile for MARTE:Modeling and analysis of real-time embedded systems. OMG Adopted Specification ptc/2010-08-33, ptc/2010-08-34.
    [6] Selic B, Gerard S. Modeling and Analysis of Real-Time and Embedded Systems with UML and MARTE:Developing Cyber-Physical Systems. New York:Elsevier, 2013.
    [7] Lopez-Grao JP, Merseguer J, Campos J. From UML activity diagrams to stochastic Petri nets:Application to software performance engineering. In:Proc. of the 4th Int'l Workshop on Software and Performance (WOSP 2004). 2004. 25-36.
    [8] Petriu DC, Woodside CM. Performance analysis with UML. In:Lavagno L, Martin G, Selic B, eds. UML for Real:Design of Embedded Real-Time Systems. Dordrecht:Kluwer Academic Publishers, 2003. 241-270.
    [9] FMPAer. http://lcs.ios.ac.cn/~zxy/tools/fmpaer.htm
    [10] Yan G, Zhu XY, Yan R, Li G. Formal throughput and response time analysis of MARTE models. In:Proc. of the 16th Int'l Conf. on Formal Engineering Methods (ICFEM 2014). LNCS 8829, 2014. 430-445.
    [11] Chai YS, Zhu XY, Yan RJ, Zhang GQ. MARTE models based system reliability prediction. Computer Science, 2015,42(12):82-86,91(in Chinese with English abstract).
    [12] Alur R, Dill DL. A theory of timed automata. Theoretical Computer Science, 1994,126(2):183-235.
    [13] Clarke EM, Emerson EA, Sistla AP. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. on Programming Languages and Systems, 1986,8(2):244-263.
    [14] Larsen KG, Pettersson P, Wang Y. UPPAAL in a nutshell. Int'l Journal on Software Tools for Technology Transfer, 1997,1(1):134-152.
    [15] Gokhale SS, Trivedi KS. Analytical models for architecture-based software reliability prediction:A unification framework. IEEE Trans. on Reliability, 2006,55(4):578-590
    [16] Cortellessa V, Singh H, Cukic B. Early reliability assessment of UML based software models. In:Proc. of the 3rd Int'l Workshop on Software and Performance. 2002. 302-309.
    [17] Forejt V, Kwiatkowska M, Norman G, Parker D. Automated verification techniques for probabilistic systems. In:Proc. of the 11th Int'l School on Formal Methods for the Design of Computer, Communication and Software Systems. Springer-Verlag, 2011. 53-113.
    [18] Kwiatkowska M, Norman G, Parker D. PRISM 4.0:Verification of probabilistic realtime systems. In:Proc. of the 23rd Int'l Conf. on Computer Aided Verification. Berlin:Springer-Verlag, 2011. 585-591.
    [19] http://www.eclipse.org/papyrus/
    [20] http://www.eclipse.org/atl/
    [21] Z3Opt. http://rise4fun.com/z3opt/tutorialcontent/guide
    附中文参考文献:
    [11] 柴叶生,朱雪阳,晏荣杰,张广泉.基于MARTE模型的系统可靠性预测.计算机科学,2015,42(12):82-86,91.
    Related
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

朱雪阳.基于模型的嵌入式系统性能分析框架.软件学报,2016,27(S2):328-335

Copy
Share
Article Metrics
  • Abstract:3044
  • PDF: 4255
  • HTML: 0
  • Cited by: 0
History
  • Received:September 20,2016
  • Revised:November 17,2016
  • Online: January 10,2017
You are the first2038320Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063