Converting from service level agreement to probabilistic temporal logic specification

Citations of this article
Mendeley users who have this article in their library.
Get full text


The need for conversion method exists due to the limitation of manual conversion at design time whenever the interested party must perform some assessments using an existing model checker tool. Manual conversion of the related requirements into the respective specification language is time-consuming especially when the person has limited knowledge and need to do the task repetitively with a different set of Service Level Agreement (SLA) configurations. This paper aims to address the need to automatically capture non-functional requirements specified in the SLA, namely, Service Level Objectives (SLO) and converting them into a specific probabilistic temporal logic specification. We tackle this problem by proposing a conversion method that utilizes a rule-based and template-based approach. The conversion method automatically extracts the required information in SLA based on certain rules and uses the extracted information to replace the elements in the prepared template. We focus on WS-Agreement language for SLA and probabilistic alternating-time temporal logic with rewards specification (rPATL) for the properties specification used in PRISM-games model checker tool. We then implement an initial proof-of concept of a conversion method to illustrate the applicability of translating between targeted specifications.




Hadi, N. D. M. A., Ismail, A., Rosli, N. S., & Zambri, S. (2019). Converting from service level agreement to probabilistic temporal logic specification. International Journal of Innovative Technology and Exploring Engineering, 8(10), 3487–3493.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free