|
This module presents several approaches for specifying correctness properties of transition system models and the modifications to the depth-first state-space (DFS) exploration algorithm that are necessary to check them. Throughout the module, students write simple specifications and check them using Bogor's property checking capabilities.
We divide the presentation of specifications and algorithms into four different parts: - State-based property checking -- we present assertions and invariants and how those are checked in the core algorithm.
- Safety properties and checking -- we present regular expressions and finite-state automata and show how they can be used to encode sequencing properties of systems and how they can be checked by adapting the DFS algorithm to explore the combined state space of the system model and property.
- Progress properties and checking -- we present simple liveness properties, introduced as special kinds of location, and how they can be checked by extending the DFS algorithm to perform nested depth-first state-space exploration.
- Linear Temporal Logic model checking -- we present linear temporal logic and show how the approach to safety property checking and the approach to progress property checking are combined to implement model checking.
We organize the presentation in this way because it allows us to tease apart several fundamentally different aspects of property checking algorithms and present them as relatively simple extensions of the core DFS algorithm. Students can become familiar with those extensions independently and, in our experience, this allows them to understand the combined model checking algorithm more easily. The lectures in this module cover this material from a foundational point of view as well as from the practical point of view of how one specifies and checks properties using Bogor. The lectures include: - Module overview -- a brief overview of this module
- Foundations of specifications -- the what and why of formal specification
- Observing system behavior -- defining which of the myriad details of a system's execution are relevant to a given correctness property
- Sequencing specifications -- presentation of regular expressions specifications and finite-state automata
- Safety checking via instrumentation -- a simple manual approach to encoding safety properties directly into the model for checking
- Safety checking via product construction -- an automatic approach for checking conformance of a model with a specified safety property
- Progress checking -- presentation of the nested depth-first search algorithm
- Linear temporal logic -- presentation of LTL specifications and Buchi automata
- LTL model checking -- the automata-based explicit state model checking algorithm
- Slides
- Module Overview [.ppt, .pdf]
- Foundations [.ppt, .pdf]
- Observables [.ppt, .pdf]
- Sequencing Properties [.ppt, .pdf]
- Instrumentation [.ppt, .pdf]
- Product Checking [.ppt, .pdf]
- Progress Checking [.ppt, .pdf]
- Temporal Logic [.ppt, .pdf]
- LTL Model Checking [.ppt, .pdf]
- Specification Patterns [.ppt, .pdf]
- Lecture Videos
- Lecture Exercises
- Text
- Homeworks
- Quizzes
- Lab Exercises
- Examples
- Bogor Configurations
- BIR Models
- Java Code
- Exams
Copyright 2001-2006, Matthew B. Dwyer, John Hatcliff, and Robby. The course materials listed here are copyrighted materials and may not be used in other course settings outside of Kansas State University and University of Nebraska-Lincoln in their current form or modified form without the express written permission of one of the copyright holders. Selling notes to or being paid for taking notes by any person or commercial firm without the express written permission of one of the copyright holders are prohibited. |
