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

ABS Online: Formal Methods as a Service

All the tools developed in the Envisage project are available in the ABS Collaboratory. ABS supports the modeling of services and SLA for deployment on the cloud. The ABS tools are now online This enables you to try the modelling language and analysis tools as a service. Try the ABS Online Tools now!

The ABS online tools include simulation with visualization support, deadlock analysis, cost analysis, deployment synthesis, and test case generation (see http://abs-models.org/abs-tools).

The ABS language manual has been updated and made web-ready at http://docs.abs-models.org/.

The tools are open source. Source code for the tools is available at https://github.com/abstools/abstools.  The tools can be compiled and installed locally (also via Vagrant or docker).

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.