ABZ 2018 (Southampton, UK)

Our talk will focus on how we get more people "onboard the FM ship", that is "Formal Methods Considered Normal". Altran has had much success with SPARK, an FM now accepted as normal part of business at Altran. We will elaborate on what has worked and why. We continue to have more challenges with using Z (and similar ABZ languages). We believe that specification structuring is a major discriminating factor for industrial scale-up. We will give examples of structuring idioms that have been especially important for the largest formal specification written by Altran. Our perspective is that of long-term users of FM in all parts of the development life cycle. A significant challenge for us is training and recruiting of specification producers and we see this as requiring a community effort involving industry and academia. We also touch on some of our on-going work on extracting further benefits from FM including automatic natural language generation for improved communication about specifications with all stake holders, and generation of monitors for improved V&V automation (lower cost).

When the field of formal methods began, it had broad and noble goals. But somehow, over time, these goals were eclipsed by a more reductionist view. Nowadays, quality is measured by defect counts, and eliminating bugs has become the central focus of our field. In this talk, I'll explain how I think this came about, why it's insidious, and what we can do about it. My key observation will be that bugs are not the causes of problems but are instead symptoms. To improve our software---to make it more secure, safe and usable---we need to move from symptoms to diagnosis, to determine the underlying causes of poor software and fix those. I will argue that design is essential to achieving this, and that we need to reinvigorate design as a central activity in formal methods research and practice. I will give examples of designs, good and bad, drawn from my ongoing work on conceptual design of software.

After more than 20 years since the publication of my book on B, and almost 10 years since the publication of my book on Event-B, the aim of this talk is to present some key points about these technologies. The talk will cover the basic principles on which B and Event-B have been developed and look at differences and similarities between B and Event-B. It will also outline where B and Event-B are spread around the world. Finally, the talk will explore challenges with the industrial application of these technologies.

A distributed system can be characterised by autonomously acting agents, where each agent executes its own program, uses shared resources and communicates with the others, but otherwise is totally oblivious to the behaviour of the other agents. In a distributed adaptive system agents may change their programs, enter or leave the collection at any time thereby changing the behaviour of the overall system. The talk will start with the motivation of a language-independent axiomatic definition of distributed adaptive systems and then present concurrent reflective Abstract State Machines (crASMs), an abstract machine model for their specification. It can be proven that any system stipulated by the definition can be step-by-step simulated by a crASM. Based on the simple observation that concurrent ASMs can be mimicked by non-deterministic parallel ASMs the complete one-step logic for non-deterministic ASMs can be exploited for the definition of a logic capturing concurrency. By making the extra-logical rules in the logic subject to being interpreted in a state the logic can be extended to capture also reflection.