Platform Dependent Verification: On Engineering Verification Tools for 21st Century ∗
2014
With the increase in complexity and degree of parallelism of computer systems, it became even more important to develop formal methods for ensuring their quality. Correctness and reliability became a must have flavor for business success, and therefore, various techniques for automated and semi-automated formal verification and analysis have been designed and successfully applied. Formal verification and analysis bring many benefits such as early integration in design process, more effective detection of logic errors, etc. Even though introduction of formal analysis is rather costly, it pays off after all as it results in significant reduction in verification time as well as development costs and time-to-market. Attempts are being made to integrate formal verification techniques and tools with other design approaches to support engineering of complex industrial systems. The iFEST Artemisia project [59] is an example of a promising tools integration in embedded systems domain. Model checking is a distinguished technique of formal verification of complex hardware and software