Design Article
DO-178C takes safety-critical software development to the next level
Tim King, DDC-I and Bill StClair, LDRA
4/2/2012 9:08 AM EDT
Model-based development and verification (MBD&V)
The incorporation of advanced modeling and objected oriented programming techniques places new demands on verification. The system must be verifiable and traceable at the model level, and verification evidence at the model level must be available to the broader verification and traceability framework.
In DO-178B, traceability is one-way and top-down, from the requirements to the target code, and provides no support for high-level modeling or object oriented programming. DO-178C introduces a distributed and collaborative two-way traceability mechanism that enables designers to trace from their models and requirements down to each line of code, and back from the code to the requirements and model, including all interceding work products and test cases.
The biggest and most contentious challenge in approving the MBD&V supplement was determining the final verification method used on the Executable Object Code (EOC) compiled, linked and loaded on the target system. In the context of the MBD&V systems under consideration, the EOC is directly traceable to the source code automatically generated by the model. Historically, there has been a precedent set in the verification of some avionics software that was tested both by and in the model itself without doing target testing on the EOC, effectively obviating the objectives for EOC testing in the DO-178C “core document.” Instead, the DO-178C plenary agreed that a form of independent verification must be performed on the EOC on the target system, thereby preserving the EOC objectives of DO-178C.
Notwithstanding the consensus reached with respect to EOC verification, the MBD&V supplement did add many objectives that provide certification credit for verification activities performed by the model, or at least defined by the model, on the model architecture and model code. These verification activities are primarily performed by “simulation cases,” which are run in lieu of test cases and other forms of verification.
Probably the most definitive of the FAQs added to any of the DO-178C tech supplements were those added to the MBD&V supplement. The scope of the new FAQs spans development and verification, including not only standard high- and low-level software requirements and the associated specification and design models, but also the system requirements allocated to software. Historically, the gaps between these model types and requirements hierarchies and their various provenances have been a leading cause of ambiguity and poorly realized designs in MBD&V projects.
Formal methods supplement
The Formal Methods supplement follows a similar trajectory to that of MBD&V in that it also eventually agrees to preserve the EOC objectives of the core document by stipulating independent verification for the EOC ultimately produced by formal methods or mathematical proofs. A key question that has not been definitively addressed by either the Formal Methods or MBD&V supplements is the obvious domain overlap that can occur between these supplements. That is, Formal Methods (FM) as a development and verification technology utilizes a form of model based development itself. This and other potential domain overlaps will be addressed by the FAA in circulars, which will be published this September.
Next: Tool qualification
The incorporation of advanced modeling and objected oriented programming techniques places new demands on verification. The system must be verifiable and traceable at the model level, and verification evidence at the model level must be available to the broader verification and traceability framework.
In DO-178B, traceability is one-way and top-down, from the requirements to the target code, and provides no support for high-level modeling or object oriented programming. DO-178C introduces a distributed and collaborative two-way traceability mechanism that enables designers to trace from their models and requirements down to each line of code, and back from the code to the requirements and model, including all interceding work products and test cases.
The biggest and most contentious challenge in approving the MBD&V supplement was determining the final verification method used on the Executable Object Code (EOC) compiled, linked and loaded on the target system. In the context of the MBD&V systems under consideration, the EOC is directly traceable to the source code automatically generated by the model. Historically, there has been a precedent set in the verification of some avionics software that was tested both by and in the model itself without doing target testing on the EOC, effectively obviating the objectives for EOC testing in the DO-178C “core document.” Instead, the DO-178C plenary agreed that a form of independent verification must be performed on the EOC on the target system, thereby preserving the EOC objectives of DO-178C.
Notwithstanding the consensus reached with respect to EOC verification, the MBD&V supplement did add many objectives that provide certification credit for verification activities performed by the model, or at least defined by the model, on the model architecture and model code. These verification activities are primarily performed by “simulation cases,” which are run in lieu of test cases and other forms of verification.
Probably the most definitive of the FAQs added to any of the DO-178C tech supplements were those added to the MBD&V supplement. The scope of the new FAQs spans development and verification, including not only standard high- and low-level software requirements and the associated specification and design models, but also the system requirements allocated to software. Historically, the gaps between these model types and requirements hierarchies and their various provenances have been a leading cause of ambiguity and poorly realized designs in MBD&V projects.
Formal methods supplement
The Formal Methods supplement follows a similar trajectory to that of MBD&V in that it also eventually agrees to preserve the EOC objectives of the core document by stipulating independent verification for the EOC ultimately produced by formal methods or mathematical proofs. A key question that has not been definitively addressed by either the Formal Methods or MBD&V supplements is the obvious domain overlap that can occur between these supplements. That is, Formal Methods (FM) as a development and verification technology utilizes a form of model based development itself. This and other potential domain overlaps will be addressed by the FAA in circulars, which will be published this September.
Next: Tool qualification
|
|
|
|
|
Navigate to related information