AbstractsEngineering

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

by Christoffer Holmstedt




Institution: Mälarden University
Department:
Year: 2014
Keywords: Engineering and Technology; Electrical Engineering, Electronic Engineering, Information Engineering; Communication Systems; Teknik och teknologier; Elektroteknik och elektronik; Kommunikationssystem
Record ID: 1330170
Full text PDF: http://urn.kb.se/resolve?urn=urn:nbn:se:mdh:diva-26858


Abstract

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.