In computer science, Formal methods refers to mathematically based techniques for the specification, development and verification of software and hardware systems. The approach is especially important in high-integrity systems, for example where safety or security is important, to help ensure that errors are not introduced into the development process. Formal methods are particularly effective early in development at the requirements and specification levels, but can be used for a completely formal development of an implementation

A Formal specification is a mathematical description of software or hardware that may be used to develop an implementation. It describes what the system should do, not (necessarily) how the system should do it. Given such a specification, it is possible to use formal verification techniques to demonstrate that a candidate system design is correct with respect to the specification. This has the advantage that incorrect candidate system designs can be revised before a major investment has been made in actually implementing the design. An alternative approach is to use provably correct refinement steps to transform a specification into a design, and ultimately into an actual implementation, that is correct by construction

In the context of hardware and software systems, Formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods. Formal verification can be used for example for systems such as cryptographic protocols, combinatorial circuits, digital circuits with internal memory, and software expressed as source code.

Correctness by Construction (CbyC), originally introduced by Praxis, is a software development method for building secure and safety critical software. CbyC provides developers a good productivity and low-defect rate. CbyC has several features such as rigorous requirements engineering, the use of formal methods, a systematic, multi-view approach to system architecture, and static analysis using SPARK.

Praxis undertook the TIS (Tokeneer ID Station) project and published the result recently. In the project, core functions of Tokeneer System were developed using the CbyC development process. They reported that they produced a high quality and low-defect system conforming to the Evaluation Assurance Level 5 (EAL5) requirements of Common Criteria.

In our lab., we are applying CbyC process into an industrial case study. The system being developed is a safety-critical component of a railway mockup system. In the system, our main focus is to ensure trains have no crash caused by software faults.

Concerns about the security of communications, transactions, and wireless networks are inhibiting realization of benefits associated with pervasive connectivity and electronic commerce. These concerns include exposure of data on systems, system compromise due to software attack, and lack of user identity assurance for authorization. Users and IT organizations need the industry to address these issues with standards-based security solutions that reduce the risks associated with participation in an interconnected world while also ensuring interoperability and protecting privacy.

There has been a movement of guiding these issues and in mainly to develop, define, and promote open, vendor-neutral industry specifications for more trusted and secure computing. These include hardware building block and software interface specifications across multiple platforms and operating environments. A critical problem is the increasing threat of software attack due to a combination of increasingly sophisticated and automated attack tools, the rapid increase in the number of vulnerabilities being discovered, and the increasing mobility of users. The large number of vulnerabilities is due to the incredible complexity of modern systems