RE: [sc] Formal method analysis



RE: [sc] Formal method analysis

From: Rich Rademacher ^lt;rich.rademacher@xxxxxx>
Date: Mon 27 Feb 2006 - 19:46:53 GMT
Message-ID: <00dc01c63bd6$8fcaf1c0$6469a8c0@xxxxxx>
Really the point of this is to prove the algorithm, no the implementation.
So I have started the sketch of a specification in PVS, and some conjectures
will be stated as challenges to see what the algorithm is made of.  The
reason I chose alloc was not because of the language, but because it
constituted a very basic form of memory allocation: one function requests
it, another releases it.  Both are done under the control of the user
process, not automatically in the background like a garbage collector.

The larger project here is to try and build an separation kernal for an RTOS
using formal methods for as much of the architecture as possible.  The
allocator is just one part.  The actual implementation is in Ada, since it
is already well-specified and that removes the distraction of proving the
language before the implementation.

Rich

>> -----Original Message-----
>> From: Peter B. Ladkin [mailto:ladkin@xxxxxx]
>> Sent: Monday, February 27, 2006 12:23 PM
>> To: rich.rademacher@xxxxxx
>> Cc: Safety Critical Systems List
>> Subject: Re: [sc] Formal method analysis
>>
>>
>> Rich Rademacher wrote:
>> > ............... Haven't found
>> > anything on a more traditional allocator like a C malloc
>> and that's what my
>> > research is focusing on.  Any ideas?
>>
>> There are good reasons why a "C alloc" operator has not been
>> subject to
>> a formal analysis. These reasons are also reasons why almost
>> no C code
>> has been subject to formal analysis, namely there is little
>> hope of proving
>> correct an algorithm coded in a language with an imprecise semantics.
>>
>> Even if one formalised a look-alike allocator in a language
>> with a precise
>> semantics, and succeeded in proving it correct, the work would have
>> only limited application to the actual behavior of such an allocator
>> written in
>> C and compiled using one of the standard compilers.
>>
>> Formalising the behavior of all but the most trivial C
>> programs in such
>> a way
>> as to allow one to check their actual behavior is beyond the
>> state of
>> the art,
>> and is likely to remain so for a while. The only work I know in
>> verifying actual system
>> code originally written in C took the machine code into which it was
>> compiled and verified
>> that. (Not that the machine code is guaranteed to have an accurate
>> semantics.
>> See SRI's work on the AAMP5 and Vaughan Pratt's work on
>> Pentium floating
>> point division.)
>>
>> PBL
>>
>> --
>> Peter B. Ladkin, Professor of Computer Networks and
>> Distributed Systems,
>> Faculty of Technology, University of Bielefeld, 33594
>> Bielefeld, Germany
>> Tel+msg +49 (0)521 880 7319  www.rvs.uni-bielefeld.de
>>
>>
>>
>>
>>
>>
Received on Mon Feb 27 19:43:11 2006