Abstract: “System relevant embedded software needs to be reliable and therefore well tested, especially for aerospace systems. A common technique to verify programs is the analysis of their abstract syntax tree (AST). Tree-like structures can be elegantly analyzed with the logic programming language Prolog. Moreover, Prolog offers further advantages for a thorough analysis: On the one hand, it natively provides versatile options to efficiently process tree- or graph-like data structures. On the other hand, Prolog’s non-determinism and backtracking allows to test different variations of the program flow without big effort. A rule-based approach with Prolog allows to characterize the verification goals ina concise and declarative way.

In this paper, we describe our approach to verify the source code of a flash file system with the help of Prolog. The flash file system is written in C++ and has been developed particularly for use within satellites. We transform a given abstract syntax tree of C++ source code into Prolog facts and derive a call graph and the execution sequence, which then are further tested against the verification goals. The different program flow branching due to control structures is derived by backtracking as subtrees of the original AST. Finally, these subtrees are verified in Prolog. We illustrate our approach with a case study, where we search for incorrect applications of semaphores in a flash file system for satellites. We rely on computation tree logic (CTL) and have designed an embedded domain specific language (DSL) in Prolog to express the verification goals.”