包含协议和语义的构件一致性验证方法
|
摘要
在基于构件的系统设计中,需要对构件的一致性进行验证。构件的一致性包括语义一致性和协议一致性,已有的一致性验证方法仅支持构件的协议一致性验证。而在实际应用中除了要进行构件的协议一致性验证外,还需要进行其语义一致性验证。为此提出了一种包含协议和语义的构件一致性验证方法。将方法语义与基于场景的需求规约相结合,使用语义扩展接口自动机模型(SIA)来建模构件的语义和协议信息,使用带有语义约束的UML交互概观图来表示基于场景的需求规约。通过对SIA和带语义约束的UML交互概观图的行为的理论分析,进一步形成了一种一致性验证算法,并用实例来说明其过程。算法不仅能够检验系统中构件的协议一致性,而且能够检验其语义一致性。该算法中的方法语义包括了该方法参数的类型和详细语义信息,更符合实际应用情形。
In the design of component-based system,it was required to verify the component consistency which included semantics consistency and protocol consistency. The existing consistency verification methods were able to verify only the protocol consistency. In practical application,it was required to verify the semantics consistency besides the protocol consistency. In order to make the consistency verification method able to verify both semantics consistency and protocol consistency,this paper proposed a component consistency verification method with both protocol and semantics by introducing the idea of method semantics into scenario-based specifications. It utilized the semantic extended interface automata( SIA) model to describe the semantics and protocols information of components. And specified the scenario-based specifications by UML interaction overview diagrams with semantic constrains. Then according to the analysis of the behavior of SIA model and UML interaction overview diagrams with semantic constrains,this paper develops an algorithm to verify the consistency between component-based designs and the scenario-based semantic specifications,and illustrates it by a real example. This algorithm not only can verify the protocol consistency but also can verify the semantic consistency which includes the type and semantic of methods and is more suitable to the cases of practical application.
In the design of component-based system,it was required to verify the component consistency which included semantics consistency and protocol consistency. The existing consistency verification methods were able to verify only the protocol consistency. In practical application,it was required to verify the semantics consistency besides the protocol consistency. In order to make the consistency verification method able to verify both semantics consistency and protocol consistency,this paper proposed a component consistency verification method with both protocol and semantics by introducing the idea of method semantics into scenario-based specifications. It utilized the semantic extended interface automata( SIA) model to describe the semantics and protocols information of components. And specified the scenario-based specifications by UML interaction overview diagrams with semantic constrains. Then according to the analysis of the behavior of SIA model and UML interaction overview diagrams with semantic constrains,this paper develops an algorithm to verify the consistency between component-based designs and the scenario-based semantic specifications,and illustrates it by a real example. This algorithm not only can verify the protocol consistency but also can verify the semantic consistency which includes the type and semantic of methods and is more suitable to the cases of practical application.
引文
[1]张岩,胡军,于笑丰,等.场景驱动的构件行为抽取[J].软件学报,2007,18(1):50-61.
[2]梅佳,缪淮扣,高洪皓.构件式实时系统建模与验证研究[J].小型微型计算机系统,2012,33(2):219-224.
[3]黄龙,缪淮扣,王皙,等.基于场景的形式化测试模型生成方法[J].上海大学学报:自然科学版,2011,17(5):595-599.
[4]胡军,于笑丰,张岩,等.基于场景构件式实时软件设计的一致性检验[J].软件学报,2006,17(1):48-58.
[5]Alfaro L D,Henzinger T A,Stoelinga M.Timed interfaces[C]//Proc of the 2nd International Conference on Embedded Software.Berlin:Springer-Verlag,2002:108-122.
[6]Alfaro L D,Henzinger T A.Interface automata[C]//Proc of the 8th Joint European Software Engineering Conference and 9th ACM SIGSOFT International Symposium on the Foundations of Software Engineering.New York:ACM Press,2001:109-120.
[7]胡军.构件化嵌入式软件设计的分析与验证[D].南京:南京大学,2005.
[8]Mouelhi S,Agrou K,Chouali S,et al.Object-oriented componentbased design using behavioral contracts:application to railway systems[C]//Proc of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering.New York:ACM Press,2015:49-58.
[9]Hu Jun,Yu Xiaofeng,Zhang Yan,et al.Scenario-based verification for component-based embedded software designs[C]//Proc of the34th International Conference on Parallel Processing Workshops.Norway:IEEE Computer Society Press,2005:240-247.
[10]郭丽娟.基于即时验证的嵌入式软件验证技术研究[D].南京:南京航空航天大学,2010.
[11]杨春霞,王映辉,王宏涛.构件组合的一致性验证和冗余行为去除[J].计算机工程,2010,36(24):54-56.
[12]张振领,贾仰理,谢圣献,等.基于协议的实时构件行为一致性验证[J].计算机科学,2012,39(6):125-128,142.
[13]赵硕,陈中育,肖春水.基于范畴论的构件行为组合研究[J].计算机工程,2012,38(15):53-55,58.
[14]张雷,陈立潮,潘理虎,等.构件标识潜在语义分析与模糊聚类方法研究[J].计算机工程与设计,2012,33(12):4557-4560,4588.
[15]岳洋,曾广平.一种面向构件的行为语义模型及其应用研究[J].计算机应用研究,2012,29(5):1751-1755..
[16]侯金奎,王成端.支持模型驱动开发的软构件形式化描述方法[J].计算机应用,2015,35(9):2692-2700.
[17]孙福振.基于模型检查的嵌入式软件构件化分析与验证[D].北京:北京理工大学,2015.
[18]王博,白晓颖,贺飞,等.可组合嵌入式软件建模与验证技术研究综述[J].软件学报,2014,25(2):234-253.
[19]张连怡.构件系统模型检测方法研究[D].北京:清华大学,2015.
[2]梅佳,缪淮扣,高洪皓.构件式实时系统建模与验证研究[J].小型微型计算机系统,2012,33(2):219-224.
[3]黄龙,缪淮扣,王皙,等.基于场景的形式化测试模型生成方法[J].上海大学学报:自然科学版,2011,17(5):595-599.
[4]胡军,于笑丰,张岩,等.基于场景构件式实时软件设计的一致性检验[J].软件学报,2006,17(1):48-58.
[5]Alfaro L D,Henzinger T A,Stoelinga M.Timed interfaces[C]//Proc of the 2nd International Conference on Embedded Software.Berlin:Springer-Verlag,2002:108-122.
[6]Alfaro L D,Henzinger T A.Interface automata[C]//Proc of the 8th Joint European Software Engineering Conference and 9th ACM SIGSOFT International Symposium on the Foundations of Software Engineering.New York:ACM Press,2001:109-120.
[7]胡军.构件化嵌入式软件设计的分析与验证[D].南京:南京大学,2005.
[8]Mouelhi S,Agrou K,Chouali S,et al.Object-oriented componentbased design using behavioral contracts:application to railway systems[C]//Proc of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering.New York:ACM Press,2015:49-58.
[9]Hu Jun,Yu Xiaofeng,Zhang Yan,et al.Scenario-based verification for component-based embedded software designs[C]//Proc of the34th International Conference on Parallel Processing Workshops.Norway:IEEE Computer Society Press,2005:240-247.
[10]郭丽娟.基于即时验证的嵌入式软件验证技术研究[D].南京:南京航空航天大学,2010.
[11]杨春霞,王映辉,王宏涛.构件组合的一致性验证和冗余行为去除[J].计算机工程,2010,36(24):54-56.
[12]张振领,贾仰理,谢圣献,等.基于协议的实时构件行为一致性验证[J].计算机科学,2012,39(6):125-128,142.
[13]赵硕,陈中育,肖春水.基于范畴论的构件行为组合研究[J].计算机工程,2012,38(15):53-55,58.
[14]张雷,陈立潮,潘理虎,等.构件标识潜在语义分析与模糊聚类方法研究[J].计算机工程与设计,2012,33(12):4557-4560,4588.
[15]岳洋,曾广平.一种面向构件的行为语义模型及其应用研究[J].计算机应用研究,2012,29(5):1751-1755..
[16]侯金奎,王成端.支持模型驱动开发的软构件形式化描述方法[J].计算机应用,2015,35(9):2692-2700.
[17]孙福振.基于模型检查的嵌入式软件构件化分析与验证[D].北京:北京理工大学,2015.
[18]王博,白晓颖,贺飞,等.可组合嵌入式软件建模与验证技术研究综述[J].软件学报,2014,25(2):234-253.
[19]张连怡.构件系统模型检测方法研究[D].北京:清华大学,2015.