FORMAL VERIFICATION OF REAL-TIME SYSTEM REQUIREMENTS

The methodology of system reąuirements verification presented in this paper is a proposition of a practical procedurę for reducing some negatives of the specification of reąuirements. The main problem that is considered is to create a complete description o f the system reąuirements without any negatives. Verification of the initially deftned reąuirements is based on the coloured Pctri nets. Those nets are useful for testing some properties of system reąuirements such as complete- ness, consistency and optimality. An example of the lift controller is presented