Category Archives: Envisage

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

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

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

Proving that Android’s, Java’s and Python’s sorting algorithm is broken (and showing how to fix it)

Tim Peters developed the Timsort hybrid sorting algorithm in 2002. It is a clever combination of ideas from merge sort and insertion sort, and designed to perform well on real world data. TimSort was first developed for Python, but later ported to Java (where it appears as java.util.Collections.sort and java.util.Arrays.sort) by Joshua Bloch (the designer of Java Collections who also pointed out that most binary search algorithms were broken). TimSort  is today used as the default sorting algorithm for Android SDK, Sun’s JDK and OpenJDK. Given the popularity of these platforms this means that the number of computers, cloud services and mobile phones that use TimSort for sorting is well into the billions.

Fast forward to 2015. After we had successfully verified Counting and Radix sort implementations in Java (J. Autom. Reasoning 53(2), 129-139) with a formal verification tool called KeY, we were looking for a new challenge.  TimSort seemed to fit the bill, as it is rather complex and widely used. Unfortunately, we weren’t able to prove its correctness. A closer analysis showed that this was, quite simply, because TimSort was broken and our theoretical considerations finally led us to a path towards finding the bug (interestingly, that bug appears already in the Python implementation). This blog post shows how we did it.

The paper with the complete analysis, and several test programs are available on our website.

Update (August 2017): The KIT group used KeY to verify the JDK’s dual pivot quicksort implementation used as default sorting algorithm for integer or long arrays. TimSort is the default for arrays of reference type. Continue reading

Envisage Industrial Case Study – Cloud-Supported Large-Scale Offline Search for Mobile Devices

The Envisage project has 3 different industrial case studies, this blog post provides a brief overview of one of them – large-scale offline search for mobile and wearable devices (inspired by Hitchhiker’s Guide to the Galaxy), followed by a repost of the feasibility of doing large-scale offline search on mobile devices.

Continue reading