TCBESD一个构件化嵌入式软件设计模型验证工具

小型微型计算机系统

Ｊｏｕｒｎａｌｏｆ

２０１０年１１月第１１期

ＶｏＬ３１

Ｎｏ．１１

２０１０

ＣｈｉｎｅｓｅＣｏｍｐｕｔｅｒＳｙｓｔｅｍｓ

Ｔ—ＣＢＥＳＤ：一个构件化嵌入式软件设计模型验证工具

徐丙凤１，胡

军ｋ３，曹

东２，黄志球１，郭丽娟１，张

剑１

１（南京航空航天大学信息科学与技术学院，江苏南京２１００１６）

２（南京航空航天大学自动化学院，江苏南京２１００１６）

３（计算机软件新技术国家重点实验室（南京大学），江苏南京２１００９３）

Ｅ—ｍａｉｌ：ｘｂｆｎｕａａ＠ｙａｈｏｏ．ｃｎ

摘要：现代复杂嵌入式软件系统的高可靠性需要有效的基于模型的设计与分析技术．传统的嵌入式软件可靠性保障技术主

要关注于系统开发后期．本文在Ｅｃｌｉｐｓｅ平台上设计并实现了一个基于接口自动机模型的构件化嵌入式软件设计的形式化验证原型工具Ｔ—ＣＢＥＳＤ（ＴｏｏｌｆｏｒＣｏｍｐｏｎｅｎｔ—ＢａｓｅｄＥｍｂｅｄｄｅｄＳｏｆｔｗａｒｅＤｅｓｉｇｎｓ）．工具直接使用ＵＭＬ顺序图模型作为系统规约。可以检验系统设计模型与场景式规约之问多种行为一致性问题；并使用消息事件的时间约束不等式，检验实时接口自动机网络与带时间约束的顺序图模型之间的实时行为一致性问题．工具设计与实现内容包括：输入输出接口、顺序图模型的预处理转换、状态空间数据结构设计、抽象验证算法的实现ｖＸ％ｔ．通信构件组合系统的实例应用分析．关键词：嵌入式软件设计；构件化设计；软件验证；接口自动机；模型检验工具中图分类号：ＴＰ３１ｌ

文献标识码：Ａ

文章编号：１０００ １２２０【２０１０）１１－２１２９－０９

Ｔ－ＣＢＥＳＤ：ａＦｏｒｍａｌＶｅｒｉｆｉｃａｔｉｏｎＴｏｏｌｆｏｒＣｏｍｐｏｎｅｎｔ－ｂａｓｅｄＥｍｂｅｄｄｅｄＳｏｆｔｗａｒｅＤｅｓｉｇｎｓ

ＸＵ

Ｂｉｎｇ．ｆｅｎ９１－ＨＵＪｕｎｌ”。ＣＡＯＤｏｎ９２。ＨＵＡＮＧＺｈｉ．ｑｉｕｌ，ＧＵＯＬｉ－ｊｕａｎｌ。ＺＨＡＮＧＪｉａｎｌ

ａｎｄ

１（ＣｏｌｌｅｇｅｏｆＩｎｆｏｒｍａｔｉｏｎＳｃｉｅｎｃｅ

Ｔｅｃｈｎｏｌｏｇｙ。ＮａｎｆｉｎｇＵｎｉｖｅｒｓｉｔｙｏｆＡｅｒｏｎａｕｔｉｃｓａｎｄＡｓｔｒｏｎａｕｔｉｃｓ。Ｎａｎｊｉｎｇ２１００１６．Ｃｈｉｎａ）

２（ＣｏｌｌｅｇｅｏｆＡｕｔｏｍａｔｉｏｎＥｎｇｉｎｅｅｒｉｎｇ。ＮａｎｆｉｎｇＵｎｉｖｅｒｓｉｔｙｏｆＡｅｒｏｎａｕｔｉｃｓａｎｄＡｓｔｒｏｎａｕｔｉｃｓ．Ｎａｎｊｉｎｇ２１００１６．Ｃｈｉｎａ）３（Ｓｔａｔｅ

Ｋｅｙ

ＬａｂｏｒａｔｏｒｙｆｏｒＮｏｖｅｌＳｏｆｔｗａｒｅ

Ｔｅｃｈｎｏｌｏｇｙ

