Formal Analysis And Verification Of Trustworthy Services In Pervasive Computing

As an emerging computing paradigm, pervasive computing generally envisionsan open, dynamic and heterogeneous environment. The typical environment is filledwith a variety of services provided by devices. These devices are often mobile andheterogeneous, and may operate with resource restrictions. Unfortunately, these char-acteristics make it difficult for programmers to rapidly develop a trustworthy pervasivesystem built upon these devices.In order to build trustworthy services in pervasive computing, this paper presentsa formal model of pervasive services and develops a formal language for describingfeatures of the services. Based on the language, a type and effect system is designedto extract dynamic behavior of a service-oriented pervasive application and analyzethe behavior-consistent service substitution. For verification of dynamic behaviors,we make use of model-checking technology to validate its correctness. Furthermore, aframework for dynamic service updates is proposed to support the dynamic evaluationof services in pervasive computing. We also formally model the framework and verifyits properties. Finally, we develop and implement a checking tool to assist program-mers. The typical scenario for pervasive applications is built in order to illustrate ourapproach, and experimental results show that the approach is effective and beneficialwhen applied to pervasive applications.The main contributions of this paper include:(1) To adapt to a dynamic and ever-changing environment, we propose a pervasiveservice model based on the generic and special features in pervasive computing. Com-pared with a typical service model, the pervasive service model has self-adaptabilityand can also be applicable to dynamic environments.(2) Service composition is an important technique which is used to build perva- sive systems. To guarantee valid dynamic behavior in the pervasive system, a staticapproach is proposed to formally analyze and verify behavior-consistent service sub-stitutions in dynamic environments. We first present a formal language to describe thebehavioral semantics of a service model. Next, we introduce a type and effect systemto automatically infer conservative approximations of all possible service behaviorrepresented by concurrent behavior expressions. Furthermore, subtyping technologyis used to analyze the type-based service substitutability and behavior-consistent ser-vice substitutions. We also mechanize the formalization and the proof of type safetyusing the Coq proof assistant. Finally, applications in Web services show that ourmethod is effective and feasible.(3) After extracting all dynamic behavior from the pervasive system using thetype and effect system, we transform the dynamic behavior into finite state machine.At the same time, the pervasive service is abstracted as a process model describedby Finite State Process (FSP) language. FSP can describe the behavior semanticsof pervasive services and then is automatically transformed into Labeled TranslationSystem (LTS) by a model-checking tool. Moreover, we use the tool to check whetherthe behavior properties of composite services comply with required policies or not.(4) The ability to dynamically change the behavior of an application is becomingan important issue in pervasive computing. Pervasive computing has highly dynamiccharacteristics which bring challenges to the rapid construction and regular mainte-nance of complex pervasive applications. Moreover, service providers need to contin-uously provide services, especially for mission-critical areas. A promising approachfor providing uninterrupted service is to permit dynamic updates while keeping ap-plications up-to-date. To solve the problem, we present a dynamic service updateframework to support transparent updates of running applications, and explain howthe framework achieves our requirements and goals, i.e. correctness, flexibility, andreal-time response. Furthermore, we propose a formal model for the framework toanalyze its correctness and verify its properties. Features of our approach are that itsupports dynamic interface adaptability if the interface type of an updated service hasbeen changed, and that it can automatically recover from update failures if the behav-ior of an updated application is unwanted. Experiments show that our approach iseffective and beneficial when applied to pervasive applications and the performance overhead is acceptable in relation to the advantages.(5) To illustrate how our approach is applied into pervasive computing, we imple-ment a typical pervasive application which is built on the OSGi service platform andR-OSGi middleware technology. Final results show that our approach is feasible andeffective when applied in pervasive computing.