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

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

  • 出版商: Morgan & Claypool
  • 出版日期: 2020-01-27
  • 售價: $2,090
  • 貴賓價: 9.5$1,986
  • 語言: 英文
  • 頁數: 99
  • 裝訂: Hardcover - also called cloth, retail trade, or trade
  • ISBN: 1681736896
  • ISBN-13: 9781681736891
  • 相關分類: 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 開發聊天系統的案例研究,以及一個社交網路屬性的正式證明案例研究。