摘要
UML统一建模语言已成为当今软件设计中的标准方法。而由于其缺乏严密的逻辑性,使得模型中存在的潜在缺陷无法在早期被发现。本文提出一种将UML时序图转换为Promela语言描述的方法,并利用SPIN自动化验证工具检验模型的正确性。从而使开发人员在软件设计阶段就能快速检测出模型中存在的缺陷,并避免错误的设计进入开发阶段。经过试验,证明了此方法的可行性和有效性。
The UML has become a standard method in software design. While it is difficult to uncover the potential flaws within the models in early stage due to lacking logicality. This paper proposed a method which translates the UML sequence chart to the Promela language description, and then checks the correctness of the model by SPIN. As a result, developers can discover the faults in models, and avoid making mistakes in developing stage. Its availability is proven through an experiment.
出处
《价值工程》
2013年第13期193-195,共3页
Value Engineering