ＮａｎｊｉｎｇＵｎｉｖｅｒｓｉｔｙ．Ｎａｎｊｉｎｇ２１００９３。Ｃｈ／ｎａ）

Ａｂｓｔｒａｃｔ：Ｈｉｇｈｒｅｌｉａｂｉｌｉｔｙｒｅｑｕｉｒｅｍｅｎｔｓｏｆａｎｄａｎａｌｙｓｉｓ．Ｔｒａｄｉｔｉｏｎａｌｐｅｒ。ａ

ｍｏｄｅｍｅｍｂｅｄｄｅｄｓｏｆｔｗａｒｅｓｙｓｔｅｍｎｅｅｄｅｆｆｅｃｔｉｖｅｍｏｄｅｌ－ｂａｓｅｄｔｅｃｈｎｉｑｕｅｓｆｏｒｓｙｓｔｅｍｄｅｓｉｇｎｓ

ｍｅｔｈｏｄｓｉｎｅｍｂｅｄｄｅｄｃｏｍｐｕｔｉｎｇｄｏｍａｉｎｍｏｓｔｌｙｃｏｎｃｅｍｅｄｔｈｅｉｍｐｌｅｍｅｎｔａｔｉｏｎａｎｄｔｅｓｔｉｎｇｐｈｒａｓｅ．Ｉｎｔｈｉｓｐａ－

ｆｏｒＣｏｍｐｏｎｅｎｔ—Ｂａｓｅｄ

ａＳ

ｐｒｏｔｏｔｙｐｅＴ－ＣＢＥＳＤ（Ｔｏｏｌ

ＥｍｂｅｄｄｅｄＳｏｆｔｗａｒｅＤｅｓｉｇｎｓ）ｈａｓｂｅｅｎ

ｏｎ

ｄｅｓｉｇｎｅｄ，ｗｈｉｃｈｉｓ

ｂａｓｅｄ

０１１

ｔｈｅｔｈｅｏｒｙ

ｏｆｉｎｔｅｒｆａｃｅ

ａｕｔｏｍａｔａａｎｄｉｓｉｍｐｌｅｍｅｎｔｅｄ

ａ

ｐｌｕｇ－ｉｎ

ｍｏｄｕｌｅｔｈｅｏｐｅｎ－ＳＯＬｌｌ＇Ｃｅ

ｐｌａｔｆｏｒｍＥｃｌｉｐｓｅ．ＴｈｅｔｏｏｌａｃｃｅｐｔｓＵＭＬｓｅｑｕｅｎｃｅｄｉ—

ａｇｒａｍｓａｓｔｈｅｉｎｐｕｔｓｙｓｔｅｍｓｐｅｃｉｆｉｃａｔｉｏｎｄｉｒｅｃｔｌｙ。ｃｈｅｃｋｉｎｇｓｅｖｅｒａｌｄｉｆｆｅｒｅｎｔｋｉｎｄｓｏｆｂｅｈａｖｉｏｒａｌｃｏｎｓｉｓｔｅｎｃｙｐｒｏｂｌｅｍｓｂｅｔｗｅｅｎｔｈｅｓｙｓ—ｔｅｍｄｅｓｉｇｎｍｏｄｅｌｓａｎｄｓｃｅｎａｒｉｏ—ｂａｓｅｄｓｐｅｃｉｆｉｃａｔｉｏｎｓ．Ｂｙｕｓｉｎｇｔｉｍｉｎｇｃｏｎｓｔｒａｉｎｔｉｎｅｑｕａｌｉｔｙｏｆｍｅｓｓａｇｅｅｖｅｎｔｓ－ｔｈｅｔｏｏｌ

ｗｈｅｔｈｅｒｔｈｅｂｅｈａｖｉｏｒｓｉｎ

ｃａｎ

ｖｅｒｉｆｙ

ｒｅａｌ－ｔｉｍｅｉｎｔｅｒｆａｃｅｎｅｔｗｏｒｋｓｓａｔｉｓｆｙｔｈｅｓｅｑｕｅｎｃｅｄｉａｇｒａｍｓｗｉｔｈｒｅａｌ－ｔｉｍｅｌｉｍｉｔａｔｉｏｎｓ．Ｔｈｅｄｅｓｉｇｎｓａｎｄ

ｔｏａｓｅｔ

ｉｍｐｌｅ—

