In: Journal of Systems and Software, Volume 68, Issue 2 , 15 November 2003, pages 153-165. Elsevier, November 2003.
Abstract: Homogeneous, shared memory multiprocessors that incorporate real-time operating systems constitute in many corporations the basic platforms for developing applications of plant monitoring and automation. In this work, a template model based on the High Level Petri Net (HLPN) formalism is proposed for this class of computers. Mapping functional and timing requirements of the application software to states of this model and searching for their existence in the reachability tree of the net can verify the satisfaction of these requirements. A state searching algorithm has been developed for the case of a shared memory multiprocessor in which there is a bus-based interconnection network supporting a single communication channel for the exchange of data among the CPUs, the common memory and the computer interfaces. This algorithm groups the infinite number of states of the HLPN to a number of finite regions, identifies the region, which the desired state belongs to, and checks for the existence of a path from the initial state that leads to this region. In order to demonstrate the use of the template in the modeling and verification of timing and functional specifications of a system of the considered class, the implementation of the automation functions of a chemical reactor by a VME-bus based multiprocessor with two CPUs and running under the control of the OS-9 operating system was studied. In this study the template model was used to create a specific for this application HLPN model. The response times of two automation functions were predicted by the use of this model and compared with those derived from the operating characteristics of the reactor.
Keywords: High Level Petri Nets; Multiprocessor systems; Performance analysis; Requirements verification.