ANN: Tokeneer material available

ANN: Tokeneer material available

[roderick.chapman]

I'm pleased to announce the immediate availability of the
Tokeneer project material.  Please see
  www.adacore.com/tokeneer

All the best,
 Rod Chapman, SPARK Team, Praxis

Re: ANN: Tokeneer material available

[Niklas Holsti]

roderick.chapman@googlemail.com wrote:
> I'm pleased to announce the immediate availability of the
> Tokeneer project material.  Please see
>   www.adacore.com/tokeneer

Lovely work. Congratulations.

The webpage reports that one defect has been discovered since 
delivery, apparently after the full report was written. Can you say 
  something about this defect -- why did it happen, and in which 
phase of development?

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .

Re: ANN: Tokeneer material available

[roderick.chapman]

On Oct 6, 1:47 pm, Niklas Holsti <niklas.hol...@tidorum.invalid>
wrote:
> roderick.chap...@googlemail.com wrote:
> > I'm pleased to announce the immediate availability of the
> > Tokeneer project material.  Please see
> >  www.adacore.com/tokeneer
>
> Lovely work. Congratulations.
>
> The webpage reports that one defect has been discovered since
> delivery, apparently after the full report was written. Can you say
>   something about this defect -- why did it happen, and in which
> phase of development?
>
> --
> Niklas Holsti
> Tidorum Ltd
> niklas holsti tidorum fi
>        .      @       .

Read the "Overview and Reader's Guide" document - this contains
a complete account of how this defect was found and corrected,
and a root-cause analysis of how it got there in the first place!
 - Rod

Re: ANN: Tokeneer material available

[Jerry]

This story made Slashdot. Idiots abound, as usual.

http://it.slashdot.org/article.pl?sid=08/10/06/1734255

Jerry

Re: ANN: Tokeneer material available

[Marc A. Criley]

Jerry wrote:
> This story made Slashdot. Idiots abound, as usual.
> 
> http://it.slashdot.org/article.pl?sid=08/10/06/1734255
> 

It also did halfway-decent, especially for an Ada oriented article, in 
the Programming sub-reddit 
(http://www.reddit.com/r/programming/comments/75gu5).

BTW, there's also an Ada-specific sub-reddit..

http://www.reddit.com/r/ada/

Marc A. Criley

Re: ANN: Tokeneer material available

[Marco]

On Oct 6, 5:38 am, roderick.chap...@googlemail.com wrote:
> I'm pleased to announce the immediate availability of the
> Tokeneer project material.  Please see
>  www.adacore.com/tokeneer
>
> All the best,
>  Rod Chapman, SPARK Team, Praxis

The development process applied to the Tokeneer ID Station high-
integrity development can be summarised in terms of the following key
phases:

    * Requirements analysis (the REVEAL® process)
    * Formal specification (using the formal language Z) <=== not many
folks can do this (or want to)
    * Design (formal refinement of the specification and the INFORMED
process)
    * Implementation in SPARK Ada
    * Verification (using the SPARK Examiner toolset)
    * Top-down system testing