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 | +------------------------------------------------------------------------+
sean@castle.ed.ac.uk (S Matthews) (05/30/90)
In article <HOWELL.90May29153054@boardwalk.mitre.org> howell@boardwalk.mitre.org (Chuck Howell) writes: > >I've seen a few references here and there to using formal methods to >specify an already implemented system; >Any references, texts, anecdotes, etc. on this topic will be >appreciated. The Oxford People have done a lot of work on this: they have big ongoing project to reverse engineer a formal specification of CICS, and they have done several other interesting projects. Try looking in Ian Hayes book from Prentice Hall called something like Formal Specification Case Studies. The paper by Sufrin and whoever on the UNIX file system is particularly good. Sorry about the vagueness, but I am too lazy to go into the next room to look at it. >Thanks a lot, >Chuck Sean P.S. this appeal would be at least as usefully posted in comp.specification, I would have thought.