Anzeige
Erschienen in:
2009 | OriginalPaper | Buchkapitel
Symbolic Execution Based Model Checking of Open Systems with Unbounded Variables
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.