國立虎尾科技大學 |

Java software development with event B : = a practical guide /

Record Type:	Language materials, printed : Monograph/item
Title/Author:	Java software development with event B :/ Néstor Cataño Collazos.
Reminder of title:	a practical guide /
Author:	Cataño Collazos, Nestor,
Description:	1 PDF (x, 89 pages) :illustrations (some color). :
Notes:	Part of: Synthesis digital library of engineering and computer science.
Subject:	Java (Computer program language) -
Online resource:	https://ieeexplore.ieee.org/servlet/opac?bknumber=8975712
Online resource:	https://doi.org/10.2200/S00957ED1V01Y201910SWE005
ISBN:	9781681736884

Java software development with event B : = a practical guide /
Cataño Collazos, Nestor,1975-

Java software development with event B :a practical guide /Néstor Cataño Collazos. - 1 PDF (x, 89 pages) :illustrations (some color). - Synthesis lectures on software engineering,#52328-3327 ;. - Synthesis digital library of engineering and computer science..

Part of: Synthesis digital library of engineering and computer science.

Includes bibliographical references (pages 83-84) and index.

1. Introduction -- 2. An overview of EVENT B -- 2.1. Relations and functions -- 2.2. EVENT B mathematical notation -- 2.3. Software development with EVENT B -- 2.4. A methodology for early validation of software requirements -- 2.5. Correctness-by-construction -- 2.6. RODIN -- 2.7. JML -- 2.8. EVENTB2JAVA -- 2.9. A Chat application

Abstract freely available; full-text restricted to subscribers or individual document purchasers.

Compendex

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.

Mode of access: World Wide Web.

ISBN: 9781681736884

Standard No.: 10.2200/S00957ED1V01Y201910SWE005doiSubjects--Topical Terms:

557657
Java (Computer program language)
Subjects--Index Terms:

correct-by-construction

LC Class. No.: QA76.73.J38 / C384 2020eb

Dewey Class. No.: 005.13/3

Java software development with event B : = a practical guide /
LDR:05004nam 2200601 i 4500 001 959785
003 IEEE
005 20200131190106.0
006 m eo d
007 cr cn |||m|||a
008 201209s2020 paua ob 001 0 eng d
020 $a 9781681736884 $q electronic
020 $z 9781681736891 $q hardcover
020 $z 9781681736877 $q paperback
024 7 $a 10.2200/S00957ED1V01Y201910SWE005 $2 doi
035 $a (CaBNVSL)thg00980010
035 $a (OCoLC)1138655327
035 $a 8975712
040 $a CaBNVSL $b eng $e rda $c CaBNVSL $d CaBNVSL
050 4 $a QA76.73.J38 $b C384 2020eb
082 0 4 $a 005.13/3 $2 23
100 1 $a Cataño Collazos, Nestor, $d 1975- $e author. $3 1253153
245 1 0 $a Java software development with event B : $b a practical guide / $c Néstor Cataño Collazos.
264 1 $a [San Rafael, California] : $b Morgan & Claypool, $c [2020]
300 $a 1 PDF (x, 89 pages) : $b illustrations (some color).
336 $a text $2 rdacontent
337 $a electronic $2 isbdmedia
338 $a online resource $2 rdacarrier
490 1 $a Synthesis lectures on software engineering, $x 2328-3327 ; $v #5
500 $a Part of: Synthesis digital library of engineering and computer science.
504 $a Includes bibliographical references (pages 83-84) and index.
505 0 $a 1. Introduction -- 2. An overview of EVENT B -- 2.1. Relations and functions -- 2.2. EVENT B mathematical notation -- 2.3. Software development with EVENT B -- 2.4. A methodology for early validation of software requirements -- 2.5. Correctness-by-construction -- 2.6. RODIN -- 2.7. JML -- 2.8. EVENTB2JAVA -- 2.9. A Chat application
505 8 $a 3. Software development of a chat system with EVENT B -- 3.1. MachineZero -- 3.2. MachineOne -- 3.3. MachineTwo -- 3.4. MachineZero in EVENT B -- 3.5. MachineOne in EVENT B -- 3.6. MachineTwo in EVENT B -- 3.7. The implementation of the chat system -- 3.8. Testing and code animation of the chat system -- 3.9. Fixing the software requirements -- 3.10. Lessons learned
505 8 $a 4. The Poporo social network -- 4.1. Poporo's general structure -- 4.2. Poporo's formalization in EVENT B -- 4.3. Invariant POs -- 4.4. Discharging POs in Rodin -- 4.5. POs for quantified expressions -- 4.6. Strengthening the specification -- 4.7. Further strengthening -- 4.8. Refinement proof obligations -- 5. Conclusion.
506 $a Abstract freely available; full-text restricted to subscribers or individual document purchasers.
510 0 $a Compendex
510 0 $a INSPEC
510 0 $a Google scholar
510 0 $a Google book search
520 $a 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.
530 $a Also available in print.
538 $a Mode of access: World Wide Web.
538 $a System requirements: Adobe Acrobat Reader.
588 $a Title from PDF title page (viewed on January 28, 2020).
650 0 $a Java (Computer program language) $3 557657
650 0 $a Formal methods (Computer science) $3 564790
650 0 $a B method (Computer science) $3 1060177
650 0 $a Computer software $x Development $v Congresses. $3 574593 $3 727349
653 $a correct-by-construction
653 $a discrete mathematics
653 $a Event B
653 $a Java
653 $a programming
653 $a refinement
653 $a software engineering
653 $a verification
776 0 8 $i Print version: $z 9781681736891 $z 9781681736877
830 0 $a Synthesis digital library of engineering and computer science. $3 598254
830 0 $a Synthesis lectures on software engineering ; $v #4. $x 2328-3319 $3 1175714
856 4 2 $3 Abstract with links to resource $u https://ieeexplore.ieee.org/servlet/opac?bknumber=8975712
856 4 0 $3 Abstract with links to full text $u https://doi.org/10.2200/S00957ED1V01Y201910SWE005