This paper will outline the approach taken to produce a certified autonomous vehicle under a project funded by the UK Technology Strategy Board. The aim of the project is to show that it is possible to automate the system design validation as well as the verification of the implementation in software. By doing so, we aim to show that there is considerably reduced time and cost while still being able to meet certification requirements. The project will use a maritime example to show that the techniques can be used to meet the highest assurance requirements of any domain, e.g. DAL A for DO178C in aerospace. This approach has been taken firstly because the available budget precludes an air domain demonstration and secondly because the significant aspects of the project should be easily be transferred to other domains.

Chapter Contents:

• 1 Introduction
• 1.1 Cross Domain
• 1.2 Detect
• 1.3 Sense
• 1.4 Avoid
• 2 Demonstrating correct behaviour
• 2.1 The environment versus the system
• 2.2 Defending against human error
• 3 About the tools
• 3.1 Model works
• 3.2 CLawZ
• 4 Certification requirements
• 4.1 General approach
• 4.2 Verification
• 4.3 Formal challenges
• 4.4 Definition of the formal method
• 4.5 Justification and Appropriateness of the Formal Method
• 4.6 Formal analysis cases and procedures are correct
• 4.7 Formal reasoning results are correct
• 4.8 Requirements formalisation is correct
• 5 Why it is novel
• 6 Limitations
• 7 Remaining work
• 8 Acknowledgements
• 9 References

Inspec keywords: formal verification; mobile robots; control engineering computing

Other keywords: certified autonomous vehicle; UK Technology Strategy Board; autonomous systems certification; software verification; certification requirements; air domain demonstration

Subjects: Formal methods; Control engineering computing; Software engineering techniques; Mobile robots