Formal models for automotive systems and vehicular networks: Benefits and challenges

Formal models have seen widespread use in the development of safety- and security-critical systems — primarily as a means of providing increased assurance. In particular, formal models of threats have the potential to give rise to numerous benefits: they can help in the understanding of vulnerabilities (and the communication of such); they also provide a means by which these vulnerabilities can be reasoned about. We give consideration to how formal models of threats might be beneficial in the development of modern automotive systems and vehicular networks, which are increasingly interconnected. To achieve this we present a formal threat model of an idealised system. We use Predicate/Transition (PrT) Nets, a graphical mathematical formalism, to represent threats and plausible attacks. In addition to understanding and analysis, the approach also has the potential to provide benefits to the design and testing of vehicles' distributed IT systems — thus contributing to an improved sense of security, privacy and safety. To this end, we give consideration to the challenges that lie ahead in terms of adopting such an approach.