Analysis of SLA Compliance in the Cloud: An Automated, Model-based Approach

White Paper Summary

This blog post contains a white paper and a questionnaire. The white paper explains how formal models combined with static analysis tools and generated runtime monitors enable SLA-aware deployment of services on the cloud. The proposed approach fits well with a DevOps methodology.

Download a pdf of this white paper here.


We would appreciate your feedback on this white paper.

Continue reading

Envisage @ Cloudscape 2016

Envisage: Simulating the Cost of Cloud Deployment


Make sure to catch the Envisage demo if you are going to Cloudscape 2016 in Brussels:

  • 8 March 15:45-16:15 Mobile Screen S.6 (live)
  • 9 March 11:45-12:15 Mobile Screen S.7 (live)

When system design does not take deployment architectures and costs into account, the savings of cloud computing are difficult to realize. The ENVISAGE project develops formal behavioral models that integrate data modeling, control flow, resource usage, and static and dynamic deployment and scaling decisions. Static analysis methods help with establishing confidence and calculating worst-case cost; simulation and visualization tools enable gaining insights into whole-system behavior already during the modeling and design phase.

Finding the bug in TimSort (Video)

Stijn de Gouw gave a presentation of his work on deductive software verification with KeY to discover the TimSort bug at Trondheim Developer Conference 2015. The details of this work have previously been presented as a blogpost on this website and as a scientific paper at CAV 2015. The guys over at TDC2015 recorded Stijn’s presentation and put it on Vimeo, so you can now watch Stijn discuss this work.

Stijn de Gouw – BUG IN TIMSORT from TrondheimDC on Vimeo.

Resource-Aware Applications with ABS

Designing Resource-Aware Cloud Applications

Realizing the full potential of virtualized computation—the cloud—requires rethinking software development. Deployment decisions, and their validation, can and should be moved up the development chain into the design phase.

The elasticity of software executed in the cloud gives designers control over the execution environment’s resource parameters, such as the number and kind of processors, memory, storage capacity, and bandwidth. Parameters can even be changed dynamically at run time. Thus, cloud-service clients can not only deploy and run software, but they can also fully control the tradeoffs between incurred costs to run the software and the quality of service (QoS) delivered.

Continue reading

KeY: Deductive Verification of Software

This is a follow-up post to the blog about the verification of TimSort. Many people have asked how KeY actually works and which resources are available. In this brief post we answer some of the questions about KeY that came up in the discussions. We also provide pointers to documentation, case studies and technical papers.

The KeY project was started in the late 1990s at University of Karlsruhe (now: Karlsruhe Institute of Technology) with the aim to develop a tool for formal specification and verification of Java that would be useful not only to the formal methods specialist, but for ordinary software developers as well. This was an ambitious and long-term goal. After more than 15 years of research and tool development, it has been partially reached, as we explain below. For example, KeY not only includes a formal verification tool, but also a debugger with novel features and an automated test case generator. In the meantime, KeY is developed and maintained at three sites. In addition to Karlsruhe, these are Technische Universität Darmstadt and Chalmers University of Technology.

The core of KeY is a software verification tool based on symbolic execution and invariant reasoning. Continue reading