Service composition testing and verification

点击翻译按钮获取中文摘要

Service composition is a key technology for developing modern applications and integrating complex systems. Composite services are designed to provide integrated functionalities that a single service cannot offer. The main challenge is to guarantee that the composition satisfies key properties such as correctness, reliability, robustness and timeliness at the design and runtime stages. Throughout the proposed research program, we plan to address three complementary research problems. The first problem is about the specification and static verification of agent-based service composition involving real-time requirements. The following challenges are yet to be addressed: i) developing an expressive formal language that allows the specification of real-time properties and timed obligations, permissions, and constraints while considering the autonomy and flexibility of individual and composite services and the business logic of the underlying applications, and ii) developing the corresponding model-checking algorithm to address the issue of verifying the timed composition model against the desired requirements while considering the scalability of concrete business applications. The second problem is the runtime verification of timed and autonomous composition systems. Such compositions may exhibit unexpected behaviors and lead to violation of properties during execution. Compared to model checking, runtime verification is lightweight as it verifies only the actual execution or traces of the running system. This alleviates the state explosion problem but faces the efficiency in terms of execution time and resource sharing with the running system. In this context, the main challenges include the expressiveness of specification languages (like model checking), automatic synthesis of the monitor that represents the property to be verified, instrumentation of individual and composite services, and scalability in terms of the number of traces or executions to be analyzed. The third problem is runtime testing of contract-driven and autonomous service compositions. The three research issues are complementary as the adage says “verify what you can and test the rest”. Runtime testing can guide the composition of services and detect faults and violation of properties. It has an observer, like the monitor, and can inject inputs to stimulate the behavior. Runtime testing uses an oracle to analyze the observed traces and needs to be done before the execution of the same component, which requires to check the readiness of part of the code/ component to be able to isolate it, inject inputs, collect the output, and based on the trace analysis, release the component or halt the composition. Further actions might be required such as repair and redo, and can be applied following a detection of faults or violations.