Background - Using Event-B for Critical Device Software Systems - page 35

2.10.11 NIST Token-Based Access Control System (TBACS)
Token-Based Access Control System (TBACS) is a smart card access control sys-
tem that is based on cryptographic technique. This system was developed by US
National Institute for Standard and Technology (NIST) [ 25 ], where they used for-
mal techniques in order to verify all the essential safety properties. A set of permit-
ted and prohibited actions were the main safety properties that were mainly focused
on information access and transmission. These safety properties were formally ex-
pressed in mathematical logic using a set of invariants. In this development process,
a theorem prover tool FDM was used for verification purpose. The FDM tool was
very useful to identify a significant flaw related to the smart token that was eas-
ily removed without any excessive cost of the system development. The TBACS
experiment provides a proper guidelines to satisfy related standards.
2.10.12 The Intel ® Core ™ i7 Processor Execution Cluster
Intel Core i7 processor [ 65 ] is used to verify using formal methods. The Intel Core i7
processor is a multi-core processor, where formal methods were used for pre-silicon
validation of the execution cluster EXE, a component that is responsible for carry-
ing out data computations for all microinstructions. The EXE cluster implements
more than 2,700 microinstructions and supports multi-threading. The formal meth-
ods were used here to verify the data-path, control logic, and the state of the com-
ponents. Formal methods based on symbolic simulation, and inductive invariants
were used in the validation process of the processor. The significant contribution
was of this project that the formal verification completely replaced traditional cov-
erage driven testing and proved that the formal verification was a viable alternative
approach for traditional testing techniques in terms of time and costs with respect to
quality of the system.
Here, we have presented a list of projects related the critical system development
using formal methods. All these projects have used different kinds of formal tech-
niques for discovering the bugs at the early stage of the system development and
have shown that formal methods could be a significant approach for verifying the
systems. Formal method techniques are very expensive and hard to apply in the sys-
tem development process due to complexity of mathematics and the limitations of
existing tools [ 26 , 64 , 88 ]. Main limitations are, each tool based on formal method
can be used for only specific purpose, and a formal model developer requires good
experience to use formal methods and knowledge of related mathematics. To know
the significant use of formal methods [ 13 , 14 , 23 , 97 ] as well as handling its com-
plexity, in this topic, we propose a new development life-cycle methodology, where
each step is based on formal techniques. In this context, we develop a chain of
techniques and tools for supporting the system development life-cycle using formal
techniques from requirement analysis to code generation.