A formal Petri net/temporal logic based tool for the analysis and design of manufacturing control systems

• Main Author: Passmore, Peter Jonathan
• Published: Kingston University 1990
• Subjects: 629.892; Robotics
• Online Access: https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.280625

The development of manufacturing control systems is a complex and expensive task for which sophisticated development tools and techniques are needed. Although there has been some progress in the development of structured methods to aid system specification and design, there has been less headway in the development of Computer Aided Software Engineering (CASE) tools. The problem addressed is the definition of a specification and analysis formalism for manufacturing control systems, which could form the basis of such a tool. Consideration of the requirements for modelling manufacturing control systems, leads to an examination of the utility of petri net models in manufacturing. A formal petri net based model (CIMNET) is subsequently developed based on extending Coloured Petri Nets (CPN) to produce ECPN (Extended Coloured Petri Nets). The ECPN model enhances the basic CPN by the inclusion of datatypes, guarded transitions and message passing. ECPNs may then be transformed into SECPN (State Enumerated Coloured Petri Nets) which can be analysed by a form of linear time temporal logic, allowing for the formal analysis of the behaviour of control systems. The inclusion of the CIMNET formalism in a wider modelling environment is then considered. This results in a high level specification of a manufacturing control system CASE tool, embedding CIMNETS in an object oriented paradigm that allows the inclusion of rule based systems. As a corollary to the specification of the CASE tool, the relationship of the IDEF structured methodology to CIMNETs is examined and the translation of IDEF2 concepts into CIMNETs presented. A number of possible extensions to this work are considered.