Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!swrinde!ucsd!ucbvax!bloom-beacon!eru!luth!sunic!mcsun!ukc!edcastle!sean From: sean@castle.ed.ac.uk (S Matthews) Newsgroups: comp.software-eng Subject: Re: formal methods and design recovery Message-ID: <4360@castle.ed.ac.uk> Date: 30 May 90 13:09:53 GMT References: Reply-To: sean@castle.ed.ac.uk (S Matthews) Distribution: comp Organization: Edinburgh University Computing Service Lines: 26 In article 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.