A Framework For Interacting With Parameterized and Infinite State Verification Tools
Abstract: We develop a tool to explore the behavior of parameterized systems (i.e., systems consisting of an arbitrary number of identical processes that synchronize using shared variables or global communications) and to ease user interaction with tools that verify them. The tool includes a user friendly GUI that allows the user to describe a parameterized system and to perform guided, interactive or random simulation. This tool empowers the user to plug in several independent verifiers to perform verification. A mockup verifier is developed in order to facilitate the development of the tool and testing the required functionalities. The mockup verifier involves parsing descriptions of the parameterized systems to be analyzed. In order to interact with the verifier, the tool is user friendly and flexible in the sense that the user can plug in a verifier developed in any language as long as it allows to perform a number of basic computations on the parameterized system (such as the set of enabled transitions or the set of successor configurations). In order to plug in a new tool, our tool needs to be able to make use of these operations, for instance using a wrapper written for a verifier particular to a class of parameterized systems. Given these operations, our tool enables the user to carry out various types of simulations like random, interactive or guided simulations. Moreover, our tool can submit verification queries to the underlying verifier and walk the user through the generated counter examples as if it was a simulation session.
AT THIS PAGE YOU CAN DOWNLOAD THE WHOLE ESSAY. (follow the link to the next page)