Consulting

Ada9X Language Precision Team

Several advisory groups were established to provide suggestions and criticism to the Ada 9X Mapping Revision Team, the small design team that revised the definition of the Ada programming language. [Gua94] provides an overview of an advisory group called the Language Precision Team, which based its criticisms on attempts to construct formal mathematical models of the design. ATC-NY directed the Language Precision Team.

The Annex H rapporteur group

Annex H of the Ada language definition addresses requirements for high integrity systems. The ISO Ada group (WG9) established the Annex H Rapporteur Group (HRG), under the chairmanship of Brian Wichmann, at the National Physical Laboratory (UK), to determine how to reduce the verification and validation costs of systems written in Ada [ISO/IEC]. ATC-NY participated in this group as a natural extension of our work on the Language Precision Team.

Compiler for a train protection system

ATC-NY served as a consultant to Union Switch and Signal on the design of a compiler for a graphical language used to program train protection systems. We provided a formal semantics to the graphical language and an efficient "code carrying proof" procedure that allowed a very simple checking program to verify automatically that a graphical program had been correctly compiled [Pro96].

References

[Gua94] D. Guaspari. Formal methods in the design of Ada 9X. In Proceedings of the Ninth Annual Conference on Computer Assurance (COMPASS '94), 29-37. http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=318469

[ISO/IEC] Guide for the Use of the Ada Programming Language in High Integrity Systems. ISO/IEC DTR 15942 http://www.open-std.org/jtc1/sc22/WG9/n359.pdf

[Pro96] J.A. Profeta III, N.P. Andrianos, B. Yu, B.W. Johnson, T.A. DeLong, D. Guaspari, and D. Jamsek. Safety-Critical Systems Built with COTS. Computer, vol 29(11) (Nov. 1996), pp. 54-60. http://doi.ieeecomputersociety.org/10.1109/2.544238