Verifying Equivalence of Procedures in Different Languages: Preliminary Results

NASA operates manned spacecraft according to rigorously- defined procedures, some of which can be executed both au- tomatically and manually. Unfortunately, the operating pro- cedures for different pieces of equipment and different exe- cution modes (onboard/offboard, manual/automatic) may be written in entirely different languages. In this paper, we de- scribe an approach to verifying that the underlying semantics of these diverse procedure representations are the same; that is, we want to verify that the two different procedures “do the same thing.” We accomplish this verification by translat- ing each procedural language into a common verification lan- guage, Promela, and using the SPIN verification tool to con- firm that the procedures behave identically when given iden- tical inputs. This paper describes the patterns of translation into Promela and explores the scalability of this approach. More generally, this work represents first steps towards defin- ing a rigorous semantics for both PRL and SCL, which can be used for future verification and validation efforts supporting high-confidence software for manned spaceflight.