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

Context-Adaptive Task models are a state-of-the-art executablemodelling language to develop pervasive computingsystems. Although these models have proven to be successfulin the automation and support of user daily tasks, they donot provide a proper checking for ensuring the correctnessof the designed systems. In this paper, we investigate anddefine mappings to translate the task models into ColouredPetri Nets (CPN), a formalism that provides powerful techniquesfor simulation and verification. By using these mappings,task models can be translated to their equivalent CPnets, enabling that the system’s behaviour described in thetask models can be exhaustively checked at design time toensure a proper system execution at runtime