Correctness by construction: developing a commercial secure system

Praxis Critical Systems recently developed a secure certification authority for smart cards that had to satisfy performance and usability requirements while meeting stringent security constraints. The authors used a systematic process from requirements elicitation through formal specification, user interface prototyping, rigorous design, and coding to ensure these objectives´ achievement. They show how a process that achieves normal commercial productivity can deliver a highly reliable system that meets all its throughput and usability goals