Néstor Cataño Collazos - Java Software Development with Event B
Here you can read online Néstor Cataño Collazos - Java Software Development with Event B full text of the book (entire story) in english for free. Download pdf and epub, get meaning, cover and reviews about this ebook. year: 2020, publisher: Morgan & Claypool Publishers, genre: Computer. Description of the work, (preface) as well as reviews are available. Best literature library LitArk.com created for fans of good reading and offers a wide selection of genres:
Romance novel
Science fiction
Adventure
Detective
Science
History
Home and family
Prose
Art
Politics
Computer
Non-fiction
Religion
Business
Children
Humor
Choose a favorite category and find really read worthwhile books. Enjoy immersion in the world of imagination, feel the emotions of the characters or learn something new for yourself, make an fascinating discovery.
- Book:Java Software Development with Event B
- Author:
- Publisher:Morgan & Claypool Publishers
- Genre:
- Year:2020
- Rating:4 / 5
- Favourites:Add to favourites
- Your mark:
- 80
- 1
- 2
- 3
- 4
- 5
Java Software Development with Event B: summary, description and annotation
We offer to read an annotation, description, summary or preface (depends on what the author of the book "Java Software Development with Event B" wrote himself). If you haven't found the necessary information about the book — write in the comments, we will try to find it.
Java Software Development with Event B — read online for free the complete book (whole text) full work
Below is the text of the book, divided by pages. System saving the place of the last page read, allows you to conveniently read the book "Java Software Development with Event B" online for free, without having to search again every time where you left off. Put a bookmark, and you can go to the page where you finished reading at any time.
Font size:
Interval:
Bookmark:
![Java Software Development with Event B A Practical Guide Synthesis Lectures - photo 1](/uploads/posts/book/256385/Images/cover.jpg)
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.
Font size:
Interval:
Bookmark:
Similar books «Java Software Development with Event B»
Look at similar books to Java Software Development with Event B. We have selected literature similar in name and meaning in the hope of providing readers with more options to find new, interesting, not yet read works.
Discussion, reviews of the book Java Software Development with Event B and just readers' own opinions. Leave your comments, write what you think about the work, its meaning or the main characters. Specify what exactly you liked and what you didn't like, and why you think so.