期刊文献+
共找到5篇文章
< 1 >
每页显示 20 50 100
软件体系结构环境中的行为规范说明与验证
1
作者 支小莉 陆鑫达 《计算机工程》 CAS CSCD 北大核心 2003年第11期8-10,共3页
以实时线性时态逻辑作为逻辑框架,以时控自动机作为计算模型,扩展了软件体 系结构环境Armani的行为规范说明与验证的能力。从而可以在体系结构描述的基础上从结构 和行为两方面分析验证系统在体系结构层次上的重要性质,减少软件开发... 以实时线性时态逻辑作为逻辑框架,以时控自动机作为计算模型,扩展了软件体 系结构环境Armani的行为规范说明与验证的能力。从而可以在体系结构描述的基础上从结构 和行为两方面分析验证系统在体系结构层次上的重要性质,减少软件开发的风险;并且支持 非完全规范说明,具有半形式化验证与组合验证的灵活性。 展开更多
关键词 软件体系结构 行为规范 时控自动机
下载PDF
Modeling research of train tracing based on UML sequence diagram and UPPAAL 被引量:5
2
作者 CHEN Yong-gang YANG Lu WANG Dong 《Journal of Measurement Science and Instrumentation》 CAS CSCD 2019年第2期157-167,共11页
The zone control subsystem is a real-time control system,which requests the correctness of the control process.Train tracing scene is an important function of the zone controller(ZC)in the communication based train co... The zone control subsystem is a real-time control system,which requests the correctness of the control process.Train tracing scene is an important function of the zone controller(ZC)in the communication based train control(CBTC)system.In the process of deep development and design,to ensure the safety of the system,the system needs to be modeled,simulated and verified to discover the system design flaws.Unified modeling language(UML)is combined with timed automata,and timed automata network models of train-filter and train tracing demarcation-point are established.At the same time,the verification tool of UPPAAL is applied to simulate the system,and verify the requirements of performance and function of system.The results show that the function of train tracing demaraction-point meets the requirements of system safety and limited activity.Therefore,the method is feasible and can be applied to the modeling and verification of other scenes of train control system. 展开更多
关键词 train tracing communication based train control(CBTC)system zone controller(ZC) timed automata UPPAAL
下载PDF
A test sequence generation method of zone controller based on timed automata 被引量:4
3
作者 SONG Shuang CHEN Yue-dong 《Journal of Measurement Science and Instrumentation》 CAS CSCD 2019年第3期266-276,共11页
In order to solve the problem of artificial generation and low efficiency of test sequences for zone controller (ZC), a model-based automatic generation method of test sequence is proposed. Firstly, the timed automata... In order to solve the problem of artificial generation and low efficiency of test sequences for zone controller (ZC), a model-based automatic generation method of test sequence is proposed. Firstly, the timed automata model is established based on function analysis of the zone controller, and the correctness of the model is verified by UPPAAL. Then by parsing the timed automata model files, state information and transition conditions can be extracted to generate test case sets. Finally, according to the serialization conditions of test cases, the test cases are serialized into test sequences by using the improved depth first search algorithm. A case, the ZC controls the train running within its jurisdiction, shows that the method is correct and can effectively improve the efficiency of test sequence generation. 展开更多
关键词 test sequence zone controller (ZC) timed automata model file parsing case serialization
下载PDF
A novel control framework for internet based tele-robotics
4
作者 王永明 肖南峰 +2 位作者 尹红丽 蒋艳荣 段鹏 《Journal of Harbin Institute of Technology(New Series)》 EI CAS 2008年第5期602-607,共6页
Aiming at the tele-operation instability caused by time delay of interuet information transfer for internet based tele-robotics, this paper proposes a novel control framework for internet based tele-roboties, which ca... Aiming at the tele-operation instability caused by time delay of interuet information transfer for internet based tele-robotics, this paper proposes a novel control framework for internet based tele-roboties, which can guarantee the non-distortion-transfer of control information and reduce the difference of action time between the local simulated virtual robot and the remote real robot. This framework is insensitive to the inherent interact time delay, and differs from other tele-robotics systems that try to use some mathematic models to describe the internet delay or take some assumptions. In order to verify the framework, a 4-DOF fischertechnik industry robot tele-operation system has been developed using the new proposed framework. Experimental results demonstrate the applicable performance of the new framework. The framework is open structured and can be applied to other general purposed tele-operation systems. 展开更多
关键词 control framework internet based tele-robotics time delay
下载PDF
一种用于无线系统的自适应QoS结构
5
作者 沈芙辉 周娅 《网络安全技术与应用》 2006年第8期92-94,共3页
本文介绍了一种通过确认的支持自动化QoS决策的体系结构。该体系结构的模型以及QoS决策功能由辅助组件完成,该辅助组件是由知识库和决策机构联合而成。这种管理体系在适应新形式的QoS请求和降低人为操作上有优势。
关键词 无线系统 QOS 时控自动机
原文传递
上一页 1 下一页 到第
使用帮助 返回顶部