Correctness Checking of Pervasive Behaviour by Mapping Task Models to Petri Nets

  • Estefanía Serral KU Leuven
  • Johannes De Smedt KU Leuven
  • Jan Vanthienen KU Leuven


Context-Adaptive Task models are a state-of-the-art executable
modelling language to develop pervasive computing
systems. Although these models have proven to be successful
in the automation and support of user daily tasks, they do
not provide a proper checking for ensuring the correctness
of the designed systems. In this paper, we investigate and
define mappings to translate the task models into Coloured
Petri Nets (CPN), a formalism that provides powerful techniques
for simulation and verification. By using these mappings,
task models can be translated to their equivalent CP
nets, enabling that the system’s behaviour described in the
task models can be exhaustively checked at design time to
ensure a proper system execution at runtime.


Download data is not yet available.


1. J Baek Jorgensen and Claus Bossen. Executable use
cases: requirements for a pervasive health care system.
Software, IEEE, 21(2):34–41, 2004.

2. S Bartkeviˇcius, R Kragnys, and K ˇ Sarkauskas. Global
variables in colored petri nets. Electronics and Electrical
engineering: Signal Technology, (5):69, 2006.

3. Peter Dadam and Manfred Reichert. The adept project: a
decade of research and development for robust and
flexible process support. Computer Science-Research
and Development, 23(2):81–97, 2009.

4. E.Serral, P.Valderas, and V.Pelechano. Supporting
runtime system evolution to adapt to user behaviour. In
Proc. of CAiSE’10, pages 378–392, 2010.

5. Kurt Jensen. Coloured petri nets. Springer, 1987.

6. P. Johnson. Tasks and situations: considerations for
models and design principles in human computer
interaction. In HCI International, pages 1199–1204,
7. Seng W Loke, Sucha Smanchat, Sea Ling, Maria
Indrawan, et al. Formal mirror models: an approach to
just-in-time reasoning for device ecologies. Int. J. Smart
Home, 2(1):15–32, 2008.

8. Chun Ouyang, Eric Verbeek, Wil MP Van Der Aalst,
Stephan Breutel, Marlon Dumas, and Arthur HM
Ter Hofstede. Formal semantics and analysis of control
flow in ws-bpel. Science of Computer Programming,
67(2):162–198, 2007.

9. Fabio Paterno. ConcurTaskTrees: An Engineered
Approach to Model-based Design of Interactive Systems.

10. Mahadev Satyanarayanan. Pervasive computing: Vision
and challenges. Personal Communications, IEEE,
8(4):10–17, 2001.

11. E. Serral, P. Valderas, and V.Pelechano.
Context-adaptive coordination of pervasive services by
interpreting models during runtime. The Computer
Journal, 56(1):87–114, 2013.
12. Estefanıa Serral, Johannes De Smedt, and Jan
Vanthienen. Extending cpn tools with ontologies to
support the management of context-adaptive business
processes. In Data- and Artifact- Centric BPM
Workshop in BPM 2014, 2014.

13. Estefan´ıa Serral, Luca Sabatucci, Chiara Leonardi,
Pedro Valderas, Angelo Susi, Massimo Zancanaro, and
Vicente Pelechano. Incorporating users into ami system
design: From requirements toward automation. In ISD
2013, pages 499–511. 2013.

14. A. Shepherd. Hierarchical Task Analysis. Taylor &
Francis, London, 2001.

15. Tony Spiteri Staines. Intuitive mapping of uml 2 activity
diagrams into fundamental modeling concept petri net
diagrams and colored petri nets. In ECBS 2008, pages
191–200, 2008.
How to Cite
SERRAL, Estefanía; DE SMEDT, Johannes; VANTHIENEN, Jan. Correctness Checking of Pervasive Behaviour by Mapping Task Models to Petri Nets. International SERIES on Information Systems and Management in Creative eMedia (CreMedia), [S.l.], n. 2014/1, p. 11-18, feb. 2015. ISSN 2341-5576. Available at: <>. Date accessed: 23 feb. 2024.


Pervasive Computing; Task Models; Petri Nets; mappings
Share |