Manfred Broy

Bengt Jonsson

Joost-Pieter Katoen

Martin Leucker

Alexander Pretschner

Testing is the primary hardware and software verification technique used by industry today. Usually, it is ad hoc, error prone, and very expensive. In recent years, however, many attempts have been made to develop more sophisticated formal testing methods. This coherent book provides an in-depth assessment of this emerging field, focusing on formal testing of reactive systems. This book is based on a seminar held in Dagstuhl Castle, Germany, in January 2004. It presents 19 carefully reviewed and revised lectures given at the seminar in a well-balanced way ensuring competent complementary coverage of all relevant aspects. An appendix provides a glossary for model-based testing and basics on finite state machines and on labelled transition systems. The lectures are presented in topical sections on testing of finite state machines, testing of labelled transition systems, model-based test case generation, tools and case studies, standardized test notation and execution architectures, and beyond testing.

Advanced Lectures

Model-Based Testing of Reactive Systems

Barbara König

This book constitutes the refereed proceedings of the 22nd International Conference on Concurrency Theory, CONCUR 2011, held in Aachen, Germany, September 5-10, 2011. The 32 revised full papers were carefully reviewed and selected from 94 submissions. The papers are organized in topics such as real-time systems, probabilistic systems, automata, separation logic, π-calculus, Petri nets, process algebra and modeling, verification, games, and bisimulation.

22nd International Conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011, Proceedings

CONCUR 2011 -- Concurrency Theory

Marsha Chechik

This book constitutes the refereed proceedings of the 25th International Symposium on Formal Methods, FM 2023, which took place in Lübeck, Germany, in March 2023. The 26 full paper, 2 short papers included in this book were carefully reviewed and selected rom 95 submissions. They have been organized in topical sections as follows: SAT/SMT; Verification; Quantitative Verification; Concurrency and Memory Models; Formal Methods in AI; Safety and Reliability. The proceedings also contain 3 keynote talks and 7 papers from the industry day.

25th International Symposium, FM 2023, Lübeck, Germany, March 6–10, 2023, Proceedings

Formal Methods

Christel Baier

A comprehensive introduction to the foundations of model checking, a fully automated technique for finding flaws in hardware and software; with extensive examples and both practical and theoretical exercises. Our growing dependence on increasingly complex computer and software systems necessitates the development of formalisms, techniques, and tools for assessing functional properties of these systems. One such technique that has emerged in the last twenty years is model checking, which systematically (and automatically) checks whether a model of a given system satisfies a desired property such as deadlock freedom, invariants, and request-response properties. This automated technique for verification and debugging has developed into a mature and widely used approach with many applications. Principles of Model Checking offers a comprehensive introduction to model checking that is not only a text suitable for classroom use but also a valuable reference for researchers and practitioners in the field. The book begins with the basic principles for modeling concurrent and communicating systems, introduces different classes of properties (including safety and liveness), presents the notion of fairness, and provides automata-based algorithms for these properties. It introduces the temporal logics LTL and CTL, compares them, and covers algorithms for verifying these logics, discussing real-time systems as well as systems subject to random phenomena. Separate chapters treat such efficiency-improving techniques as abstraction and symbolic manipulation. The book includes an extensive set of examples (most of which run through several chapters) and a complete set of basic results accompanied by detailed proofs. Each chapter concludes with a summary, bibliographic notes, and an extensive list of exercises of both practical and theoretical nature.

Principles of Model Checking

Gilles Barthe

Alexandra Silva

This book provides an overview of the theoretical underpinnings of modern probabilistic programming and presents applications in e.g., machine learning, security, and approximate computing. Comprehensive survey chapters make the material accessible to graduate students and non-experts. This title is also available as Open Access on Cambridge Core.

Foundations of Probabilistic Programming

Perdita Stevens

ETAPS 2002 was the ?fth instance of the European Joint Conferences on Theory and Practice of Software. ETAPS is an annual federated conference that was established in 1998by combining a number of existing and new conferences. This year it comprised 5 conferences (FOSSACS, FASE, ESOP, CC, TACAS), 13 satellite workshops (ACL2, AGT, CMCS, COCV, DCC, INT, LDTA, SC, SFEDL, SLAP, SPIN, TPTS, and VISS), 8invited lectures (not including those speci?c to the satellite events), and several tutorials. The events that comprise ETAPS address various aspects of the system - velopment process, including speci?cation, design, implementation, analysis, and improvement. The languages, methodologies, and tools which support these - tivities are all well within its scope. Di?erent blends of theory and practice are represented, with an inclination towards theory with a practical motivation on one hand and soundly-based practice on the other. Many of the issues involved in software design apply to systems in general, including hardware systems, and the emphasis on software is not intended to be exclusive.

8th International Conference, TACAS 2002, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002. Proceedings

Tools and Algorithms for the Construction and Analysis of Systems

Arend Rensink

Rom Langerak

This Festschrift volume has been published in honor of Ed Brinksma, on the occasion of his 60th birthday. The contributions in this Festschrift are written by a number of Ed's former Ph.D. students and collaborators. The papers are a reflection on his research contributions and interests and all fall into the area of formal methods, or in Ed's terminology applied mathematics in computer science. The papers address modeling languages and semantics, model-based testing, verification and performance analysis, probabilistic computation, system dynamics, and applications of formal methods.

Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday

ModelEd, TestEd, TrustEd

Our growing dependence on increasingly complex computer and software systemsnecessitates the development of formalisms, techniques, and tools for assessing functionalproperties of these systems. One such technique that has emerged in the last twenty years is modelchecking, which systematically (and automatically) checks whether a model of a given systemsatisfies a desired property such as deadlock freedom, invariants, and request-response properties.This automated technique for verification and debugging has developed into a mature and widely usedapproach with many applications. Principles of Model Checking offers a comprehensive introduction tomodel checking that is not only a text suitable for classroom use but also a valuable reference forresearchers and practitioners in the field. The book begins with the basic principles for modelingconcurrent and communicating systems, introduces different classes of properties (including safetyand liveness), presents the notion of fairness, and provides automata-based algorithms for theseproperties. It introduces the temporal logics LTL and CTL, compares them, and covers algorithms forverifying these logics, discussing real-time systems as well as systems subject to random phenomena.Separate chapters treat such efficiency-improving techniques as abstraction and symbolicmanipulation. The book includes an extensive set of examples (most of which run through severalchapters) and a complete set of basic results accompanied by detailed proofs. Each chapter concludeswith a summary, bibliographic notes, and an extensive list of exercises of both practical andtheoretical nature.Christel Baier is Professor and Chair for Algebraic and Logical Foundations ofComputer Science in the Faculty of Computer Science at the Technical University of Dresden.Joost-Pieter Katoen is Professor at the RWTH Aachen University and leads the Software Modeling andVerification Group within the Department of Computer Science. He is affiliated with the FormalMethods and Tools Group at the University of Twente.

Joost-Pieter Katoen

About

Books

Join the club