The "software" problem, i.e., the development of correct and error free software in a cost effective manner is one of the major problems of Computer Science. Application of Formal Methods towards development of software can be one of the promising methods for solving this problem. Formal Methods becomes more important for the case of Concurrent and Distributed Software Systems due to increase in complexity of these systems. They can be applied at the various levels in a software development cycle starting from the Requirements Phase, Design Phase and up to the Coding and Testing Phases.
Model checking Based Techniques have been used fairly effectively for verification and debugging of some of the real world Hardware Systems. Our next challenge is to take these techniques for applying to software systems also. To do this, firstly, we need to develop methods that can handle large problem sizes and for containing the state explosion problem in reachability based methods. Techniques such as the Symmetry based methods etc. and hybrid methods ,i.e. methods based on combining different techniques need to be further explored. Secondly, we need to concentrate on real-world applications. That is, we need to apply our tools on real-world problems and see their effectiveness on these problems. For this, collaboration between industry and university researchers is essential. Finally, more tools need to be developed to integrate modelchecking systems into standard CASE tools.