Structure and behavior preservation by Petri-net-based refinements in system design

A refinement is a transformation for 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 unneeded properties ma...

Full description

Saved in:
Bibliographic Details
Published in:Theoretical computer science 2004-12, Vol.328 (3), p.245-269
Main Authors: Huang, Hejiao, Cheung, To-yat, Ming Mak, Wai
Format: Article
Language:English
Subjects:
Applied sciences
Computer science
control theory
systems
Computer systems and distributed systems. User interface
Design
Exact sciences and technology
Petri net
Preservation
Property
Refinement
Software
Software engineering
Specification
Verification
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:A refinement is a transformation for 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 unneeded properties may have been created. For systems specified in pure ordinary Petri nets, this paper proposes the conditions imposed on several types of refinement under which the following 19 properties will be preserved: state machine, marked graph, free choice net, asymmetric choice net, conservativeness, structural boundedness, consistence, repetitiveness, rank, cluster, rank-cluster-property, coverability by minimal state-machines, siphon, trap, cyclomatic complexity, longest path, boundedness, liveness and reversibility. Such results have significance in three aspects: (1) It releases the designer's burden for having to provide different methods for individual properties. (2) In the literature, refinements have been shown preserving several equivalence relations and behavioral properties. Our results show that they also preserve many structural properties. (3) It greatly enlarges the scope of applicability of refinements because they can now be applied on systems that satisfy more properties than just liveness and boundedness.
ISSN:0304-3975
1879-2294
DOI:10.1016/j.tcs.2004.07.016