Prev: Small changes in Ada handling in Gentoo
Next: [FYI] Joachim Schueth Interviews
From: S�nke Brix on 24 Jan 2008 14:37
Hi Softwareengineers and Testgurus,

I read something about the tool "PolySpace". The test approach of this tool
seems a little bit different. In an advertisment the company describes that
"PolySpace"
- ...statically analyses the dynamics of sw applications by relying solely
on the source code,
- ...no test cases to write
- ...no instrumentation of the code
- ...no execution of the application
Hmmm ????
How does this stuff work? I found some infos, but they were not very
helpful. Something over "semantic analysis", but not very deep. I this a
pure mathematically analysis scheme?

So, who has a deep knowledge and is able to explain the secrets of this test
tool and especially the mathematics and techniques behind the scenes.

Thanx

S. Brix



From: Ludovic Brenta on 24 Jan 2008 16:20
"S�nke Brix" writes:
> Hi Softwareengineers and Testgurus,
>
> I read something about the tool "PolySpace". The test approach of this tool
> seems a little bit different. In an advertisment the company describes that
> "PolySpace"
> - ...statically analyses the dynamics of sw applications by relying solely
> on the source code,
> - ...no test cases to write
> - ...no instrumentation of the code
> - ...no execution of the application
> Hmmm ????
> How does this stuff work? I found some infos, but they were not very
> helpful. Something over "semantic analysis", but not very deep. I this a
> pure mathematically analysis scheme?
>
> So, who has a deep knowledge and is able to explain the secrets of this test
> tool and especially the mathematics and techniques behind the scenes.
>
> Thanx

I think you should qsk them for the details. I attended their
presentation at the Ada-Belgium general assembly in 2003 [1]. The
basic principle is to leverage the rich information contained in a
typical Ada program, especially the range constraints, and then
propagating these constraints down every execution path to detect
possible violations. This analysis is only possible in Ada; lesser
languages require annotations to provide the information about range
constraints.

[1] http://www.cs.kuleuven.be/~dirk/ada-belgium/events/03/030225-abga-event.html

--
Ludovic Brenta.
From: Stuart on 25 Jan 2008 03:48
"S�nke Brix" <soenke.brix(a)fernuni-hagen.de> wrote in message
news:fnapeb$5ra$1(a)tamarack.fernuni-hagen.de...
>
> I read something about the tool "PolySpace". The test approach of this
> tool
> seems a little bit different. In an advertisment the company describes
> that
> "PolySpace"
> - ...statically analyses the dynamics of sw applications by relying solely
> on the source code,
> - ...no test cases to write
> - ...no instrumentation of the code
> - ...no execution of the application
> Hmmm ????
> How does this stuff work? I found some infos, but they were not very
> helpful. Something over "semantic analysis", but not very deep. I this a
> pure mathematically analysis scheme?

The general technique used is called 'Abstract Interpretation'. By
modelling the semantics of a program and knowing the possible values of the
variables at one point in the program, the values at another point can be
determined.

For instance given an integer 'x' which might have the values 1..20, and the
statement:
y := x *2;

We can determine the set of values of 'y'. By following the computations
through in this manner it is possible to determine whether, at any point, a
constraint error would arise. Normally such an event would indicate there
was an error or deficiency in the program. Whether the program does what
you want is another matter - and in this respect I do not think the tool as
described helps you. That said, it is often a greater challenge to ensure a
program is free from defects than check whether it does what you want in
most circumstances.

The interesting challenge for 'Abstract Interpretation' tools is deciding
how much detail to preserve at each stage. From the example should the tool
note that 'y' might have the values 2..40 or the set of values {2, 4, 6,
...., 40}.

This can become important, for instance if you had the statement:
z := 1000 / (y - 9);

Could a divide by zero occur? If you had a lax model of 'y' [2..40] you
would be concerned, but a more accurate model would dispel the concern. The
problem with keeping fully accurate models is that the modelling can quickly
become very complex. Addressing these issues, to reduce false warnings but
still give good performance, is a significant matter for these tools.
[BTW - on such a simple example the tools would easily determine that a
divide by zero would not occur].

A similar tool to Polyspace is ASTREE - and there are others. There is a
fair deal of information out there on the internet.

Interestingly, with an appropriately designed Ada program much of the
information needed to enhance code analysis can be derived from the type
system. When analysing C programs you typically need a Data Dictionary to
help manage the analysis effectively [though it is still possible to perform
useful analyses without one].

Regards
--
Stuart


From: Dmitry A. Kazakov on 25 Jan 2008 04:31
On Fri, 25 Jan 2008 08:48:35 -0000, Stuart wrote:

> The interesting challenge for 'Abstract Interpretation' tools is deciding
> how much detail to preserve at each stage. From the example should the tool
> note that 'y' might have the values 2..40 or the set of values {2, 4, 6,
> ..., 40}.
>
> This can become important, for instance if you had the statement:
> z := 1000 / (y - 9);
>
> Could a divide by zero occur? If you had a lax model of 'y' [2..40] you
> would be concerned, but a more accurate model would dispel the concern.

There is another difficult aspect of the problem of uncertain computations.
It is dependency analysis. For example:

y := x;
z := x * y;

When x is in [-1, 2] then without knowing that y equals x, i.e. assuming
that x and y are independent, the best possible estimation of z is [-2, 4].
With this knowledge it is [0, 4].

--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
From: T. Taft on 25 Jan 2008 23:57
On Jan 25, 4:31 am, "Dmitry A. Kazakov" <mail...(a)dmitry-kazakov.de>
wrote:
> On Fri, 25 Jan 2008 08:48:35 -0000, Stuart wrote:
> > The interesting challenge for 'Abstract Interpretation' tools is deciding
> > how much detail to preserve at each stage. From the example should the tool
> > note that 'y' might have the values 2..40 or the set of values {2, 4, 6,
> > ..., 40}.
>
> > This can become important, for instance if you had the statement:
> > z := 1000 / (y - 9);
>
> > Could a divide by zero occur? If you had a lax model of 'y' [2..40] you
> > would be concerned, but a more accurate model would dispel the concern.
>
> There is another difficult aspect of the problem of uncertain computations.
> It is dependency analysis. For example:
>
> y := x;
> z := x * y;
>
> When x is in [-1, 2] then without knowing that y equals x, i.e. assuming
> that x and y are independent, the best possible estimation of z is [-2, 4].
> With this knowledge it is [0, 4].

The SofCheck Inspector is another static analysis tool that
supports Ada. We keep track of the kinds of symbolic
relationships you mention (such as X = Y) in addition
to pure value range information.

Our website is http://www.sofcheck.com

You might check wikipedia for "static analysis" or
"source code analysis".

>
> --
> Regards,
> Dmitry A. Kazakovhttp://www.dmitry-kazakov.de

Sincerely,
-Tucker Taft
SofCheck, Inc.
Burlington, MA USA
 | 
Pages: 1
Prev: Small changes in Ada handling in Gentoo
Next: [FYI] Joachim Schueth Interviews