Java Software Development with Event B: A Practical Guide
暫譯: Java 軟體開發與 Event B：實用指南

Collazos, Néstor Cataño, Baresi, Luciano

Java Software Development with Event B: A Practical Guide
  • 出版商: Morgan & Claypool
  • 出版日期: 2020-01-27
  • 售價: $1,450
  • 貴賓價: 9.5 折 $1,378
  • 語言: 英文
  • 頁數: 99
  • 裝訂: Quality Paper - also called trade paper
  • ISBN: 168173687X
  • ISBN-13: 9781681736877
  • 相關分類: Java 程式語言

    • 海外代購書籍(需單獨結帳)

相關主題

商品描述

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.

商品描述(中文翻譯)

軟體產品完成後修正設計缺陷的成本非常高，因此在軟體開發的早期階段（例如在軟體需求、分析活動或軟體設計階段）找出軟體設計缺陷的方法是至關重要的，這些階段應該在開始編碼之前進行。

軟體需求模糊或相互矛盾並不罕見。模糊性因為軟體需求通常是用自然語言撰寫的，而自然語言並不與任何正式語義相連結，這一點使得模糊性更加嚴重。解決軟體需求模糊性的一種方法是將其語法限制為範本，即帶有佔位符的文本模板。然而，由於非正式需求並不具備任何特定的語義，因此無法輕易證明它們（或它們試圖描述的系統）的任何基本屬性。正式方法是解決這個問題的另一種選擇。它們提供了一系列數學技術和數學工具，以在軟體開發的早期階段驗證軟體需求。

本書是使用正式方法開發軟體的活生生的證據。我們使用的特定形式化方法是 EVENT B 和精煉演算。簡而言之：（i）軟體需求以用戶故事的形式撰寫；（ii）它們被轉換為正式規範；（iii）根據需要進行精煉；（iv）以原型的形式實現；最後（v）對不一致性進行測試。如果某個單元測試失敗，則會重新檢視和演進軟體系統的非正式和正式規範。

本書展示了一個使用 EVENT B 開發聊天系統的案例研究，以及一個社交網路屬性的正式證明案例研究。

作者簡介

Néstor Cataño Collazos is a software engineer, computer scientist, and enthusiastic formal methods tool developer. His main research area is the use of formal methods for software engineering. Néstor specializes in program specification and verification using JML and design-by-contract, and in a formal method called EVENT B. His main goal is to build Formal Methods tools that increase people's trust in the correct behavior of Software Systems. His main tool contributions are the design and implementation of the EVENTB2JAVA and EVENTB2JML code generators, the design and implementation of the EVENTB2DAFNY Proof Obligation generator, and the design and implementation of the Chase syntactic checker of JML's assignable clause. Néstor's research work with EVENTB2DAFNY was funded by Microsoft Research through the SEIF program in 2011. He has worked in academia since 2004 and regularly teaches software engineering, formal methods, and programming courses to graduate and undergraduate students.

Dr. Collazos earned a Master Degree and a Ph.D. in Computer Science from The University Paris 7. He is currently taking part in the Master in Information and Cybersecurity at UC Berkeley.

作者簡介(中文翻譯)

Néstor Cataño Collazos 是一位軟體工程師、計算機科學家，以及熱衷於形式方法工具開發的專家。他的主要研究領域是形式方法在軟體工程中的應用。Néstor 專注於使用 JML 進行程式規範和驗證，以及一種名為 EVENT B 的形式方法。他的主要目標是建立形式方法工具，以增強人們對軟體系統正確行為的信任。他的主要工具貢獻包括 EVENTB2JAVA 和 EVENTB2JML 代碼生成器的設計與實現、EVENTB2DAFNY 證明義務生成器的設計與實現，以及 JML 的可指派條款的 Chase 語法檢查器的設計與實現。Néstor 在 2011 年的研究工作 EVENTB2DAFNY 得到了微軟研究院透過 SEIF 計畫的資助。他自 2004 年以來一直在學術界工作，並定期教授軟體工程、形式方法和程式設計課程給研究生和本科生。

Collazos 博士在巴黎第七大學獲得計算機科學碩士學位和博士學位。他目前正在加州大學伯克利分校參加資訊與網路安全碩士課程。

類似商品

最後瀏覽商品 (20)