howell@boardwalk.mitre.org (Chuck Howell) (05/30/90)
I've seen a few references here and there to using formal methods to specify an already implemented system; the claim is that this exercise was useful in identifying previously latent errors/ambiguities, and that the end product was a formal specification that corresponded pretty well with the implementations. I'm very interested in this approach, which seemingly is in the intersection of formal methods, reverse engineering/design recovery, and (corrective/perfective) maintenance. Any references, texts, anecdotes, etc. on this topic will be appreciated. If there's enough interest I'll post a summary to the net. Thanks a lot, Chuck -- +------------------------------------------------------------------------+ | Chuck Howell, M/S Z645 INTERNET: howell@community-chest.mitre.org | | The MITRE Corporation OR howell@mwunix.mitre.org | | 7525 Colshire Drive VOICE: (703) 883-6080 | | McLean VA 22102-3481 FAX: (703) 883-5519 | +------------------------------------------------------------------------+