Bogor Software Model Checking Framework: User Manual
		Next

Bogor Software Model Checking Framework: User Manual

SAnToS Laboratory

Last updated on June 10, 2005

Copyright © 2002-2005 Kansas State University

Table of Contents

1. Introduction

1.1. Trends in Software Model Checking

1.2. Bogor Overview

1.3. Installing Bogor

1.4. Using Bogor

1.4.1. Model Checking BIR Models
1.4.2. Counter-example Display
1.4.3. Random Simulation Mode
1.4.4. User-guided Simulation Mode
1.4.5. Selecting Core Model Checker Components
1.4.6. Bogor Command-line Interface

2. BIR: Bogor Modeling Language

2.1. Overview

2.2. System

2.3. Identifiers

2.4.1. Primitive Types
2.4.2. Non-Primitive Types
2.4.3. Alias Type
2.4.4. Generic Type
2.4.5. Fun Type

2.5. Literals

2.6. Constant Declaration

2.7. Enumeration Declaration

2.8. Record Declaration

2.9. Extension Declaration

2.9.1. Type Extension Declaration
2.9.2. Expression Extension Declaration
2.9.3. Action Extension Declaration

2.10. Type-alias Declaration

2.11. Global Variable Declaration

2.12. Thread and Function Declarations

2.12.1. Parameters and Local Variables

2.13. Low-level Thread or Function Body

2.13.1. Location
2.13.2. Transformation
2.13.3. Jump
2.13.4. Catch

2.14. High-level Thread or Function Body

2.14.1. Statement

2.15. Virtual Table Declaration

2.15.1. Record-based
2.15.2. Enumeration-based

2.16. Functional Expression Declaration

2.17. Expressions

2.17.1. Literal Expressions
2.17.2. Variable Expression
2.17.3. Unary Expression
2.17.4. Binary Expression
2.17.5. Conditional Expression
2.17.6. Parenthesis Expression
2.17.7. Atomic Expression
2.17.8. Record, Array, and Lock Creation Expressions
2.17.9. Field Access Expression
2.17.10. Array Access Expression
2.17.11. Cast Expression
2.17.12. Kind-of Expression
2.17.13. Instance-of Expression
2.17.14. Lock Test Expressions
2.17.15. Thread Test Expression
2.17.16. Let Binding Expression
2.17.17. Application Expression
2.17.18. Extension Call Expression

2.18. Actions

2.18.1. Assign Action
2.18.2. Assert Action
2.18.3. Assume Action
2.18.4. Lock Operation Action
2.18.5. Throw Exception Action
2.18.6. Start Thread Action
2.18.7. Exit Thread Action
2.18.8. Extension Call Action

3. Bogor Architecture

3.1. ISearcher: State Space Exploration

4. Extensions

4.1. Language Extension

4.1.1. Syntax Extension
4.1.2. Semantics Implementation

4.2. Module Extension

A. BIR Reference

A.1. Syntax
A.2. Semantics
A.3. Keywords

B. Bogor API

List of Figures

1.1. Declaration of set ADT and operations
1.2. Bogor Architecture
1.3. Bogor Counter Example Display
1.4. Eclipse Screen Shot
1.5. Creating a simple Eclipse project to contain BIR models
1.6. Creating a new BIR model
1.7. Bogor BIR Editor
1.8. A 2 Dining Philosophers BIR Model
1.9. Bogor Model Checker
1.10. Bogor Counter-example Display
1.11. Bogor User-guided Simulation
1.12. Selecting Branches in User-guided Simulation
1.13. Bogor Configuration
1.14. Configuring Module-specific Options
2.1. Concrete Syntax for Systems
2.2. Java AST for System
2.3. Concrete Syntax for Identifiers
2.4. Concrete Syntax for Types
2.5. Java AST of Syntactic Type
2.6. Concrete Syntax for Literals
2.7. Java AST for Literal
2.8. Concrete Syntax for Constant Declaration
2.9. Java AST for Constant Declaration
2.10. Concrete Syntax for Enumeration Declaration
2.11. Java AST for Enumeration Declaration
2.12. Concrete Syntax for Record Declaration
2.13. Java AST for Record Declaration
2.14. Concrete Syntax for Extension Declaration
2.15. Java AST for Extension Declaration
2.16. Concrete Syntax for Type-alias Declaration
2.17. Java AST for Type-alias Declaration
2.18. Concrete Syntax for Global Variable Declaration
2.19. Java AST for Global Variable Declaration
2.20. Concrete Syntax for Thread and Function Declarations
2.21. Java AST for Threads and Functions
2.22. Concrete Syntax for Low-level Thread or Function Body
2.23. Concrete Syntax for High-level Thread or Function Body
2.24. Java AST for Statement
2.25. Concrete Syntax for Virtual Table Declaration
2.26. Java AST for Virtual Table Declaration
2.27. Concrete Syntax for Functional Expression Declaration
2.28. Java AST for Functional Expression Declaration
2.29. Concrete Syntax for Expressions
2.30. Java AST for Expressions
2.31. Concrete Syntax for Actions
2.32. Java AST for Actions
3.1. Bogor Architecture
4.1. Declaration of set ADT and operations
4.2. Required methods for a Bogor extension module (IModule.java)
4.3. Method signatures for extension operator implementations
4.4. Required methods for any Bogor ADT extension type (INonPrimitiveExtValue.java)
4.5. Required operations for all set types (ISetValue.java)

		Next
		Chapter 1. Introduction