| 摘要: |
| 在现代嵌入式系统中，性能的重要性日益凸显.传统的基于测量的性能分析方法在运行时对性能进行测试，往往在代码实现后才考虑实施.若此时发现的问题是体系结构或设计因素造成的，修复的代价将非常昂贵.提出了一种基于形式化模型的性能分析（formal method-based performance analysis，简称FMPA)方法框架，希望在系统开发的早期，对系统设计模型进行性能分析，以便尽早发现并解决潜在的性能问题.FMPA具有统一的对外接口（UML-MARTE)，基于多种形式化模型，并可对多种系统性能指标进行分析.该方法适用于基于模型的开发过程，可为实时嵌入式系统的设计开发提供多项性能指标的参考.通过介绍利用实时模型检测技术分析响应时间与吞吐量，利用概率模型检测技术分析系统可靠性，以及FMPA方法的支撑工具FMPAer的总体设计方案，说明了FMPA方法框架的可行性. |
| 关键词: UML MARTE 模型检测 响应时间 吞吐量 系统可靠性 |
| DOI： |
| 分类号: |
| 基金项目:国家自然科学基金（61572478，61472406，61472474) |
|
| Model-Based Performance Analysis Framework for Embedded Systems |
|
ZHU Xue-Yang
|
|
State Key Laboratory of Computer Science(Institute of Software, The Chinese Academy of Sciences), Beijing 100190, China
|
| 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. |
| Key words: UML MARTE model checking response time throughput system reliability |
