Checking System Properties via Integer Programming.

Title:: Checking System Properties via Integer Programming.
Document type:: Technical Report
Author(s):: S. Melzer; J. Esparza
Abstract:: The marking equation is a well known verification method in the Petri net community. It has also be applied by Avrunin, Corbett et al. to automata models. It is a semidecision method, and it may fail to give an answer for some systems, in particular for those communicating by means of shared variables. In this paper, we complement the marking equation by a so called trap equation. We show that both together significantly extend the range of verifiable systems by conducting several case studies.
Keywords:: Integer Programming; Petri net; marking equation; trap equation
Year:: 1995
Year / month:: 1995-12-11 00:00:00
Pages:: 26
BibTeX

Occurrences: