Correctness by construction: Developing a commercial secure system

Anthony Hall

doi:10.1109/52.976937

2002-01-01

105

PRE

Anthony Hall

Roderick Chapman

DOI：10.1109/52.976937

原文链接

原文求助

摘要

En 中文

By Anthony Hall and Roderick Chapman, pp. 18-25. 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.