Software

From Task Descriptions via CPN towards Implementation of Electronic Patient Record

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.

  • J.B. Jørgensen, K.B. Lassen, W.M.P. van der Aalst: From Task Descriptions via Coloured Petri Nets Towards an Implementation of a New Electronic Patient Record. In International Journal on Software Tools for Technology Transfer, 10(1), 2008, Springer-Verlag, 15-28.

  • J.B. Jørgensen, K.B. Lassen, W.M.P. van der Aalst: From Task Descriptions via Coloured Petri Nets Towards an Implementation of a New Electronic Patient Record. In K. Jensen (ed.): Proceedings of the Seventh Worskhop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, October 2006, Department of Computer Science, University of Aarhus, PB-579, 17-36.

Composite Web Services

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.

  • K. Zurowska and R. Deters: Overcoming Failures in Composite Web Services by Analysing Colored Petri Nets . In K. Jensen (ed.): Proceedings of the Eighth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, October 2007, Department of Computer Science, University of Aarhus, PB-584, 87-106.

Mobile Phones at Nokia

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.

Feature Interaction in Mobile Phones at Nokia

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.

  • L. Lorentsen, A.-P. Touvinene, J. Xu: Modelling Feature Interaction Patterns in Nokia Mobile Phones using Coloured Petri Nets and Design/CPN. In: K. Jensen (ed.): Proceedings of the Third Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, August 2001, Department of Computer Science, University of Aarhus, PB-554, 1-14.

Bank Transactions and Interconnect Fabric at Hewlett-Packard

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.

  • L. Cherkasova, V. Kotov, T. Rokicki: On Net Modelling of Industrial Size Concurrent Systems. In: M. Ajmone-Marsan (ed.): Application and Theory of Petri Nets 1993. Proceedings of the 14th International Petri Net Conference, Chicago 1993, Lecture Notes in Computer Science Vol. 691, Springer-Verlag 1993, 552-561.
  • L. Cherkasova, V. Kotov, T. Rokicki: On Scalable Net Modeling of OLTP. In PNPM93: Petri Nets and Performance Models. Proceedings of the 5th International Workshop, Toulouse, France 1993, IEEE Computer Society Press, 270-279.

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.

Mutual Exclusion Algorithm at University of Aarhus

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.

  • J.B. Jørgensen, L.M. Kristensen: Computer Aided Verification of Lamport's Fast Mutual Exclusion Algorithm Using Coloured Petri Nets and Occurrence Graphs with Symmetries. IEEE Transactions on Parallel and Distributed Systems. Vol.10, No. 7, July 1999, 714-732.

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.

Distributed Program Execution at University of Aarhus

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.

  • J.B. Jørgensen, K.H. Mortensen: Modelling and Analysis of Distributed Program Execution in BETA Using Coloured Petri Nets. In J. Billington and W. Reisig (eds.): Application and Theory of Petri Nets 1996.Proceedings of the 17th International Petri Net Conference, Osaka 1996, Lecture Notes in Computer Science Vol. 1091, Springer-Verlag 1996, 249-268.

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.

Internet Object Cache at the Hungarian Academy of Science

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.

  • B. Kolics, K.M. Hangos: A CPN Model of an Internet Object Cache. In: K. Jensen (ed.): Proceedings of the Workshop on Practical Use of Coloured Petri Nets and Design/CPN, Aarhus 1998, Department of Computer Science, University of Aarhus, PB-532, 233-251.

Electronic Funds Transfer in the US

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.

  • V.O. Pinci, R.M. Shapiro: An Integrated Software Development Methodology Based on Hierarchical Colored Petri Nets. In: G. Rozenberg (ed.): Advances in Petri Nets 1991, Lecture Notes in Computer Science Vol. 524, Springer-Verlag 1991, 227-252. Also in K. Jensen, G. Rozenberg (eds.): High-level Petri Nets. Theory and Application. Springer-Verlag, 1991, 649-667.

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.

Document Storage System at Bull AG

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.

  • G. Scheschonk, M. Timpe: Simulation and Analysis of a Document Storage System. In: R. Valette (ed.): Application and Theory of Petri Nets 1994. Proceedings of the 15th International Petri Net Conference, Zaragoza 1994, Lecture Notes in Computer Science vol. 815, Springer-Verlag 1992, 454-470.

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.

ADA Program at Draper Laboratories

The following paper describes how state spaces were used to identify a number of deadlocks in the communication patterns of an ADA program.

  • W.W. McLendon, R.F. Vidale: Analysis of an Ada System Using Coloured Petri Nets and Occurrence Graphs. In: K. Jensen (ed.): Application and Theory of Petri Nets 1992. Proceedings of the 13th International Petri Net Conference, Sheffield 1992, Lecture Notes in Computer Science Vol. 616, Springer-Verlag 1992, 384-388.

Performance of Distributed Generation of State Spaces at Memorial University

The paper analyses the performance of an algorithm for distributed state space generation for timed Petri Nets, using CP-nets.

  • W.M. Zuberek. Performance Study of Distributed Generation of State Spaces Using Coloured Petri Nets. In: K. Jensen (ed.): Proceedings of the Fourth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, August 2002, Department of Computer Science, University of Aarhus, PB-560, 81-98.