Néstor Cataño Collazos - Java Software Development with Event B

Java Software Development with Event B

A Practical Guide

Synthesis Lectures on Software Engineering

Editor

Luciano Baresi,Politecnico di Milano

The Synthesis Lectures on Software Engineering series publishes short books (75-125 pages) on conceiving, specifying, architecting, designing, implementing, managing, measuring, analyzing, validating, and verifying complex software systems. The goal is to provide both focused monographs on the different phases of the software process and detailed presentations of frontier topics. Premier software engineering conferences, such as ICSE, ESEC/FSE, and ASE will help shape the purview of the series and make it evolve.

Java Software Development with Event B: A Practical Guide

Nstor Catao Collazos

2020

Model-Driven Software Engineering in Practice: Second Edition

Marco Brambilla, Jordi Cabot, and Manuel Wimmer

2017

Testing iOS Apps with HadoopUnit: Rapid Distributed GUI Testing

Scott Tilley and Krissada Dechokul

2014

Hard Problems in Software Testing: Solutions Using Testing as a Service (TaaS)

Scott Tilley and Brianna Floss

2014

Model-Driven Software Engineering in Practice

Marco Brambilla, Jordi Cabot, and Manuel Wimmer

2012

Copyright 2020 by Morgan and Claypool

All rights reserved. No part of this publication may be reproduced, stored in a retrieval system, or transmitted in any form or by any meanselectronic, mechanical, photocopy, recording, or any other except for brief quotations in printed reviews, without the prior permission of the publisher.

Java Software Development with Event B: A Practical Guide

Nstor Catao Collazos

www.morganclaypool.com

ISBN: 9781681736877 paperback

ISBN: 9781681736884 ebook

ISBN: 9781681736891 hardcover

DOI 10.2200/S00957ED1V01Y201910SWE005

A Publication in the Morgan and Claypool Publishers series

SYNTHESIS LECTURES ON SOFTWARE ENGINEERING

Lecture #5

Series Editor: Luciano Baresi, Politecnico di Milano

Series ISSN2328-3319 Print2328-3327 Electronic

Java Software Development with Event B

A Practical Guide

Nstor Catao Collazos

Google, Inc.

SYNTHESIS LECTURES ON SOFTWARE ENGINEERING #5

ABSTRACT

The cost of fixing software design flaws after the completion of a software product is so high that it is vital to come up with ways to detect software design flaws in the early stages of software development, for instance, during the software requirements, the analysis activity, or during software design, before coding starts. It is not uncommon that software requirements are ambiguous or contradict each other. Ambiguity is exacerbated by the fact that software requirements are typically written in a natural language, which is not tied to any formal semantics. A palliative to the ambiguity of software requirements is to restrict their syntax to boilerplates, textual templates with placeholders. However, as informal requirements do not enjoy any particular semantics, no essential properties about them (or about the system they attempt to describe) can be proven easily. Formal methods are an alternative to address this problem. They offer a range of mathematical techniques and mathematical tools to validate software requirements in the early stages of software development. This book is a living proof of the use of formal methods to develop software. The particular formalisms that we use are EVENT B and refinement calculus. In short: (i) software requirements as written as User Stories; (ii) they are ported to formal specifications; (iii) they are refined as desired; (iv) they are implemented in the form of a prototype; and finally (v) they are tested for inconsistencies. If some unit-test fails, then informal as well as formal specifications of the software system are revisited and evolved.

This book presents a case study of software development of a chat system with EVENT B and a case study of formal proof of properties of a social network.

KEYWORDS

correct-by-construction, discrete mathematics, EVENT B, formal methods, Java, programming, refinement, software engineering, verification

Contents

Preface

This book is a discourse explaining the software engineering task by means of mathematics. The particular formalism that we use is called predicate calculus. The book starts by introducing predicate calculus objects such as relations and functions and all the underlying operations used to manipulate these objects, giving examples of how they can be composed together to model software. The fundamental reason of using mathematics, and, in particular, predicate calculus to model software is that it allows us to reason about the software we want to build; we are interested in being able to verify if the software we build adheres to certain properties, which are typically condensed in a software requirements document. This is not an easy task and the main motivation behind our actions is to build correct software, software that enjoys those properties described in the software requirements document.

Software testing has had a major impact on software development for the past decades. It has shaped the way people think about the task of software construction. People are not surprised to get to implement software that is infested with bugs. They expect that bugs will be decanted once the software implementation phase finishes. This book uses a different approach; our starting point is that we can and should write software that is correct from the very early stages of software development. Nonetheless, we use testing to animate the software and to check if its running behavior matches its expected behavior.

Our software construction return to mathematics is based on the idea of assigning meaning to software. The idea is to build software the same way that mathematical proofs are conducted, guaranteeing that software product lives up to some intended meaning. The particular mathematical formalism and language we have chosen is called EVENT B, which originated from the Z formalism. Although EVENT B shares essentially the same modeling language for stating state properties as Z, EVENT B and Z offer different modeling mechanisms that are specialized in distinct mathematical aspects. EVENT B and Z are both models for state transition systems. EVENT Bs language for expressing the dynamic behavior of state machines is based on events. On the other hand, Z uses a rich schema calculus mechanism for expressing the dynamic behavior of models. Z Schema calculus and EVENT B events coupled with model refinement are different mechanisms. Z also offers refinement, but in practice, Z focuses more on formal specification and EVENT B focuses more on model refinement and coding (whereas it is manually written or tool-generated). Another major difference between EVENT B and Z is in the undertaking and use of invariants. In EVENT B, each event definition produces proof obligations that attest to the correctness of machine invariants. These invariants might encode safety properties. On the other hand, in Z, invariants are incorporated into the model definitions, altering their meanings. They do not generate proof obligations.

The main motivation for using mathematical formalisms in software development is economical. The cost of fixing software design flaws after the completing of a software product is so high that it is vital to come up with ways to detect software design flaws in the early stages of software development, for instance, during the software requirements, the analysis activity, or during software design, before coding starts. The approach to software construction presented in this book is based on the idea of program refinement and correctness-by-construction.