The following papers describe how CP-nets can be used to close the gap between requirements specification and the realization of the requirements in an IT system. The papers describe how informal task descriptions are used as a basis for constructing two CPN models of a new electronic patient record. The first CPN model is a prototype-like representation of the task descriptions that helps to validate and elicit requirements. The second CPN model is a Colored Workflow Net (CWN) that is derived from the first model. The papers demonstrate how the CWN can be translated into the YAWL workflow language, thus resulting in an operational IT system.
Existing web services can be aggregated into new composite web services (CWS). It can be difficult to ensure that composite web services deal efficiently with faults and failures of their underlying services and components. This paper focuses on the issue of faults and failures in composite web services . This paper shows how CP-nets can be used to model CWS and interactions with other web services, and how the model is analyzed to make CWS more robust.
The following paper deals with the modelling and analysis of the execution architecture of a new family of mobile phone software being developed by Nokia, Finland. The paper shows how architectural modelling can be used to control properties of industrial scale products and product families. The requirements of the architecture were checked by means of the CPN model, evaluating alternative mechanisms and policies. This meant that some potential problems were located. The modelling and analysis were done during the design of the architecture and hence it provided immediate feedback to the designers. The CPN model was used to analyse both the time and space complexity of the software in the product family. The CPN model is also expected to become a valuable tool in configuring different members of the product family. The analysis of the CPN model was primarily done by means of simulation. However, the paper also reports on some initial studies on the use of state spaces.
The following paper describes a project on modelling feature interaction patterns of Nokia mobile phones by means of CP-nets. A modern mobile phone supports many features such as voice and data calls, text messaging, WAP browsing, games, etc. The limited user interface and the seamless intertwining of logically separate features cause many problems in the software development of the user interface of mobile phones. The CP-net model was instructed with visualisation and interaction facilities to allow the user to control and get information from simulations without interacting with the underlying CP-nets. Inconsistencies in the specifications were identified.
The following papers describe two projects at the Hewlett-Packard Laboratories, in Palo Alto, USA. One of the projects dealt with on-line transaction processing systems while the other dealt with a complex interconnection fabric: The papers conclude that Petri-net based tools are very useful in the initial design phases when key decisions about the system structure and behaviour need to be evaluated from simulation studies. CP-nets provide both graphical and mathematical system modelling views and enable both quantitative and qualitative analysis of the design.
The projects are also described in Chapter 4 of:
K. Jensen: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Volume 3, Practical Use. Monographs in Theoretical Computer Science, Springer-Verlag, 1997. ISBN: 3-540-62867-3.
The following paper describes how state spaces of CP-nets were used to verify the correctness of a mutual exclusion algorithm designed by Lamport. It is proved that the algorithm has all the properties to be expected from a mutual exclusion algorithm, e.g., that there are no deadlocks and that at any time no more than one process is in the critical section. The construction and analysis of state spaces are done by the CPN tools totally automatically. This means that state spaces are easy to use, requiring very limited human work. Hence, this kind of verification is cheap and reliable.
The project is also described in Chapter 5 of:
K. Jensen: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Volume 3, Practical Use. Monographs in Theoretical Computer Science, Springer-Verlag, 1997. ISBN: 3-540-62867-3.
The following paper presents a project in which CP-nets and the CPN tools were used to investigate a protocol used in the distributed implementation of an object-oriented programming language. The language allows objects to be distributed on several computers. The protocol is used when an object on one computer invokes an object on another computer. This works in a way which is similar to remote procedure calls.
The project is also described in Chapter 13 of:
K. Jensen: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Volume 3, Practical Use. Monographs in Theoretical Computer Science, Springer-Verlag, 1997. ISBN: 3-540-62867-3.
The following paper presents a project in which CP-nets and the CPN tools were used to investigate an Internet object cache. The results obtained from the model has compared to real measured data.
The following paper describe how CP-nets and the CPN tools were used to develop a bank software application for supervising electronic funds transfer using a new software development methodology. Requirements analysis and system specification were done by means of Structured Analysis and Design Technique (SADT), producing a functional description of the system activities. System design and verification were done by means of CP-nets, creating executable models used for rapid prototyping and validation of behavioural properties. Finally, implementation was done by means of the Standard ML programming language. The three parts of the development process were closely interconnected. The CP-nets were derived from the SADT diagrams, while the final ML code was derived from the CP-nets.
The project is also described in Chapter 14 of:
K. Jensen: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Volume 3, Practical Use. Monographs in Theoretical Computer Science, Springer-Verlag, 1997. ISBN: 3-540-62867-3.
The following paper describes how CP-nets and the CPN tools were used for modelling and simulation of a document storage system. The modelled system is part of a large system which is capable of storing 20-30 million documents corresponding to a storage capacity of 10 000-15 000 Gbytes.
The project is also described in Chapter 12 of:
K. Jensen: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Volume 3, Practical Use. Monographs in Theoretical Computer Science, Springer-Verlag, 1997. ISBN: 3-540-62867-3.
The following paper describes how state spaces were used to identify a number of deadlocks in the communication patterns of an ADA program.
The paper analyses the performance of an algorithm for distributed state space generation for timed Petri Nets, using CP-nets.
