|
These web pages provide a variety of course materials on foundations and applications of model checking -- a tool-supported technology for analysis, debugging, and verification of concurrent and reactive systems (click here to learn more about the motivation and capabilities of model checking technology). These materials have been developed by researchers of the SAnToS Laboratory at Kansas State University (KSU) and University of Nebraska-Lincoln (UNL) including Dr. Matthew Dwyer (UNL), Dr. John Hatcliff (KSU), and Dr. Robby (KSU). While there are several fine textbooks that are available for teaching a course on model checking technology, the material presented on these pages is unique in several ways, and its unique presentation centers around the use of Bogor -- a state-of-the-art extensible software model checker developed in the SAnToS Laboratory. - Once foundational concepts of model-checking including state-space exploration algorithms, temporal logic specifications, and reduction strategies have been introduced from an abstract perspective using concise mathematical notations, these concepts are immediately tied to exercises and pedagogical visualizations in Bogor that concretely communicate the purpose and intuition of the concepts.
- Similar in spirit to many courses on compiler technology, this course reinforces basic theoretical and algorithmic concepts by directing students in programming projects that modify and extend the implementation of the core modules of Bogor's model checking engine.
- The course teaches effective methodologies for applying model checking by describing steps that must be taken in practice to apply a model checking tool like Bogor to real-world examples, and by illustrating how information specific to particular application domains can be captured and exploited using Bogor's extension and customization facilities.
These pages contain a variety of materials for running the course including:
In the material above, the textbook companion is a document distinct from the course textbook but with parallel structure that provides commentary on the foundational material in the textbook by (a) describing how foundational concepts in the textbook are implemented in Bogor or presented at Bogor's user interface and (b) providing guided solutions to selected exercises. These materials are publicly available in both student and instructor distributions (the instructor distribution contains solutions for homeworks, quizzes, exams, etc.) (click here to request a download of one of the distributions). The material is organized into modules to make it easier for instructors to all or only select portions of the material (e.g., for courses of different length or for using a subset of the material above as one unit in a broader course, e.g., on general software specification). The modules included in the current course distribution include:
Click here (pending link) for an overview of how we organize and administer the course at Kansas State and Nebraska and some brief notes on alternative ways of structuring the course. The distribution of these materials is part of a broader educational effort that emphasizes tool-supported formal methods. For example, course material that we have prepared on Software Specifications (including languages and tools such as Alloy, UML/USE, and JML, and ESC/Java) can be found here . To download these materials, you will be required to register as a user on our artifact management system (click here to register), and agree to our software distribution license. Some of our materials (for example, the textbook draft) are currently only available to students at Kansas State and the University of Nebraska. These materials are declared as "moderated" in the download system.
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. |
Model Checking