The VFSM toolset supports the development of protocols and systems defined as a network of virtual finite state machines (VFSMs). In the VFSM approach one first defines finite state machines that process virtual inputs and outputs. Then these state machines are compiled to code and linked with user-written code that implements the virtual inputs and outputs.
Besides a code generator, the VFSM toolset also includes simulation and validation tools. The validator has two main capabilities. Using its reachability analysis, the tool will search all system states for generic problems such as deadlocks, livelocks, and queue overflows. The tool will also search for states that are bad in a sense defined by the user. Using the tools model checking feature, the tool does checking of more complex temporal properties defined by the user. For example, a user can check whether an event will eventually enter a queue if a machine reaches an error state. The temporal properties are expressed in linear temporal logic. If a property fails to hold, the tool shows a error scenario of the system.
With Michael Benedict I have tried to improve on existing proofs for the model-checking algorithms used in the VFSM Validator. See my improved proofs.