comp.lang.ada
 help / color / mirror / Atom feed
From: StationSteve <Steven.Suchting@computer.org>
Subject: Re: Worst Case Execution Time Tool?
Date: Wed, 5 Dec 2001 14:54:46 GMT
Date: 2001-12-05T14:54:46+00:00	[thread overview]
Message-ID: <3C0E3535.58437022@computer.org> (raw)
In-Reply-To: ba18d5cb.0112050200.14bb96cd@posting.google.com

Oh, I guess I read the SPARK-Examiner web page wrong:
http://www.sparkada.com/examiner.html

I thought because the following words were on the SPARK-Examiner page, that Examiner could actually DO
WCET analysis of a SPARK program:

The Examiner checks conformance of a SPARK source text to the rules of SPARK by performing the
             following analyses.
...
other bullets here
...
Worst-Case Execution Time Analysis
                  The static analysis of program execution time requires analysis of program source text,
object code, and
                  user-supplied annotations. The latter supply information that cannot be determined
automatically, such as
                  a bound on the number of iterations made by each looping statement. By combining the
control-flow
                  graph for each subprogram, the program's call-tree, and the worst-case execution time
for each object
                  code fragment, the worst-case execution time (WCET) of a subprogram can be determined.
Such
                  analysis has several uses:
                       - Potential timing problems can be found earlier than usual, and thus can be
corrected more cheaply
                       and effectively.
                       - Watchdog timers can be set to monitor and control the execution of time-critical
code.
                       The program path that leads to WCET can be identified and tested with confidence.
...

Guess the marketing guys got tricky again, eh? ;-)

So how (or do?) people typically PROVE that their program will actually meet their deadlines?  If
somebody does a rate monotonic design, they have to assume the execution time of task.  How does one
determine the true execution time so that the design can be shown to be correct?

Thanks again...

Rod Chapman wrote:

> StationSteve <Steven.Suchting@computer.org> wrote in message news:<3C0D536C.2E059EE8@computer.org>...
> > Are there any tools that quantitatively determine the worst case
> > execution time (WCET) of an Ada83 program or subprogram?  Execution
> > platform is Intel 80386SX bare machine.  I think I'm looking for
> > something similar to SPARK Examiner's WCET analysis, but for Ada83.
> >
> > Thanks in advance for any help...
>
> Now here's a blast from the past... :-)
>
> I developed the SPATS toolset as part of my DPhil work - it was a
> static WCET tool for SPARK targetting 68020.  It was very much a
> "research prototype" (i.e. total hack) and so never saw the light
> of day.
>
> York Software Engineering Ltd then went on to develop a tool
> called STAMP that incorporated some of the ideas from SPATS.  As far
> as I know, STAMP remains the only commercially available static WCET tool.
> It has been ported to analyse 68020 and PPC 603e object code - no
> 386SX I'm afraid...
>
> There is no "offical" SPARK WCET tool, or (currently) any support
> for it in the Examiner, other than the inherent analysability of the
> language in the first place.  We have the annotations and analysis
> all worked out, but the funding (either internal or external) to
> make it a reality has never materialized - it's just not a priority
> for our customers I'm afraid.
>
>  - Rod




  reply	other threads:[~2001-12-05 14:54 UTC|newest]

Thread overview: 13+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2001-12-04 22:51 Worst Case Execution Time Tool? StationSteve
2001-12-05  0:10 ` Ted Dennison
2001-12-05 17:28   ` Stuart Palin
2001-12-05 18:33     ` Ted Dennison
2001-12-06 14:05       ` StationSteve
2001-12-06 16:40         ` Ted Dennison
2001-12-06 21:27           ` StationSteve
2001-12-06 22:44             ` Ted Dennison
2001-12-07  1:00               ` annonymous
2001-12-05 10:00 ` Rod Chapman
2001-12-05 14:54   ` StationSteve [this message]
2001-12-05 15:31     ` Jeffrey L. Susanj
2001-12-05 17:32     ` Stuart Palin
replies disabled

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox