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,93dafc912fab0c6a,start X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2002-11-27 05:30:16 PST Path: archiver1.google.com!postnews1.google.com!not-for-mail From: rod@praxis-cs.co.uk (Rod Chapman) Newsgroups: comp.lang.ada Subject: ANNONUCE: Public technical briefing on SPARK, Houston Date: 27 Nov 2002 05:30:16 -0800 Organization: http://groups.google.com/ Message-ID: NNTP-Posting-Host: 213.155.153.242 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-Trace: posting.google.com 1038403816 16891 127.0.0.1 (27 Nov 2002 13:30:16 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: 27 Nov 2002 13:30:16 GMT Xref: archiver1.google.com comp.lang.ada:31250 Date: 2002-11-27T13:30:16+00:00 List-Id: 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.