The expeditious development of technology in the past decades resulted in the introduction of concurrent systems that incorporate both ubiquitous and pervasive computing, the ambient systems. These systems are named after their ability to be completely embedded in the environment in which they operate and interact with the users, in a silent and non distracting way, facilitating the completion of their tasks. Hence, there is a growing need to introduce and develop formal techniques for computational models capable of faithfully modelling the behaviour of these systems. One way of capturing the intricate behaviours of the ambient systems is to use Petri nets, which are a modelling language that is used for the representation and analysis of concurrent systems. Within the domain of rigorous system design, verification of systems effectively checks and guarantees the correctness of the examined models with respect to the specification. This work investigates the modelling and the analysis of ambient systems using Petri nets. To examine the modelling of these systems, their taxonomy into Ambient Guidance Systems and Ambient Information Systems is carried out and a case study is used for the modelling of each category. To model ambient systems, the step-modelling approach and a variant class of Coloured Petri Nets, the Ambient Petri Nets (APNs), are introduced. Step modelling approach focuses on the interaction between the system and the user and Ambient Petri Nets is a class of nets with colour-sensitive inhibitor arcs that is used especially for the structural and behavioural representation of ambient systems. For the modelling of general ambient systems, the compositionality of the Ambient Petri Nets is used. To verify the correctness of the produced Ambient Petri Nets models, the introduction of the Transformed Ambient Petri Nets class that has no colour-sensitive inhibitor arcs is required since Charlie and generally most of the existing verification tools do not support the analysis of inhibitor nets. To address this problem, a construction is defined to translate the Ambient Petri Nets into Transformed Ambient Petri Nets. Afterwards, the Step Transition Systems are used to prove the behavioural equivalence of the nets that are associated through the construction. Subsequently, the Transformed Ambient Petri Nets models of the chosen case studies are verified against model checking and qualitative properties. For the first category, Computation Tree Logic (CTL) is used to check the models against important properties of the ambient systems that are related to their features and their general functioning. Finally, qualitative properties consider fundamental structural and behavioural properties of Petri nets that provide useful outcome about the systems under consideration.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:692663 |
| Date | January 2015 |
| Creators | Konios, Alexandros |
| Publisher | University of Newcastle upon Tyne |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
| Source | http://hdl.handle.net/10443/3054 |
Page generated in 0.0017 seconds