Using Kilim's Isolation Types for Multicore Efficiency
Alan Mycroft, Cambridge University
We identify a `memory isolation' property which enables multi-core programs to avoid slowdown due to cache contention. We give a tutorial on existing work on Kilim and its isolation-type system building bridges with both substructural types and memory isolation.
The Practical Application of Formal Methods:
Where is the Benefit for Industry?
James J. Hunt, aicas incorporated
Though the use of formal methods for software verification has progress tremendously in the last ten year, its take up in industry has been meager, but with the right emphasis this could change dramatically. Software certification standards have started to take formal methods seriously as an alternative to testing. By focusing on practical issues such as common specification languages, adaption to industrial processes for safety certification, scalability, training, and synergies between tools, common reservations about using formal methods could be lain to rest. This could help formal methods become the center of software engineering in the coming decade.
Local Reasoning for Verification of Object-based Programs Using First-order Assertions
Shared mutable objects pose challenges in reasoning, especially for
Modelling Distributed Adaptable Object Oriented Systems using HATS Approach:
A Fredhopper Case Study
Peter Wong, Fredhopper
The HATS project aims at developing a model-centric methodology for the design, the implementation and the verification of distributed, concurrent and highly configurable systems. Such systems also have high demands on their dependability and trustworthiness. The HATS approach is centered around the Abstract Behavioural Specification modelling language (ABS) and its accompanying tools suite. The HATS approach allows precisely specifying and analyzing the abstract behaviour of distributed software systems and their spatial and temporal variability. The HATS project measures its success by applying its framework not only to toy examples, but to real industrial scenarios.
In this talk, we consider the HATS approach for modelling an industrial scale case study provided by the eCommerce company Fredhopper. In this case study we consider Fredhopper Access Server (FAS). We show how to model the commonality and variability of FAS's replication system using ABS and discuss our experience.