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.
While autonomous systems such as path planning take advantage of artificial intelligence to replace human functions, the changes resulting from the AI intervention are not verifiable and hence difficult to use in high integrity applications. There is therefore a need to develop a high integrity safety monitor in order to meet Beyond Visual Line of Sight Operations once communications with the UAV are lost. The monitor needs to interface with the UAV’s systems and be able to control the air vehicle as a pilot would obeying the rules of the air.
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.
A design was developed in Simulink/Stateflow® to reflect the software requirements previously written in Kapture®. This design complied with the subset of Simulink/ Stateflow® used by Modelworks®. Applying Modelworks® automatically and exhaustively to the design checks that it satisfies the requirements through the use of a mathematical check. The check exploits the mathematical semantics given to the requirements and a similar set of semantics given to the design. This provides evidence to support the safety case and hence the platform certification. Also, it significantly cuts down the amount of verification effort needed to a bare minimum whilst also removing any subjectivity. This reduces not only errors in the first pass but also the cost of undertaking rework when requirements change due to the extensive automation. In independent trials the cost reduction using Modelworks® over traditional methods has shown to be of the order of 80%.
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.
The source code has to be compiled and verified to run on the target processor and constitutes the binary code that actually executes within the system. At present a set of tests have to be generated and executed to verify this code. D-RisQ is developing an automatic, independent verification technology that will automatically verify that the binary code is correct with respect to the source code. This provides evidence to support the safety case and hence platform certification. It also further reduces the costs of development and provides significant alleviation from the regulatory requirements around structural coverage, if used in conjunction with the other D-RisQ tools.
· 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
The Safety Monitor application software was loaded onto the aircraft platform and run through various simulations. This ranged from simple to extremely complex collision avoidance scenarios and the unmanned air vehicle behaved exactly as expected. The trials also provided the opportunity to add an extra layer of functionality that incorporated knowledge of how a pilot flies rather than strict adherence to the rules of the air. The software developed in this case study can be adapted for other sectors such as road and marine, where truly autonomous vehicles require a failsafe mechanism for ensuring the behaviour of the vehicle if communication and control is lost.
Privacy Policy | Terms & Conditions
Drisq Ltd 2023. All rights reserved. Design by Design in the Shires
