Definition, analysis and implementation of a model-checked Space Plug-and-play Architecture adaptation for the Controller Area Network

Abstract: The Virtual Network (VN) protocol is a communications protocol software compatible with the Space Plug-and-play Architecture (SPA). This Master Thesis defines a protocol that extends the Virtual Network protocol to cover communication over the Controller Area Network (CAN). The Virtual Network for the Controller Area Network (VN-CAN) is defined, modelled and verified using UPPAAL as well as implemented and tested while running on actual hardware. The VN-CAN protocol enables components on the CAN network to communicate with other components both inside and outside of the CAN network, which together with the modularity of both the protocol and the implementation enables application level software to be agnostic of their physical position in the network. The implementation enables components to automatically discover routes to other components on the VN network without the need for any prior knowledge about the network topology. A method for direct addressing, i.e. that two components on the CAN network can communicate directly without sending messages via a central router, has been added to the VN-CAN protocol in order to reduce traffic on the CAN network. UPPAAL modelling and verification of the VN-CAN protocol has been done to give a high level of confidence in the correctness of the protocol. Testing on actual hardware has shown that the protocol achieves the goals of address resolution, self addressing and transfer of VN messages over CAN.