构件式系统的建模与验证

计算机科学与探索 ›› 2008, Vol. 2 ›› Issue (2): 198-205.

构件式系统的建模与验证

曾红卫+,缪淮扣

上海大学计算机工程与科学学院，上海 200072

收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2008-04-20 发布日期:2008-04-20
通讯作者: 曾红卫

Modeling and verification of component-based system

ZENG Hongwei+, MIAO Huaikou

College of Computer Engineering and Science， Shanghai University， Shanghai 200072， China

Received:1900-01-01 Revised:1900-01-01 Online:2008-04-20 Published:2008-04-20
Contact: ZENG Hongwei

摘要/Abstract

摘要： 构件的组合与安全性是构件式系统开发的一个挑战性问题。提出了一种新的描述构件交互行为的模型－构件消息自动机，其特点是保留了构件的所有交互特性以便进一步进行构件的验证。给出了使用同步积操作将多个构件组合成单个复杂的组合构件的方法。基于监控理论的可控性概念，设计了一个验证构件系统安全性质的算法。为了说明论文建议的方法，详细讨论了一个简单的、贯穿整个论文的示例系统。

关键词: 构件消息自动机, 可控性, 验证, 构件组合

Abstract: Composition and safety checking of components give rise to the challenges in component-based system development process. A new model， component message automaton， is proposed to model interaction behavior of components. The model is an extended automaton that is designed to preserve all the interaction properties of components to provide a rich base for further verification. Then synchronous product operation is employed to combine multiple components into a single complex component. Based on controllability from supervisory control theory， the algorithm verifying safety properties of component-based system is developed. A simple example through this paper is studied in detail to illustrate how to apply the proposed approach.

Key words: component message automaton, controllability, verification, component composition

曾红卫+,缪淮扣. 构件式系统的建模与验证[J]. 计算机科学与探索, 2008, 2(2): 198-205.

ZENG Hongwei+, MIAO Huaikou. Modeling and verification of component-based system[J]. Journal of Frontiers of Computer Science and Technology, 2008, 2(2): 198-205.

[1]	张俊. SCVerify：抗功耗侧信道攻击软件实现的验证[J]. 计算机科学与探索, 2021, 15(6): 1074-1083.
[2]	郭帆, 范威威. 面向Java EE程序的SQLIA漏洞分析和验证方法[J]. 计算机科学与探索, 2021, 15(2): 270-283.
[3]	陈钦况，陈珂，伍赛，寿黎但，陈刚. 关于主动学习下的知识图谱补全研究[J]. 计算机科学与探索, 2020, 14(5): 769-782.
[4]	房立超，王钰，杨杏丽，李济洪. 方差正则化的分类模型选择准则[J]. 计算机科学与探索, 2019, 13(3): 457-467.
[5]	贾大宇，信俊昌，王之琼，郭薇，王国仁. 区块链的存储容量可扩展模型[J]. 计算机科学与探索, 2018, 12(4): 525-535.
[6]	祝义，黄志球，周航. 采用函数式语言的BPEL模型形式化验证方法[J]. 计算机科学与探索, 2018, 12(2): 185-196.
[7]	戴华，王敏，易训，杨庚，叶庆群. 无线传感器网络安全MAX/MIN查询技术综述[J]. 计算机科学与探索, 2017, 11(8): 1191-1203.
[8]	仵志鹏，胡军，陈松，石娇洁. 面向AltaRica模型的嵌入式系统安全性验证方法[J]. 计算机科学与探索, 2017, 11(1): 24-36.
[9]	杨柳，王钰. 组块3×2交叉验证的F1度量的方差分析[J]. 计算机科学与探索, 2016, 10(8): 1176-1183.
[10]	秦晓倩，谭晓阳，陈松灿. 基于大间隔双线性分类器进行亲子关系验证[J]. 计算机科学与探索, 2016, 10(4): 524-532.
[11]	胡军，马金晶，刘雪，程桢，石娇洁，黄志球. 模型驱动的安全关键系统重配置信息验证方法[J]. 计算机科学与探索, 2015, 9(4): 385-402.
[12]	谢晴晴，王良民. 基于PMD的外包数据流范围查询验证方案[J]. 计算机科学与探索, 2015, 9(10): 1209-1218.
[13]	胡良文，马金晶，孙博. 基于Spin的SysML活动图验证框架[J]. 计算机科学与探索, 2014, 8(7): 836-847.
[14]	王丹，常建生，赵文兵. 使用Pi演算的构件交互可信性验证模型[J]. 计算机科学与探索, 2012, 6(5): 419-429.
[15]	蒋曹清, 应时, 文静, 贾向阳, 管华 . 面向服务软件异常处理过程的可终止性验证[J]. 计算机科学与探索, 2012, 6(3): 208-220.