All posts by Einar Broch Johnsen

Modeling Deployment Decisions for Elastic Services with ABS

White Paper Summary

The use of cloud technology can offer significant savings for the deployment of services, provided that the service is able to make efficient use of the available virtual resources to meet service-level requirements. To avoid software designs that scale poorly, it is important to make deployment decisions for the service at design time, early in the development of the service itself. ABS offers a formal, model-based approach which integrates the design of services with the modeling of deployment decisions. In this paper, we illustrate the main concepts of this approach by modeling a scalable pool of workers with an auto-scaling strategy and by using the model to compare deployment decisions with respect to client traffic with peak loads.

PDF
Download a pdf of this white paper here.

 

Questionnaire
We would appreciate your feedback on this white paper.


Continue reading

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.

PDF
Download a pdf of this white paper here.

 

Questionnaire
We would appreciate your feedback on this white paper.

 
Continue reading

Envisage @ Cloudscape 2016

Envisage: Simulating the Cost of Cloud Deployment

Cloudscape2016_claim

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 with Envisage

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

Envisage @ ISoLA 2014

Envisage organized a track at ISoLA 2014 on Engineering Virtualized Services. The event took place in the Hotel Imperial, Corfu, Greece on Wednesday, October 8, 2014.

Abstract

Virtualized computing services, such as cloud services, create new opportunities, but also pose new challenges for users and providers alike. Over-provisioning of resources and compensative penalties for breaching an SLA are among the only too real downsides of virtualization. At the same time, formal models of software services and advanced static analysis tools promise vast improvements of productivity and cost effectiveness in cloud computing. This track explores the state-of-art in modeling of services deployed on the cloud and in the formalization as well as verification of SLAs.

Continue reading