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

Hanbo Wang, Xingshe Zhou, Yunwei Dong, Lei Tang

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

3 Scopus citations

Abstract

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.

Original languageEnglish
Title of host publication2nd International Conference on Information Engineering and Computer Science - Proceedings, ICIECS 2010
DOIs
StatePublished - 2010
Event2nd International Conference on Information Engineering and Computer Science, ICIECS 2010 - Wuhan, China
Duration: 25 Dec 201026 Dec 2010

Publication series

Name2nd International Conference on Information Engineering and Computer Science - Proceedings, ICIECS 2010

Conference

Conference2nd International Conference on Information Engineering and Computer Science, ICIECS 2010
Country/TerritoryChina
CityWuhan
Period25/12/1026/12/10

Keywords

  • Hierarchical
  • Real-time embedded systems
  • Timed Petri-Net
  • Verification

Fingerprint

Dive into the research topics of 'A hierarchical verification procedure of timed Petri-Net model for real-time embedded systems'. Together they form a unique fingerprint.

Cite this