Service composition testing and verification

服务组合是开发现代应用和集成复杂系统的关键技术。组合服务旨在提供单个服务无法提供的集成功能。主要的挑战是保证组合在设计和运行阶段满足诸如正确性、可靠性、健壮性和及时性等关键属性。在整个拟议的研究计划中，我们计划解决三个互补的研究问题。第一个问题是关于涉及实时需求的基于代理的服务组合的规范和静态验证。我们还需要应对以下挑战：1)开发一种表达性的正式语言，允许对实时属性和定时义务、权限和约束进行规范，同时考虑到单个和组合服务的自主性和灵活性以及底层应用程序的业务逻辑；ii)开发相应的模型检查算法，以解决在考虑具体业务应用程序的可扩展性的同时根据所需需求验证定时组合模型的问题。第二个问题是定时和自主组合系统的运行时验证。这样的组合可能会表现出意想不到的行为，并导致在执行期间违反属性。与模型检查相比，运行时验证是轻量级的，因为它只验证正在运行的系统的实际执行或跟踪。这缓解了状态爆炸问题，但在执行时间和与运行系统的资源共享方面面临效率问题。在这种情况下，主要的挑战包括规范语言的表达性（如模型检查）、表示要验证的属性的监视器的自动合成、单个和组合服务的工具化，以及要分析的跟踪或执行的数量方面的可伸缩性。第三个问题是契约驱动和自治服务组合的运行时测试。正如谚语所说，这三个研究问题是互补的，“验证你能验证的，测试其余的”。运行时测试可以指导服务的组合，检测故障和违反属性。它有一个观察者，就像监视器一样，可以注入输入来刺激行为。运行时测试使用oracle来分析观察到的跟踪，并且需要在执行相同组件之前完成，这需要检查代码/组件的准备情况，以便能够隔离它，注入输入，收集输出，并基于跟踪分析，释放组件或停止组合。可能需要进一步的操作，例如修复和重做，并且可以在检测到错误或违规之后应用。

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.