In: IEICE Trans. on Fundamentals in Electronics, Communications and Computer Science, Vol. E78-A, No. 11, pages 1468-1478. 1995.
Abstract: Due to the large and complex information processing systems, formal description methods are needed for specification of systems and their efficient and reliable designs. During the early stage of system design, it is often necessary to modify or change system requirements which may influence the whole system design. A new flexible description methodology is proposed which copes with the modifications or changes in the system requirements, in order to obtain the formal specification of the system. It is shown that function requirements can be modeled by a logical Petri net (LPN), which is a kind of extended Petri net in order to derive the formal specification. This paper proposes a verification method of system requirements which contain some kind of logical errors. Further, it describes a method to decompose and refine a requirement description hierarchically, and discusses how to derive a formal specification from a requirement description flexibly along the proposed refinement method against the changes of the requirement description of the system.
Keywords: formal specifications, formal verification, logical Petri nets, requirement refinements, state transitions, system requirements.