Converting from Service Level Agreement to Probabilistic Temporal Logic Specification
Nur Diana Madinah Ab Hadi1, Azlan Ismail2, Nur Syazleen Rosli3, Suzana Zambri4
1Nur Diana Madinah Ab Hadi, Faculty of Computer and Mathematical Sciences, Universiti Teknologi MARA (UiTM), 40450 Shah Alam, Selangor, Malaysia.
2Azlan Ismail, Faculty of Computer and Mathematical Sciences, Universiti Teknologi MARA (UiTM), 40450 Shah Alam, Selangor, Malaysia.
3Nur Syazleen Rosli, Faculty of Computer and Mathematical Sciences, Universiti Teknologi MARA (UiTM), 40450 Shah Alam, Selangor, Malaysia.
4Suzana Zambri, Faculty of Computer and Mathematical Sciences, Universiti Teknologi MARA (UiTM), 40450 Shah Alam, Selangor, Malaysia.
Manuscript received on 05 August 2019 | Revised Manuscript received on 09 August 2019 | Manuscript published on 30 August 2019 | PP: 3487-3493 | Volume-8 Issue-10, August 2019 | Retrieval Number: J97360881019/19©BEIESP | DOI: 10.35940/ijitee.J9736.0881019
Open Access | Ethics and Policies | Cite | Mendeley | Indexing and Abstracting
© The Authors. Blue Eyes Intelligence Engineering and Sciences Publication (BEIESP). This is an open access article under the CC-BY-NC-ND license (http://creativecommons.org/licenses/by-nc-nd/4.0/)
Abstract: 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.
Keywords: Software Conversion, Service Level Agreement, Probabilistic Temporal Logic, Quality of Service
Scope of the Article: Probabilistic Models and Methods