Baltimore and DC SIGAda


Our Next Joint Baltimore and DC SIGAda Chapter Meeting
is scheduled for
Thursday, 10 March 2004 at 7:30 P.M.
Rod Chapman and Martin Croxford, both of Praxis High Integrity Systems
will be speaking on
Recent Results with Correctness-by-Construction and SPARK
at the MITRE 2 Building in McLean, Virginia
We welcome the Washington DC ASQ Software SIG, who will be joining us for this special meeting.


Attention:

To Members and Friends of Baltimore and DC SIGAda and the Washington DC ASQ Software SIG

Next Meeting:

Our Next Meeting is scheduled for Thursday, 10 March 2005, as a Joint Meeting of the ACM Baltimore SIGAda Chapter, the ACM DC SIGAda Chapter, and the Washington DC ASQ Software SIG. Ron Chaptman and Martin Croxford both of Praxis High Integrity Systems will be speaking on "Recent Results with Correctness-by-Construction and SPARK".

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.

Abstract: Recent Results with Correctness-by-Construction and SPARK

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.

Presenters:

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.

Rod_Chapman.jpg
Rod Chapman
Martin_Croxford.jpg
Martin Croxford

Venue

MITRE2
Room 1N100 A/B
The MITRE Corporation
7515 Colshire Drive
McLean, Virginia 22102-7508

Directions

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.
Once on Colshire Road, MITRE2 is the building immediately in front of you. A tiny traffic circle is designed to take you to the front of MITRE2 and to MITRE1 (the Hayes Building). The directions below route you to the parking garage behind the MITRE2 Building. This is a logical left-hand turn at the traffic circle. After the turn, MITRE2 will be on your right.

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

1. Take Exit 46B (McLean, Route 123);
2. Go North onto Route 123;
3. Turn right onto Colshire Drive (at second light);
4. Take third right off of the small traffic circle;
   (a logical left hand turn);
5. Proceed ~ 50 meters; Turn right into parking garage.
6. Visitor Parking is located on Levels 2 and 3
   (the walkway to the lobby is on Parking Level 2)
7. If door is locked, contact Security using phone by door
   (at entrance to MITRE2 from the Parking Garage)
8. Check in with Security at Security desk in lobby
   (You will need a photo ID)

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

1. Take the Dulles Airport Access and Toll Road to Exit 19;
   (From I-495, this is labeled "To East I-66");
2. Take Exit 19A;
   (following signs to Route 123 South, Tysons Corner);
3. Bear right onto Route 123 (towards Tysons Corner)
4. Turn left onto Colshire Drive (at first light);
5. Take third right off of the small traffic circle;
   (a logical left hand turn);
6. Proceed ~ 50 meters; Turn right into parking garage.
7. Visitor Parking is located on Levels 2 and 3
   (the walkway to the lobby is on Parking Level 2)
8. If door is locked, contact Security using phone by door
   (at entrance to MITRE2 from the Parking Garage)
9. Check in with Security at Security desk in lobby
   (You will need a photo ID)

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

Slides From Recent Presentations Available:

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 Put on Your Calendar:

  • 12 April 2005 - The next meeting of the ACM Baltimore SIGAda Chapter Meeting for Tuesday - TBD will be speaking on TBD.
  • 12 May 2005 - The next meeting of the ACM DC SIGAda Chapter Meeting for Thursday - TBD will be speaking on TBD.
  • 13-17 November 2005 - SIGAda 2005 will be held in Atlanta, Georgia. Details at http://www.acm.org/sigada/conf/sigada2005

DC SIGAda Home Page and Maillist:

Please visit the DC SIGAda Web site at http://www.acm.org/sigada/locals/dc/ and the Baltimore SIGAda web site at http://www.jhuapl.edu/sigada/index.html for additional information.

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:

LISTSERV@ACM.Org

with the body containing:

subscribe SIGAda-DC Your Name

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

LISTSERV@ACM.Org

with the body containing:

signoff SIGAda-DC

Business:

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.

Jeff Castellow, Chair, DC SIGAda


If you have comments or suggestions, email the DC SIGAda Webmaster

updated 22 February 2005