Static analysis and dynamic analysis are the yin and yang of program analysis. Static analysis has the benefit that it can reason about many, or all, runs of a program at once. However, to do that it must abstract aspects of the programs semantics. For large or complicated programs, the resulting imprecision can lead to an intolerable number of false-positive alarms. Dynamic analysis reasons about particular program executions precisely, using a (perhaps automatically generated) test suite.
The state-of-the-art in systems assurance is based on testing, simulation and certification, and it is currently incorporating formal verification for some of the system's components. Formal verification has a limited use at present because it calls for a clean slate design and development, which are not always possible or practical, and because it is computationally challenging for large systems. Therefore, formal verification is commonly constrained to single software or hardware components that can be adequately modeled.
Cyber-Physical Systems (CPS) have been increasingly subject to cyber-attacks including code Non-control data attacks have become widely popular for circumventing authentication mechanisms in websites, servers, and personal computers. Moreover, in the context of Cyber-Physical Systems (CPS) attacks can be executed against not only authentication but also safety. With the tightly coupled nature between the cyber components and physical dynamics, any unauthorized change to safety-critical variables may cause damage or even catastrophic consequences.
Formal methods provide powerful tools for the analysis of complex software, enabling engineers to establish assurance of high quality in their software. The SPARK language and tools build upon the foundation of Ada and allow engineers to program not only their software, but also their specifications and their proofs. SPARK thus provides engineers a practical, industrial strength formal method.
