Formal Modelling of an Adaptable Service System
Mazen Malek Shiaa, Finn Arve Aagesen, Cyril Carrez · 2006
Adaptable service systems are service systems that adapt dynamically to changes in both time and position related to users, nodes, capabilities, status, and changed service requirements. We present a formal model for the basic entity used for the implementation of the service functionality in the Telematics Architecture for Play-based Adaptable Service systems (TAPAS). This basic entity is the role-figure, which executes in the nodes of the network. The formal model is denoted as the role-figure model. It comprises behaviour specification, interfaces, capabilities, queue of messages, and executing methods for role-figures. Its semantics is based on an ODP (Open Distributed Processing) semantic model and rewriting logic, and is used to prove properties such as: plug ability, consumption ability, and play ability.