This report summarises the work in the CPN Centre in year 2002. The CPN Centre (CIT partnership No. 202) was established as a continuation of the HP-CPN Centre and has a staff of 15-20 persons. The work within the CPN Centre focuses on three main areas:

· Design and analysis of communication protocols and other kinds of distributed systems.

· Performance analysis and capacity planning.

· Tools, algorithms, and techniques to support the two areas above.

The partners in the project are:

· University of Aarhus, Aarhus, Denmark,

· Nokia Research Center, Helsinki, Finland,

· George Mason University, Fairfax VA, USA,

· Hewlett-Packard.

2 Tool Support for Coloured Petri Nets

The aim of this project has been to develop a state-of-the-art computer tool to support the practical use of Coloured Petri Nets. The new tool is called CPN Tools, and within the next year it is expected to fully replace our old tool, Design/CPN, which is being licensed to nearly 1000 organisations in 60 countries, including 200 commercial companies.

The CPN Tools project started in 1999, and it is now at a stage where CPN Tools has been released for use outside the CPN group. In March 2003, CPN Tools are being used by more than 250 organisations in 47 countries, and this figure is rapidly increasing. The present version is so stable that it can be used for work in smaller projects.

The development of the CPN Tools has been supported via a number of projects in which the CPN group has worked as subcontractors for George Mason University, Fairfax VA, USA. In 2000 the project was also supported by a grant from Microsoft Research Limited in Cambridge, UK. The following subsections describe some of the main facilities that have been developed for the new tool.

2.1 New User Interface

The user interface of the CPN Tools has been designed in close cooperation with leading researchers within the field of Human-Computer Interaction (HCI). The user interface has attracted a lot of interest and excitement, both among HCI researchers and Petri Net researchers. It has been presented at a number of international conferences.

Unlike standard graphical applications, our user interface does not use menu bars, scrollbars or dialog boxes, and there is no need to select objects before editing them. Yet the system is much faster to operate than a traditional desktop interface. Windows are replaced by “sheets” that can be collected together into “binders”, making it easy to flip between sheets and to organise the workspace. A track-ball, operated by the left hand (if you are right-handed) supplements the mouse in the right hand. Using these two input devices, it is possible to resize and zoom objects by stretching them as one would do with a physical object. It is also possible to move an object with the right hand while flipping sheets with the left hand to find its destination. Another two-handed input technique consists of moving a semi-transparent palette called a toolglass with the left hand while clicking through the tools in it with the right hand. Finally, circular menus that pop-up where the mouse is clicked allow a very fast selection of commands. When the selection is made quickly, a command can be invoked without displaying the menu. This substitutes the use of keyboard shortcuts.

2.2 New Simulation Engine

The CPN Tools use a new simulation engine that is much faster than our old simulation engine. This is particularly important for simulation-based performance analysis and capacity planning. Simulations of complex CPN models are often as much as 1000 times faster. This means that many simulations can now be run in a few seconds instead of hours. The efficiency of the new simulation engine is based on the following modifications:

· The data structures for multi-sets are a special kind of self-balancing trees.

· Priority queues are used for timed tokens.

· The algorithm for enabling calculation is significantly improved.

· The scheduler is modified to make a more efficient search for enabled transitions.

The simulation engine is a very complicated piece of software and hence it is a non-trivial and lengthy task to debug it as it is being used for more and more complicated CPN models.

2.3 Monitoring Facilities

The monitoring facilities provide means to observe ongoing simulations of a CPN model and to take appropriate actions based on the observations. During the simulation of a CPN model it is possible to examine the states and events of the system, periodically extract information from the states and events, and then use the information for very diverse purposes, such as:

· stopping the simulation when a certain condition is fulfilled,

· visualisation of behaviour using domain-specific graphics,

· data collection for performance analysis,

· communication with other processes,

· formal analysis methods.

General patterns in how ad-hoc monitoring has been done in the past have been identified, and these patterns have been generalised to create a uniform and flexible framework for monitoring simulations of CPN models. One of the advantages of the monitoring framework is that it is now possible to use monitors to inspect or control a simulation without having to alter the CPN model itself. The monitoring facilities support both standard monitors and user-defined monitors. Current work focuses on integrating an existing prototype of the monitoring facilities into CPN Tools, and the facilities are expected to be available by the end of 2003.

2.4 Analysis of Simulation Results

Performance is often a central issue in the design, development, and configuration of systems. Prototype support for collecting and analysis of data from simulations of CPN models has been developed for the new simulation engine. These facilities can, e.g., be used for:

· analysing the performance of existing systems,

· estimating the performance of newly designed systems,

· comparing the performance of different systems,

