Test tool not only for Ada

Test tool not only for Ada

[S�nke Brix]

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

Re: Test tool not only for Ada

[Ludovic Brenta]

"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.

Re: Test tool not only for Ada

[Stuart]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 2883 bytes --]

"S�nke Brix" <soenke.brix@fernuni-hagen.de> wrote in message 
news:fnapeb$5ra$1@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 

Re: Test tool not only for Ada

[Dmitry A. Kazakov]

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

Re: Test tool not only for Ada

[T. Taft]

On Jan 25, 4:31 am, "Dmitry A. Kazakov" <mail...@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