Lightweight Mobile Service Creation Models, Approaches, And Formal Verification

Owing to the popularity of wireless network and mobile terminals,mobile services have been widely used in people's daily life, such as Online Meal Ordering app and Smart Parking Lot app. Especially, with the advances in mobile technology, more and more powerful applications are provided for mobile devices that attract more users into mobile community. This phenomenon leads to the "longtail requirements"(i.e.personalized requirements) of mobile applications. However, many userscannot often find appropriate apps from the app market to meet their personalized needs. Service mashup development provides an effective solution to deal with the personalized application requirements. It enables end-users who are non-professional programmers to rapidly develop applications according to their requirements. Mashup development is becoming one of the hot topics in both mobile computing and service-based software development. However, existing mashup approaches not only require users that develop applications equipped with more or less programming skills, but also focus on the type-specific mobile applications. Moreover, these approaches have no guarantee mechanism for the development process. In this thesis, we propose an end-user-oriented lightweight service creation approach for developing mobile applications.The main research contents and contributions of this thesis can be summarized as follows:(1) We propose a model-driven mobile application framework,called MobiMVL. To ensure the completeness of application architecture, MobiMVL introduces a ternary paradigm for mobile applications, including unified service model, business logic model and GUI model. These models of MobiMVL formalize respectively the application's component domain, business logics, and graphical interface together with application behavior. Each element of MobiMVL is implemented independently through a model-driven development process. For component domain, we propose a unified service data model(SDM) that can be used for repackaging heterogeneous services in a unified way. To facilitate service providers to access heterogeneous Web services into our platform,we also implement two service templates of SDM: IFrame template and Component template, which two implementations are respectively used for service development and service execution. For GUI, we propose a widget-based GUI model that can create user interface by WYSIWYG mode. To adapt different mobile platform,we propose an adaptive widget model for basic elements of GUI. For business logic, we propose a service relation model (SRM) for representation and refinement of data interaction between services,and the service process graph (SPG)for describing business logics of mashup applications. To adapt the dynamic application scenarios, we also construct an event-driven execution mechanism for SPG.MobiMVL introduces the idea of "Software as Services" so that it can create and supply mobile services systematically through lightweight software development approach. Based on MobiMVL,we implement an integrated development platform that includes three sub-systems: ServiceAccess, EasyApp and LSCE. These three tools can be used to design the three elements of MobiMVL respectively. Then, we introduce a development case of smart parking lot to validate the availability of MobiMVL framework and our platform. Finally, the feature capabilities of our platform are compared to other similar tools, and the end-user evaluation and performance evaluation are conducted to evaluate our platform.(2) We propose an incomplete information-oriented semi-automatic service mashup approach. In existing mashup approaches, the technical threshold and domain knowledge faced by end-users become obstacles to mashup development. We present an assisted approach for service mashup using AI planning techniques. The feature of this approach is that the mashup service can be created automatically without end-user participating in specific development.In this approach, an enhanced service semantics model is presented based on incomplete information, a dataflow-based mashup model is presented as the basic unit of service interaction, and the service mashup is transformed into a planning problem using K planning to support incomplete and nondeterministic planning. An integrated mashup system is implemented through development and integration of two sub-systems, namely ICP4SM and LSCE. ICP4SM is a flexible planning system used to automatically provide solutions for mashup problem by invoking DLVk planner. LSCE is responsible for further processing of returned solutions by end-users. A case study is presented to illustrate the mashup development using the integrated mashup system; meanwhile, the system performance and effectiveness are also evaluated in terms of concurrent planning and incomplete information planning.(3) We propose a model checking approach for behavioral compatibility analysis of service mashup. In existing mashup environment, end-users take charge of checking the behavioral compatibility of mashup services. Actually, because of the limited ability of end-users in both programming technique and domain knowledge, they cannot always find the mismatch of services'behavior. We present an automatic approach for analyzing the behavioral compatibility of service mashup with verification techniques of Communication Sequence Processes(CSP). The feature of this approach is that if a service process includes some incompatibilities, the counterexample would be returned to end-users to track the source of errors. In this approach, a service behavior model(SBM) is presented to facilitate the modeling of services with CSP, and an automatic modeling approach is presented for service processes through a modular way. Furthermore, two types of behavioral compatibility are introduced based on the development practice, and an automatic specification approach is presented for each type of compatibility properties. Finally, a case study is presented to analyze the behavioral compatibility based on our approach with PAT checker.