Beyond Visual Line of Sight operations for Unmanned Air Vehicles can only realistically be undertaken if the aircraft can operate fully autonomously in accordance with the rules-of-the-air (i.e. SERA), especially where collision avoidance is concerned. A human cannot be expected to intervene in time, over a link, in all circumstances, as the time delay alone could mean that the intervention is received after the incident has already happened. Therefore, a resident failsafe software control monitor has to be on board ready to take over when external control is lost and short notice collision avoidance is necessary. Such a system has to have high assurance software developed to the highest level of integrity, typically meeting RTCA DO-178C. Meeting this standard is notoriously expensive, so finding a method of providing the required integrity at low cost is a design imperative.
Describing the desired behaviours of a software system in a clear and easily understood format and therefore generating “good” requirements, is essential for developers and certifiers. A key attribute of “good” requirements (that should be checked prior to their use in software development) is ensuring that they are verifiable. D-RisQ therefore developed a set of syntactic constructs in English to ensure that they have a very clear meaning and then generated an automatic translation to a formal representation for semantic checks so that automatic verification could take place. These functions were incorporated within a user friendly interface allowing software engineers to easily generate verifiable software requirements. This is the D-RisQ Kapture® tool. These requirements then become the sole source of information for the development of the software design and architecture. The use of Kapture® also supports software certification as requirements are verifiable, consistent and comply with the highest standards.
The source code was produced from the Simulink/Stateflow® model using an automatic code generator that can only generate code that is compliant with a subset of C. This subset of C is an implementation of the widely used MISRA-C guidelines that has an independently proven set of formal semantics. The code is then used in a further automatic verification using the proof within the D-RisQ CLawZ® tool. This significantly reduces the cost of coding and removes the need for unit test. Evidence is also generated to support the safety case and platform certification. As the requirements are encapsulated in Kapture® any changes to the requirements can easily be modified in Kapture® and automatically proven using Modelworks. This allows very quick generation of new autocode which can then be auto-proven using CLawZ®. This saves a considerable amount of time and cost, providing between 60-80% savings in the costs of the overall software development life cycle compared with traditional methods.
· Greatly reduces the opportunity for error introduction through the development process.
· Costs are significantly reduced with the potential for 80% savings
· Simple compliance to standards
· Easy to use by all software engineers involved in control systems development