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

Re: [PVS-Help] PVS Help (fwd)



Hello,

We have verified similar protocols using PVS.  Our original formulation was 
based on the work reported in Walter, Lincoln, and Suri.  Our results are 
documented in

http://techreports.larc.nasa.gov/ltrs/PDF/2004/tm/NASA-2004-tm212432.pdf

Included in that report are links to our PVS files.  We have further 
generalized the results, and expect to make them available as part of a PVS 
fault-tolerance library later this year.

Regards,
---

At 04:05 AM 2/16/2005, Sam Owre wrote:
>Hello Purnendu Sinha,
>
>This is an old spec, and it looks like the LaTeX is not quite right.
>What it used to have for the measure is
>
>   MEASURE (LAMBDA pset, R, OldAccuse -> nat : R)
>
>But this is no longer legal syntax.  The correct syntax is
>
>   MEASURE (LAMBDA pset, R, OldAccuse : R)
>
>Although you can also shorten this to
>
>   MEASURE R
>
>I have an older version of the spec, as well as it's supporting
>theories.  I want to check with one of the authors; if it is OK with him
>I will send it to you shortly.
>
>Regards,
>Sam Owre
>
>Dr. Purnendu Sinha <sinha@encs.concordia.ca> wrote:
>
> >
> > Hello,
> >
> > I am trying to work with a PVS theory that appeared in the paper "Formally
> > Verified On-Line Diagnosis" by Walter, Lincoln and Suri. As the PVS source
> > is not available, I tried to reproduce the code from latex-ified code
> > which appears in the paper. A pvs file is attached to this mail.
> >
> > I am running into problems as described below:
> >
> > 1. While doing type-check (M-x tcp), it always gives an error ", expected
> > here". But I do not see a need for "," in line 102. (part of MEASURE...)
> >
> > 2. Also, if I change MEASURE to something different to get pass that
> > error, it then complains about the theories that are being imported.
> >
> > I am using PVS 3.1 running on Solaris. I would appreciate if you could
> > guide me to resolve this problem.
> >
> > It would be much appreciated if a complete dump file with a complete proof
> > could be provided.
> >
> > Thanks in advance.
> >
> > Best regards,
> > Purnendu Sinha

| Paul S. Miner, Ph.D.                  | phone: (757) 864-6201
| Senior Research Engineer              | fax:   (757) 864-4234
| Mail Stop 130                         | mailto:paul.s.miner@nasa.gov
| NASA Langley Research Center  | http://shemesh.larc.nasa.gov/people/psm/
| Hampton, Virginia 23681-2199
-----------------------------------------------------
The contents herein do not necessarily reflect the positions of the United 
States Government.
-----------------------------------------------------