Property Analysis of Refinement of Petri Net Based Representation for Embedded Systems

ABSTRACT

Petri net refinement is a transformation by replacing a simple entity of a system with its functional and operational details. In general, the refined system may become incorrect even if the original system is correct because some of its original properties may have been lost or some undesired properties may have been created. For systems specified in an expended Petri net, this paper proposes conditions imposed on a kind of transition subnet refinement under which timing, functionality and reachability will be preserved. Such results can be applied nicely to solve design problems in intelligent building and also enhance the property-preserving approach and characterization-based approach for system verification.

Keywords: