Verification and semantic parallelization of goal-driven autonomous software

Future space missions such as the Mars Science Laboratory demand the engineering of some of the most complex manrated autonomous software systems. According to some recent estimates, the certification cost for mission-critical software exceeds its development cost. The current processoriented methodologies do not reach the level of detail of providing guidelines for the development and validation of concurrent software. Time and concurrency are the most critical notions in an autonomous space system. In this work we present the design and implementation of a first concurrency and time centered framework for verification and semantic parallelization of real-time C++ within the JPL Mission Data System Framework (MDS). The end goal of the industrial project that motivated our work is to provide certification artifacts and accelerated testing of the complex software interactions in autonomous flight systems. As a case study we demonstrate the verification and semantic parallelization of the MDS Goal Networks.