Correctness by construction: developing a commercial secure system
Top Cited Papers
- 7 August 2002
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Software
- Vol. 19 (1) , 18-25
- https://doi.org/10.1109/52.976937
Abstract
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.Keywords
This publication has 4 references indexed in Scilit:
- Is proof more cost-effective than testing?IEEE Transactions on Software Engineering, 2000
- Investigating the influence of formal methodsComputer, 1997
- Information-flow and data-flow analysis of while-programsACM Transactions on Programming Languages and Systems, 1985
- Certification of programs for secure information flowCommunications of the ACM, 1977