CheckOff-M is a formal verification tool which performs model checking. Model checking allows you to find errors in a design and to verify critical properties, such as the absence of dealdlocks and whether the design performs specified functions. You provide a set of logical properties which the design should possess, and CheckOff-M tells you if the design omits required behavior or includes unwanted behavior. For example, you can check that (i) mutually exclusive events cannot occur concurrently, or (ii) a desired event will occur at a specific time.
展开▼
