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.
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 outcomes were showcased as part of the SIRIUS booth at the Subsea Valley Conference 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.
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.
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