Abstract

This talk will focus Praxis’ experience in building so-called “High-Integrity” software, where ultra-low defect rate at first deployment is required for reasons of safety or security. The talk will describe Correctness by Construction (CbyC) – an engineering approach developed by Praxis for such systems, and SPARK - a programming language that is designed for strong and entirely static verification. Productivity and defect rate data from several industrial-scale CbyC projects will be presented.

Speaker’s biography:

Roderick Chapman received MEng and DPhil degrees from the University of York, England in 1991 and 1995 respectively. He is currently a principal engineer at Praxis High Integrity Systems, leading the design and development of the SPARK language and toolset. Before joining SPARK team, Rod was involved in the implementation high-integrity real-time and embedded systems, including SHOLIS (the first system implemented to the Def Stan 00-55 SIL4 standard), the Lockheed Martin C130J Mission Computer, and the MULTOS CA . Rod has presented tutorials, papers and panel sessions at many conferences, including NSA HCSS , Ada Europe, and SSTC . He is also an SEI -certified PSP instructor and a Fellow of the British Computer Society.