Ｓｅ－

ｍｅｎｔａｔｉｏｎｓｏｆｔｈｉｓｗｏｒｋｉｎｃｌｕｄｅｔｈｅｉｎｐｕｔ／ｏｕｔｐｕｔｍｅｃｈａｎｉｓｍｓ。ｔｈｅｐｒｅ－ｔｒａｎｓｌａｔｉｏｎｆｒｏｍｓｅｑｕｅｎｃｅｄｉａｇｒａｍｓ

ｑｕｅｎｃｅｓ，ｔｈｅｓｔａｔｅｓｐａｃｅｄａｔａｓｙｓｔｅｍｖｅｒｉｆｉｃａｔｉｏｎ

ｓｔｒｕｃｔｕｒｅ

ｏｆ

ａ

ｍｅｓｓａｇｅｅｖｅｎｔ

ｄｅｓｉｇｎｓ．ｄｅｔａｉｌ

ｉｍｐｌｅｍｅｎｔａｔｉｏｎｉｓｓｕｅｓｏｆｓｅｖｅｒａｌｖｅｒｉｆｉｃａｔｉｏｎｆｌｇｏｆｉｔｈｒａｓａｎｄ

ｃｏｍｐｏｎｅｎｔ－ｂａｓｅｄ

ｅｘａｍｐｌｅ．

Ｋｅｙｗｏｒｄｓ：ｅｍｂｅｄｄｅｄｓｏｆｔｗａｒｅｄｅｓｉｇｎ；ｃｏｍｐｏｎｅｎｔ－ｂａｓｅｄｄｅｓｉｇｎ；ｓｏｆｔｗａｒｅｖｅｒｉｆｉｃａｔｉｏｎ；ｉｎｔｅｒｆａｃｅａｕｔｏｍａｔａ；ｍｏｄｅｌｃｈｅｃｋｉｎｇｔｏｏｌ

１引’言

嵌入式计算系统已经广泛的应用于生活中的各个领域，如：交通、能源、医疗、控制、通信、军事等．近年来随着计算机硬件性能的不断提高，嵌入式系统中软件的规模和复杂性不断增加，使软件对整个系统的影响逐渐占据了统治地位．关键系统中的嵌入式软件失效将会导致生命与财产的重大损失．因此，嵌入式软件通常具有极高的功能可靠性、严格的实时性等要求，如何保证系统同时满足给定的功能和非功能需求已

成为当前高可信嵌入式计算领域中的研究热点¨。３’．目前，工业界已有一些比较有效的嵌入式软件测试和调试方法（如：在处理器中嵌入ＩＣＥ功能，调试代理软件，ＪＴＡＧ模拟等）．但从软件工程的角度来看，这些方法都是在系统的开发中后期阶段所使用，而在嵌入式软件设计与分析的前期阶段还缺乏有效的方法和工具对系统设计进行分析与验证．

本文基于接口自动机模型对构件化嵌入式软件设计（ＣＢＥＳＤ：Ｃｏｍｐｏｎｅｎｔ．ＢａｓｅｄＥｍｂｅｄｄｅｄＳｏｆｔｗａｒｅＤｅｓｉｇｎｓ）的分析与验证方法展开进一步研究，在Ｅｃｌｉｐｓｅ开放平台上实现了

收稿日期：２００９－０８－２０收修改稿日期：２００９－１０－２９基金项目：航空基金项目（２００７ＺＤ５２０４３）资助；教育士点基金项目（２００７０２８７０５２）资助．

作者简介：徐丙凤，女，１９８６年生，硕士研究生，ＣＣＦ学生会员，研究方向为软件工程、嵌入式软件建模与分析；胡军，男，１９７３年生，副教授．

ＣＣＦ会员，研究方向为软件分析与验证、嵌入式系统、形式化方法；曹东，男，１９７２年生，副研究员，研究方向为复杂嵌入式系统、航空控制工程、软件工程；黄志球。男，１９６５年生，教授．博士生导师。ＣＣＦ高级会员，研究方向为软件工程；郭丽娟，女，１９８６年生，硕士研究生．ＣＣＦ学生会

员，研究方向为软件工程、ＵＭＬ建模与分析；张剑，男，１９８５年生，硕士研究生，ＣＣＦ学生会员，研究方向为嵌入式系统、多核计算．

万方数据