Model-checked Space Plug-and-Play Architecture Local Subnet Adaptation implemented in Ada with Ravenscar restrictions

• Main Author: Holmstedt, Christoffer
• Format: Others
• Language: English
• Published: Mälardalens högskola, Akademin för innovation, design och teknik 2014
• Online Access: http://urn.kb.se/resolve?urn=urn:nbn:se:mdh:diva-26858

Space Plug-and-Play Architecture (SPA) is a set of standards to make it easier to build small satellites. Focus is put on improving the integration phase andthe time consuming validation and verification process by introducing plug-and-play functionality. From mission call-up to operational satellite it should only take six days. A SPA network consists of several different types of subnets with differentpros and cons. For each processing node there must be one Local Subnet Manager (SM-L). The SM-L can communicate over different communication protocols depending on how the respective local subnet is set up, one option is UDP/IP. In this thesis Ada Protected Objects is presented as a viable option for inter-process communication instead of UDP/IP in a SPA network. This thesis presents the initial work towards a SPA Local Subnet Adaptation that builds onlanguage constructs in Ada such as Ada Tasks and Protected Objects. The system design and implementation is verified deadlock free with UPPAAL but showsindications of livelock possibilities. The severity of these livelocksituations is discussed in the conclusion.