面向验证的SysML模型的形式化转换研究

摘要

随着嵌入式系统中软件的规模和复杂度急剧增大，软件可靠性在嵌入式系统中的重要性逐渐凸显。嵌入式系统更加注重软件和硬件相结合的协同设计，如何创建出有效的模型使得不同技术背景和有不同专长的人能够提高开发效率、协同设计并联合开发出高可靠性的系统成为了一个亟待解决的问题。
　　 基于MDA的软件开发，并对软件模型进行形式化转换与验证可以有效解决这一问题。SysML是UML Profile，采用图形化描述方式建模，大幅度增强了开发者管理复杂系统的能力，在嵌入式系统设计中使用SysML建模可以提高开发效率。但是SysML缺乏精确的语义约束，无法进行形式化验证，难以满足系统的高可靠性的需求，且SysML缺乏时间描述，难以满足嵌入式系统实时性的要求。
　　 本文通过对SysML添加时钟构造型描述时间约束，提出基于MDA的SysML模型的形式化转换方法，并对转换结果进行验证分析，提高软件的可靠性。本文研究工作包括以下三个方面：
　　 1.首先，提出基于MDA的SysML模型的形式化转换方法。该方法将SysML模型到形式化模型--时间自动机模型的转换分为两部分：SysML与时间自动机的同构化、模型转换实现，模型转换实现包括语义映射和语法转换。
　　 2.通过元建模实现SysML和时间自动机的同构化。为SysML添加时钟构造型扩展时间语义，然后根据SysML和时间自动机的语义和语法对两者进行元建模，将两者集成到同一个元元模型体系中，为模型转换实现中的语义映射和语法转换做准备。
　　 3.使用模型转换技术实现SysML模型的形式化转换。在元建模的基础上，使用ATL构造元模型间的语义映射，实现语义层的转换；使用TCS为时间自动机的元模型构造具体语法规约，生成与SysML模型具有相同语义的形式化模型，实现语法层的转换。
　　 最后，本文结合智能会议室光感控制系统，使用SysML对系统建模，通过SysML模型的形式化转换方法实现SysML模型到时间自动机模型的转换，使用工具UPPAAL就系统安全性等属性对模型转换结果进行形式化验证分析，说明了该方法能够提高SysML模型的有效性和正确性，证明了该方法的可行性。