A mathematical model for system design and refinement

Vijay Varadharajan*

*Corresponding author for this work

Research output: Contribution to journalArticle

Abstract

This paper considers the use of Petri nets in the system design process. It proposes a new class of Petri nets called Information Flow Nets (IFNs) which are particularly suitable for performing refinement in the system design. We first define the class of IFNs and describe their behaviour and some of their useful properties, such as clean termination. The notion of a “well-behaved IFN” is then defined and a top-down refinement technique is presented which allows us to construct arbitrary size well-behaved IFNs. The conditions required for the refinement technique to preserve the properties of a well-behaved IFN are derived. We formally prove that a refined IFN N” obtained by substituting a well-behaved IFN N' in a well-behaved IFN N, is itself well -behaved. The significance of such a technique is that it can be used, in a top-down approach to system design, to build systems that are automatically well-behaved. This in turn helps to avoid the difficulty of analyzing large and complex nets.

Original languageEnglish
Pages (from-to)13-31
Number of pages19
JournalInternational Journal of Computer Mathematics
Volume34
Issue number1-2
DOIs
Publication statusPublished - 1990
Externally publishedYes

Keywords

  • liveness and safeness
  • Petri nets
  • refinement
  • system design
  • top-down design analysis

Fingerprint Dive into the research topics of 'A mathematical model for system design and refinement'. Together they form a unique fingerprint.

Cite this