RTEMS Documentation Project RTEMS Software Engineering
  • 1. Preface
  • 2. RTEMS Project Mission Statement
    • 2.1. Free Software Project
    • 2.2. Design and Development Goals
    • 2.3. Open Development Environment
  • 3. RTEMS Stakeholders
  • 4. Introduction to Pre-Qualification
    • 4.1. Stakeholder Involvement
  • 5. Software Requirements Engineering
    • 5.1. Requirements for Requirements
      • 5.1.1. Identification
      • 5.1.2. Level of Requirements
        • 5.1.2.1. Absolute Requirements
        • 5.1.2.2. Absolute Prohibitions
        • 5.1.2.3. Recommendations
        • 5.1.2.4. Permissions
        • 5.1.2.5. Possibilities and Capabilities
      • 5.1.3. Syntax
      • 5.1.4. Wording Restrictions
      • 5.1.5. Separate Requirements
      • 5.1.6. Conflict Free Requirements
      • 5.1.7. Use of Project-Specific Terms and Abbreviations
      • 5.1.8. Justification of Requirements
      • 5.1.9. Requirement Validation
      • 5.1.10. Resources and Performance
    • 5.2. Specification Items
      • 5.2.1. Specification Item Hierarchy
      • 5.2.2. Specification Item Types
        • 5.2.2.1. Root Item Type
        • 5.2.2.2. Build Item Type
        • 5.2.2.3. Build Ada Test Program Item Type
        • 5.2.2.4. Build BSP Item Type
        • 5.2.2.5. Build Configuration File Item Type
        • 5.2.2.6. Build Configuration Header Item Type
        • 5.2.2.7. Build Group Item Type
        • 5.2.2.8. Build Library Item Type
        • 5.2.2.9. Build Objects Item Type
        • 5.2.2.10. Build Option Item Type
        • 5.2.2.11. Build Script Item Type
        • 5.2.2.12. Build Start File Item Type
        • 5.2.2.13. Build Test Program Item Type
        • 5.2.2.14. Constraint Item Type
        • 5.2.2.15. Glossary Item Type
        • 5.2.2.16. Glossary Group Item Type
        • 5.2.2.17. Glossary Term Item Type
        • 5.2.2.18. Interface Item Type
        • 5.2.2.19. Application Configuration Group Item Type
        • 5.2.2.20. Application Configuration Option Item Type
        • 5.2.2.21. Application Configuration Feature Enable Option Item Type
        • 5.2.2.22. Application Configuration Feature Option Item Type
        • 5.2.2.23. Application Configuration Value Option Item Type
        • 5.2.2.24. Interface Compound Item Type
        • 5.2.2.25. Interface Define Item Type
        • 5.2.2.26. Interface Domain Item Type
        • 5.2.2.27. Interface Enum Item Type
        • 5.2.2.28. Interface Enumerator Item Type
        • 5.2.2.29. Interface Forward Declaration Item Type
        • 5.2.2.30. Interface Function or Macro Item Type
        • 5.2.2.31. Interface Group Item Type
        • 5.2.2.32. Interface Header File Item Type
        • 5.2.2.33. Interface Typedef Item Type
        • 5.2.2.34. Interface Unspecified Header File Item Type
        • 5.2.2.35. Interface Unspecified Item Type
        • 5.2.2.36. Interface Variable Item Type
        • 5.2.2.37. Register Block Item Type
        • 5.2.2.38. Proxy Item Types
        • 5.2.2.39. Requirement Item Type
        • 5.2.2.40. Functional Requirement Item Type
        • 5.2.2.41. Action Requirement Item Type
        • 5.2.2.42. Generic Functional Requirement Item Type
        • 5.2.2.43. Non-Functional Requirement Item Type
        • 5.2.2.44. Design Group Requirement Item Type
        • 5.2.2.45. Design Target Item Type
        • 5.2.2.46. Generic Non-Functional Requirement Item Type
        • 5.2.2.47. Runtime Measurement Environment Item Type
        • 5.2.2.48. Runtime Performance Requirement Item Type
        • 5.2.2.49. Requirement Validation Item Type
        • 5.2.2.50. Requirement Validation Method
        • 5.2.2.51. Runtime Measurement Test Item Type
        • 5.2.2.52. Specification Item Type
        • 5.2.2.53. Test Case Item Type
        • 5.2.2.54. Test Platform Item Type
        • 5.2.2.55. Test Procedure Item Type
        • 5.2.2.56. Test Suite Item Type
      • 5.2.3. Specification Attribute Sets and Value Types
        • 5.2.3.1. Action Requirement Boolean Expression
        • 5.2.3.2. Action Requirement Condition
        • 5.2.3.3. Action Requirement Expression
        • 5.2.3.4. Action Requirement Expression Condition Set
        • 5.2.3.5. Action Requirement Expression State Name
        • 5.2.3.6. Action Requirement Expression State Set
        • 5.2.3.7. Action Requirement Name
        • 5.2.3.8. Action Requirement Skip Reasons
        • 5.2.3.9. Action Requirement State
        • 5.2.3.10. Action Requirement Transition
        • 5.2.3.11. Action Requirement Transition Post-Condition State
        • 5.2.3.12. Action Requirement Transition Post-Conditions
        • 5.2.3.13. Action Requirement Transition Pre-Condition State Set
        • 5.2.3.14. Action Requirement Transition Pre-Conditions
        • 5.2.3.15. Application Configuration Option Name
        • 5.2.3.16. Boolean or Integer or String
        • 5.2.3.17. Build Assembler Option
        • 5.2.3.18. Build C Compiler Option
        • 5.2.3.19. Build C Preprocessor Option
        • 5.2.3.20. Build C++ Compiler Option
        • 5.2.3.21. Build Dependency Conditional Link Role
        • 5.2.3.22. Build Dependency Link Role
        • 5.2.3.23. Build Include Path
        • 5.2.3.24. Build Install Directive
        • 5.2.3.25. Build Install Path
        • 5.2.3.26. Build Link Static Library Directive
        • 5.2.3.27. Build Linker Option
        • 5.2.3.28. Build Option Action
        • 5.2.3.29. Build Option C Compiler Check Action
        • 5.2.3.30. Build Option C++ Compiler Check Action
        • 5.2.3.31. Build Option Name
        • 5.2.3.32. Build Option Set Test State Action
        • 5.2.3.33. Build Option Value
        • 5.2.3.34. Build Source
        • 5.2.3.35. Build Target
        • 5.2.3.36. Build Test State
        • 5.2.3.37. Build Use After Directive
        • 5.2.3.38. Build Use Before Directive
        • 5.2.3.39. Constraint Link Role
        • 5.2.3.40. Copyright
        • 5.2.3.41. Enabled-By Expression
        • 5.2.3.42. External Document Reference
        • 5.2.3.43. External File Reference
        • 5.2.3.44. External Reference
        • 5.2.3.45. Function Implementation Link Role
        • 5.2.3.46. Generic External Reference
        • 5.2.3.47. Glossary Membership Link Role
        • 5.2.3.48. Integer or String
        • 5.2.3.49. Interface Brief Description
        • 5.2.3.50. Interface Compound Definition Kind
        • 5.2.3.51. Interface Compound Member Compound
        • 5.2.3.52. Interface Compound Member Declaration
        • 5.2.3.53. Interface Compound Member Definition
        • 5.2.3.54. Interface Compound Member Definition Directive
        • 5.2.3.55. Interface Compound Member Definition Variant
        • 5.2.3.56. Interface Definition
        • 5.2.3.57. Interface Definition Directive
        • 5.2.3.58. Interface Definition Variant
        • 5.2.3.59. Interface Description
        • 5.2.3.60. Interface Enabled-By Expression
        • 5.2.3.61. Interface Enum Definition Kind
        • 5.2.3.62. Interface Enumerator Link Role
        • 5.2.3.63. Interface Function Link Role
        • 5.2.3.64. Interface Function or Macro Definition
        • 5.2.3.65. Interface Function or Macro Definition Directive
        • 5.2.3.66. Interface Function or Macro Definition Variant
        • 5.2.3.67. Interface Group Identifier
        • 5.2.3.68. Interface Group Membership Link Role
        • 5.2.3.69. Interface Hidden Group Membership Link Role
        • 5.2.3.70. Interface Include Link Role
        • 5.2.3.71. Interface Notes
        • 5.2.3.72. Interface Parameter
        • 5.2.3.73. Interface Parameter Direction
        • 5.2.3.74. Interface Placement Link Role
        • 5.2.3.75. Interface Return Directive
        • 5.2.3.76. Interface Return Value
        • 5.2.3.77. Interface Target Link Role
        • 5.2.3.78. Link
        • 5.2.3.79. Name
        • 5.2.3.80. Optional Floating-Point Number
        • 5.2.3.81. Optional Integer
        • 5.2.3.82. Optional String
        • 5.2.3.83. Performance Runtime Limits Link Role
        • 5.2.3.84. Placement Order Link Role
        • 5.2.3.85. Proxy Member Link Role
        • 5.2.3.86. Register Bits Definition
        • 5.2.3.87. Register Bits Definition Directive
        • 5.2.3.88. Register Bits Definition Variant
        • 5.2.3.89. Register Block Include Role
        • 5.2.3.90. Register Block Member Definition
        • 5.2.3.91. Register Block Member Definition Directive
        • 5.2.3.92. Register Block Member Definition Variant
        • 5.2.3.93. Register Definition
        • 5.2.3.94. Register Name
        • 5.2.3.95. Requirement Design Group Identifier
        • 5.2.3.96. Requirement Refinement Link Role
        • 5.2.3.97. Requirement Text
        • 5.2.3.98. Requirement Validation Link Role
        • 5.2.3.99. Runtime Measurement Environment Name
        • 5.2.3.100. Runtime Measurement Environment Table
        • 5.2.3.101. Runtime Measurement Parameter Set
        • 5.2.3.102. Runtime Measurement Request Link Role
        • 5.2.3.103. Runtime Measurement Value Kind
        • 5.2.3.104. Runtime Measurement Value Table
        • 5.2.3.105. Runtime Performance Parameter Set
        • 5.2.3.106. SHA256 Hash Value
        • 5.2.3.107. SPDX License Identifier
        • 5.2.3.108. Specification Attribute Set
        • 5.2.3.109. Specification Attribute Value
        • 5.2.3.110. Specification Boolean Value
        • 5.2.3.111. Specification Explicit Attributes
        • 5.2.3.112. Specification Floating-Point Assert
        • 5.2.3.113. Specification Floating-Point Value
        • 5.2.3.114. Specification Generic Attributes
        • 5.2.3.115. Specification Information
        • 5.2.3.116. Specification Integer Assert
        • 5.2.3.117. Specification Integer Value
        • 5.2.3.118. Specification List
        • 5.2.3.119. Specification Mandatory Attributes
        • 5.2.3.120. Specification Member Link Role
        • 5.2.3.121. Specification Refinement Link Role
        • 5.2.3.122. Specification String Assert
        • 5.2.3.123. Specification String Value
        • 5.2.3.124. Test Case Action
        • 5.2.3.125. Test Case Check
        • 5.2.3.126. Test Context Member
        • 5.2.3.127. Test Header
        • 5.2.3.128. Test Run Parameter
        • 5.2.3.129. Test Support Method
        • 5.2.3.130. UID
        • 5.2.3.131. Unit Test Link Role
    • 5.3. Traceability of Specification Items
      • 5.3.1. History of Specification Items
      • 5.3.2. Backward Traceability of Specification Items
      • 5.3.3. Forward Traceability of Specification Items
      • 5.3.4. Traceability between Software Requirements, Architecture and Design
    • 5.4. Requirement Management
      • 5.4.1. Change Control Board
      • 5.4.2. Add a Requirement
      • 5.4.3. Modify a Requirement
      • 5.4.4. Mark a Requirement as Obsolete
    • 5.5. Tooling
      • 5.5.1. Tool Requirements
      • 5.5.2. Tool Evaluation
      • 5.5.3. Best Available Tool - Doorstop
      • 5.5.4. Custom Requirements Management Tool
    • 5.6. How-To
      • 5.6.1. Getting Started
      • 5.6.2. View the Specification Graph
      • 5.6.3. Generate Files from Specification Items
      • 5.6.4. Application Configuration Options
        • 5.6.4.1. Modify an Existing Group
        • 5.6.4.2. Modify an Existing Option
        • 5.6.4.3. Add a New Group
        • 5.6.4.4. Add a New Option
        • 5.6.4.5. Generate Content after Changes
      • 5.6.5. Glossary Specification
      • 5.6.6. Interface Specification
        • 5.6.6.1. Specify an API Header File
        • 5.6.6.2. Specify an API Element
      • 5.6.7. Requirements Depending on Build Configuration Options
      • 5.6.8. Requirements Depending on Application Configuration Options
      • 5.6.9. Action Requirements
        • 5.6.9.1. Example
        • 5.6.9.2. Pre-Condition Templates
        • 5.6.9.3. Post-Condition Templates
      • 5.6.10. Validation Test Guidelines
      • 5.6.11. Verify the Specification Items
  • 6. Software Development Management
    • 6.1. Software Development (Git Users)
      • 6.1.1. Browse the Git Repository Online
      • 6.1.2. Using the Git Repository
      • 6.1.3. Making Changes
      • 6.1.4. Working with Branches
      • 6.1.5. Viewing Changes
      • 6.1.6. Reverting Changes
      • 6.1.7. git reset
      • 6.1.8. git revert
      • 6.1.9. Merging Changes
      • 6.1.10. Rebasing
      • 6.1.11. Accessing a Developer’s Repository
      • 6.1.12. Commit Message Guidance
      • 6.1.13. Creating a Patch
      • 6.1.14. Submitting a Patch
      • 6.1.15. Configuring git send-email to use Gmail
      • 6.1.16. Sending Email
      • 6.1.17. Manage Your Code
      • 6.1.18. Private Servers
      • 6.1.19. Learn more about Git
    • 6.2. Software Development (Git Writers)
      • 6.2.1. SSH Access
      • 6.2.2. Personal Repository
      • 6.2.3. Create a personal repository
        • 6.2.3.1. Check your setup
        • 6.2.3.2. Push commits to personal repo master from local master
        • 6.2.3.3. Push a branch onto personal repo
        • 6.2.3.4. Update from upstream master (RTEMS head)
      • 6.2.4. Migrate a Personal Repository to top-level
      • 6.2.5. GIT Push Configuration
      • 6.2.6. Pull a Developer’s Repo
      • 6.2.7. Committing
        • 6.2.7.1. Ticket Updates
        • 6.2.7.2. Commands
      • 6.2.8. Pushing Multiple Commits
      • 6.2.9. Ooops!
    • 6.3. Coding Standards
      • 6.3.1. Coding Conventions
        • 6.3.1.1. Source Documentation
        • 6.3.1.2. Licenses
        • 6.3.1.3. Language and Compiler
        • 6.3.1.4. Readability
        • 6.3.1.5. Robustness
        • 6.3.1.6. Portability
        • 6.3.1.7. Maintainability
        • 6.3.1.8. Performance
        • 6.3.1.9. Miscellaneous
        • 6.3.1.10. Header Files
        • 6.3.1.11. Layering
        • 6.3.1.12. Exceptions to the Rules
        • 6.3.1.13. Tools
      • 6.3.2. Formatting
        • 6.3.2.1. Rules
        • 6.3.2.2. Eighty Character Line Limit
        • 6.3.2.3. Breaking Long Lines
      • 6.3.3. Deprectating Interfaces
        • 6.3.3.1. Use the deprecate attribute
        • 6.3.3.2. Add a warning
        • 6.3.3.3. Update documentation
        • 6.3.3.4. Update support code
        • 6.3.3.5. Disable deprecated warnings
        • 6.3.3.6. Add a release note
      • 6.3.4. Doxygen Guidelines
        • 6.3.4.1. Group Names
        • 6.3.4.2. Use Groups
        • 6.3.4.3. Files
        • 6.3.4.4. Type Definitions
        • 6.3.4.5. Function Declarations
        • 6.3.4.6. Header File Examples
      • 6.3.5. File Templates
        • 6.3.5.1. Copyright and License Block
        • 6.3.5.2. C/C++ Header File Template
        • 6.3.5.3. C/C++/Assembler Source File Template
        • 6.3.5.4. Python File Template
        • 6.3.5.5. Shell Scripts
        • 6.3.5.6. reStructuredText File Template
      • 6.3.6. Naming Rules
        • 6.3.6.1. General Rules
    • 6.4. Documentation Guidelines
      • 6.4.1. Application Configuration Options
    • 6.5. Python Development Guidelines
      • 6.5.1. Python Language Versions
      • 6.5.2. Python Code Formatting
      • 6.5.3. Static Analysis Tools
      • 6.5.4. Type Annotations
      • 6.5.5. Testing
        • 6.5.5.1. Test Organization
      • 6.5.6. Documentation
      • 6.5.7. Existing Code
      • 6.5.8. Third-Party Code
    • 6.6. Change Management
    • 6.7. Issue Tracking
  • 7. Software Test Plan Assurance and Procedures
    • 7.1. Testing and Coverage
      • 7.1.1. Test Suites
        • 7.1.1.1. Legacy Test Suites
      • 7.1.2. RTEMS Tester
  • 8. Software Test Framework
    • 8.1. The RTEMS Test Framework
      • 8.1.1. Nomenclature
      • 8.1.2. Test Cases
      • 8.1.3. Test Fixture
      • 8.1.4. Test Case Planning
      • 8.1.5. Test Case Resource Accounting
      • 8.1.6. Test Case Scoped Dynamic Memory
      • 8.1.7. Test Case Destructors
      • 8.1.8. Test Checks
        • 8.1.8.1. Test Check Variant Conventions
        • 8.1.8.2. Test Check Parameter Conventions
        • 8.1.8.3. Test Check Condition Conventions
        • 8.1.8.4. Test Check Type Conventions
        • 8.1.8.5. Integers
        • 8.1.8.6. Boolean Expressions
        • 8.1.8.7. Generic Types
        • 8.1.8.8. Pointers
        • 8.1.8.9. Memory Areas
        • 8.1.8.10. Strings
        • 8.1.8.11. Characters
        • 8.1.8.12. RTEMS Status Codes
        • 8.1.8.13. POSIX Error Numbers
        • 8.1.8.14. POSIX Status Codes
      • 8.1.9. Log Messages and Formatted Output
      • 8.1.10. Utility
      • 8.1.11. Time Services
      • 8.1.12. Code Runtime Measurements
      • 8.1.13. Interrupt Tests
      • 8.1.14. Test Runner
      • 8.1.15. Test Verbosity
      • 8.1.16. Test Reporting
      • 8.1.17. Test Report Validation
      • 8.1.18. Supported Platforms
    • 8.2. Test Framework Requirements for RTEMS
      • 8.2.1. License Requirements
      • 8.2.2. Portability Requirements
      • 8.2.3. Reporting Requirements
      • 8.2.4. Environment Requirements
      • 8.2.5. Usability Requirements
      • 8.2.6. Performance Requirements
    • 8.3. Off-the-shelf Test Frameworks
      • 8.3.1. bdd-for-c
      • 8.3.2. CBDD
      • 8.3.3. Google Test
      • 8.3.4. Unity
    • 8.4. Standard Test Report Formats
      • 8.4.1. JUnit XML
      • 8.4.2. Test Anything Protocol
  • 9. Formal Verification
    • 9.1. Formal Verification Overview
    • 9.2. Formal Verification Approaches
      • 9.2.1. Formal Methods Overview
      • 9.2.2. Formal Methods actively considered
        • 9.2.2.1. Frama-C
        • 9.2.2.2. Isabelle/HOL
      • 9.2.3. Formal Method actually used
        • 9.2.3.1. Promela/SPIN
    • 9.3. Test Generation Methodology
      • 9.3.1. Model desired behavior
      • 9.3.2. Make claims about undesired behavior
      • 9.3.3. Map good behavior scenarios to tests
    • 9.4. Formal Tools Setup
      • 9.4.1. Installing Tools
        • 9.4.1.1. Installing Promela/SPIN
        • 9.4.1.2. Installing Test Generation Tools
      • 9.4.2. Tool Configuration
        • 9.4.2.1. Testsuite Setup
      • 9.4.3. Running Test Generation
    • 9.5. Modelling with Promela
      • 9.5.1. Promela Execution
        • 9.5.1.1. Simulation vs. Verification
      • 9.5.2. Promela Datatypes
      • 9.5.3. Promela Declarations
        • 9.5.3.1. Special Identifiers
      • 9.5.4. Promela Atomic Statements
      • 9.5.5. Promela Composite Statements
      • 9.5.6. Promela Top-Level
    • 9.6. Promela to C Refinement
      • 9.6.1. Model Annotations
        • 9.6.1.1. Annotation Syntax
      • 9.6.2. Annotation Lookup
      • 9.6.3. Specifying Refinement
        • 9.6.3.1. Lookup Example
      • 9.6.4. Annotation Refinement Guide
        • 9.6.4.1. LOG
        • 9.6.4.2. NAME
        • 9.6.4.3. INIT
        • 9.6.4.4. TASK
        • 9.6.4.5. SIGNAL
        • 9.6.4.6. WAIT
        • 9.6.4.7. DEF
        • 9.6.4.8. DECL
        • 9.6.4.9. DCLARRAY
        • 9.6.4.10. CALL
        • 9.6.4.11. STATE
        • 9.6.4.12. STRUCT
        • 9.6.4.13. SEQ
        • 9.6.4.14. PTR
        • 9.6.4.15. SCALAR
        • 9.6.4.16. END
        • 9.6.4.17. SUSPEND and WAKEUP
      • 9.6.5. Annotation Ordering
      • 9.6.6. Test Code Assembly
        • 9.6.6.1. Scenario Generation
        • 9.6.6.2. Test Code Generation
        • 9.6.6.3. Test Code Deployment
        • 9.6.6.4. Performing Tests
      • 9.6.7. Traceability
  • 10. BSP Build System
    • 10.1. Goals
    • 10.2. Overview
    • 10.3. Commands
      • 10.3.1. BSP List
      • 10.3.2. BSP Defaults
      • 10.3.3. Configure
      • 10.3.4. Build, Clean, and Install
    • 10.4. UID Naming Conventions
    • 10.5. Build Specification Items
    • 10.6. How-To
      • 10.6.1. Find the Right Item
      • 10.6.2. Create a BSP Architecture
      • 10.6.3. Create a BSP Family
      • 10.6.4. Add a Base BSP to a BSP Family
      • 10.6.5. Add a BSP Option
      • 10.6.6. Extend a BSP Family with a Group
      • 10.6.7. Add a Test Program
      • 10.6.8. Add a Library
      • 10.6.9. Add an Object
  • 11. Software Release Management
    • 11.1. Release Process
      • 11.1.1. Releases
        • 11.1.1.1. Release Layout
        • 11.1.1.2. Release Version Numbering
        • 11.1.1.3. Release Scripts
        • 11.1.1.4. Release Snapshots
      • 11.1.2. Release Repositories
      • 11.1.3. Pre-Release Procedure
      • 11.1.4. Release Branching
        • 11.1.4.1. LibBSD Release Branch
        • 11.1.4.2. Pre-Branch Procedure
        • 11.1.4.3. Branch Procedure
        • 11.1.4.4. Post-Branch Procedure
      • 11.1.5. Release Procedure
      • 11.1.6. Post-Release Procedure
      • 11.1.7. VERSION File Format
    • 11.2. Software Change Report Generation
    • 11.3. Version Description Document (VDD) Generation
  • 12. User’s Manuals
    • 12.1. Documentation Style Guidelines
  • 13. Licensing Requirements
    • 13.1. Rationale
    • 13.2. License restrictions
  • 14. Appendix: Core Qualification Artifacts/Documents
  • 15. Appendix: RTEMS Formal Model Guide
    • 15.1. Testing Chains
      • 15.1.1. API Model
        • 15.1.1.1. Data Structures
        • 15.1.1.2. Function Calls
      • 15.1.2. Behavior patterns
      • 15.1.3. Annotations
        • 15.1.3.1. Data Structures
        • 15.1.3.2. Function Calls
      • 15.1.4. Refinement
        • 15.1.4.1. Data Structures
        • 15.1.4.2. Function Calls
    • 15.2. Testing Concurrent Managers
      • 15.2.1. Testing Strategy
      • 15.2.2. Model Structure
      • 15.2.3. Transforming Model Behavior to C Code
    • 15.3. Testing the Event Manager
      • 15.3.1. API Model
        • 15.3.1.1. Event Send
        • 15.3.1.2. Event Receive
      • 15.3.2. Behaviour Patterns
        • 15.3.2.1. Task Scheduling
        • 15.3.2.2. Scenarios
        • 15.3.2.3. Sender Process (Worker Task)
        • 15.3.2.4. Receiver Process (Runner Task)
        • 15.3.2.5. System Process
        • 15.3.2.6. Clock Process
        • 15.3.2.7. init Process
      • 15.3.3. Annotations
      • 15.3.4. Refinement
    • 15.4. Testing the Barrier Mananger
      • 15.4.1. API Model
      • 15.4.2. Behaviour Patterns
      • 15.4.3. Annotations
      • 15.4.4. Refinement
    • 15.5. Testing the Message Manager
      • 15.5.1. API Model
      • 15.5.2. Behaviour Patterns
      • 15.5.3. Annotations
      • 15.5.4. Refinement
    • 15.6. Current State of Play
      • 15.6.1. Model State
      • 15.6.2. Model Refactoring
      • 15.6.3. Test Code Refactoring
  • 16. Glossary
  • 17. References
