Formal Methods for Software Engineering: Languages, Methods, Application Domains
暫譯: 軟體工程的形式方法：語言、方法與應用領域

軟體程式是具有精確意義的正式實體，與其程式設計師無關，因此從想法到程式的轉變必然涉及某種形式的正式化。

這本研究生級別的正式方法入門書的第一部分發展了對正式方法的理解，以及它們在軟體工程中的地位。它還介紹了邏輯作為描述推理的語言，以及過程代數 CSP 作為表示行為的語言。第二部分提供了基於建模語言 CASL 和 UML 的正式軟體開發的規範和測試方法。第三部分將讀者帶入規範性文件、人機介面和安全性等應用領域。全書對符號和形式的使用保持一致。

主題和特點：
- 解釋基礎，並介紹規範、驗證和測試方法
- 探索各種應用領域
- 提供現實且實用的例子，說明概念
- 彙集來自經驗豐富的教育工作者和研究人員的貢獻
- 提供正式軟體開發的建模和分析方法

這本獨特的實用教科書適合用於軟體工程的研究生和本科課程，對於資訊學的學生以及希望學習或更有效地使用正式理論和方法的科學家和實務工程師也具有價值。

**Markus Roggenbach** 是斯旺西大學計算機科學系的教授。**Antonio Cerone** 是納扎爾巴耶夫大學計算機科學系的副教授。**Bernd-Holger Schlingloff** 是柏林洪堡大學計算機科學研究所的教授。**Gerardo Schneider** 是哥德堡大學計算機科學與工程系的教授。**Siraj Ahmed Shaikh** 是考文垂大學未來交通與城市研究所的教授。

本書的伴隨網站提供額外資源，包括為選定章節準備的進一步材料、實驗課程、勘誤表、幻燈片和教學材料，以及預裝工具和資源的虛擬機，以便讀者能夠親自體驗書中的例子。網址為：https://sefm-book.github.io

Antonio Cerone is an Associate Professor of Computer Science at Nazarbayev University, Kazakhstan. Previously he has been working at the IMT School for Advanced Studies Lucca, the United Nations University, the University of Queensland, the University of South Australia, the Goethe University Frankfurt and the University of Pisa. His main research focus is on formal methods and their application to several domains, including human-computer interaction, safety, security, systems biology, and ecology. He is also interested in cognitive science, open-source development, and collaborative learning. He is the founder and Chair of the Steering Committee of the International Conference on Software Engineering and Formal Methods SEFM.

Dr Hoang Nga Nguyen is an Associate Professor in Automotive Cybersecurity at the Centre for Future Transport and Cities, Coventry University, UK. His research agenda includes cybersecurity in automotive and autonomous systems. His work focuses on automotive threat modelling, risk assessment, security solutions, and security testbed.

Liam O'Reilly is a Senior Lecturer and Programme Director in the Department of Computer Science at Swansea University, UK. His research is in the areas of Formal Methods, Algebraic Specification, Process Algebra, and the Pedagogy of Computer Science and Software Engineering. Liam has also worked as a Software Engineer in industry developing embedded systems. He has extensive experience in the teaching and delivery of Software Engineering including, but not limited to, the design of software, UML, algorithms, and web technology.

Markus Roggenbach is a Professor of Computer Science at Swansea University, UK. He leads the Security Group in Swansea University's department of Computer Science, where he also has been Director of Research (2016 - 2021). His research foci are formal methods for safety and for cyber security, their semantics, how to utilise them throughout the software life cycle, how to support them with tools, and their application in industrial contexts, e.g., the railway domain. He is a member of the Federation for Information Processing (IFIP) Working Group 1.3 "Foundations of System Specification" (chair in 2015 - 2021).

Bernd-Holger Schlingloff is a Professor of Software Engineering at the Institute for Computer Science of Humboldt University, Berlin, and chief scientist at the Fraunhofer Institute for Open Communication Systems (Fraunhofer FOKUS). Moreover, he is chairman of the boards of the society for the advancement of embedded systems (ZeSys e.V.), and the society for the advancement of applied computer science (GFaI e.V.). His main subject is the specification, verification and testing of embedded safety-critical software. This includes quality assurance of embedded control software, model-based development and model checking, logical verification of requirements, and automated test generation. In his work, he is applying formal methods in industrial projects in the automotive, railway, and medical technology domain.

Gerardo Schneider is a Professor of Computer Science at the University of Gothenburg, Sweden. He had previously been at VERIMAG (Grenoble, France), Uppsala University (Sweden), Irisa/INRIA (Rennes, France), and the University of Oslo (Norway). He has been the Head of the Formal Methods Division at the Department of Computer Science and Engineering since 2017. His research interests include formal verification (runtime verification, model checking, and verification of real-time and hybrid systems), the specification and analysis of normative documents, and privacy.

