Design, analysis and verification of real-time systems based on time petri net refinement

Zhijun Ding, Changjun Jiang, Mengchu Zhou

Research output: Contribution to journalArticlepeer-review

25 Scopus citations


A type of refinement operations of time Petri nets is presented for design, analysis and verification of complex real-time systems. First, the behavior preservation is studied under time constraints in a refinement operation, and a sufficient condition for behavior preservation is obtained. Then, the property preservation is considered, and the results indicate that if the refinement operation of time Petri nets satisfies behavior preservation, it can also preserve properties such as boundedness and liveness. Finally, based on the behavior preservation, a reachability decidability algorithm of a refined time Petri net is designed using the reachability trees of its original net and subnet. The research results are illustrated by an example of designing, analyzing and verifying a real-time manufacturing system.

Original languageEnglish (US)
Article number4
JournalTransactions on Embedded Computing Systems
Issue number1
StatePublished - Jan 2013

All Science Journal Classification (ASJC) codes

  • Software
  • Hardware and Architecture


  • Automated manufacturing system
  • Reachability
  • Real-time
  • Refinement


Dive into the research topics of 'Design, analysis and verification of real-time systems based on time petri net refinement'. Together they form a unique fingerprint.

Cite this