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

Morasca, S., Pezze', M. (1989). Validation of Concurrent ADA Programs using Symbolic Execution. In Proceedings of the 2nd European Software Engineering Conference (pp.469-486). Springer Verlag [10.1007/3-540-51635-2_55].

Validation of Concurrent ADA Programs using Symbolic Execution

PEZZE', MAURO
1989

Abstract

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
paper
Software validation, Concurrent programs, Ada, Symbolic execution
English
European Software Engineering Conference, ESEC 1989 11-15 September
1989
Ghezzi, C; McDermid, JA
Proceedings of the 2nd European Software Engineering Conference
978-354051635-4
1989
387
469
486
none
Morasca, S., Pezze', M. (1989). Validation of Concurrent ADA Programs using Symbolic Execution. In Proceedings of the 2nd European Software Engineering Conference (pp.469-486). Springer Verlag [10.1007/3-540-51635-2_55].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10281/15753
Citazioni
  • Scopus 4
  • ???jsp.display-item.citation.isi??? 0
Social impact