基于形式化模型的性能分析FMPA方法及工具设计概述.PDF
文本预览下载声明
基于形式化模型的性能分析(FMPA)方法及工具设计概述
朱雪阳
中国科学院软件研究所计算机科学实验室
摘要
传统的基于测量的性能分析方法往往在代码实现后才考虑实施，而有些性能
问题在开发过程的早期已经被引入，这时才予以考虑，为时太晚；因为修改必须
回溯到系统的早期模型，势必增加开发成本及周期。因此，我们提出了一种基于
形式化模型的性能分析(FMPA)方法，希望在系统开发的早期，利用模型对性能
进行分析以尽早发现并解决性能问题。本文还概述了该方法支撑工具(FMPAer)
的设计方案。
FMPA 方法旨在为实时嵌入式系统的设计开发提供多项性能指标的参考，适
用于基于模型的开发过程。FMPA 具有统一对外接口(UML+MARTE)、基于多种
形式化模型、可对多种系统性能指标进行分析的方法。FMPAer 的输入为UML+
MARTE 模型及所需分析的性能指标，输入为相关性能指标值。
1. 研究背景
随着计算机系统的广泛使用，软件性能问题得到越来越多的关注；特别是安
全攸关的软件，其性能更是关键。在很多情况下，无法满足性能需求的软件已不
能算正确。
传统的基于测量的性能分析方法在运行时对性能进行测试，往往在代码实现
后才考虑实施。实践经验表明，有些性能问题既不能通过代码的性能调优加以解
决，也不能通过增加硬件得到改善；这是由于这些问题是体系结构或设计因素造
成的，而不是低效的编码引起的。这样的性能问题在开发过程的早期已经被引入，
到集成测试或更晚的时候才予以考虑，为时太晚；因为修改必须回溯到系统的早
期模型，势必增加开发成本及周期。
因此，有必要研究在系统开发的早期，利用模型对性能进行分析与优化方法
以便尽早发现并解决性能问题，提高开发效率并降低成本。
统一建模语言 UML 作为面向对象建模语言，因其建模的灵活性和实用性，
且可对系统的多个侧面进行建模，在软件开发中得到广泛应用，并已成为事实的
工业标准。为了对实时嵌入式系统进行建模与分析，OMG 又提出 UML-MARTE
（Modeling and Analysis of Real-Time Embedded system ）标准，对UML 在性能
和时间属性建模方面进行扩充。但 UML 缺乏精确的语义，难以直接对 UML 模
型进行性能分析。形式化方法是基于数学的手段为软件和硬件系统提供精确规约、
开发和验证的方法，以严格的形式化模型为中心，可以弥补 UML 在这方面的不
足。但是形式化方法技术一般较难学习与掌握，因为在对系统进行性能分析时，
需要软件设计人员对系统构造形式化模型，软件设计人员需要具有相关的数学知
识背景。
如何结合 UML 模型与形式化方法的研究成果，形成优势互补，以对系统性
能进行分析是一重要且复杂的科学问题。本文提出的 FMPA (Formal Models based
Performance Analysis)方法正是希望通过部分地解决这一问题，将形式化方法应
用于软件性能分析，为实时嵌入式系统的开发提供多项性能指标评估参考。相关
支撑工具 FMPAer (Formal Models based Performance Analyzer)具有统一的对外接
口(UML+MARTE)、基于多种形式化模型、可对多种系统性能指标进行分析。
2. FMPA 方法框架
FMPA 方法总体研究框架如图 1 所示。
图1 FMPA 总体研究框架
以下就性能建模、性能分析及性能优化三方面简述之。
1) 性能建模
为了兼顾工程上使用的方便性及分析所需的严格性，FMPA 建模语言分抽象
与具体两个层次：抽象层提供对外一致接口；具体层为形式化分析提供基础。为
方便工程师使用，抽象层采用工业界的事实标准 UML-MARTE 中的性能模型；
具体层为针对不同性能指标、不同系统特点，采用不同的具有严格语义模型的形
式化语言，包括模型 Petri 网、数据流图、时间自动机及马尔柯夫决策过程等。
UML-MARTE 用状态机、活动图、顺序图等行为图描述系统行为，相关性能分
析参数作为注
显示全部