| Popis: |
With the proliferation of ubiquitous computing devices and mobile internet, it is envisaged that future pervasive services will be increasingly large-scale and operate at an inter-organizational level. Designing and implementing pervasive services will therefore become a more complex and challenging task. Significant interest exists within the pervasive computing community for representing pervasive services at different stages of the software life cycle. While most of these efforts have focused on the detailed design or implementation of pervasive services little work has been done at the software architectural level. In this research, we propose a novel approach based on behavioral modeling and analysis techniques for representing pervasive software services and their compositions and verifying the process behavior of these models against specified system properties. This systematic, architecture-centric approach combines the benefits of principles such as UML, model transformation of Model Driven Architecture, and formal behavioural modeling and analysis techniques through model-checking, for engineering pervasive software services. In order to illustrate the validity and practical feasibility of the proposed approach we use an existing case study in transport and logistics. The approach will be evaluated to demonstrate the effectiveness of model-checking as a technique for verifying pervasive software services. |