· capacity planning.

Data collection is implemented using the monitoring framework that was previously mentioned. As a result, data can be collected during a simulation without having to modify the CPN model, and performance measures, such as throughput or average response time, can be calculated on-the-fly. Facilities for executing batches of simulations for a given CPN model have also been created and applied in several case studies. Confidence intervals, which indicate the reliability and precision of estimated performance measures, are automatically calculated during batch simulations. The large amount of data output that is generated during simulations is saved in a systematic manner, and scripts are automatically generated for plotting simulation output with an external application. Additional facilities for running batches of simulations for several different configurations of a given CPN model have been developed and tested. Support is also provided for a variance reduction technique that can be used in an attempt to reduce the number of simulations that need to be run in order to obtain sufficiently precise results. Current work focuses on integrating prototype performance facilities into CPN Tools, and the facilities are also expected to be available by the end of 2003.

2.5 Tool Support for State Space Analysis

The state space tool from Design/CPN has been modified so that it now works on top of the new simulation engine mentioned above. The user interface for CPN Tools has been extended such that state spaces can now be constructed and analysed directly in CPN Tools, whereas in the past, users had to construct the model in CPN Tools and then load it into Design/CPN to perform the state space analysis. Future work includes the design and implementation of facilities for drawing full and partial state spaces.

2.6 Consolidation and Completion

During 2002 a lot of effort has been invested in making CPN Tools much more stable and extending it with additional features, such as:

· support for generating and analysing state spaces,

· general undo and redo facilities,

· support for fusion sets,

· support for arbitrarily many pointing devices,

· improved error feedback,

· improved visual appearance.

Many internal parts of the tool have been thoroughly refactored in order to support the new features as well as to make the software more stable. A year and a half has passed since CPN Tools was initially released to the public as version 0.1.1. The work that was completed in 2002 has led to an improved, mature, and well-tested version of CPN Tools which is expected to be released as version 1.0 in May 2003.

3 State Space Methods

State spaces are one of the main analysis methods for CP-nets and formal methods in general. They allow the system developer to investigate and reason about the logical correctness of systems. The basic idea is to compute all possible behaviours of the system and represent these as a directed graph called the state space. The nodes correspond to the set of reachable states while the arcs correspond to transitions between reachable states.

The main advantage of state space methods is that they can be supported by computer tools – hiding the underlying mathematics and making them highly automatic to use. This makes state space methods attractive for industrial use. The main disadvantage of state space methods is that for complex systems the demands on the speed and memory of the computer where the state space analysis is being conducted are strong. The improvement of state space methods is therefore closely related to the development of state space reduction methods capable of reducing the time and space requirements for the analysis. The development of a number of new reduction methods allow still more complex systems to be analysed. The CPN Centre has a number of ongoing research activities concerned with the development of state space reduction methods and efficient implementation techniques. The research in 2002 has primarily focussed on the further development of the sweep-line state space method.

The sweep-line method was developed by members of the CPN Centre in 2001. The basic idea of the sweep-line method is to exploit a certain kind of progress present in many distributed and concurrent systems. Exploiting progress makes it possible to sweep through the full state space of the system while storing only small fragments of the state space in computer memory at a time. This can lead to significant reduction in peak memory usage for the state space analysis of the system. Practical experiments have shown that the method also leads to savings in the time used to construct state spaces.

3.1 A Generalised Sweep-Line Method

A limitation of the basic sweep-line method is that it is based on a monotonic measure of progress. This means that the method could not be used on reactive systems with a cyclic behaviour. To remedy this situation, the basic sweep-line method has been generalised to allow the use of non-monotonic progress measures. The key idea is to recognise, on-the-fly during the state space exploration, situations where the monotonic progress notion is violated – taking necessary actions to handle the violation. The generalised sweep-line method is guaranteed to find all reachable states, but it may explore the same state several times. The generalisation significantly broadens the class of systems for which sweep-line methods can be applied.

3.2 Automatic Computation of Progress Measures

A shortcoming of the basic sweep-line method is that it requires the user to provide a progress measure based on his/her understanding of the system behaviour. A technique has been developed which allows the automatic computation of the progress measure from a system description. The technique is based on a compositional framework where systems are specified as parallel composition of subsystems, and where the state space of the subsystems can be computed prior to computing the state space of the full system. A positive side-effect of considering a compositional framework was that it led to a variant of the sweep-line method capable of exploiting the compositional structure of systems.

3.3 Path Generation

A main advantage of state space methods is that they can provide the analyst with diagnostic information as to why the system does not possess required properties. This diagnostic information is useful for debugging of systems and is often in the form of directed paths in the state space. Obtaining such directed paths is difficult with the sweep-line method because states and arcs of the state space are deleted from main memory during the state space exploration. The sweep-line method has been combined with the use of external storage on disk to support the generation of diagnostic information. The basic idea of the method is to write states and arcs of the state space to disk as they are deleted from main memory. A desired directed path can subsequently be reconstructed based on the information stored on disk. An advantage of the developed method, compared to related methods using external storage, is that it avoids any costly searches in external storage during the state space exploration.

3.4 Combining the Sweep-Line Method and Other Reduction Methods

An abundance of state space reduction methods have been developed. These reduction methods typically exploit certain characteristics of systems such as symmetry, independence between events, and progress. These characteristics are typically orthogonal which means that it is of interest to use several state space reduction methods simultaneously. The combined use of reduction methods typically leads to better reduction results than when either method is use alone. This idea has been pursued by studying the combination of the equivalence class method and the sweep-line method, and developing the required theoretical foundation. The equivalence class method is a generalisation of the state space reduction method exploiting symmetries in systems. The basic idea of the equivalence class method is to group states and events into equivalence classes, and then store a representative from each equivalence class in memory instead of storing all members of the equivalence class. This can significantly reduce memory consumption. Some initial practical experiments have shown that the combination of the sweep-line method and the equivalence class method indeed gives better reduction results than when either method is used in isolation.

4 COAST/CPN: State Space Analysis in Operational Planning

This project is concerned with the development of CPN-based tool support for operational planning environments. The project is a co-operation with the Australian Defence Science and Technology Organisation (DSTO) and focuses on the use of CP-nets to formally model business processes for operational planning and on the use of CP-nets for developing operational plans.

The analysis of business processes and synthesis of operational plans are based on the state space method. The state space of a business process represents all the possible ways in which the process can be executed. State spaces are being used as a basis for formally reasoning about properties of the planning process and for re-engineering purposes. The state space of an operational plan represents the possible ways in which the operational plan can be executed, subject to resource, timing, and synchronisation constraints. The project contributes to the server part of the Course of Action Scheduling Tool (COAST) currently being developed by DSTO. The work in 2002 has spanned the following areas:

Lines of Operation Generation

The key functionality of the COAST server is the capability to compute lines of operation (LOPs) from a constructed state space. Algorithms have been developed and implemented to support the generation of LOPs leading to desired and undesired end-states of an operational plan.

Resource Availability Intervals

Resources are a central concept in the COAST framework. Resources represent the planes, ships, and tanks required to execute tasks. The CPN model providing the semantic foundation of the COAST server has been extended to support resource availability intervals. These resource availability intervals make it possible to describe that a resource is only available in certain intervals of time due to, e.g., service intervals.

Diagnostic Capabilities

An important part of COAST is to support the planner in debugging an operational plan, i.e., to determine the reason as to why a desired end-state cannot be reached with the set of tasks provided and the assigned resources. The COAST server has been extended with a number of diagnostic capabilities such that errors and problems in an operational plan can be identified fully automatically.

5 CPN in Pervasive Health Care

In a joint research project with participation of Aarhus County Hospital, the software company Systematic Software Engineering A/S, and the Centre for Pervasive Computing at the University of Aarhus, a new pervasive health care system for the hospitals in Aarhus is being envisioned.

The envisioning of the new system brings up new challenges that software developers are confronted with in relation to pervasive computing. In collaboration with colleagues from the Department of Computer Science at the University of Aarhus, personnel from hospitals in Aarhus, and software developers from involved companies, we are investigating how CP-nets can be used to meet some of these challenges. We have gained evidence that CP-nets can be an effective means for requirements engineering – to facilitate communication and collaboration between users and software developers – and also for design of middleware components for the new system.

6 PhD Theses in 2002

During 2002 three PhD students in the CPN Centre delivered and successfully defended their PhD theses. A fourth thesis was delivered in the beginning of 2003 and will be defended in April 2003. Abstracts for the four PhD theses are contained in the following four sections.

6.1 The Symmetry Method for Coloured Petri Nets - Theory, Tools, and Practical Use

A way to increase reliability of systems is to use formal methods, which are mathematically based methods for specifying and reasoning about systems. An example of a formal method for reasoning about systems is the state space method. The full state space of a system is a directed graph with a node for each reachable state of the system and an arc for each state change. From the full state space it is possible to verify whether the system satisfies a set of desired properties.

Several reduction techniques have been suggested for reducing the state space. With these reduction techniques only a subset of the full state space is represented or the full state space is represented in a compact form. An example of such a reduction technique is the symmetry method. The basic observation is that many distributed and concurrent systems posses a certain degree of symmetry, e.g., a system composed of identical components whose identities are interchangeable from a verification point of view. This kind of structural symmetry in the system is also reflected in the full state space of the system. The idea behind the symmetry method is to factor out this symmetry and obtain a condensed state space which is typically much smaller than the full state space, but from which the same kind of properties of the system can be derived without unfolding the condensed state space to the full state space.

State spaces and the symmetry method are not restricted to a specific modelling language. However, in the work presented in this thesis the symmetry method is considered in the context of Coloured Petri Nets.

Louise Elgaard’s (née Lorentsen) dissertation consists of two parts. Part I is the mandatory overview paper witch summarises the work which have been done. Part II is composed of four individual papers. Three of the papers have been published as conference papers in international conferences. One paper has been published as a workshop paper. The full dissertation is available online (http://www.daimi.au.dk/CPnets/phd/louisel/).

6.2 Facilitating the Practical Use of Coloured Petri Nets

Design and development of systems is a complex task which is even more complex if the systems are distributed and concurrent. Therefore models are often created of such systems to investigate the systems in various ways. Due to the complexity of such models it is essential that modelling tools exist with support for examining the models.

Coloured Petri Nets is a formally founded graphical language for modelling and analysis of concurrent and distributed systems. The industrial use of CP-nets has increased during the latest years. This is in particular due to the extensive development of tools supporting various uses of CP-nets.

The primary purpose of this dissertation is to investigate and advance tools for practical use of CP-nets. This includes development of facilities for creating domain-specific graphical user interfaces, a proposal for facilities for including auxiliary information in a CP-net without modifying the CP-net itself, and development of general facilities for extracting information from a CP-net during simulations. The tool facilities have been developed based on concrete needs arising during practical projects, and have when possible been tested in these projects.

Bo Lindstrøm’s dissertation consists of two parts. Part I is the mandatory overview paper which summarises the research. Part II is composed of five individual papers and constitutes the core of this dissertation. All five papers have been published as workshop or journal papers. The full dissertation is available online (http://www.daimi.au.dk/CPnets/phd/blind/).

6.3 Performance Analysis using Coloured Petri Nets

Performance is often a central issue in the design, development, and configuration of systems. It is not always enough to know that systems work properly, they must also work efficiently. There are numerous studies, e.g. in the areas of computer and telecommunication systems, manufacturing, military, health care, and transportation, that have shown that time, money, and even lives can be saved if the performance of a system is improved. Performance analysis studies are conducted to evaluate existing or planned systems, to compare alternative configurations, or to find an optimal configuration of a system. There are three alternative techniques for analysing the performance of a system: measurement, analytical models, and simulation models.

This dissertation focuses on the use of Coloured Petri Nets for simulation-based performance analysis of industrial-sized systems. Coloured Petri Nets are particularly well suited for modelling and analysing large and complex systems for several reasons: they have an intuitive graphical representation; they are executable; hierarchical models can be constructed; it is possible to model the time used by different activities in a system; and mature and well-tested tools exist for creating, simulating, and analysing Coloured Petri Net models.

Lisa Wells’ dissertation consists of two parts. Part II is composed of four individual papers and constitutes the core of the dissertation. All four papers have been published as workshop papers. Part I is the obligatory overview paper with summarises the work that has been done. The overview paper introduces the research field of performance analysis using Coloured Petri Nets, and it summarises the contents and contributions of the four individual papers. The full dissertation is available online (http://www.daimi.au.dk/CPnets/phd/wells/).

6.4 Sweeping the State Space

The thesis describes the sweep-line method, a newly developed reduction method for alleviating the state explosion problem inherent in explicit-state state space exploration. The basic idea underlying the sweep-line method is, when calculating the state space, to recognise and delete states that are not reachable from the currently unprocessed states. Intuitively we drag a sweep-line through the state space with the invariant that all states behind the sweep-line have been processed and are unreachable from the states in front of the sweep-line. When calculating the state space of a system, we iteratively calculate successors of new states, and we need to distinguish between previously seen states and truly new states to avoid reprocessing the same states indefinitely. When calculating the successors of the known unprocessed states, all successors are in front of the sweep-line. Consequently, the states behind the sweep-line are not needed for distinguishing between new and old states and can therefore be deleted.

Thomas Mailund’s thesis consists of two parts: Part I gives an overview of the sweep-line method while Part II consists of eight individual papers on different aspects of the sweep-line method. Four of these papers have been published as conference papers, one has been published as a workshop paper, while the remaining are submitted as either journal or conference papers. The full dissertation will eventually become available online (http://www.daimi.au.dk/CPnets/phd/).

7 Master's Thesis Projects in 2002

During 2002 the CPN Centre has been involved in the following thesis projects:

Disk-Based Generation of State Spaces

The thesis of Stefan Sørensen describes the design and implementation of a state space tool that makes efficient use of disk storage. Traditional state space tools keep all data structures in the main memory of the computer. The aim of the thesis is to be able to construct much larger state spaces. The thesis was successfully defended in June 2002.

Distributed State Space Exploration

Farret Guillaume and Carre Guillaume were exchange students from France. Their thesis investigates the use of parallel algorithms in the context of state space generation and analysis. Parallel algorithms have been applied in many other application areas to speed-up demanding computations. The thesis was successfully defended in June 2002.

Hand-Over Between Mobile@Home and GSM Networks

The thesis of René M. Jensen and Jonas M. Thomsen investigates the design of a new set of protocols for combining wireless networks. The thesis project is done in cooperation with Ericsson Diax A/S. The thesis was successfully defended in January 2003.

Modelling and Analysis of Multicast Protocols

The thesis of Lone H. Olesen is part of the GCAP project (Global Communication Architecture & Protocols for new QoS services over IPv6 networks) which is an EU project with 4 commercial companies and 5 educational institutions from 6 countries. The thesis is done in close cooperation with Ericsson Telebit A/S, which is the Danish partner in GCAP. As part of the project three multicast protocols are specified and implemented – with different capabilities in terms of Quality of Service. The aim of the thesis is to model and analyse interesting parts of these protocols. This thesis has not yet been completed.

Evaluation of TCP and Routing Protocols in Mobile Ad-Hoc Networks

The thesis of Eva Kjær Troels and Henrik Refslund Sørensen describes a use of the network simulation tool ns-2 to investigate various routing protocols for mobile ad-hoc networks. A particular focus is to evaluate how the routing protocols support TCP connections. This thesis has not yet been completed.

Modular State Spaces in Design/CPN

Thibaut Ribes and Benjamin Bayart are exchange students from France. Their thesis examines methods for constructing state spaces that try to bypass the state space explosion problem by differentiating between local and global behaviour of modules in a CP-net. The thesis will consider alternative methods for creating modular CP-nets, space-efficient data structures for representing modular state spaces, and methods for inspecting modular state spaces that can be used to examine properties of a system. This thesis has not yet been completed.

8 Continuation of the CPN Centre

The support from the Danish National Centre for IT Research finished with the end of year 2002. However, the activities in the CPN Centre continue supported by grants and subcontracting from the following organisations:

· University of Aarhus, Aarhus, Denmark,

· Nokia Research Center, Helsinki, Finland,

· Ericsson Telebit A/S, Aarhus, Denmark,

· Australian Defence Science and Technology Organisation, Australia

· Danish National Centre for IT Research (PhD grant).

Some of the main activities in 2003 are described in the following subsections.

8.1 State Spaces Methods

We plan to continue the development of the sweep-line method. We will continue the development techniques for automatic identification of progress and for the generation of diagnostic information. These areas of work were described in Sections. 3.2 and 3.3, respectively.

We also plan to initiate the design and implementation of the next generation of state space tools. This is a rather complex and time-consuming task that is similar to the development of the new simulation engine some years ago. The new state space tool is expected to increase the size of systems that can be analysed by several orders of magnitude. The sweep-line method (with the paradigm of deleting states and state information on-the-fly) will put special requirements on the design.

8.2 Development of Communication Protocols

We have started a project on the use of formal methods for specification, validation, verification, and implementation of communication protocols. The project is concerned with the theoretical foundations, supporting computer tools, and applications of formal methods in the areas of Internet protocols and protocols for pervasive computing. The project covers the following areas:

· Modelling languages for design and specification of protocols.

· Algorithms and data-structures for efficient analysis, validation, and verification of protocols. This work will focus on state space methods, model checking, and the recently developed sweep-line method.

· Development and implementation of computer tools supporting protocol development.

· Application of formal methods and supporting computer tools to improve and further develop protocols. This work will focus on Internet protocols and protocols for pervasive computing.

· Implementation of Internet protocols and protocols for pervasive computing. Development of methodology for protocol development using formal methods.

Part of the project will be conducted in cooperation with Ericsson Telebit A/S which is a branch of Ericsson specialising in IP router technology, including routers for IPv6.

8.3 CPN Models in UML-based Software Development – Software for Mobile Phones

In a joint project with Nokia Research Center in Helsinki, a combined use of CP-nets and the Unified Modelling Language (UML) for the development of software for mobile phones is being investigated.

In modern mobile phones, there is a need to balance required functionality with the available system resources. The amount of memory that is needed for executing applications is one of the major limiting factors for the number of features in a mobile device. Therefore, it is important to monitor the amount of memory consumed by the software components and subsystems through the whole software development process and throughout the whole life cycle of components.

Nokia’s existing software architecture descriptions include information about the memory required by each component. In addition to this, the architects are required to present a worst case usage scenario for their system. Doing these calculations by hand is tedious and error prone, since it involves detailed knowledge about the behaviour of the system. It is quite obvious that automated tools can help the system architect in these calculations and make them more precise, since it will be possible to automatically review all possible use patterns of the components. The CPN modelling language and the CPN Tools provide a simulation environment that can be used for analysing memory usage scenarios.

The project described above should be seen as an investigation of the possibility to more generally integrate CPN models in UML-based system development methods, including supporting exchange of information between CPN Tools and Rational Rose which is the UML tool used by Nokia.

8.4 State Space Analysis in Operational Planning

We expect to continue and possibly expand the cooperation with the Australian Defence Science and Technology Organisation in 2003/2004. The continuation of the project will be concerned with the further development of the COAST server, in particular the addition of a number of advanced analysis capabilities as well as extensions of the conceptual framework underlying COAST.

8.5 Modelling and Analysis of Danfoss Flowmeters

We have started a joint project with the Flow Division of Danfoss A/S. The purpose of the project is to use CP-nets to model and analyse the behaviour of a new flowmeter that is being developed by Danfoss. The new flowmeters measure water flow, especially in water supply networks, and they also contain facilities for calculating statistics and for logging information concerning water consumption and leakage. Flowmeters are components in a distributed system, and as such they can communicate with external equipment, such as PCs, via both wired and wireless connections.

When designing the flowmeters, the developers had to consider both strict timing requirements of the measurement software and communication patterns that support a high degree of parallelism within the system. A workable flowmeter and accompanying software has been developed by Danfoss, but they have lacked a method for analysing the complex behaviour of the flowmeters. This project will use CP-nets to examine the dynamic aspects and parallelism within flowmeter systems. There are two main goals of the project. The first is to use verification methods to show either that the flowmeters behave properly or that there are shortcomings in the existing design. The second goal is to evaluate the analysis methods that are used and to illuminate possible shortcomings of the analysis methods.

9 Staff of CPN Centre, March 2003

The staff of the CPN Centre is now as follows:

· Two Research Managers: professor, Dr. Scient, Kurt Jensen, and associate professor, PhD, Søren Christensen.

· Four PostDocs: Jens Bæk Jørgensen, Lars M. Kristensen, Kjeld Høyer Mortensen, Lisa M. Wells.

· One PhD student: Jonas Martin Thomsen. Two additional PhD students will start within the next few months.

· One research assistant: Anne Vinter Ratzer

· Six half-time student programmers: Henry Michael Lassen, Kristian Bisgaard Lassen, Mads Laursen, Peter Julian Marstrand Mechlenborg, Martin Stig Stissing, Michael Westergaard.

· Five Master’s Thesis students: Benjamin Bayart, Lone H. Olsen, Thibaut Ribes, Henrik Refslund Sørensen, and Eva Kjær Troels.

All PhD students and all Master’s thesis students participate in the activities in the CPN Centre, and we consider this to be a very valuable part of their education.

10 Publications from CPN Centre in 2002

[1] Billington J., Christensen S., Hee K. van, Kindler E., Kummer O., Petrucci L., Post R., Stehno C., Weber M.: The Petri Net Markup Language: Concepts, Technology, and Tools. In Proceedings of the 24th International Conference on Application and Theory of Petri Nets (ICATPN'2003). Lecture Notes in Computer Science. Springer-Verlag, 2003. To appear.

[2] Billington, J., Gallasch, G.E., Kristensen, L.M., Mailund, T.: Exploiting Equivalence Reduction and the Sweep-Line Method for Detecting Terminal States. Submitted to IEEE Special Issue on Deadlock Resolution in Computer Integrated Systems, Transactions on Systems, Man and Cybernetics: Part A. Systems and Humans, September 2002.

[3] Elgaard, L.: The Symmetry Method for Coloured Petri Nets - Theory, Tools, and Practical Use. Ph.D. thesis, Department of Computer Science, University of Aarhus, Denmark, July 2002.

[4] Elliot, M., Billington, J., Kristensen, L.M.: Using Design/CPN to Design a Visualisation Extension to Design/CPN. In Proceedings of Fourth Workshop and Tutorial on Practice Use of Coloured Petri Nets and CPN Tools (CPN'02), pp. 21-38. DAIMI PB-560, Department of Computer Science, University of Aarhus, 2002. ISSN 0105-8517.

[5] Gallasch, G.E.; Kristensen, L.M.; Mailund, T.: Sweep-Line State Space Exploration for Coloured Petri Nets. In Proceedings of Fourth Workshop on Practical Use of Coloured Petri Nets and the CPN Tools (CPN 2002). DAIMI PB-560 pp. 101-119, Aarhus, Denmark, 2002.

[6] Gordon, S., Kristensen, L.M., Billington, J.: Verification of a Revised WAP Wireless Transaction Protocol. In J. Esparza, C. Lakos (eds.): Application and Theory of Petri Nets 2002. Proceedings of the 23rd International Petri Net Conference (ICATPN 2002). Volume 2360 of Lecture Notes in Computer Science, pp.182-202. Springer-Verlag, 2002.

[7] Jensen, K. (Ed.): Fourth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, Aarhus, Denmark, August 28-30, 2002. Proceedings. Department of Computer Science, University of Aarhus, PB-560, 2002.

[8] Jørgensen, J.B.: Coloured Petri Nets in Development of a Pervasive Health Care System. In Proceedings of the 24th International Conference on the Application and Theory of Petri Nets (ICATPN 2003). Lecture Notes in Computer Science, Springer-Verlag, 2003. To appear.

[9] Jørgensen, J.B.: Coloured Petri Nets in UML-Based Software Development – Designing Middleware for Pervasive Healthcare. In: Proceedings of the Fourth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools. Jensen, K. (Ed.). August 28-30, Aarhus, Denmark: pp. 61-80, 2002.

[10] Jørgensen, J.B., Bossen, C: Executable Use Cases for Pervasive Healthcare. In Proceedings of the 2nd Workshop on Modelling of Objects, Components, and Agents. Moldt, D. (Ed). August 26-27, Aarhus, Denmark: pp. 89-104, 2002.

[11] Jørgensen, J.B, Christensen, S: Executable Design Models for a Pervasive Healthcare Middleware System. In: Proceedings of the 5th International Conference on the Unified Modeling Language, UML2002. Jezequel, J.-M.; Hussmann, H.; Cook, S. (Eds.). September 30 - October 4, Dresden, Germany. Lecture Notes in Computer Science volume 2460, Springer-Verlag, pp.140-149, 2002.

[12] Kristensen, L.M., Billington, J. (Eds): Proceedings of Workshop on Formal Methods Applied to Defence Systems. Volume 12 of Conference in Research and Practice of Information Technology. Australian Computer Society, 2002. Satellite Workshop of the 23rd International Conference on Application and Theory of Petri Nets, Adelaide, 2002.

[13] Kristensen, L.M., Billington, J., Petrucci, L., Qureshi, Z.H., Kiefer, R.: Formal Specification and Analysis of Airborne Mission Systems. In Proceedings of the 21st AIAA/IEEE Digital Avionics Systems Conference. To appear.

[14] Kristensen, L.M.; Mailund, T.: A Compositional Sweep-Line State Space Exploration Method. In Proceedings of Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE 2002). Volume 2529 of Lecture Notes in Computer Science, pp. 327-343, Springer-Verlag, 2002.

[15] Kristensen, L.M., Mailund, T.: A Generalised Sweep-Line Method for Safety Properties. In Proceedings of Formal Methods Europe (FME 2002). Volume 2391 of Lecture Notes in Computer Science, pp. 549-567, Springer-Verlag, 2002.

[16] Kristensen, L.M., Mailund, T.: Path Finding with the Sweep-Line Method using External Storage. Submitted to International Formal Methods Europe Symposium, March 2003.

[17] Kristensen, L.M., Mitchell, B., Zhang, L., Billington, J.: Modelling and Initial Analysis of Operational Planning Processes using Coloured Petri Nets. In Proceedings of Workshop on Formal Methods Applied to Defence Systems, pp.105-114, Volume 12 of Conferences in Research and Practice in Information Technology, Australian Computer Society, 2002.

[18] Lindstrøm, B.: Facilitating the Practical Use of Coloured Petri Nets. Ph.D. thesis, Department of Computer Science, University of Aarhus, Denmark, July 2002.

[19] Lindstrøm, B., Wagenhals, L.W.: Operational Planning using Web-Based Interfaces to a Coloured Petri Net Simulator of Influence Nets. In C. Lakos, R. Esser, L. Kristensen, and J. Billington (Eds.): Formal Methods in Software Engineering and Defence Systems 2002. Vol. 12 of Conferences in Research and Practice in Information Technology, pp. 115-124. Australian Computer Society, June 2002.

[20] Lindstrøm, B., Wells, L.: Annotating 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 28-30, Aarhus, Denmark. Dept. of Computer Science, University of Aarhus: pp. 39-58, 2002.

[21] Lindstrøm, B., Wells, L.: Towards a Monitoring Framework for Discrete-Event System Simulations. In M. Silva, A. Giva, and J.M. Colom (Eds.): Proceedings of the 6th International Workshop on Discrete Event Systems (WODES'02). October 2-4, Zaragoza, Spain. IEEE Computer Society: pp. 127-134, 2002.

[22] Lorentsen, L.: Coloured Petri Nets and State Space Generation with the Symmetry Method In K. Jensen, editor, Proceedings of the 4th Workshop on Practical Use of Coloured Petri Nets and the CPN Tools, Dept. of Computer Science, University of Aarhus, 2002.

[23] Lorentsen, L., Tuovinen, A-P., Xu, J.: Modelling Features and Feature Interactions of Nokia Mobile Phones Using Coloured Petri Nets. In J. Esparza and C. Lakos, editors, Proceedings of the 23rd International Conference on Application and Theory of Petri Nets (ICATPN'2002), Volume 2360 of Lecture Notes in Computer Science, Springer-Verlag, 2002.

[24] Lorentsen, L., Tuovinen, A-P., Xu, J.: Capturing Feature Interaction Patterns with Coloured Petri Nets. In Acta Cybernetica 15 (2002) 621-632, on December 5, 2002.

[25] Mailund, T.: Analysing Infinite-State Systems by Combining Equivalence Reduction and the Sweep-Line Method. Proceedings of International Conference on Application and Theory of Petri Nets (ICATPN 2002). Volume 2360 of Lecture Notes in Computer Science pp. 314-333, Springer-Verlag.

[26] Ouyang, C., Billington, J., Kristensen, L.M.: An Assessment of the Internet Open Trading Protocol. Submitted to Journal of Electronic Commerce Research (JECR), February 2003.

[27] Ouyang, C., Kristensen, L.M., Billington, J.: A Formal Service Specification for the Internet Open Trading Protocol. In Proceedings of the 23rd International Conference on Application and Theory of Petri Nets (ICATPN'2002). Volume 2360 of Lecture Notes in Computer Science, pp. 352-373. Springer-Verlag, 2002.

[28] Ouyang, C., Kristensen, L.M., Billington, J.: A Formal and Executable Specification of the Internet Open Trading Protocol. In Proceedings of the 3rd International Conference on Electronic Commerce and Web Technologies. Vol. 2455 of Lecture Notes in Computer Science, pp. 377-387, Springer-Verlag, 2002.

[29] Petrucci, L., Billington, J., Kristensen, L.M., Qureshi, Z.H.: Developing a Formal Specification for the Mission Systems of a Maritime Surveillance Aircraft. Proceedings of Third International Conference on Application of Concurrency to System Design. IEEE Computer Society, 2003. To appear.

[30] Petrucci, L., Kristensen, L.M., Billington, J., Qureshi, Z.: Towards Formal Specification and Analysis of Avionics Mission System. In Proceedings of Workshop on Formal Methods Applied to Defence Systems, pp. 95-104, Volume 12 of Conferences in Research and Practice in Information Technology, Australian Computer Society, 2002.

[31] Ratzer, A.V., Wells, L., Lassen, H.M., Laursen, M., Qvortrup, J.F., Stissing, M.S., Westergaard, M., Christensen, S., Jensen, K.: CPN Tools for Editing, Simulating, and Analysing Coloured Petri Nets. In Proceedings of the 24th International Conference on the Application and Theory of Petri Nets (ICATPN 2003). Lecture Notes in Computer Science, Springer-Verlag, 2003. To appear.

[32] Wells, L.: Performance Analysis Using Coloured Petri Nets. In A. Boukerche, S.K. Das, and S. Majumdar (Eds.): Proceedings of the Tenth IEEE International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS'02). IEEE Computer Society: pp. 217-221, 2002.

[33] Wells, L.: Performance Analysis using Coloured Petri Nets. Ph.D. thesis, Department of Computer Science, University of Aarhus, Denmark, July 2002.

[34] Westergaard, M: Supporting Multiple Pointing Devices in Microsoft Windows. In Proceedings of Summer Research Workshop 2002, 2002.

[35] Zhang, L., Kristensen, L.M., Janczura, C., Gallasch, G., Billington, J.: A Coloured Petri Net based Tool for Course of Action Development and Analysis. In Proceedings of Workshop on Formal Methods Applied to Defence Systems, pp. 125-134, Volume 12 of Conferences in Research and Practice in Information Technology, Australian Computer Society, 2002.