Baltimore and DC SIGAda

The meeting will be held in Rom 1N100A/B of the MITRE 2 Building in McLean, Virginia.

Please post the announcement for this meeting. A convenient 2-page announcement is available at http://www.acm.org/sigada/locals/dc/200503_Correctness_by_Construction.doc

Pizza and soda will be available at 6:30 PM for a contribution of $5.00. You are encouraged to arrive by 7:00 to network. The program will start by 7:30 PM.

Please register for the meeting by COB Tuesday, 8 March 2005 by contacting Scott Ankrum at (703) 883-6127 or ankrums@mitre.org. Please include your company affiliation and citizenship.

This presentation covers some recent developments and industrial projects using Praxis' Correctness-by-Construction process and the SPARK language and toolset. Metrics from five recent projects will be presented, covering project size, criticality, productivity and defect rate. Finally, we will compare the Correctness-by-Construction approach with that of the SEI's PSP and TSP.

Correctness by Construction (C-by-C) is a development approach that aims to tackle the risks of producing high-integrity software systems. Its fundamental principles are:

1. Don't introduce defects in the first place.
2. If you do introduce defects, find and remove them as soon as possible.
3. Appropriate use of "formal" notations and methods.
4. Produce certification evidence as a natural by-product of the development process.

C-by-C has been used to develop the highest-integrity safety- and security-critical systems, meeting the most demanding industry standards. Results, in terms of productivity and defect rate, are an order of magnitude better than those reported for CMM Level 5 organizations, and are comparable with those reported for the best PSP/TSP projects.

SPARK is an annotated subset of Ada designed for the development of high-integrity systems. The annotations strengthen Ada's existing package/contract model to allow full "design-by-contract" to be used. Contracts in SPARK are enforced entirely statically by the SPARK toolset, prior to compilation or testing. The toolset performs static semantic analysis, information flow analysis and verification condition generation, and is supported by an industrial-strength theorem prover.

Dr Roderick Chapman is Product Manager of SPARK with Praxis High Integrity Systems, specializing in the development of programming languages and static analysis tools for high integrity systems. He holds a DPhil in computer science and is a chartered engineer with over 10 years experience of high integrity real-time systems. Rod is internationally renowned for his work on verification of correctness properties of high integrity software.

Martin Croxford is Associate Director for security with Praxis High Integrity Systems, a UK-based systems engineering company specializing in mission-critical systems. He is a chartered engineer with 15 years experience in the software industry. He has worked on software development projects in a range of organizations, and as a software development manager has used Correctness by Construction to successfully deliver a multi-million pound security-critical system.

Rod Chapman and Martin Croxford are both members of the SPARK Team. The SPARK Team recently was awarded the prestigious Outstanding Ada Community Contribution Award at SIGAda 2004.

MITRE2 is on Colshire Drive just inside the beltway south of Route 123. Colshire Road is known as "Scotts Xing" on the North side of Route 123.

Colshire Road is located on Route 123, East of I-495 and West of the Dulles Access Highway.

• Going Northbound on 123 from I-495, Colshire Road is located 2 stoplights on the right.
• Going Southbound on 123 from the Dulles Access Highway, Colshire Road is located at the first stoplight on the left.

From I-495 south of Route 123 (Dolley Madison Boulevard):

From Dulles Access Toll Road or I-495 north of the Dulles Access Toll Road:

To obtain a map of MITRE2 Building and the MITRE Campus, visit =>
http://www.acm.org/sigada/locals/dc/Directions_MITRE2.html.

At the Baltimore SIGAda meeting on 8 February 2005, Stephen Leake of NASA gave an excellent presentation titled: "Stephe's Ada Library; 15 years of Useful Ada Packages" Slides from his presentation are available online as a PowerPoint Presentation at http://www.acm.org/sigada/locals/dc/200502_Stephe_Ada_Library.pdf (pdf, 72.8KB).

Please provide suggestions on the Web sites and its contents. We are particularly interested in ways the Baltimore and DC SIGAda Home Pages can serve you better.

Consider subscribing to our e-mail list. Simply send an email to:

with the body containing:

To be removed from the list, send an email request to:

with the body containing:

Please forward this message to people who might be interested in attending. We welcome all new members as our attendance and interests grow.

Many thanks to all earlier participants, contributors, speakers, advisors, and friends, who are involved in helping to produce and attend the meetings.