2015/11/03 by Janet Barnes, Barnes, Janet
Computer Science · #Advanced Malware Detection Techniques #Formal Methods in Verification #Security and Verification in Computing
paper · doi:10.14279/tuj.eceasst.46.680
openalex publication_date 2024/03/25 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/01
Altran Praxis has used formal methods within its high integrity development approach, Correctness by Construction (CbyC), for a number of years. The Tokeneer ID Station (TIS) developed for the US National Security Agency (NSA) is one example of a development using formal methods and the CbyC approach. This project used a number of rigorous techniques including formalisation of the specification using the Z Notation, refinement of the specification to a formal design, software development in SPARK with proof of absence of run-time errors of the software and proof of system properties. The project has stood up well to the intense scrutiny it has been subject to since it became available to the wider community in 2008, with only five errors being found. Despite the general success of the approach there are challenges to using formal methods in an industrial context. By looking at a number of key properties that affect the success of deployment of tools and techniques in industry we attempt to put the challenges of industrial deployment of formal methods into perspective.