Symbolic Execution Based Model Checking of Open Systems with Unbounded Variables

摘要

We describe fundamental aspects of a method we have developed in order to check linear temporal logic formulas over Input Output Symbolic Transition Systems (IOSTSs). IOSTSs are used to describe reactive systems with communication channels and variables of different types ; in particular variables can take unbounded values. Thus the method can be applied to open systems, communicating with their environment, or with other modules that are not precisely specified. The method consists in a semi-decision algorithm based on symbolic execution techniques, usually used for tests generation purposes. We provide an adaptation of this technique in order to evaluate a LTL formula along a symbolic path ; moreover we have developed a termination criterion of the semi-decision algorithm for IOSTSs whose data part is specified by a decidable first order theory.