Index
RTEMS Software Engineering
  • 9. Formal Verification
  • <no title>
  • 9.4. Formal Tools Setup
    • 9.4.1. Installing Tools
      • 9.4.1.1. Installing Promela/SPIN
      • 9.4.1.2. Installing Test Generation Tools
    • 9.4.2. Tool Configuration
      • 9.4.2.1. Testsuite Setup
    • 9.4.3. Running Test Generation
  • 9.5. Modelling with Promela
    • 9.5.1. Promela Execution
      • 9.5.1.1. Simulation vs. Verification
    • 9.5.2. Promela Datatypes
    • 9.5.3. Promela Declarations
      • 9.5.3.1. Special Identifiers
    • 9.5.4. Promela Atomic Statements
    • 9.5.5. Promela Composite Statements
    • 9.5.6. Promela Top-Level
  • 9.6. Promela to C Refinement
    • 9.6.1. Model Annotations
      • 9.6.1.1. Annotation Syntax
    • 9.6.2. Annotation Lookup
    • 9.6.3. Specifying Refinement
      • 9.6.3.1. Lookup Example
    • 9.6.4. Annotation Refinement Guide
      • 9.6.4.1. LOG
      • 9.6.4.2. NAME
      • 9.6.4.3. INIT
      • 9.6.4.4. TASK
      • 9.6.4.5. SIGNAL
      • 9.6.4.6. WAIT
      • 9.6.4.7. DEF
      • 9.6.4.8. DECL
      • 9.6.4.9. DCLARRAY
      • 9.6.4.10. CALL
      • 9.6.4.11. STATE
      • 9.6.4.12. STRUCT
      • 9.6.4.13. SEQ
      • 9.6.4.14. PTR
      • 9.6.4.15. SCALAR
      • 9.6.4.16. END
      • 9.6.4.17. SUSPEND and WAKEUP
    • 9.6.5. Annotation Ordering
    • 9.6.6. Test Code Assembly
      • 9.6.6.1. Scenario Generation
      • 9.6.6.2. Test Code Generation
      • 9.6.6.3. Test Code Deployment
      • 9.6.6.4. Performing Tests
    • 9.6.7. Traceability
Previous Next

© Copyright 1988, 2024 RTEMS Project and contributors.

Built with Sphinx using a theme provided by Read the Docs.