【作者】 杨年华；

【导师】 虞慧群；

【作者基本信息】 华东理工大学 ， 计算机应用技术， 2011， 博士

【摘要】 随着硬件性能的快速提升,通信与网络的迅速发展,嵌入式系统及其应用不断涌现。嵌入式软件系统的复杂性也在迅速增长。软件在嵌入式系统中占据重要地位。如何利用现代软件工程的方法与技术,降低软件开发的复杂性、适应经常变化的客户需求、降低开发成本、提高软件可信性已经成为嵌入式软件开发领域的重要课题。将软件需求描述与特定平台的实现分离是实现缩短软件开发时间、适应不断变化的需求、降低开发成本的有效手段。模型驱动架构(Model Driven Architecture, MDA)是目前实现这一目标的最有吸引力的方法之一。在基于MDA的软件早期设计阶段,目标系统的可选方案可以做充分的检查和比较。软件的开发风险因而可以被降低。模型是基于MDA的软件开发过程中最主要的元素。UML已经是事实上的软件建模标准,并且被OMG推荐用来描述MDA中的建模。然而UML无法描述系统非功能属性。非功能属性在可信软件开发过程中非常重要。OMG最近针对嵌入式系统建模和分析的需要提出了MARTE Profile来描述嵌入式系统的非功能属性。本文将MARTE的Stereotype和标签值标注在UML模型的相关节点上。带MARTE标注的UML模型记为UML/MARTE。形式化方法是提高软件可信性的重要手段。为了形式化地描述嵌入式系统,本文给出了带抑止弧的时延着色Petri网(TCPNIA),并围绕TCPNIA给出了相应的模型验证与分析方法。为了在MDA的早期开发阶段利用TCPNIA形式化地验证和分析UML模型,文章给出了从UML/MARTE模型到TCPNIA模型的转换方法。本文的主要研究成果包括如下方面：(1)给出了在UML图形中利用MARTE Profile标注非功能属性的方法。通过在活动图与序列图中选择恰当的被标注节点,该方法可以实现层次化地标注UML图形,从而可以提高模型及相关验证结果的可重用性。给出了UML/MARTE模型元素的形式化定义,这为模型的形式化转换与分析奠定了基础。(2)提出了一种融合时延Petri网、着色Petri网和抑制弧的特征的模型TCPNIA,并在变迁中引入能量消耗特征和数据操作函数,给出了TCPNIA的形式化语法和语义。这一模型既可以实现对复杂系统的功能和非功能属性建模,又可以充分利用现有Petri网的分析技术。TCPNIA模型为利用Petri网建模与分析实时嵌入式系统提供了基础。(3)给出了从TCPNIA到时间自动机(Timed Automaton, TA)的转换算法。该算法引入变迁冲突调解机制,保证时延变迁语义在时间自动机中得到保持。本文的方法也适用于利用Uppaal验证一般时延Petri网。(4)给出了一种在时间和资源限制下的TCPNIA模型的任务调度算法。在计算时间消耗时考虑了路径中变迁的并行执行情况。为了提高模型分析结果的重用性和计算效率,本文分析了可调度路径的分解与组合分析方法。该算法采用递归的深度优先搜索方法,只需产生部分状态空间,从而在一定程度上减轻了状态爆炸问题。(5)分别以图形化和形式化语法方式给出了从UML/MARTE到TCPNIA的转换方法。该方法根据UML模型特征确定面向方面的切入点,并给出了自动生成方面的算法。在面向方面编织规则的基础上,给出了Petri网模型的自动组合算法。这些方法为开发从UML/MARTE到TCPNIA模型的自动转换工具提供了理论基础。更多还原

【Abstract】 Embedded systems and their applications emerge continuously with the rapid upgrading of hardware performance and rapid development of communications and networks. Software plays an important role in an embedded system. How to use modern software engineering methods and techniques, reduce the complexity of software development, meet the constantly evaluation of customer requirements, reduce development costs and improve software trustworthiness has become an important topic in the field of embedded software development.Separating the application description from the platform specific implementation is a promising solution to reduce software development time, meet contant evaluation of customer requirements and reduce development costs. MDA (Model Driven Architecture, MDA) is one of the most attractive approaches to achieving this goal at present. In the early design phase of MDA, alternative solutions to the target system can be investigated and compared. So software development risks can be minimized.Models are the most important objects during software development processes in MDA. UML has become the de facto standard modeling language for software development. And it is recommended by OMG to describe models in MDA. But UML lacks the ability to describe non-functional properties which are important in trustworthy software development processes. A new UML profile dedicated for modeling and analysis of real-time and embedded (MARTE) systems is recently presented by OMG to describe non-function properties in an embedded system. MARTE stereotypes and tags are annotated on the related nodes in a UML diagram in this thesis. A UML diagram annotated with MARTE is expressed as UML/MARTE.Formal methods are important means to improve software trustworthy. To formally describe embedded systems, timed colored Petri net with inhibitor arcs (TCPNIA) is proposed in thesis. Model checking and analysis methods for TCPNIA models are also proposed. In order to formally verify and analyze UML models using TCPNIA in the early development stage of MDA, model transformation methods from UML/MARTE to TCPNIA are proposed.Contributions of this thesis are summarized as follows.(1) Methods to annotate non-functional properties on UML diagrams with MARTE Profile are proposed. UML diagrams can be annotated hierarchically using the methods in this thesis through selecting appropriate nodes in activity diagrams and sequence diagrams. The hierarchical method can improve the reusability of models and related verification results. Formal definitions of elements in a UML/MARTE model are proposed. They provide foundation for formal model transformations and analyses.(2) TCPNIA model is proposed. It integrates characteristics of timed Petri nets, colored Petri nets and inhibitor arcs. Energy consuming and data process functions are introduced for each transition in the model. Formal syntax and semantics of the TCPNIA model are defined. It can not only model functional and non-functional propertis of a complex system, but also make full use of existing Petri nets analysis techniques. TCPNIA model provides a foundation for modeling and analyzing real-time embedded systems with Petri nets.(3) An algorithm for transforming a TCPNIA model into a timed automaton is proposed. A conflict mediation mechanism is introduced in the algorithm for maintaining the semantics of timed transitions in the corresponding timed automaton. The method also applies for verifing general timed Petri nets using Uppaal.(4) A task scheduling algorithm with time and resources constraints for TCPNIA is proposed. The algorithm has considered parallel executions for time consuming calculation in a path. In order to improve the reusability of models’ analysis results and computing efficiency, decomposition and composition methods for schedulable paths are analyzed. Depth-first recursive search method is used. State explosion problem can be mitigated for only a part of the state spaces are generated.(5) Model transformation methods from UML/MARTE to TCPNIA are proposed in graphical and formal systax forms respectively. Pointcuts in aspects are determined by the characteristics of a UML model in these methods. Automatic aspect generating algorithms are proposed. Automatic composing algorithms for TCPNIA models are proposed based on aspect-oriented weaving rules. These methods provide theoretical foundation for developing a tool to transform a UML/MARTE model into a TCPNIA model.更多还原