Service composition testing and verification

服务组合测试和验证

• 批准号: RGPIN-2018-06796
• 负责人: Dssouli, Rachida
• 金额: $ 2.04万
• 依托单位: Concordia University
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2020
• 资助国家: 加拿大
• 起止时间: 2020-01-01 至 2021-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=714449
• 关键词: Service; composition; testing; 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.

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