基于UML的嵌入式系统模型验证机制的研究

随着嵌入式系统在各个领域的广泛应用,嵌入式系统变得越来越复杂,研究一种支持嵌入式系统从分析、设计、验证到编码这一整个开发过程的模型系统及建模方法变得越来越重要。UML(UnifiedModelingLanguage,统一建模语言)作为面向对象的分析与设计技术的代表,已经获得了广泛的承认,并在多个领域中有成功的应用。然而,UML是一种符号化语言系统,其语义采用自然语言描述,没有完全形式化,无法精确和严格地描述模型的行为从而实现模型的验证。为了解决这个问题,文章提出了一种用于嵌入式系统UML模型验证的方法,其核心是可执行(Executable)UML,它是UML的增强性子集,采用与UML相同的符号表示法,并集成了状态图(StateChart)所用的形式化语义定义。嵌入式系统的UML模型经过语义分析能够很方便地生成可执行UML模型,并实现系统模型的验证。

Research on Verification for UML-Based Model of Embedded System

Embedded system becomes more and more complicated with its widespread use in a variety of domains.Methods for analyzing,developing,modeling and verifying embedded system are increasingly important.A number of object-oriented techniques and notations have been introduced,but recently Unified Modeling Language(UML)could be a notation broad enough in scope to represent a variety of domains and gains acknowledgements widely.Currently,however,UML is only a notation,with no formal semantics attached to its individual diagrams.Behavior definition and expression are not precise and detailed enough to execute model verification.In order to address the problem,a new method based on Executable UML is proposed in this paper.Executable UML,which adopts the same notations as UML and integrates with formal semantics as State Chart,could be viewed as an enhanced subset of UML.Executable UML-based model can be derived from UML-based model through semantics analysis conveniently and provides precise and detailed behavior information enough to perform model verification.