RTEMS Documentation Project
RTEMS Software Engineering
6.150c2e8
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 Default Value
5.2.3.32. Build Option Name
5.2.3.33. Build Option Set Test State Action
5.2.3.34. Build Option Value
5.2.3.35. Build Source
5.2.3.36. Build Target
5.2.3.37. Build Test State
5.2.3.38. Build Use After Directive
5.2.3.39. Build Use Before Directive
5.2.3.40. Constraint Link Role
5.2.3.41. Copyright
5.2.3.42. Enabled-By Expression
5.2.3.43. External Document Reference
5.2.3.44. External File Reference
5.2.3.45. External Reference
5.2.3.46. Function Implementation Link Role
5.2.3.47. Generic External Reference
5.2.3.48. Glossary Membership Link Role
5.2.3.49. Integer or String
5.2.3.50. Interface Brief Description
5.2.3.51. Interface Compound Definition Kind
5.2.3.52. Interface Compound Member Compound
5.2.3.53. Interface Compound Member Declaration
5.2.3.54. Interface Compound Member Definition
5.2.3.55. Interface Compound Member Definition Directive
5.2.3.56. Interface Compound Member Definition Variant
5.2.3.57. Interface Definition
5.2.3.58. Interface Definition Directive
5.2.3.59. Interface Definition Variant
5.2.3.60. Interface Description
5.2.3.61. Interface Enabled-By Expression
5.2.3.62. Interface Enum Definition Kind
5.2.3.63. Interface Enumerator Link Role
5.2.3.64. Interface Function Link Role
5.2.3.65. Interface Function or Macro Definition
5.2.3.66. Interface Function or Macro Definition Directive
5.2.3.67. Interface Function or Macro Definition Variant
5.2.3.68. Interface Group Identifier
5.2.3.69. Interface Group Membership Link Role
5.2.3.70. Interface Hidden Group Membership Link Role
5.2.3.71. Interface Include Link Role
5.2.3.72. Interface Notes
5.2.3.73. Interface Parameter
5.2.3.74. Interface Parameter Direction
5.2.3.75. Interface Placement Link Role
5.2.3.76. Interface Return Directive
5.2.3.77. Interface Return Value
5.2.3.78. Interface Target Link Role
5.2.3.79. Link
5.2.3.80. Name
5.2.3.81. Optional Floating-Point Number
5.2.3.82. Optional Integer
5.2.3.83. Optional String
5.2.3.84. Performance Runtime Limits Link Role
5.2.3.85. Placement Order Link Role
5.2.3.86. Proxy Member Link Role
5.2.3.87. Register Bits Definition
5.2.3.88. Register Bits Definition Directive
5.2.3.89. Register Bits Definition Variant
5.2.3.90. Register Block Include Role
5.2.3.91. Register Block Member Definition
5.2.3.92. Register Block Member Definition Directive
5.2.3.93. Register Block Member Definition Variant
5.2.3.94. Register Definition
5.2.3.95. Register Name
5.2.3.96. Requirement Design Group Identifier
5.2.3.97. Requirement Refinement Link Role
5.2.3.98. Requirement Text
5.2.3.99. Requirement Validation Link Role
5.2.3.100. Runtime Measurement Environment Name
5.2.3.101. Runtime Measurement Environment Table
5.2.3.102. Runtime Measurement Parameter Set
5.2.3.103. Runtime Measurement Request Link Role
5.2.3.104. Runtime Measurement Value Kind
5.2.3.105. Runtime Measurement Value Table
5.2.3.106. Runtime Performance Parameter Set
5.2.3.107. SHA256 Hash Value
5.2.3.108. SPDX License Identifier
5.2.3.109. Specification Attribute Set
5.2.3.110. Specification Attribute Value
5.2.3.111. Specification Boolean Value
5.2.3.112. Specification Explicit Attributes
5.2.3.113. Specification Floating-Point Assert
5.2.3.114. Specification Floating-Point Value
5.2.3.115. Specification Generic Attributes
5.2.3.116. Specification Information
5.2.3.117. Specification Integer Assert
5.2.3.118. Specification Integer Value
5.2.3.119. Specification List
5.2.3.120. Specification Mandatory Attributes
5.2.3.121. Specification Member Link Role
5.2.3.122. Specification Refinement Link Role
5.2.3.123. Specification String Assert
5.2.3.124. Specification String Value
5.2.3.125. Test Case Action
5.2.3.126. Test Case Check
5.2.3.127. Test Context Member
5.2.3.128. Test Header
5.2.3.129. Test Run Parameter
5.2.3.130. Test Support Method
5.2.3.131. UID
5.2.3.132. 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. Troubleshooting
6.1.18. Manage Your Code
6.1.19. Private Servers
6.1.20. 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.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.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
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