From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,ba6120170d8e7faf X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2001-12-05 07:13:43 PST Newsgroups: comp.lang.ada Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!news-spur1.maxwell.syr.edu!news.maxwell.syr.edu!upp1.onvoy!onvoy.com!news-out.visi.com!hermes.visi.com!uunet!ash.uu.net!xyzzy!nntp From: StationSteve Subject: Re: Worst Case Execution Time Tool? X-Nntp-Posting-Host: hl20s04182.tx.boeing.com Content-Type: text/plain; charset=us-ascii Message-ID: <3C0E3535.58437022@computer.org> Sender: nntp@news.boeing.com (Boeing NNTP News Access) Content-Transfer-Encoding: 7bit Organization: The Boeing Company X-Accept-Language: en References: <3C0D536C.2E059EE8@computer.org> Mime-Version: 1.0 Date: Wed, 5 Dec 2001 14:54:46 GMT X-Mailer: Mozilla 4.61 [en] (Win95; U) Xref: archiver1.google.com comp.lang.ada:17446 Date: 2001-12-05T14:54:46+00:00 List-Id: 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 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