Formal Methods for Software Engineering - Roggenbach, Markus

. .

Résumé :
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 Exploresvarious 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...

Biographie:
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 G...

Sommaire:
Stefan Gruner is an Associate Professor of Computer Science at the University of Pretoria, Republic of South Africa. Together with Tom Maibaum, he co-supervised Apurva Kumar during her Master's project, on the results of which some parts of this book are based. He has also collaborated with Markus Roggenbach for many years, particularly on questions concerning the formal semantics of CSP. At the University of Pretoria, Stefan Gruner lectures mostly theory based courses such as compiler construction or formal methods. With his additional qualification in philosophy, he is also active in interdisciplinary fields such as philosophy of science, philosophy of technology, and philosophy of informatics (meta informatics). Apurva Kumar completed her Masters in Applied Science from McMaster University in 2015 under the supervision of Stefan Gruner and Tom Maibaum. Many of the findings in her Master's thesis are incorporated in this book.Apurva Kumar is currently a security researcher on the Threat Intelligence team at Lookout Inc. She spends most of her time uncovering and tracking threats as they emerge in and around the mobile space. Her main focus is on exposing and defending against nation state surveillance campaigns. Apurva's current work incorporates threat hunting, reverse engineering and penetration testing. Tom Maibaum is an Emeritus Professor of the Foundations of Software Engineering in the Department of Computing and Software, McMaster University, Canada. He now lives in The United Kingdom. Previously, he held similarly named Chairs at King's College London and Imperial College London. Throughout his career, his research has focused on the logical and categorical bases of software engineering and on the applications of these topics to software engineering methods. He has studied the philosophical and epistemological bases of engineering and, in particular, software engineering. Over the past 15 years he has worked with Mark Lawford and Alan Wassyng at McMaster University in the context of the McMaster Centre for Software Certification, developing new logical and epistemological foundations of safety reasoning. Markus Roggenbach is a Professor of Computer Science at Swansea University, The United Kingdom. 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. For more than a decade, he has been collaborating with Siemens Rail Automation (formerly Invensys Rail) to answer questions concerning safety with regard to railway signalling systems. He leads the Swansea Railway Verification Group, the European Technical Working Group on Formal Methods in Railway Control, and chairs the International Federation for Information Processing (IFIP) Working Group 1.3 Foundations of System Specification. ...