Formal Methods for Software Engineering: Languages, Methods, Application Domains

Software programs are formal entities with precise meanings independent of their programmers, so the transition from ideas to programs necessarily involves a formalisation at some point.

The first part of this graduate-level introduction to formal methods develops an understanding of what constitutes formal methods and what their place is in Software Engineering. It also introduces logics as languages to describe reasoning and the process algebra CSP as a language to represent behaviours. The second part offers specification and testing methods for formal development of software, based on the modelling languages CASL and UML. The third part takes the reader into the application domains of normative documents, human machine interfaces, and security. Use of notations and formalisms is uniform throughout the book.

Topics and features:

• Explains foundations, and introduces specification, verification, and testing methods
• Explores various application domains
• Presents realistic and practical examples, illustrating concepts
Brings together contributions from highly experienced educators and researchers
• Offers modelling and analysis methods for formal development of software

Suitable for graduate and undergraduate courses in software engineering, this uniquely practical textbook will also be of value to students in informatics, as well as to scientists and practical engineers, who want to learn about or work more effectively with formal theories and methods.

Markus Roggenbach is a Professor in the Dept. of Computer Science of Swansea University. Antonio Cerone is an Associate Professor in the Dept. of Computer Science of Nazarbayev University, Nur-Sultan. Bernd-Holger Schlingloff is a Professor in the Institut für Informatik of Humboldt-Universität zu Berlin. Gerardo Schneider is a Professor in the Dept. of Computer Science and Engineering of University of Gothenburg. Siraj Ahmed Shaikh is a Professor in the Institute for Future Transport and Cities of Coventry University.

The companion site for the book offers additional resources, including further material for selected chapters, prepared lab classes, a list of errata, slides and teaching material, and virtual machines with preinstalled tools and resources for hands-on experience with examples from the book. The URL is: https: //sefm-book.github.io

軟體程式是具有精確意義且獨立於程式設計師的正式實體，因此從概念到程式的轉換在某個時刻必然涉及形式化的過程。

這本研究生級的形式方法入門的第一部分，旨在培養對形式方法的理解以及其在軟體工程中的地位。它還介紹了作為描述推理的語言的邏輯，以及作為表示行為的語言的過程代數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 是哈薩克斯坦納扎爾巴耶夫大學的計算機科學副教授。他曾在IMT School for Advanced Studies Lucca、聯合國大學、昆士蘭大學、南澳大學、法蘭克福歌德大學和比薩大學工作。他的主要研究方向是形式方法及其在人機交互、安全、系統生物學和生態學等多個領域的應用。他還對認知科學、開源開發和協作學習感興趣。他是國際軟件工程和形式方法SEFM國際會議的創始人和主席。

Dr Hoang Nga Nguyen 是英國考文垂大學未來交通與城市中心的汽車網絡安全副教授。他的研究議程包括汽車和自主系統的網絡安全。他的工作重點是汽車威脅建模、風險評估、安全解決方案和安全測試平台。

Liam O'Reilly 是英國斯旺西大學計算機科學系的高級講師和課程主任。他的研究領域包括形式方法、代數規範、過程代數和計算機科學和軟件工程的教學法。Liam還曾在工業界擔任軟件工程師，開發嵌入式系統。他在軟件工程的教學和交付方面有豐富的經驗，包括但不限於軟件設計、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的系統安全組，他的研究興趣集中在網絡安全和系統工程的交叉領域。