RTEMS Software Engineering (6.17c582f)

Copyrights and License

© 2022 Trinity College Dublin

© 2018, 2020 embedded brains GmbH & Co. KG

© 2018, 2020 Sebastian Huber

© 1988, 2015 On-Line Applications Research Corporation (OAR)

This document is available under the Creative Commons Attribution-ShareAlike 4.0 International Public License.

The authors have used their best efforts in preparing this material. These efforts include the development, research, and testing of the theories and programs to determine their effectiveness. No warranty of any kind, expressed or implied, with regard to the software or the material contained in this document is provided. No liability arising out of the application or use of any product described in this document is assumed. The authors reserve the right to revise this material and to make changes from time to time in the content hereof without obligation to notify anyone of such revision or changes.

The RTEMS Project is hosted at https://www.rtems.org. Any inquiries concerning RTEMS, its related support components, or its documentation should be directed to the RTEMS Project community.

RTEMS Online Resources

Home	https://www.rtems.org
Documentation	https://docs.rtems.org
Mailing Lists	https://lists.rtems.org
Bug Reporting	https://gitlab.rtems.org
Git Repositories	https://gitlab.rtems.org
Developers	https://gitlab.rtems.org

• 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. Release Maintenance
    • 11.2.1. Release Branch Maintenance
    • 11.2.2. Release Labels
    • 11.2.3. Release Epics and Issues
    • 11.2.4. Release Merge Requests
  • 11.3. Software Change Report Generation
  • 11.4. 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