鉴于模型在软件系统开发中日趋重要的地位和AADL模型在嵌入式软件建模中的良好应用前景,为了在嵌入式软件系统开发前期保证AADL模型的质量,提出了一种基于模型测试的AADL架构和NuSMV模型的验证方法.文中首先对当前的AADL发展情况作简单介绍,然后对NuSMV验证模型的结构作大致分析,在随后的文章中对NuSMV的验证过程作详细的介绍.与此同时,使用具体的汽车巡航控制系统作为实例进行具体分析.文中通过测试用例执行输出进行验证来判断该方法的正确性.%As models take important part in software development and AADL can describe embedded software effectively, a method for AADL model and NuSMV model testing is put forward to insure the quality of the models in early step of software developing. Proposed a test based on the AADL architecture model and NuSMV model validation methods. The development of the current AADL is introduced briefly, then the structure of the NuSMV model validation is analysed,in the subsequent article in the verification process of the NuSMV is described in detail. At the same time,the use of specific automobile cruise control system as the example is analysed. At last,verify the correctness of the method through an example.
展开▼
