ANNONUCE: Public technical briefing on SPARK, Houston

ANNONUCE: Public technical briefing on SPARK, Houston

[Rod Chapman]

As a "warm up" event for ACM SigAda 2002, Praxis Critical Systems will
be
presented a public technical briefing on SPARK on Friday 6th December.
This event in aimed at engineers and managers involved in the design
and procurement of high-integrity software, and especially those
involved in the the aviation and space industries centred around NASA
JSC.

Title: SPARK - A state-of-the-practice approach to High-Integrity
Software

Where: Houston Holiday Inn / NASA, 1300 NASA Road 1, Houston

When: Friday 6th December 2002, 09:30 - 12:00

RSVP: To sparkinfo@praxis-cs.co.uk (mainly so I know how much food and
how many chairs to order!)

Other contacts: rod.chapman@praxis-cs.co.uk  www.sparkada.com

Abstract:  Building truly high-integrity software requires a
qualitatively different approach - simply "being more careful"
is not good enough.  In the UK and Europe, Praxis has pioneered
an approach known as "Correctness by Construction" that has proven
to be both a technical and commercial success in this domain.
C-by-C is characterized by an emphasis on a rigorous approach, the
appropriate use of formal notations, and the static verification of
software, rather than relying on the inherently more risk-prone and
expensive
use of testing as the principal verification activity.

SPARK is a programming language that facilitates
Correctness-by-Construction.
Its most important property is that it has a totally unambiguous
semantics.
This enables static analysis of the language to be both precise (i.e.
the
results really mean something and there's a very low "false alarm"
rate)
and efficient so the tool support is actually actually useful during
development rather than just being used retrospectively.  SPARK is an
annotated subset of Ada95, so the language inherits all of the support
for commerical compilers, tools and training available from the wider
Ada community.  The "annotations" extend the subset's support for
design-by-contract(tm), allowing packages and subprograms to specify
their
intended behaviour precisely at various levels of rigour and detail.

SPARK has over 10 years of industrial use, mainly in the European
Aerospace and Rail industries, but remains less well known in the USA,
although SPARK is actually recommended by NASA's own guidance for
safety-critical software.  This briefing will examine some of the
most notable SPARK projects, including the Lockheed C130J, and how
SPARK
is effective in meeting standards such as DO-178B.  Finally, we will
consider some of the barriers (both actual and mythical) that may have
hindered the adoption of SPARK in other projects.

Outline:

1) What's so hard about High-Integrity Software?
    What's the problem?
    What's different about High-Integrity?
    The problem of relying on testing.

2) Correctness by Construction and SPARK.
    Ambiguity versus precision.
    Static analysis.

3) SPARK Analyses and Examples.
    A real-world example.

4) SPARK and Standards.
    DO-178B and the C130J story
    Observations on DO-178B
    Other Standards

5) Barriers to SPARK...

6) Conclusions and Questions.

Speaker biography:

Roderick Chapman received MEng and DPhil degrees from the University
of
York, England in 1991 and 1995 respectively. As a software engineer
with
Praxis Critical Systems, he specialised in the design and
implementation
of high-integrity real-time and embedded systems.  He worked with
Lockheed
Martin on the adoption of SPARK on the C130J Mission Computer, and
went
on to build safety- and security-critical systems such as the Royal
Navy's SHOLIS system and the MULTOS CA.  Praxis' work on these systems
has
been published in CrossTalk Journal, IEEE Transactions on Software
Engineering
and IEEE Software respectively.

Rod is currently SPARK product manager with overall responsibility for
the
continued development of the SPARK Examiner and its associated tools. 
He
is a member of the British Computer Society and is a Chartered
Engineer.  He
has given technical papers, briefings and tutorials at many
conferences
including Ada Europe, ACM SigAda, and STC.

"design-by-contract" is a trademark of Interactive Software
Engineering Inc.

Re: ANNONUCE: Public technical briefing on SPARK, Houston

[Vinzent Hoefler]

rod@praxis-cs.co.uk (Rod Chapman) wrote:

>As a "warm up" event for ACM SigAda 2002, Praxis Critical Systems will
>be
>presented a public technical briefing on SPARK on Friday 6th December.

Alas, too early for me. :-(

>"design-by-contract" is a trademark of Interactive Software
>Engineering Inc.

Oops? But "programming-by-contract" can be used freely, I hope!?


Vinzent.