Re: Safety-critical development in Ada and Eiffel

[donh@syd.csa.com.au (Don Harrison)]

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


Karel Th�nissen wrote:

:Don Harrison wrote:

:> I agree - it's belongs in a contract.
:
:I think it only belongs in a contract if the timing of an method
:invocation is concerned. 

I don't agree. I'll outline what we *can* do and then address your specific 
examples.

1) We can time how long it takes for a method to execute using a postcondition:

     do_something (.., time_started: TIME) is
     do
       ...
     ensure (time_now - time_started <= allowable_duration) <<<<
     end

   (We agree on this). 

2) You can time the periodicity (time between drinks) of a call using a 
   precondition and an attribute of the enclosing class which records the time 
   last called:

     class SOME_CLASS 
     creation make
     feature
       do_something (..) is
       require 
         not called_before or else (time_now - time_last_called <= max_duration) <<<<
       do 
         time_last_called := time_now
         called_before := TRUE
         ...
       end

       make is
       do called_before := FALSE; end

     feature {NONE}
       time_last_called: TIME
       called_before: BOOLEAN
     end

3) You can time how long it takes to perform any action within the body of a 
   routine using a check-instruction and a local attribute recording the time
   the action started:

 a)  do_something (..) is
     local time_started: TIME
     do
       ...
       time_started := time_now
       ... -- timed action
       check (time_now - time_started < max_duration) end <<<<
       ...
     end

   Note that the check-instruction can appear anywhere so can be used to time
   a conditional branch or the average duration of a loop iteration:

 b)  time_started := time_now
     no_of_iterations := 0
     loop
       no_of_iterations := no_of_iterations + 1
       ...
     end
     check 
       (time_now - time_started) / no_of_iterations <= max_iteration_duration <<<<
     end

4) You can time the periodicity of calls made by a caller by using a 
   check-instruction and an attribute in the caller's class which records the 
   time the last call was made:

     class CALLING_CLASS 
     creation make
     feature
       ...
       !!a.make
       ...
       check 
         not called_before or else (time_now - time_of_last_call <= max_duration) <<<<
       end
       time_of_last_call := time_now
       a.do_something -- the call
       ...

       make is
       do called_before := FALSE; end

     feature {NONE}
       a: CALLED_CLASS
       time_of_last_call: TIME
       called_before: BOOLEAN
     end

5) You can ensure that no call made by a caller takes longer than a specified 
   duration by using an invariant and an attribute in the caller's class which 
   records the time a call was made:

     class CALLING_CLASS 
     feature
       ...
       !!a.make
       ...
       time_started := time_now
       a.do_something -- the call
       ...

     feature {NONE}
       a: CALLED_CLASS
       time_started: TIME

     invariant
       time_now - time_started <= max_duration <<<<
     end

6) You can ensure that no call made to a callee takes longer than a specified 
   duration by using an invariant and an attribute in the enclosing class which 
   records the time a call was made:

   (Details omitted - similar to 5) ).


:However, this avenue of the thread was started
:with the observation that a program should not depend on timing in an
:unspecified/undocumented way.

I agree. However, I think you'll agree on the basis of the examples above,
Eiffel assertions are a powerful means of, not only specifying and documenting 
timing dependencies, but validating at runtime that they're complied with.


:... there are a lot more things we may have to time, but that are
:not directly linked to a particular (interface of) an object. 

Correct - hence the need for check-instructions.


For example:
:
:- the timing between two iterations of a loop

  See 3) b) above.

:- the interval between two read outs of a memory mapped IO-port

  See 4) above.

:- the timing of the execution of a method where the timing is critical
:  on the part of the calling method and not of the called method itself

  See 4) above.

:- timing of the interaction with the user (which is not a method for
:  which one can specify a contract)

  Nor should we. No action (or not taken by a user) should ever be the basis 
  of an assertion. Such cases should be catered for by logic in the code 
  proper because are not indicative of errors in the software. A couple of 
  examples are a) user input validation and b) failure of a pilot to take 
  remedial action (or taking too much remedial action - Ken's example).

:- timing of a number of instructions within a method

  See 3) a) above.

 - timing of any call made by an object

  See 5) above.

 - timing of any call made to an object

  See 6) above.


:So even though timing specifications with postconditions are useful, it
:definitely is not sufficient for many HRT systems.

Agree, you also need preconditions, check-instructions and invariants.


Don.
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
Don Harrison             donh@syd.csa.com.au