Systems and software verification. Model-checking techniques and tools
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
In significant hardware designs or embedded software projects the system complexity, and hence the likely number of design errors, grows exponentially with the number of interacting system components. Traditional debugging and validation techniques are inadequate for detecting errors. Better suited are model-checking-based techniques. Model checking was invented more than twenty years ago but it is still developing and has more recently been introduced in many application fields. The book is an intelligible introduction to model checking. It is divided into three parts presenting fundamentals, including modelling with finite automata, synchronized product automata, introduction to temporal logics (CTL*, CTL, PLTL), algorithms of model checking and symbolic model checking, and an introduction to timed automata together with TCTL; specification and proof of selected properties, widely used in practice (reachability of states, safety, liveness, fairness, deadlock-freeness); an introduction to six tools, freely available in the academic world, considered from a user's point of view. The book can be used as an introductory textbook at an undergraduate or graduate level even though it has not the form of a typical modern textbook. More practically oriented readers will find a lot of examples illustrating theoretical considerations and hints how to catch special practical problems as, e.g., the state explosion problem.
- Vivid: a framework for heterogeneous problem solving
- Enhancing model checking in verification by AI techniques
- Reasoning about graded strategy quantifiers
- Provably correct systems. Papers based on the ProCoS workshop, London, UK, March 2015
- A logical characterization of data languages.
- Pragmatics of model checking: An STTT special section
- Is your model checker on time? On the complexity of model checking for timed modal logics
- Syntax-directed model checking of sequential programs
- Model checking techniqes for the analysis of reactive systems
- On the computation of counterexamples in compositional nonblocking verification
- Dealing with incompleteness in automata-based model checking
- Formal verification of mobile robot protocols
- Deterministic delay analysis of AVB switched Ethernet networks using an extended trajectory approach
- Periodicity based decidable classes in a first order timed logic
- Efficient timed model checking for discrete-time systems
- Formal verification of multitasking applications based on timed automata model
- A parametric analysis of the state-explosion problem in model checking
- Model-based testing of reactive systems. Advanced lectures.
- Formal analysis of oscillatory behaviors in biological regulatory networks: an alternative approach
- Model checking syllabi and student careers
- Automated formal analysis and verification: an overview
- Verification of component-based system using model checking
- Model checking safety-critical systems specified as X-machines
- Introduction to model checking
- Explicit-state model checking
- Formal models for software development. Model checking, verification, analysis and simulation
- Model checking technology and tool development based on Groebner base
- \(2^{5}\) years of model checking
- Symbolic model checking of actor-oriented high-level SystemC models with interval diagrams
- CTL Model Checking for Boolean Program
- Synergistic verification and validation of systems and software engineering models
- scientific article; zbMATH DE number 88991 (Why is no real title available?)
- Introduction to formal hardware verification
- scientific article; zbMATH DE number 527259 (Why is no real title available?)
- scientific article; zbMATH DE number 2021573 (Why is no real title available?)
- scientific article; zbMATH DE number 2080037 (Why is no real title available?)
- scientific article; zbMATH DE number 2080188 (Why is no real title available?)
- scientific article; zbMATH DE number 1519897 (Why is no real title available?)
- A model checking project at Philips Research
- Handbook of model checking
- Separation logics and modalities: a survey
- Formal system verification. State-of the-art and future trends
- Linear temporal logic symbolic model checking
- The tool TINA – Construction of abstract state spaces for petri nets and time petri nets
- Automatic verification of reduction techniques in higher order logic
- Model checking RAISE applicative specifications
- scientific article; zbMATH DE number 2087531 (Why is no real title available?)
- scientific article; zbMATH DE number 2087633 (Why is no real title available?)
- Software analysis and model checking
- Logic in Computer Science
- Truth -- a verification platform for concurrent systems
- Model checking
- Computer Science Logic
- Abstracting models from execution traces for performing formal verification
- Model Checking Software
- Database Theory - ICDT 2005
- An e-business assurance technique based on model-checking
- Software Model Checking: Searching for Computations in the Abstract or the Concrete
- Model-Checking Large Finite-State Systems and Beyond
- Formal reliability analysis of combinational circuits using theorem proving
- Principles of the SPIN model checker. Foreword by Gerard J. Holzmann
- Software Verification and Analysis
- Verification of software requirements on program systems represented by attribute transition systems
- Computer Aided Verification
- Computer Aided Verification
- Computer Aided Verification
- FM 2005: Formal Methods
- Challenges of software verification. Contributions of the first workshop, CSV, Venice, Italy, May 20, 2022
- Model checking, synthesis, and learning
- A survey on compositional algorithms for verification and synthesis in supervisory control
- Partially Bounded Context-Aware Verification
- Quantitatively nonblocking supervisory control of discrete-event systems
- Bounded-time nonblocking supervisory control of timed discrete-event systems
- From NuSMV to SPIN: Experiences with model checking flight guidance systems
- Verification of scope-dependent hierarchical state machines
This page was built for publication: Systems and software verification. Model-checking techniques and tools
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2733893)
