Tracking design changes with formal machine-checked proof | Zendy

Paul Curzon | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Tracking design changes with formal machine-checked proof

Author(s) -

Paul Curzon

Publication year - 1995

Publication title -

the computer journal

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.319

H-Index - 64

eISSN - 1460-2067

pISSN - 0010-4620

DOI - 10.1093/comjnl/38.2.91

Subject(s) - computer science , formal verification , formal methods , tracking (education) , component (thermodynamics) , software engineering , programming language , psychology , pedagogy , physics , thermodynamics

Design are often modified for use in new circumstances. If formal proof is to be an acceptable verification methodology for industry, it must be capable of tracking design changes quickly. We describe our experiences formally verifying an implementation of an ATM network component, and on our subsequent verification of modified designs. Three of the designs verified are in use in a working network. They were designed and implemented with no consideration for formal methods. This case study gives an application of the difficulties in formally verifying a real design and of subsequently tracking design changes.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research