Siraj Ahmed Shaikh is a Professor of Systems Security and Director for the Centre for Future Transport and Cities (CFTC) at Coventry University, UK. He also leads the Systems Security Group at CFTC, where his research interests sit at the intersection of cybersecurity, systems engineering and computer science with particular application to automotive and transport systems. He is also Co-Founder and Chief Scientist at CyberOwl, which is dedicated to cyber-physical systems security monitoring for the maritime sector. He has served as the Royal Academy of Engineering (RAEng) Industrial Fellow at HORIBA MIRA (2015-16) where he investigated security testing for the automotive industry.

John V Tucker is a Professor of Computer Science at Swansea University, UK. His research over five decades explores the scope and limits of digital data and computation in mathematical, physical, and social systems. A scholar of the history of technology, he founded Swansea University's History of Computing Collection, and is an expert on the history of science and technology in Wales. He is a Founding Fellow of the Learned Society of Wales and a Member of Academia Europaea.

安東尼奧·切羅尼（Antonio Cerone）是哈薩克斯坦納扎爾巴耶夫大學（Nazarbayev University）計算機科學的副教授。之前，他曾在意大利盧卡的IMT高等研究學校、聯合國大學、昆士蘭大學、南澳大利亞大學、法蘭克福歌德大學和比薩大學工作。他的主要研究重點是形式方法及其在多個領域的應用，包括人機互動、安全性、系統安全、生物系統學和生態學。他還對認知科學、開源開發和協作學習感興趣。他是國際軟體工程與形式方法會議（SEFM）指導委員會的創始人和主席。

黃芽阮博士（Dr Hoang Nga Nguyen）是英國考文垂大學（Coventry University）未來交通與城市中心的汽車網路安全副教授。他的研究議程包括汽車和自主系統中的網路安全。他的工作專注於汽車威脅建模、風險評估、安全解決方案和安全測試平台。

利亞姆·奧萊利（Liam O'Reilly）是英國斯旺西大學（Swansea University）計算機科學系的高級講師和課程主任。他的研究領域包括形式方法、代數規範、過程代數以及計算機科學和軟體工程的教學法。利亞姆還曾在業界擔任嵌入式系統的軟體工程師。他在軟體工程的教學和實施方面擁有豐富的經驗，包括但不限於軟體設計、UML、演算法和網路技術。

馬庫斯·羅根巴赫（Markus Roggenbach）是英國斯旺西大學的計算機科學教授。他領導斯旺西大學計算機科學系的安全小組，並曾擔任研究主任（2016 - 2021）。他的研究重點是安全和網路安全的形式方法、其語義、如何在軟體生命週期中利用它們、如何用工具支持它們，以及它們在工業背景下的應用，例如鐵路領域。他是資訊處理聯盟（IFIP）工作組1.3「系統規範的基礎」（2015 - 2021年主席）的成員。

伯恩德·霍爾格·施林格洛夫（Bernd-Holger Schlingloff）是德國柏林洪堡大學計算機科學研究所的軟體工程教授，也是法蘭霍夫開放通信系統研究所（Fraunhofer FOKUS）的首席科學家。此外，他還是嵌入式系統促進協會（ZeSys e.V.）和應用計算機科學促進協會（GFaI e.V.）的董事會主席。他的主要研究主題是嵌入式安全關鍵軟體的規範、驗證和測試，包括嵌入式控制軟體的質量保證、基於模型的開發和模型檢查、需求的邏輯驗證以及自動化測試生成。在他的工作中，他在汽車、鐵路和醫療技術領域的工業項目中應用形式方法。

赫拉多·施奈德（Gerardo Schneider）是瑞典哥德堡大學的計算機科學教授。他曾在法國格勒諾布爾的VERIMAG、瑞典烏普薩拉大學、法國雷恩的Irisa/INRIA和挪威奧斯陸大學工作。自2017年以來，他一直擔任計算機科學與工程系形式方法部門的負責人。他的研究興趣包括形式驗證（運行時驗證、模型檢查和實時及混合系統的驗證）、規範文件的規範與分析以及隱私。

西拉吉·艾哈邁德·謝赫（Siraj Ahmed Shaikh）是英國考文垂大學未來交通與城市中心（CFTC）的系統安全教授和主任。他還領導CFTC的系統安全小組，他的研究興趣位於網路安全、系統工程和計算機科學的交集，特別應用於汽車和交通系統。他還是CyberOwl的共同創始人和首席科學家，該公司專注於海事領域的網路物理系統安全監控。他曾擔任皇家工程院（RAEng）工業研究員，於HORIBA MIRA（2015-16年）調查汽車行業的安全測試。

約翰·V·塔克（John V Tucker）是英國斯旺西大學的計算機科學教授。他五十年來的研究探索數位數據和計算在數學、物理和社會系統中的範圍和限制。作為技術史學者，他創立了斯旺西大學的《計算機歷史收藏》（History of Computing Collection），並且是威爾斯科學與技術歷史的專家。他是威爾斯學術學會的創始成員，也是歐洲學院的成員。