The Challenge
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 react in time in all circumstances over a link as the time delay alone may mean that an accident may have already happened. Something else has to be on board ready to take over when short notice collision avoidance is needed. In order to be able to describe the behaviour a software system should exhibit, the requirements have to be written such that they can be easily read, for example, by certifiers as well as developers.
Formalising Software Requirements
There are a number of attributes of requirements that should be checked prior to their use in software development; one of which is to ensure that they are verifiable. We therefore developed a set of syntactic constructs in English and ensured that they have a very clear meaning.
An automatic translation to a formal representation for semantic checks has been developed, so that automatic verification could subsequently take place. This was encapsulated in a user friendly interface so that software requirements could be easily entered by a software engineer; this is Kapture®. These requirements then become the sole source of information for development of the software design and architecture. The use of Kapture® also supports software certification as requirements are verifiable, consistent and comply with standards.
Required Behaviour
While it is easy to say “avoid all collisions”, describing what that behaviour should be for an autonomous aircraft in simple and then more complex scenarios needs to be clear. First we described the desired behaviour at a system level and wrote a System Requirements Document in natural English for our partner Callen-Lenz. This was the communication mechanism between the system engineers and the software engineers.
‘Kapturing’ the Software Requirements
Using Kapture®, we then developed the Software Requirements Specification for the decision making system based upon the system requirements. A review was conducted to assure that the Software Requirements accurately and completely captured the System Requirements. The requirements are automatically transformed into a formal representation for use in verification.
Kapture® Advantages
Reduces the opportunity for error
Requirements are verifiable
Simple compliance to standards
Automatic checks for consistency
Reduces the opportunity for error
Requirements are verifiable
Simple compliance
to standards
Automatic checks for consistency
Next Steps
The output from Kapture® was the input to the design stage where a model in Simulink was produced. The model was then automatically checked against the requirements using D-RisQ Modelworks®.
