A formal approach to system design and refinement

Vijay Varadharajan*

*Corresponding author for this work

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

1 Citation (Scopus)

Abstract

The Petri net formalism is used in the synthesis of system designs. A methodology is used that makes it possible to synthesize arbitrary size well-behaved Petri nets, using a stepwise refinement technique. This technique provides a method for constructing large systems that are well-behaved by design. The steps that are required in developing a synthesis procedure are outlined and brief mention is made of some of the work that has been done in this area. A subclass of nets called information flow nets (IFNs) is proposed, and the notion of a well-behaved IFN is defined. A refinement procedure for IFNs is presented, and the conditions required for the refinement procedure to preserve well-behavedness are derived. The theorem of refinement of IFNs is given. The author formulates appropriate interpretations for the properties of the nets, enabling him to synthesize systems in different applications.

Original languageEnglish
Title of host publicationCOMPEURO'90: Proceedings of the 1990 IEEE International Conference on Computer Systems and Software Engineering - Systems Engineering Aspects of Complex Computerized Systems
Place of PublicationPiscataway, N.J.
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Pages544-545
Number of pages2
ISBN (Print)0818620412
DOIs
Publication statusPublished - May 1990
Externally publishedYes
EventProceedings of the 1990 IEEE International Conference on Computer Systems and Software Engineering - COMPEURO '90 - Tel-Aviv, Isr
Duration: 8 May 199010 May 1990

Other

OtherProceedings of the 1990 IEEE International Conference on Computer Systems and Software Engineering - COMPEURO '90
CityTel-Aviv, Isr
Period8/05/9010/05/90

Fingerprint Dive into the research topics of 'A formal approach to system design and refinement'. Together they form a unique fingerprint.

Cite this