BAS：可信模型驱动开发中的建模和验证案例研究

【文件属性】：
文件名称：BAS：可信模型驱动开发中的建模和验证案例研究
文件大小：2.02MB
文件格式：PDF
更新时间：2021-02-23 22:21:08
MDA, Verification, Contract, UTP, LTL 多视图建模和关注点分离被广泛用于降低设计的复杂度。 大型软件系统。 为了确保多视图需求模型的正确性和一致性， 正式的验证技术应应用于模型驱动的开发过程。 然而， 对于严格的建模方法仍然缺乏统一的理论基础和工具支持。 解决这些问题，我们实施了一个集成的建模和验证环境tMDA（可信任MDA）。 在tMDA中，开发人员使用UML静态模型对系统需求进行建模动态模型，并验证不同模型的正确性和一致性。 多维提出了模型，该模型支持一致性验证，活动性和安全性验证， OCL约束和LTL公式验证。 引入银行ATM系统（BAS）进行演示如何利用tMDA进行设计和验证。