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.
PICASSOS - A Collaborative Project
D-RisQ was invited to participate in a collaborative project run by Ricardo called ‘Proving Integrity of Complex Automotive Systems of Systems’. The consortium included Jaguar Land Rover, Johnson Matthey Battery System, York Metrics, Warwick Manufacturing Group, Coven-try and Oxford Universities. It was on this project that Modelworks was evolved and the foundations of Kapture were laid. The project was used to trial analysis techniques in order to reduce the time and cost impact of poor requirements and design. This was conducted in the context of the automotive safety standard ISO26262. Other activities such as coding and test were outside the scope of the trials documented here.
Project Aim
The aim was to not only develop these technologies but to also independently measure how effective they were in terms of error detection and the time taken to undertake verification when compared to other techniques. At this stage, Kapture was not available and requirements had to be translated written in a semi-formal manner that required some training. Modelworks also required some small amount of manual intervention. Engineers in 2 companies were trained how to use the tools which only took about half a day.
The Trial
Warwick Manufacturing Group used an electric vehicle charging systems being developed for Jaguar Land Rover as the trial; this had 6 major areas of functionality. There were 7 trials run on the various parts of the software 48 errors were seeded into either the requirements or the Simulink/Stateflow design. One company did all the trials while another only did one; hence a total of 7 trials. York Metrics had set the measurement processes for the activities undertaken by the 3 sets of software engineers who were to work in the trial. The 1st set used the traditional review based techniques, the second used Simulink Design Verifier, while the third used the D-RisQ technologies. Time for the various parts of the verification process were measured, which, for the D-RisQ process, also included the translation of the requirements into the semi-formal representation. York Metrics monitored the trials and collated results. Note that D-RisQ personnel were not involved in the trials.
The Results
The graph below show the time results. The time allocated for the trial ran out hence the example PP had no results for D-RisQ (it was subsequently all proven). All 3 processes were able to detect all 48 seeded errors (not including PP), but the D-RisQ process detected an additional unknown 49th error. It can be seen that there is a consistent 60-80% saving through the use of D-RisQ prototype tools over traditional techniques and a broad range of savings over Simulink Design Verifier. Possibly the most interesting result was the repeat of TA independently done by the 2nd company as TA2 gave almost the same results. [Perhaps another result of interest was the 4 occasions where Simulink Design Verifier gave no savings.]
Copyright © D-RisQ | Website Design by Design in the Shires
