FM-BIASED is a study project to establish the business impact of formal methods in several industrial and business sectors where security standards are enforced.
In most of those sectors, compliance verification may be difficult because most automation are legacy systems, so that industrial stakeholders must face the prospect of either trying to validate ageing systems designed many years ago, or redesigning their functions anew.
Increasing stress of several critical infrastructures, and increasing danger for attacks to key Critical Infrastructure components, such as automation and controls, has promoted development of security standards for critical infrastructure protection and process automation at large, such as the NERC CIP and ISA 99, within the broader framework of the Common Criteria.
Crucial system functions tend to be hardwired, such as protocols, parallel processing algorithms, operating system kernels etc. This opens a prospect for the application of formal methods to prove properties of relevant system components where those functions are embedded, like standard compliance.