On B and Event-B: Principles, Success and Challenges: Jean-Raymond Abrial, Marseille, France
Abstract
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.
Bio
Jean-Raymond Abrial is the co-inventor of various formal method approaches: Z, B and Event-B. He is the author of the "B-book" (CUP 1996), which presents the B-Method and "Modeling in Event-B: System and Software Engineering" (CUP 2010). He was a guest Professor at ETH Zurich from 2004 to 2009 where he led the team developing the Rodin Platform tool for Event-B (funded by the European RODIN and DEPLOY Projects). He is frequently invited to China giving formal method courses in various Chinese Universities (Peking University in Beijing, East China Normal University in Shanghai). Before being in Zurich, he was a consultant for more than 20 years working in close contact with industrial companies but also with various universities around the world .
Formal Methods Considered Normal: Janet Barnes and Angela Wallenburg, Altran, UK
Abstract
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).
Bio
Janet Barnes and Angela Wallenburg are both Principal Engineers at Altran, Bath, UK, a software house that specializes in the design and implementation of safety and security critical systems.
Dr Janet Barnes has been involved in the development of high integrity software for critical systems with Altran for over 20 years. During her time with Altran she has specialised in early lifecycle activities, with an emphasis on using formal techniques to produce unambiguous specifications of systems. Highlights of her career include her involvement in the development of Altran's largest Z specification and being a key contributor to the Tokeneer project authoring the specification and functional design in Z. Janet was a recipient the Microsoft Verified Software Award in 2011 recognising the contribution of the Tokeneer Project to the Verified Software Initiative of the use of formal techniques to develop software cost effectively.
Angela Wallenburg has worked on specification technologies and software verification tool building for the last 15 years. She has contributed mostly to behavioural interface specification languages and their associated static verifiers, for the languages Java, C# and Ada (KeY, Spec# and SPARK). Angela joined Altran and the SPARK team in 2009. She is experienced in successfully applying cutting edge research to industrial problems, and also a frequent trainer in and promoter of industrial use of formal methods. Angela has intermittently used ABZ languages throughout her career and recently turned her full attention to improving their usage and tooling at Altran.
How Bugs Led Us Astray: Daniel Jackson, Massachusetts Institute of Technology
Abstract
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.
Bio
Daniel Jackson is Professor of Computer Science at MIT, a MacVicar teaching fellow, and Associate Director of the Computer Science and Artificial Intelligence Laboratory, MIT’s largest laboratory. He is the lead designer of the Alloy modeling language and author of Software Abstractions: Logic, Language, and Analysis (MIT Press, 2nd ed., 2012). He was chair of the National Academies study Software for Dependable Systems: Sufficient Evidence? (2007). His research currently focuses on a new approach to software design, on new programming paradigms, and on cybersecurity.
Distributed Adaptive Systems -- Theory, Specification, Reasoning: Klaus-Dieter Schewe, Software Competence Centre Hagenberg, Austria
Abstract
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.
Bio
Klaus-Dieter Schewe has worked in group representation theory, software engineering, knowledge representation, database theory and rigorous methods, bringing these diverse fields together. His particular interest is on mathematical and logical foundations, semantics and expressiveness. He investigated methods for consistency enforcement, contributed to many results in dependency theory for complex-value databases (together with Sali, Link and Hartmann), developed a thorough methodology for the design and development of web information systems (together with Thalheim), created a client-centric middleware for cloud computing (together with Bosa and others), and developed a theory of knowledge patterns for entity resolution (together with Qing Wang). He recently developed behavioural theories for unbounded parallel and reflective algorithms (together with Ferrarotti, Wang and Tec) and for concurrent systems (together with Börger), with which he contributed to the foundations of rigorous methods. He graduated in Pure Mathematics at University of Bonn, received a Ph.D. from University of Bonn in Mathematics, and later received his D.Sc. from Brandenburg Technical University in Theoretical Computer Science. He was Chair of Information Systems at Massey University and Director of the Information Science Research Centre in New Zealand, and Scientific Director of the Software Competence Center Hagenberg in Austria.