Validation of Concurrent ADA Programs using Symbolic Execution

Symbolic execution is a well known technique for analyzing sequential programs. It has a set of important applications: it can be used for verifying the correctness of a particular path for all the input data which cause the execution of that path. It can support testing tools identifying the constraints that characterize the set of data which exercize a particular execution path. With suitable assertions it can provide a verification mechanism. Finally, it can be used as a basis for a documentation tool. In this paper we propose an extension of sequential symbolic execution for Ada tasking. A net based formalism, EF net, is used for representing the Ada task system. EF nets are suitable for representing all the aspects of Ada tasking, except for time related commands, which are not considered in this paper. Two symbolic execution algorithms are then defined on EF nets. The first one, called SEA, suitable for the execution of every EF net, can be used for symbolically executing every concurrent Ada program. The second algorithm allows the execution of a relevant subset of EF nets, and improves the SEA algorithm reducing the produced results, dropping some aspects which do not add any significance