EXAMINING CONCURRENT SYSTEM STATES

摘要

An illustrative embodiment of a computer-implemented process for examining concurrent system state space models a system having concurrent events to create a modeled system and creates a minimal chain decomposition of the modeled system to identify a set of chains. The computer-implemented process extends all chains in the set of chains, and generates a first set of paths, wherein the first set of paths is a minimal set of paths covering all states of the modeled system. The computer-implemented process explores the first set of paths and optionally determining whether all transitions have been covered and responsive to a determination that all transitions have not been covered, exploring remaining paths by traversing a graph induced by the modeled system using a depth-first strategy.