- To be more precise; it is not the formal methods in itself I dislike, but the prominence they seem to have at prestigious software engineering conferences. I think it is not at all in proportion to how well-used formal methods are among professional development.
- Formal methods are really attractive from a researchers perspective. You can use concepts as theorem, proof and deduction and other nice things. But nice is not the same as relevant.
- Even though I have heard about formal methods as one of the enablers to establish software engineering as a "real" engineering discipline for almost ten years I still don't think they are nearer being well-established now than then.
- Some claim that you can never be sure of the software unless you can prove properties about it, and I agree that presently formal methods are the only technique that promises to do so. But there is a lot of successful software out there which have not been proven.
- Specifications that fulfil the requirement of being interpreted formally are hard to write. Compare it to learn a new programming language and be proficient enough to use it without any side effects.
- I don't know if formal methods scale well. It is one thing to use it on a nice prototype system with 30 entities developed in your lab. It is another thing to use it on a system with 500 entities, many of these with quite varying quality in requirements and code.
- I still don't know of any that uses formal methods for real; i.e. as part of the normal way in products shipped to customers in business intent on making money. Not in one-shot attempts, pilot projects or by non-profit organisations.
A search on google skolar of industrial+software+formal+methods list papers from the 90s as the top results. And these seem more to be arguments against what I claim above rather than actual reports of usage. I really would welcome examples.
16 September 2010
Why I don't like formal methods...
I know the title of this port is a bit controversial and with it I alienate a lot of researchers, even at my own department. But I will try to clarify my arguments and hope that someone can prove them to be wrong.
Subscribe to:
Post Comments (Atom)
9 comments:
Take a look at
http://www.astree.ens.fr/
Does verification of production code for aerospace count?
Ian Peake
Yes, it sure does count.
Astree is one example where formal methods have been used for produciton code and is a counterpoint to my last item on the list above.
I am curious if it was integrated in every programmers toolbox, e.g. they used as often as they pushed "compile" (same as lint many years ago).
Hi,
So, I recognize your points, and note that it can be difficult to find "success" stories for formal tools.
You are definitely correct when it comes to the price of using formal. It is far more effective to use tests and then fix bugs that customers report for over 95% of the software out there (maybe it's as high a number as 99.9%). However, for the remaining software, this iteration-based approach doesn't work. Quite often the remaining 0.1-5% involves either security applications or hardware designs (where it's often impossible to fix a processor after its been fabricated without a serious performance penalty). In these cases, the extra cost of formal can be worth it.
Also, formal methods are going to be more important in the future than the past, because systems are growing to be too complicated for testing alone to be a satisfactory verification story -- there are just too many border cases, and formal specification and verification is the only thing that guarantees we catch them all. This being said, you will probably never find a formal methods person that says we need to get rid of tests. It's just that testing is no longer as productive as it once was.
Finally, I'll address the point about scaling. Model checking (one of the main subfields of FM) has made a lot of progress, but it is commonly known as the formal approach that doesn't scale (the machine runs out of memory or time). Of course, this technology will continue to improve and its limits will be raised. But, then so will the verification challenges grow more complex. Theorem proving is the other subcategory of formal methods -- and this, even though it takes a lot of person-hours, scales much better. Instead of just opening up the problem and blasting through every state, the proof engineer must make abstractions and then prevent the theorem prover from using that implementation when doing the verification. This is a very scalable approach.
As for the success of FM, I know mostly of ACL2 successes, as that's my pedigree. ACL2 was used to achieve EAL level 7 (or maybe it was 6) status from a US security agency for a particular hardware stack. Here are some other success stories of ACL2:
http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html#Processor-Models
Hope this helps,
David
ignore this -- seeing whether using a particular account will auto-subscribe me
I conclude I have selected the smart and inconceivable website along with interesting stuff.Mark
We got about an hour away and my car started making very odd noises. I checked the temperature..everything was normal...so we carried on. spoconcept.com
I agree that presently formal methods are the only technique that promises to do so. ipad repair
This written piece gives fastidious understanding yet.
whole life insurance policy cash value
It feels awe-inspiring to read such informative and distinctive articles on your websites.
payday loans is st paul mn
Post a Comment