TRACKING DESIGN CHANGES WITH FORMAL MACHINE-CHECKED PROOF

Designs are often modified for use in new circumstances. If formal pro of is to be an acceptable verification methodology for industry, it mu st be capable of tracking design changes quickly. We describe our expe riences formally verifying an implementation of an ATM network compone nt, and on our subsequent verification of modified designs. Three of t he designs verified are in use in a working network. They were designe d and implemented with no consideration for formal methods. This case study gives an indication of the difficulties in formally verifying a real design and of subsequently tracking design changes.