Path: utzoo!yunexus!ists!helios.physics.utoronto.ca!news-server.csri.toronto.edu!cs.utexas.edu!uwm.edu!zaphod.mps.ohio-state.edu!think!linus!howell
From: howell@boardwalk.mitre.org (Chuck Howell)
Newsgroups: comp.specification
Subject: extracting spec of existing system
Message-ID: <HOWELL.90May29152934@boardwalk.mitre.org>
Date: 29 May 90 19:29:34 GMT
Article-I.D.: boardwal.HOWELL.90May29152934
Sender: root@linus.UUCP
Distribution: comp
Organization: MITRE McLean C3I Software Center
Lines: 24


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                    |
+------------------------------------------------------------------------+