This is the mail archive of the gdb@sourceware.org mailing list for the GDB project.


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]
Other format: [Raw text]

Re: Light Formal Methods in GDB


Hi,

The principle works as follows:

It it possible to create an automaton from an LTL formula, with
expressions for values of variables as the transitions from one state
to the next.

Then the tricky part is building an automaton which represents the
program. But once you have these it is possible to see if the
automaton 'match' and if they do then the property holds.

With regards to building the system automaton, at the very simplest
you could single step the code, get values of variables at each step
and make an appropriate transition on the automaton. However, this is
obviously very inefficient, and improvements would most likely be made
by building a control flow graph of the program (in some way) and use
the nodes of that graph as the points get get values, or something
like that.

The advantage of including something like this in GDB is that once the
property that the programmer expected to hold becomes false, program
execution can stop and he programmer can use the standard GDB tools.
Well, that'd be the idea anyway.

The original idea was to do the same thing but for concurrent programs
because there is research which says that using LTL formulas and the
automaton technique, you can say whether properties of concurrent
programs hold for all the possible interleavings. However, it was
decided that that was too complicated, so it was narrowed to
non-concurrent programs.

Rob

On 12/10/06, Michael Snyder <Michael.Snyder@palmsource.com> wrote:
On Thu, 2006-10-12 at 15:07 +0100, Rob Quill wrote:
> Hi,
>
> What I am aiming to do is allow the programmer to debug his program
> using linear temporal logic formulas to verify sections of code and
> check that specified properties hold.
>
> I consider this important to be included in a debugger as it allows
> the programmer to stop the program execution at a certain point, and
> check at run-time that parts (or all) of the program are formally
> correct.
>
> An example would be the Until operator, which allows the programmer to
> specify that expression A must be true until expression B is true.
>
> I know this is a brief explanation, and if it unclear please feel free
> to ask me more about it, but I just wanted to see what people think of
> the idea.

Well, gdb can answer questions such as "is expression A true?",
but only in the context of a specific, static point in the
execution.  And gdb doesn't know anything about formal or temporal
logic.  Those are way outside its scope.

Are you thinking in terms of, say, a pre-processor that could
come up with a set of properties or propositions, translate them
into language that gdb can understand (eg. "stop here, and see if
expression A is true"), write the results to a file, and then
have a post-processor go over the results and test them against
the logical propositions?





Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]