[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Summary of generic verified refinement steps

This is a rather belated summary of the answers to my question about
generic verified refinement steps a while back. My excuse is that I
already sent it once, but apparently the pvs list was down at the

Many thanks to everyone who responded to my query. The summary is


There is some work on program transformations, see references for
Shankar's work using PVS, Dold's work also using PVS, and Butler et al
who use HOL as the reasoning engine.

On the hardware side, there is work by Gopalakrishnan et al that I
found extremely interesting. The formalism (CSP) they use is different
from the one I am using (action systems), but the motivation is the
same: design and verify at a synchronous level, and derive an
asynchronous specification from that.

Steve Johnson from Indiana kindly pointed me to their Hardware Methods

	I assume you mean formalized-and-mechanically-verified when
	you say "verified".  I haven't done that, but I have been
	working for 15 years on a formal system based on
	transformation and refinement, and oriented toward hardware
	and system design.  Our papers are at

Although not directly related to what I have in mind, their work seems
to be very interesting.

There is also related work done on Petri nets by Gargantini et al,
but this unfortunately falls outside my competence:

	I don't know if it is exactly what are you looking for, but if
	it can be useful see our paper:
	M.Felder, A.Gargantini, A.Morzenti, " A Theory of Implementation and
	Refinement in Timed Petri Nets",
	We define formally the notion of correct refinement for timed
	Petri nets using the temporal logic TRIO.  We introduce some
	rules to refine an atomic transition in many transitions.  We
	present a method to formally prove the correctness of
	refinements and apply it to the rules presented (but by hand)
	You can find an abstract at the URL
	and you can download the postscript too.
  author =       "Michael Butler and Jim Grundy and Thomas L{\aa}ngbacka
                 and Rimvydas Ruk{\v{s}\.{e}}nas and Joakim {von
  editor =       "Lindsay Groves and Steve Reeves",
  booktitle =    "Formal Methods Pacific'97: Proceedings of FMP'97",
  title =        "The Refinement Calculator: Proof Support for Program
  publisher =    "Springer-Verlag",
  address =      "Wellington, New Zealand",
  pages =        "40--61",
  month =        jul,
  year =         "1997",
  series =       "Discrete Mathematics \& Theoretical Computer Science",

  title =        "Steps Towards Mechanizing Program Transformations
                 Using {PVS}",
  author =       "N. Shankar",
  journal =      "Science of Computer Programming",
  pages =        "33--57",
  volume =       "26",
  number =       "1--3",
  year =         "1996",
  OPTnote =         {Rushby: It's available from our web page at
http://www.csl.sri.com/fm.html (follow links either to Shankar's page
or to "our papers").}

  author = 	 {Ratan Nalumasu and Ganesh Gopalakrishnan},
  title = 	 {Deriving Efficient Cache Coherence Protocols through
                  Refinement, UUCS-97-009},
  institution =  {Department of Computer Science, University of Utah},
  year = 	 {1998},
  OPTkey = 	 {},
  OPTtype = 	 {},
  OPTnumber = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {This work is also in Proceedings of FMPPTA'98, but I
                  dont't have a reference to that. Available at
  OPTannote = 	 {}

  author =       "A. Dold",
  title =        "Representing, Verifying and Applying Software
                 Development Steps using the {PVS} System",
  journal =      "Lecture Notes in Computer Science",
  volume =       "936",
  OPTpages =        "431--??",
  year =         "1995",
  coden =        "LNCSD9",
  ISSN =         "0302-9743",
  bibdate =      "Sat May 11 13:45:32 MDT 1996",
  acknowledgement = ack-nhfb,
  OPTnote =      "See http://www.informatik.uni-ulm.de/ki/dold.html"