We developed a tool for the static verification task associated to the work in secondment 67. We developed an efficient two phase procedure for evaluating quantitative SLA based on an existing approach to the analysis of hybrid systems’ specification and verification, integrating SMT-solving with convex constraints, under the name of SMC – Satisfiability Modulo Convex Optimization. The analysis technique relays on SMC but is adapted to profit from the fact that contracts (both provision Pr and requirement Rq) can be minimised in a preprocessing phase, referred to as Minimisation through Convex Optimisation – MCO, when the service is registered in the repository. Results show that such preprocessing produces an efficiency gain when Pr ⊢ Rq is checked to evaluate if an SLA is met. Moreover, as finding the minimum size contract requires, at least, enumerating all boolean assignments satisfying a SAT problem, we developed the tool in a way that contract minimisation can be performed as semantics preserving incremental partial minimizations.
Task T.4.3 states that techniques, algorithms, and methodologies developed in WP2 will be turned into effective tools. As we mentioned before, the core activity of the secondment was devoted to the final stage of the implementation of analysis mechanisms for determining QoS SLA between an executing software system and a service. We not only developed a tool capable of performing such analysis but also performed an empirical study of its performance supporting its applicability.
The tool for QoS SLA determination was developed and empirical evaluated; results were published as “Automating Quality-of-Service evaluation in Service-Oriented Computing” on Coordination Models and Languages – 21th IFIP WG 6.1 International Conference, COORDINATION 2019.
Our ongoing work is devoted to the integration of this type of contracts and formal analysis to choreographic and orchestration mechanisms, aiming at the enrichment of the languages for describing API composition and their associated analysis procedures.
This secondment was related to Task T.4.3 – (O.4.2)