In this paper, we introduce a formal model of the availability, budget compliance and sustainability of istributed services, where service sustainability is a new concept which arises as the composition of service availability and budget compliance. The model formalizes a distributed platform for monitoring the above service characteristics in terms of a parallel composition of task automata, where dynamically generated tasks model asynchronous events with deadlines. The main result of this paper is a formal model to optimize and reason about service characteristics through monitoring. In particular, we use schedulability analysis of the underlying timed automata to optimize and guarantee service sustainability.
Additional Metadata
ACM Testing and Debugging (acm D.2.5), Concurrent Programming (acm D.1.3), Metrics (acm D.2.8)
THEME Software (theme 1)
Stakeholder Unspecified
Editor S. Dustdar , F. Leymann , M. Villari
Project Engineering Virtualized Services
Conference European Conference on Service-Oriented and Cloud Computing
Note Published paper: DOI: 10.1007/978-3-319-24072-5_9
Citation
Nobakht, B, de Gouw, C.P.T, & de Boer, F.S. (2015). Formal Verification of Service Level Agreements Through Distributed Monitoring. In S Dustdar, F Leymann, & M Villari (Eds.), .