Study of model and verification about hybrid system based on extended timed automata

Computer Engineering and Applications ›› 2012, Vol. 48 ›› Issue (8): 73-75.

• 研发、设计、测试 • Previous Articles Next Articles

Study of model and verification about hybrid system based on extended timed automata

JI Lixia1, MA Jianhong1, ZHOU Qinglei2

1.School of Software Technology, Zhengzhou University, Zhengzhou 450000, China
2.School of Information Engineering, Zhengzhou University, Zhengzhou 450000, China

Received:1900-01-01 Revised:1900-01-01 Online:2012-03-11 Published:2012-03-11

混杂系统的扩展时间自动机模型及验证研究

姬莉霞1，马建红1，周清雷2

1.郑州大学软件技术学院，郑州 450000
2.郑州大学信息工程学院，郑州 450000

Abstract

Abstract: Hybrid system is high complex and involves extensive area, there is no general way to solve it’s problems such as analysis and design. To model and check a class of industrial control hybrid systems, this paper extends the semantics of timed automata. After conversion, it contains a continuous variable and variable constraint. The method uses extended timed automata to model such hybrid systems, uses tool UPPAAL to analysis and simulate, and then uses a simplified version of CTL to verify the requirement specification of systems. The specific case study shows that the method is feasible and effective for a class of hybrid systems analysis and design.

Key words: timed automata, hybrid system, UPPAAL, pumping station, model checking

摘要： 混杂系统复杂度高且涉及领域广，没有通用的方法来解决分析、设计等问题。为解决一类工业控制混杂系统的建模和验证问题，对时间自动机进行了语义扩展，使其含有连续变量以及映射在其上的约束，使用扩展后的时间自动机对此类混杂系统进行建模，采用验证工具UPPAAL进行模型分析模拟，并使用简化的CTL对系统需求规范进行验证。具体实例研究表明，该方法对于分析设计一类混杂系统具有可行性和有效性。

关键词: 时间自动机, 混杂系统, UPPAAL, 泵站, 模型验证

JI Lixia1, MA Jianhong1, ZHOU Qinglei2. Study of model and verification about hybrid system based on extended timed automata[J]. Computer Engineering and Applications, 2012, 48(8): 73-75.

姬莉霞1，马建红1，周清雷2. 混杂系统的扩展时间自动机模型及验证研究[J]. 计算机工程与应用, 2012, 48(8): 73-75.

[1]	LI Qian1, WANG Zheng1, MA Jianfen1, LI Na2. Lightweight mobile payment protocol fairness analysis [J]. Computer Engineering and Applications, 2018, 54(19): 82-87.
[2]	SUN Haoran1，2, SHI Zhiping1，2，3, GUAN Yong1，3, WANG Rui2，3. Analysis and formal modeling of puncturing robot’s sports safety [J]. Computer Engineering and Applications, 2018, 54(18): 263-270.
[3]	WANG Xinyue, GUO Jianquan. Subsidy strategy model of multi-period closed-loop hybrid system under carbon tax [J]. Computer Engineering and Applications, 2018, 54(14): 236-240.
[4]	PEI Changfu1, WANG Bin1, XUE Jie2, LIU Hui1, XIONG Xin1. Spatio-temporal evolution modeling method of brain network based on time automata [J]. Computer Engineering and Applications, 2018, 54(14): 45-51.
[5]	QIN Manman, WANG Zheng, WANG Li. Formal analysis and improvement of remote attestation protocol based on the SPIN [J]. Computer Engineering and Applications, 2017, 53(1): 34-38.
[6]	LV Jianghua1, LIU Zhifeng1, XU Yatao2, ZHOU Conghua1. Verification of correctness of attribute based access control [J]. Computer Engineering and Applications, 2016, 52(18): 98-103.
[7]	XIA Chunrui1, WANG Rui1, LI Xiaojuan1, GUAN Yong1, ZHANG Jie2, WEI Hongxing3. Probabilistic model checking for path planning in dynamic environment [J]. Computer Engineering and Applications, 2016, 52(12): 5-11.
[8]	HUANG Yankai, ZHOU Yu, WEI Ou. Novel approach for attributed graph grammar response specification verification [J]. Computer Engineering and Applications, 2016, 52(12): 15-18.
[9]	WANG Ming1, WANG Rui1, LI Xiaojuan1, GUAN Yong1, ZHANG Jie2, WEI Hongxing3. Verification of mobile robot obstacle avoidance strategies in uncertain environment based on formal modeling and probabilistic analysis [J]. Computer Engineering and Applications, 2016, 52(10): 31-38.
[10]	ZHANG Shuqing, XU Zhongwei, CHEN Zuxi. Research on modeling and verification methods of interlocking system based on term rewriting system [J]. Computer Engineering and Applications, 2014, 50(3): 49-54.
[11]	WANG Changda1，2, DONG Xuegang1, ZHOU Conghua1，2. Security analysis of E-bank online-payment based on UCON [J]. Computer Engineering and Applications, 2014, 50(16): 90-94.
[12]	TONG Chao, WANG Jianxin, QI Jiandong. Approach of constructing defect rule base and detecting source code based on formal specification [J]. Computer Engineering and Applications, 2014, 50(13): 66-72.
[13]	YOU Qifang, YANG Jinji. Model checking of SIP protocol via SPIN [J]. Computer Engineering and Applications, 2014, 50(13): 87-89.
[14]	LV Wei, HUANG Zhiqiu, CHEN Zhe, KAN Shuanglong, WEI Ou. ESpin：SPIN-based Eclipse model checking environment [J]. Computer Engineering and Applications, 2013, 49(7): 45-51.
[15]	GAO Chen, BAI Xue, ZHAO Buhui. Stability analysis of a class of stochastic hybrid systems [J]. Computer Engineering and Applications, 2013, 49(6): 62-64.

Study of model and verification about hybrid system based on extended timed automata

混杂系统的扩展时间自动机模型及验证研究

PDF

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics