| This page has been archived; please check our new web-page to see if an updated version exists, and update your bookmarks and links. |
2 User Interfaces for Mobile Phones
2.1 Features
and Feature Interaction
3.1 The Sweep-Line State Space Method
3.2 Sweep-Line
Method for Timed CPN Models
3.3 Improved
Support for Symmetry Method
4 Tool Support for Coloured Petri Nets
4.4 Analysis of Simulation Results
4.5 Tool Support for State Space Analysis
5 Master's Thesis Projects in 2001
6 Plans for New Projects in 2002 and 2003
6.2 Development
of Communication Protocols
6.3 CPN
Models in UML-based Software Development
6.4 Cooperation
with Hewlett-Packard
8 Publications from CPN Centre in 2001
This report summarises the work in the CPN
Centre in year 2001. The CPN Centre (CIT partnership No. 202) was established
as a continuation of the HP-CPN Centre and has a staff of approximately 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:
·
·
·
·
Hewlett-Packard.
The MAFIA project (Modelling and Analysis
of Feature Interaction patterns in mobile phone software Architectures)
is a joint project between
The first phase of the MAFIA project ran from
November 2000 to November 2001 with a total size of 15 man-months. The project
group consisted of two people from
The project may be continued with one or more new
phases starting in 2002 or 2003.
Modern mobile phones provide an increasingly
complex and diverse set of features. Besides basic communication facilities
there is a growing demand for facilities for personal information management, data
transmission, entertainment, etc. To support flexibility and smooth operation,
the user interface (UI) of the mobile phone is designed to allow many features
to interplay and be active at the same time. The dependencies or interplay of
features are called feature interactions.
Prior to the MAFIA project, feature interactions were not systematically documented at Nokia. The description of feature interactions could only be found in the specification of the individual features. The most complex feature interactions were often not fully understood before implementation. This led to costly delays in the integration phase of a set of independently developed features. Therefore, a need for more focus on feature interactions were identified, and this motivated the MAFIA project. The main goals of the project were:
· To increase the focus on the role of feature interactions during design and software development.
· To identify and document typical patterns of feature interactions.
· To develop a systematic methodology for describing feature interactions.
· To provide an environment for interactive exploration and simulation of the feature interactions for demonstrational or analytical purposes.
One of the main activities in the MAFIA project was
to construct a quite complex CPN model. Feature interactions were investigated using
simulations of the CPN model. The CPN model was extended with domain specific
graphics which allowed UI designers and software developers who are not
familiar with Petri Nets to control and gain information from the simulations
without directly interacting with the underlying CP-net and its token game:
· The state of the phone was visualised via an animation of the display.
· The CPN model was extended with graphical feedback in the form of Message Sequence Charts (MSCs) which are similar to diagrams that are already in use in Nokia.
· The CPN model was extended with facilities for allowing the users to control the simulations via the mouse and keyboard (without seeing the underlying CPN model).
The CPN model is intended to be used in very different settings:
· UI designers can simulate the model without having any knowledge of CP‑nets. They get feedback by means of the animation of the phone display and MSCs (with detailed information about the flow of user interaction and snapshots of the phone display).
· Architectural designers view more detailed feedback about the states of the individual features and the messages being sent between them.
·
For people with knowledge of
CPN modelling, it is relatively easy to add new features and simulate these
together with the features already included in the model.
The MAFIA project created a common conceptual framework and terminology for analysing and describing feature interactions during UI design. The framework was proposed to the UI specification and design team in Nokia and has already been used in UI specification documents. The CPN model is currently maintained by Nokia project members with the technical support from the CPN group. The technology transfer to UI specifier and software development teams is still ongoing in Nokia.
Nokia is very interested in extending the project with one or more new phases starting late 2002 or 2003. The main research issues in the extension phases will be:
· detection of unknown and unpredicted feature interactions,
· integration of CPN Tools and CPN models with the current OO-development environment in Nokia.
Nokia is planning and negotiating with the CPN group about the work in the extension phase.
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 allows 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 2001 has primarily
focussed on the sweep-line state space method.
The sweep-line method is a novel state space
reduction method being proposed and developed by the CPN Centre. The
development of the sweep-line method was initiated in late 2000, and the development
has continued throughout 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. To conduct initial experiments with the sweep-line method, a
prototype tool has been implemented on top of the Design/CPN state space tool.
Early case studies have shown a reduction in memory usage in the order of 80-90
%, and a reduction in time in the order of 60-70 %.
A limitation of the basic sweep-line method is
that it is based on a strict 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-strict progress measures. The key
idea is to recognise, on-the-fly during the state space exploration, situations
where the strict 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 twice. The generalisation
significantly broadens the class of systems for which sweep-line methods can be
applied.
CPN models can be annotated with information to reflect the timing aspects of systems. This is based on the introduction of a global clock representing the current time in the modelled system. During the execution of the CPN model the clock increases monotonically, and hence it can be used as a progress measure for the sweep-line method.
Due to the absolute time values of the global clock, the state space of a timed CPN model usually becomes infinite. Some years ago, we developed a notion of equivalence for abstracting away the absolute time values – reducing the infinite state spaces of timed CPN models to finite state spaces. However, this factors out the global clock required for the sweep-line method, thereby making the two methods incompatible. To overcome this problem, we have developed a variant of the equivalence reduction method that does not compromise the progress property. This makes it possible to use the equivalence method and the sweep-line method together. The first practical experiments on a few case studies have showed significant savings in usage of both time and space.
The symmetry method is a state space reduction
method that exploits the symmetry found in many distributed and concurrent systems.
The basic idea is to factor out this symmetry, hereby obtaining a reduced state
space that is typically orders of magnitudes smaller than the corresponding
full state space. Until now, the construction of symmetry reduced state spaces
has required the user to implement (in Standard ML) an equivalence predicate to
determine whether two states are symmetric or not. Experience has shown that
this is a complex, error-prone, and time-consuming task. To overcome this
problem, improved tool support has been developed that allows the user to write
high-level symmetry specifications by annotating the colour sets of the CPN
model. The equivalence predicate is then automatically generated from this
high-level symmetry specification. This represents an important step towards
making the symmetry method fully automatic.
The aim of this project is 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 a couple of years 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 2002, CPN Tools are being used by more than 100 organisations in 35
countries and this figure is rapidly increasing. During 2002 we will make 2-3
new releases of the CPN Tools. The last of these is expected to be so stable
that it can be used for work in large 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
The user interface of the CPN Tools has been designed in close cooperation with leading researchers within the HCI field. 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 “pages”
that can be collected together into “binders”, making it easy to flip between
pages and 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 pages with the
left hand to find its destination. Another two-handed input technique consists
in moving a semi-transparent palette called a tool-glass 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.
The CPN Tools use a new simulation engine that is much faster than our old simulation engine. This is important, in particular 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.
The monitoring facilities provide means to observe ongoing simulations of a CPN model and 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 state is reached,
·
visualisation of behaviour using domain-specific graphics,
·
data collection for performance analysis,
·
communication with other processes,
·
use of 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.
Performance is often a central issue in the design, development, and configuration of systems. Support for collecting and analysis of data from simulations of CPN models has been integrated in 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.
The state space tool from Design/CPN has been
modified so that it now works on top of the new simulation engine mentioned
above. For the moment we are creating a user interface which will allow state
spaces to be constructed and analysed from CPN Tools. The work is expected to
be finished in the summer of 2002. It will give users of CPN Tools direct access
to state space analysis – for the moment they need to construct the model in
CPN Tools and then load it into Design/CPN to perform the state space analysis.
During 2001 the CPN Centre has been involved in the following thesis
projects:
Disk-Based Generation of State
Spaces
The thesis of Stefan Sørensen designs and implements 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.
Distributed State Space
Exploration
Farret Guillaume and Carre Guillaume are
exchange students from
On-the-fly LTL Model
Checking
The thesis of Anders M. Mikkelsen, has resulted in a prototype tool that allows system properties expressed in Linear Temporal Logic (LTL) to be checked on-the-fly during state space exploration in Design/CPN. On-the-fly and question-guided model checking can significantly reduce the time and memory required for verification as it allows the state space construction to be terminated as soon as the answer has been determined.
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.
Support for Design of
Interactive Multimedia Systems
The thesis of Jakob Færch investigates the use of formal models to support the decision making of multimedia designers. The thesis demonstrates how a class of interactive multimedia systems can be modelled and simulated in an easy and efficient way.
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.
We plan to continue the development of the sweep-line method:
· One area is the automatic identification of progress. Usually, it is easy for the user to find a suitable progress measure, and the validity of it can be verified automatically. However, it is still of interest to investigate how progress can be identified automatically by a computer tool. This will make the sweep-line method fully automatic to use.
· Another area is the generation of diagnostic information such as an error-trace showing why the system does not have a desired property. For traditional state space methods it is trivial to construct error-traces. With the sweep-line method it is much harder, since states are deleted from memory when they have been explored. The combination of the sweep-line method and disk-based storage seems to offer a promising solution to this problem.
We also plan to initiate the design and implementation of the next generation of CPN 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 means of state spaces 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.
We expect to start 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 is likely to be conducted in cooperation with Ericsson Telebit A/S which is a branch of Ericsson specialised in IP router technology, including routers for IPv6.
The Unified Modelling Language (UML) is today almost universally accepted by the software industry as the modelling language. UML is well-suited to model the static aspects of software systems. However, as it is currently standardised, the UML language is much weaker with respect to the modelling of behavioural aspects. Thus, for development of software components with complex behaviours, UML often cannot stand alone. In many cases, CPN models may be a viable supplement.
We
have started a project where we
explore combined use of UML and CPN in software
development, including:
·
Combined use of UML class diagrams and CPN models for consistent and coherent
design of both static and behavioural aspects of software systems and software
components.
·
Design-level testing using CPN.
·
Automatic code generation from CPN models.
·
Use of CPN in requirements specification (as an alternative to UML use cases).
There has been no direct cooperation with
Hewlett-Packard in 2001, and due to a number of reorganisations and changes of
business strategies, Hewlett Packard has decided to stop their grant to the CPN
Centre
The staff of the CPN
Centre is as follows:
·
Two
Research Managers: professor, Dr. Scient, Kurt Jensen,
and associate professor, PhD, Søren Christensen.
·
Three PostDocs: Kjeld Høyer
Mortensen, Lars M. Kristensen and Jens Bæk Jørgensen. Lars M. Kristensen
has spent the entire 2001 at the
·
Four
PhD students: Bo Lindstrøm, Louise Lorentsen, Thomas Mailund, and
Lisa M.Wells.
·
Eight
half-time student programmers: Mads Sig Ager Jensen, Henry Michael Lassen, Mads Laursen,
Jacob Frank Qvortrup, Martin Stig
Stissing, Stefan Sørensen, Troels Bjerre Sørensen, and Michael Westergaard.
·
Eight Master’s Thesis students: Jakob
Færch, Carré Guillaume, Farret Guillaume, René M.
Jensen, Anders M. Mikkelsen, Lone H. Olsen, Stefan Sørensen, and Jonas M. Thomsen.
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.
[1]
Beaudouin-Lafon, M., Mackay,
P. Andersen, W.E., Janecek, P., Jensen, M., Lassen, M.,
[2]
Beaudouin-Lafon, M., Mackay,
W.E., Andersen, P., Janecek, P., Jensen, M., Lassen, M.,
[3]
Christensen, S., Jensen, K., Mailund, T.:
State Space Methods for Timed Petri Nets.
In: H. Weber, H. Ehrig and W. Reisig: In Proceedings of 2nd International
Colloquium on Petri Net Technologies for Modelling Communication Based Systems,
Berlin, Germany, September 14-15, 2001, 33-42.
[4]
Christensen, S., Kristensen, L.M., Mailund, T.:
A Sweep-Line Method for State Space
Exploration. In Proceedings
of Tools and Algorithms for the Construction and Analysis of Systems (TACAS
2001). Genova
[5]
Christensen, S., Kristensen, L.M., Mailund, T.:
Condensed State Spaces for Timed Petri
Nets. J-M Colom, M. Koutny (eds.): Application and Theory of Petri Nets
2001. Proceedings of the 22nd International Petri Net Conference (ICATPN'2001).
[6]
Gallasch, G., Kristensen, L.M.:
Comms/CPN: A Communication Infrastructure
for External Communication with Design/CPN. In Proceedings of 3rd Workshop
and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools
(CPN'01), pp. 79-93. DAIMI PB-554, Department of Computer Science,
[7]
Gordon, S., Kristensen, L.M., Billington, J.: An Approach to Generalising the State Space
of a Distributed Missile Simulator. In Proceedings of 11th Annual
International Symposium on System Engineering (INCOSE'2001).
[8]
Gorden, S., Kristensen, L.M., Billington, J.: Verification of a Revised WAP Transaction
Protocol. Accepted for publication in J. Esparza, C. Lakos
(eds.): Application and Theory of Petri Nets 2002. Proceedings of the 23nd
International Petri Net Conference (ICATPN'2002),
[9]
Jensen K. (ed.): Third
Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN
Tools. Proceedings. Department of Computer Science,
[10]
Jensen K. (ed.): Special
Section on Practical Use of High-level Petri Nets. Int. Journal on Software
Tools for Technology Transfer,3/4 (2001), Springer Verlag, 369-430.
[11]
Kristensen, L.M.: Exploiting
Place Invariants in Condensed State Space Construction for Coloured Petri Nets.
In Proceedings of International Conference on Parallel Processing Techniques
and Applications (PDPTA'2001). pp. 661-667, Vol II, CSREA Press 2001.
[12]
Lindstrøm, B.: Web-Based
Interfaces for Simulation of Coloured Petri Net Models. In K. Jensen (ed.):
Special Section on Practical Use of High-level Petri Nets. Int. Journal on
Software Tools for Technology Transfer 3/4 (2001), Springer-Verlag, pp.
405-416, 2001.
[13]
Lorentsen, L., Kristensen, L.M.: Exploiting Stabilizers and Parallelism in State Space Generation with
the Symmetry Method. In Proceedings of the Second Internationel conference
on Application of Concurrency to System Design (ICACSD'01), 211-220, IEEE 2001.
[14]
Lorentsen, L., Tuovinen, A-P., Xu, J.:
Modelling Feature Interaction Patterns in
Nokia Mobile Phones using Coloured Petri Nets and Design/CPN. In K.Jensen,
(ed.), Proceedings of the third workshop on practical use of Coloured Petri
Nets and the CPN Tools, August 2001.
[15]
Lorentsen, L., Tuovinen, A-P., Xu, J.:
Modelling Feature Interactions in Mobile
Phones. ECOOP 2001 Workshop: Feature Interaction in Composed Systems,
[16]
Lorentsen, L., Tuovinen, A-P., Xu, J.:
Capturing Feature Interaction Patterns
with Coloured Petri Nets. Seventh Symposium on Programming Languages and
Software Tools (SPLST'2001),
[17]
Mortensen, K.H.: Efficient
Data-Structures and Algorithms for a Coloured Petri Nets Simulator. In:
Kurt Jensen (Ed.): 3rd Workshop and Tutorial on Practical Use of Coloured Petri
Nets and the CPN Tools (CPN'01), pp. 57-74. DAIMI PB-554, University of Aarhus,
August 2001.
[18]
Ouyang, C., Kristensen,
L.M., Billington, J.: A Formel Service
Specification for the Internet Open Trading Protocol. Accepted for
publication in J. Esparza,
C. Lakos (eds.): Application and Theory of Petri Nets
2002. Proceedings of the 23nd International Petri Net Conference (ICATPN'2002),
[19]
Ouyang, C., Kristensen, L.M., Billington, J.: Towards Modelling and Analysis of the
Internet Open Trading Protocol Transactions Using Coloured Petri Nets. In
Proceedings of 11th Annual International Symposium on System Engineering
(INCOSE'2001).
[20]
Ouyang, C., Kristensen, L.M., Billington, J.: An Improved Architectural Specification of
the Internet Open Trading Protocol Transactions. In Proceedings of 3rd
Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools
(CPN'01), pp. 119-137. DAIMI PB-554, Department of Computer Science,
[21]
Qureshi, Z., Billington, J.,
Kristensen, L.M.: Modelling
Military Airborne
[22]
Wells, L., Christensen, S., Kristensen, L.M., Mortensen K.: Simulation Based Performance Analysis of
Webs Servers. In R. German and B. Haverkort (eds.) Proceedings of the 9th
International Workshop on Petri Nets and Performance Models, IEEE, September
2001, pp. 59-68.
[23]
Zhang, L., Kristensen, L.M., Falzon, L., Davies, M., Mitchell,
B., Billington, J.: Model-based Operational Planning using Coloured Petri Nets. In
Proceedings og 6th International Command and Control Research and Technology
Symposium (CCRTS), 2001.