A hierarchical verification procedure of timed Petri-Net model for real-time embedded systems

Hanbo Wang, Xingshe Zhou, Yunwei Dong, Lei Tang

科研成果: 书/报告/会议事项章节会议稿件同行评审

3 引用 (Scopus)

摘要

A novel approach to verify the timed Petri-Net model is proposed in this paper. A non-instantaneous model is abstracted from the timed Petri-Net model in a hierarchical structure. The non-instantaneous model which is verified with a model-checking tool is used to reduce the state space of the timed Petri-Net model for verification with a satisfiability modulo theories solver. The proposed approach is applied in verifying the non-functional properties of real-time embedded systems. The timed Petri-Net is used to model the interacting relations of the software components and the binding relations between software and hardware. A platform-independent model which abstracted from the scheduling model is transformed into the noninstantaneous model. The performance evaluation shows the improvement on the running time for verification with the proposed approach.

源语言英语
主期刊名2nd International Conference on Information Engineering and Computer Science - Proceedings, ICIECS 2010
DOI
出版状态已出版 - 2010
活动2nd International Conference on Information Engineering and Computer Science, ICIECS 2010 - Wuhan, 中国
期限: 25 12月 201026 12月 2010

出版系列

姓名2nd International Conference on Information Engineering and Computer Science - Proceedings, ICIECS 2010

会议

会议2nd International Conference on Information Engineering and Computer Science, ICIECS 2010
国家/地区中国
Wuhan
时期25/12/1026/12/10

指纹

探究 'A hierarchical verification procedure of timed Petri-Net model for real-time embedded systems' 的科研主题。它们共同构成独一无二的指纹。

引用此