Einar Broch Johnsen gave a talk on Designing Resource-Aware Applications for the Cloud with ABS at the 1st International Workshop on Formal Methods for and on the Cloud (iFMCloud 2016), co-located with the 12th International Conference on integrated Formal Methods (iFM 2016) in Reykjavik, Iceland. The slide set is available from SlideShare.
Our approach to predicting deployment on the cloud using ABS and formal methods, as developed in the Envisage project, was presented at the kick-off event of the Sirius Center for Research-driven Innovation on Scalable Data Access on May 19, 2016.
Envisage will attend Net Futures 2016 in Brussels 20-21 April 2016.
There will be an Envisage demo in the booth of the
Cluster on Software Engineering for Services and Applications.
Hope to see you there!
Envisage: Simulating the Cost of Cloud Deployment
- 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.
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.
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.
This blog post describes the IT infrastructure used for running the EU FP7 project Envisage, an international research project involving 8 partner sites across Europe. We describe the chosen project setup (mostly software) used for Envisage, report on our experiences with this setup, and discuss what is working and what is not working so well.
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
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. Continue reading