23.2MB zip File
Here’s what’s included:
- The “Core” Tokeneer ID System Software
- The test cases derived from the system test specification
- The “Support” Tokeneer ID System Software
- The test tokens and biometric data
- The project documents
Tools to get the most out of Tokeneer
In order to reproduce the proofs for Tokeneer, create new proofs, or change Tokeneer and prove properties in the updated version you will need the SPARK Toolset.
You can use the SPARK Pro toolset:
If you are a free software developer or an academic you can use the SPARK GPL 2012 edition toolset available on AdaCore’s Libre site.
Ada Development Environment
To run Tokeneer (currently available on Windows only) you will need an Ada compiler such as the one that comes with the GNAT Pro Ada Development Environment.
If you are a free software developer or an academic you can use the compiler in the latest GNAT GPL release available from AdaCore’s Libre site.
Specialized Tools for Type Checking and Formatting Z Documents
Three of the Tokeneer project documents use the Z notation. To reproduce or modify these documents, you will need the MikTex typesetting system and the FUZZ typechecker.
In this video, project manager Janet Barnes discusses the story and details behind the Tokeneer project. View Video »