Compositional verification using interface recognizers/suppliers (IRS)

Type Thesis

Rate 0.0 /5

Details

Files

Reviews

Download

Summary

In this thesis, we review recent developments in compositional and assume guarantee verification. We discuss whether each method supports circular/non circular reasoning and whether it can be used when proving safety/liveness properties. We formulate interface recognizers/suppliers (IRS), which are recognizers augmented with Boolean constraints. The constraints specify what values may occur on IRS inputs at each state. In other words, IRS can constrain its inputs. We discuss a composition theorem for circular reasoning using IRS. In this way, IRS framework extends non-circular constraint model checking [25] to a circular constrainted model checking. We demonstrate an application of IRS in (1) specifying environment assumptions and in (2) modeling pre conditions/post conditions of properties of an ATM switch. Using IRS, we specify and then verify the switch.