For the most recent entries see the Petri Nets Newsletter.

Validation of Concurrent Ada Programs Using Symbolic Execution.

Morasca, Sandro; Pezzè, Mauro

In: Ghezzi, C.; et al.: Lecture Notes in Computer Science, Vol. 387; ESEC'89. Proceedings of the 2nd European Software Engineering Conference, 1989, Coventry, UK, pages 469-486. Berlin: Springer-Verlag, 1989.

Abstract: The authors 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 high level Petri nets, suitable for representing all 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, 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.

Keywords: validation (of concurrent) ada program; symbolic execution; high-level net.


Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography