Browse Prior Art Database

Petri Net Approach to Correctness Checking on Changing Software

IP.com Disclosure Number: IPCOM000104490D
Original Publication Date: 1993-Apr-01
Included in the Prior Art Database: 2005-Mar-19
Document File: 1 page(s) / 36K

Publishing Venue

IBM

Related People

Li, SG: AUTHOR

Abstract

As software systems become indispensable in many areas, more software systems require dynamic change support that allows structural change on the system while in continuous operation. However, any dynamic change should not damage the system's correctness. Deciding if a change should be granted and determining the states for a safe change are difficult but vital to assure the system's reliability. This paper proposes a Petri net approach using the path property notion for software correctness checking. The path property notion can describe a system's dynamic aspects statically. It provides a set of linear expressions in logical relationships to overcome the difficulty of articulating and reasoning a dynamically changing system.

This text was extracted from an ASCII text file.
This is the abbreviated version, containing approximately 100% of the total text.

Petri Net Approach to Correctness Checking on Changing Software

      As software systems become indispensable in many areas, more
software systems require dynamic change support that allows
structural change on the system while in continuous operation.
However, any dynamic change should not damage the system's
correctness.  Deciding if a change should be granted and determining
the states for a safe change are difficult but vital to assure the
system's reliability.  This paper proposes a Petri net approach using
the path property notion for software correctness checking.  The path
property notion can describe a system's dynamic aspects statically.
It provides a set of linear expressions in logical relationships to
overcome the difficulty of articulating and reasoning a dynamically
changing system.  By deploying a change decomposition strategy, a
change session can be divided into a set of valid elementary changes.
In this research, it was discovered that only certain types of
elementary changes have impact on the correctness of path property.
For reducing the computational complexity of correctness checking,
this research has developed a Changed Region Analysis technique to
identify the necessary parts for further correctness checking.  An
operational prototype that is implemented in Prolog has shown the
proposed Petri net approach's feasibility and usefulness in
correctness checking on dynamically changing software.

Disclosed Anonymously.