Paper Info
Title
Model Checking Aspectual Pervasive Software Services
Abstract
Context-dependent information is tightly coupling or crosscutting the core functionality of a service at the service interface level. This results in a complex design, which is difficult to implement and maintain. The crosscutting context-dependent functionality of interacting pervasive services can be modeled as aspect-oriented models in UML. However, this has two challenges: the semi-formal nature of UML notations, and the expressive power of aspects. This paper explores model checking as a solution for modeling aspectual pervasive software services and their compositions, and rigorously verifying the process behavior of these models against specified system properties. Model checking is applied, first to check the behavior of the individual pervasive aspects and components, and second to verify the overall behavior of the woven model even if no errors are found in the individual pervasive aspects and components. These verification stages have been used to gain confidence before the complex pervasive services are actually implemented. The approach is explored using a real-world case study in intelligent transport with more than 30 properties formalized to provide a comprehensive coverage of the system requirements. An evaluation framework has been established to validate the main methods and tools employed in the study.
Year
DOI
Venue
2011
10.1109/COMPSAC.2011.41
Computer Software and Applications Conference
Keywords
Field
DocType
model checking aspectual pervasive,process behavior,complex pervasive service,overall behavior,model checking,uml notation,pervasive service,software services,individual pervasive aspect,aspectual pervasive software service,aspect-oriented model,complex design,ubiquitous computing,context dependent,context model,service model,formal verification,expressive power,weaving,unified modeling language,context modeling
Notation,Model checking,Systems engineering,Unified Modeling Language,Computer science,Context model,Software,Ubiquitous computing,System requirements,Formal verification
Conference
Volume
ISSN
ISBN
0
0730-3157 E-ISBN : 978-0-7695-4439-7
978-0-7695-4439-7
Citations 
PageRank 
References 
0
0.34
9
Authors
2
Name
Order
Citations
PageRank
Dhaminda B. Abeywickrama1758.00
Sita Ramakrishnan25812.36