1. Introduction
The client required support in development of flight control system software. This software has to meet DO-178C Level A and they wanted to develop this software through taking advantage of D-RisQ automatic verification tools in order to achieve significant cost savings. This case study describes the use of tools and the support provided for the initial development of the software.
2. Certification - Use of DO-178C/DO-333
The software will have to be assessed by a regulator for compliance to RTCA DO-178C. This case study will not go into detail on this process but a short overview is provided here. There are over 70 Objectives to be met, some related to Planning, Configuration Management, Software QA and Certification Liaison which are described in DO-178C. While these are accounted for, the focus is on verification as this is where cost savings can be made. The D-RisQ tools are built upon automated formal methods and hence DO-333, the Formal Methods Supplement to DO-178C is used. The diagram at Figure 1 outlines the verification objectives that have to be met for DO-333:
The focus is on objectives relating to System Requirements, High Level Requirements and Design, ie Objectives FM.A-3 and FM.A-4, followed by source code to meet FM.A-5 and afterwards, Executable Object Code to meet FM.A-6 and then coverage objectives in FM.A-7. Within the above figure it can be seen that there 4 groups of Additional Objectives. These are specific to the use of Formal Methods and claims for certification credit. These are largely covered by Tool Qualification under DO-330 and details of which are not covered in this case study.
3. Requirements
There are at least 3 levels of requirements necessary for development of software:
• System requirements: These should be developed by the systems engineer and include safety requirements that specifically address hazards identified by a Functional Hazard Analysis and linked to a Preliminary System Safety Assessment. They identify what needs to be achieved at a systems level and should not, with some exceptions, contain any implementation detail.
• Software High Level Requirements (HLR): these are a translation of the system requirements into a form that is useful to a software engineer. They describe what needs to be achieved by software developers and are used by testers and regulators.
• Software Low Level Requirements (LLR): these are a translation of the HLRs into a design (which also incorporates software architecture). From these a developer can produce source code.
Separation between these different sets of requirements is important to enable effective verification giving multiple opportunities for increasing understanding and for error detection. The client required assistance in ensuring that system requirements and HLRs were well written.
4. Writing Good Requirements
D-RisQ were passed 3 documents that represented the System Requirements, an Interface Control Document and the HLRs. Combined these documents were 200 pages long. On initial review we found a number of issues:
• Each of the documents contained a mix of system requirements, software HLRs and design detail; there was therefore overlap and unnecessary duplication.
• System requirements were too detailed.
• There were errors in the requirements.
• There was no link to safety.
Had the development continued with these documents, there would have been major re-work required later in the project. This would have been needed in order to provide effective verification evidence and hence to support certification. We had no view of a Preliminary System Safety Assessment or Functional Hazard Analysis, so were operating in isolation of these documents. We decided to use Kapture® as the focus for our efforts to undertake the following:
• Distil Software HLRs from both documents (written using Kapture®).
• Remaining text to be reviewed and written as System Requirements.
• Design to be completely removed from both documents (more on this later)
• Provide trace information to/from our suggested System Requirements and the HLRs.
• Provide a trace matrix from our suggested set of requirements to the original set.
• Measure effort to do the above work
• Link the outcomes to certification objectives
5. Outcomes
5.1 Speeding up the process – Kapture® Development
Following a brief review, it was found that we had an opportunity to add a feature to Kapture® that would enable users to write software HLRs more efficiently. Development of this new feature took about 1 week and was used on an experimental branch of Kapture® development. Note that this new Kapture® feature was not necessary to produce the HLRs, it just made it easier.
5.2 Production of Software High Level Requirements (HLRs)
We produced a library of user defined functions in Kapture® and then we populated the library with the actual signal names used. This included expansion of signal sets described in the library into specific instantiations. The result was that we had produced verifiable, unambiguous, consistent software HLRs. These comply with Requirements Standards thus relieving the cost associated with a review and providing compliance to DO-333 sections:
• FM.6.3.b, FM.6.3.c, FM.6.3.1.b (see Annex A FM.A-3 Objective 2 ‘High-level requirements are accurate and consistent’ ).
• FM.6.3.e and FM.6.3.1.d (see Annex A FM.A-3 Objective 4 ‘High-level requirements are verifiable’).
• FM.6.3.f and FM.6.3.1.e (see Annex A FM.A-3 Objective 5 ‘High-level requirements conform to standards’).
5.3 Production of System Requirements
While this effort was underway, we were also distilling much clearer system requirements from the original documents. These were suitable for tracing to the suggested software HLRs and showing that these did completely, accurately and unambiguously encapsulate the system requirements. A review of HLRs against this set of system requirements, including the trace information, was undertaken. This gave compliance to DO-333 sections:
• FM.6.3.a, FM.6.3.1.a (see Annex A FM.A-3 Objective 1 ‘High-level requirements comply with system requirements’)
• FM.6.3.g, FM.6.3.1.f (see Annex A FM.A-3 Objective 6 ‘High-level requirements are traceable to system requirements’)
Note that this was our informal view of achievement of the Objectives, but was left to the client to undertake formal activities. The remaining Objectives were for the client to achieve once they had had a chance to review our suggested sets of requirements. Another delivered document was a trace from the original requirements to our suggested system requirements in order to demonstrate that complete coverage had been achieved. This resulted in only 23 System Requirements.
5.4. Time
This overall effort took around 3 weeks and involved only one person doing the majority of the work. They were backed up by an expert user of Kapture® and, as mentioned, we had a Kapture® developer involved to develop a new feature but was not involved in the production of requirements.
5.5. Statistics
The following statistics are of interest
• 23 System requirements were produced which were translated into:
• Nearly 700 declarations of signal names and constants that were used in the software requirements, and there were:
• 25 user defined functions that were used in the software requirements:
· Which numbered nearly 400.
