Safety critical systems require to be highly reliable and thus special care is taken when verifying them in order to increase the confidence in their behavior. This paper addresses the problem of formal verification of safety critical systems by providing empirical evidence of the practical applicability of symbolic execution and of its usefulness for checking safety-related properties. In this paper, symbolic execution is used for building an operational model of the software on which safety properties, expressed by means of a Path Description Language (PDL), can be assessed.
Coen, A., Denaro, G., Ghezzi, C., Pezze', M. (2001). Using symbolic execution for verifying safety-critical systems. In Joint 8th European Software Engineering Conference and 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (pp.142-151) [10.1145/503209.503230].
Using symbolic execution for verifying safety-critical systems
DENARO, GIOVANNI;PEZZE', MAURO
2001
Abstract
Safety critical systems require to be highly reliable and thus special care is taken when verifying them in order to increase the confidence in their behavior. This paper addresses the problem of formal verification of safety critical systems by providing empirical evidence of the practical applicability of symbolic execution and of its usefulness for checking safety-related properties. In this paper, symbolic execution is used for building an operational model of the software on which safety properties, expressed by means of a Path Description Language (PDL), can be assessed.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
