俞晓锋，王立松

(南京航空航天大学 计算机科学与技术学院，江苏 南京 210016)

SysML(Systems Modeling Language)［1］是UML 在系统工程应用领域的延续和拓展。与其他建模语言一样，SysML 是一种通用标准建模语言。

随着应用系统越发复杂，系统的任意环节均可能会影响到系统的整体运行。例如民航业务系统，作为一个巨大的系统，不能保证其对象在整个生命期内均能安全稳健运行，而一旦出现异常状况会造成巨大的经济损失。用SysML 建模可抽象表示应用系统的对象，本文研究的对象是类模型中某个主动类的实例，通过验证行为模型来模拟出对象在生命期内的运行过程，用这种方式来演练其实现的每一个用例场景。SysML 状态图用于建立类对象在其生命期内的行为模型，尤其是当对象具有依赖于状态的行为。

SysML 和UML 一样，为保持描述的清晰易懂，在给出自身语义说明的同时，采用半形式化的描述方法，使用自然语言表示约束和语义，力求实现形式化与易于理解之间的平衡。因此，SysML 本身缺乏分析和验证的手段，针对这一问题，本文对SysML 状态图进行拓展，使用SCXML(State Chart XML)［2］作为SysML 状态图的形式化描述语言并引用动作规约语言［3］(Action Specification Language，ASL)描述状态图对象的行为动作。其中ASL 是WilKie 等人在2002 年提出的平台无关动作描述语言，其提供了操作平台无关模型元素的方法。通过使用SCXML 和ASL 可建立精确无歧义的行为模型，并在此基础上进行分析验证。

SysML 状态图的体系结构验证无需考虑业务需求的偏好，使用Kripke 结构可表示对象的状态空间。……