* Test tool not only for Ada @ 2008-01-24 19:37 S�nke Brix 2008-01-24 21:20 ` Ludovic Brenta 2008-01-25 8:48 ` Stuart 0 siblings, 2 replies; 5+ messages in thread From: S�nke Brix @ 2008-01-24 19:37 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Test tool not only for Ada 2008-01-24 19:37 Test tool not only for Ada S�nke Brix @ 2008-01-24 21:20 ` Ludovic Brenta 2008-01-25 8:48 ` Stuart 1 sibling, 0 replies; 5+ messages in thread From: Ludovic Brenta @ 2008-01-24 21:20 UTC (permalink / raw) "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. ^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Test tool not only for Ada 2008-01-24 19:37 Test tool not only for Ada S�nke Brix 2008-01-24 21:20 ` Ludovic Brenta @ 2008-01-25 8:48 ` Stuart 2008-01-25 9:31 ` Dmitry A. Kazakov 1 sibling, 1 reply; 5+ messages in thread From: Stuart @ 2008-01-25 8:48 UTC (permalink / raw) [-- 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 ^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Test tool not only for Ada 2008-01-25 8:48 ` Stuart @ 2008-01-25 9:31 ` Dmitry A. Kazakov 2008-01-26 4:57 ` T. Taft 0 siblings, 1 reply; 5+ messages in thread From: Dmitry A. Kazakov @ 2008-01-25 9:31 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Test tool not only for Ada 2008-01-25 9:31 ` Dmitry A. Kazakov @ 2008-01-26 4:57 ` T. Taft 0 siblings, 0 replies; 5+ messages in thread From: T. Taft @ 2008-01-26 4:57 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 5+ messages in thread
end of thread, other threads:[~2008-01-26 4:57 UTC | newest] Thread overview: 5+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2008-01-24 19:37 Test tool not only for Ada S�nke Brix 2008-01-24 21:20 ` Ludovic Brenta 2008-01-25 8:48 ` Stuart 2008-01-25 9:31 ` Dmitry A. Kazakov 2008-01-26 4:57 ` T. Taft
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox