In his book, "Software abstractions", Daniel Jackson gives two reasons why he thinks formal specification is not used more widely (page 2). The first obstacle is that the notations have had a mathematical syntax that makes them intimidating to software designers. A second obstacle is the lack of tool support beyond type checking and pretty printing. Although theorem provers have advanced dramatically in the last 20 years, they still demand more investment of effort than is feasible for most software projects. Daniel Jackson's approach, Alloy, is a well-balanced solution to these obstacles.You may have a look at http://alloy.mit.edu/

With more than ten years of industrial experience, I would definitely say, it is a matter of knowledge of the engineers (not everyone knows a suggested method, and quite often, there is the not-invented-here symptom); but also non-IT-managers simply are not able to understand those abstractions and thus quite often neglect that they are useful.

I Think you must go for the book written by Daniel Jackson as the same Valedon has written in his post for this question..... This book is good and focus on the different aspects of issues encountered by the engineers....

There is one more issue to point out. The question “Do they justify their costs?” is related to business policy of the software provider. In many cases it is more important to be the first or to be the cheapest with a product, than to provide reliable and dependable software – it just the question: to be or not to be? In other cases the money gain is in a long software maintenance contract or possibilities to provide new and new versions. Hence the product has to be imperfect.

Only very few software projects have to be of good quality. When a bug in software can lead to a disaster (human injury, financial loss), when the risk of juridical costs is high, then spending money on good quality software is justified. Than managers accept the cleanroom software engineering process or similar ones, where not only testing team but also formal method team is formed.

Looking on less formal methods than mentioned above, there are PragmaDev tool suit, which is based on SDL-RT language. This technique is useful, when a solution for communication between autonomous entities is under development. Other such technique is SPIN/Promela.

I'd say it depends on what you are designing. If you look at it from a process perspective, the whole software development process is like a funnel, from vague requirements over a (hopefully) not so vague design to a concrete implementation.

While this is usually fine for systems where there is no "right" or "wrong" solution (the look and feel of a web shop, for example), other systems are much more restrictive. You don't want to be vague about alarm and shutdown criteria in the control software of a nuclear power plant or in aircraft control.

So I think using formal methods will be worthwile in only some scenarios, while in others semi-formal notation (such as UML) will suffice.

Having worked as an industrial software engineer for 20 years, but also participated in formal methods research, I think one of the major reasons that they are not widely used is that they are developed without much reference to the problems that actually cause us problems in industry. The return on the investment required to apply them to realistic problems often isn't given much consideration either.

I won't deny that ignorance and "NIH" attitudes play their part too, but there are quite a number of us in industry who have tried formal methods for real and yet have difficulty identifying many places where they would be a great help.

(My affiliation on Research Gate is a university, but that's just a part time affiliation, I'm really a working software engineer).

the thing is they know the logical findings. According to the formal methods, it is academical part, so they know the logical part on that. in the integration stage they face manual v/s logical outputs of their projects. As a software engineer, he may know the formal methods. But if he knows academically then he can incorporate. otherwise it will be an issue.

Software Reliability is also very much concern.

Ignorance and absence of new forms to adopt methods and techniques. Those whom work with formal methods have used the same [tool kit] during years and it [sometimes] cannot be applicable to modern software development processes and tools. Thus, it's a challenge, because them are convicting all developers to change your view for using something older, lower, and fewer smart from the project stakeholders view point, resulting in -> [growth up the estimated cost]

V&V processes need be updated to something like it -> [OWL to AspectJ] a tool that integrates V&V in the software development process in an easier way!! https://www.youtube.com/playlist?list=PL2A1683ADE582CA00

Major issues in software development are Quality, Cost and Schedule.

We have been very successful with using formal models in OS development. However, every time we start a new project using formal models, we have to face the question on how detailed the model should be. If it is too detailed on an industrial serious software project, formal models will very soon reach its practical limits. On the other side, with increasing abstraction levels formal models lose their additive effect rapidly. We noticed that there is no one-fits all solution for that. We did also not find yet good decision criteria to help us on finding the right abstraction level for a formal model.

It depends of how formal the method is... I try to make a list of issues based on my experience:

1. EXCEPTIONS OF THE METHOD. A lot of formal methods contain arguments like "without restricting the generality, suppose that ...." (however, the set is sorted, ordered, the determinant is different from Zero, etc) There are a lot of conditions and preparation steps that must be designed, and were not clearly mentioned in the formal method. Finally, the implemented method is about three time longer than the formal method, because we implement preparation steps and we recognize exceptions inside the implemented method.

2. SPACE ISSUES. We must reuse and rewrite buffers, combine RAM and hard disk, etc. Not all ideas come from the first time, there are many versions to implement and a lot of experiments to do.

3. NUMERICAL TYPE ISSUES. Very frequently numerical types like int (32 bit) are not enough to carry out a formal method.

4. NUMERICAL ISSUES, like bad behavior if some matrices are almost singular. Again, a lot of conditions must be implemented. It is diifficult to guess the best epsilons making an application robust and secure.

5. TIME ISSUES. Every application can be optimized and done three to eight times faster than it was in its first implementation. However, I recommend to do this when all other issues have been solved sufficiently well. Moreover, the experience got with the method and its domain of application, which has been accumulated by solving the other issues, can be now used to optimize time issues.

6. PARALLELIZATION ISSUES. This is the ultimate optimization for time issues, and suppose the best knowledge and understanding of the method, of the steps which need more computation time, etc. I recommend to do this first wenn all possibilities of one-core optimization have been used.

I will be happy for commentaries and answers. Thank you.

Frequently the fact that formal methods don't solve a problem which the industrial engineering teams believe that they have.  Along with lack of tool support, which can be a show-stopper, lack of commercial awareness and poor cultural fit between the researchers and practitioners.

Another issue that I did not see in the tread is that most regulators require "objective evidence" of functionality. To provide this objective evidence they rely on bench testing, because it is generally considered most definitive and has the fewest number of assumptions. The UK might be the exception to this notion.

Like Mr. Woods, my primary background is 35 years of developing and testing safety critical/high reliability software.

Dear All.

Firstly, all projects follow the same template, but all projects do not need to implement all aspects of the template. So, whether it is industrial or laboratory, bigger software projects are made up of smaller modular units.

Secondly, software development is more about real-life issues than theoretical trappings. Critical decisions to be made has nothing to do with formal or no-formal methods. I do suppose that some of us must have come in contact with this principle, "Working From The End." The same principle applies in software development. Their is always an issue to solve. That is why money is involved.

Thirdly, that a program code section looks ok by principle does not mean that it will run without errors when passed through the Integrated Development Environment compiler. Furthermore, the precisions from considerations for mathematical foundations in software development depend on which part of the PC is being considered - RAM, HDD, CPU, Video, etcetera.

Finally, every project is special and thus a degree of study must be made in order to evaluate a lot of approaches.

The attached document is titled, "Software Development at Microsoft Observed: It’s about people … working together."

Always remember that, until AI software eventually takes over software development, it is still people doing the coding. Even at that, the robot must still be switched on.

Thanks All.