Formal Methods and Enterprises...

Question

So...

I teach formal methods in software engineering. I also teach "agile methodologies". Most people seem to think this is contradictory. I think it makes a lot of sense... I also work for a company, where we need to actually get things done :) While I can apply my earned skill points on "specification" in a day-to-day basis, my colleagues typically flee away from the word "formal".

I used to think that this was due to the intrinsic way we learn how to program: we are usually driven to find a working solution, not to understand the problem. Then I thought this was due to the fact that most people in the formal community are not engineers, but mathematicians or computer scientists. Nowadays, I wonder if it just because the formal-methods community hide behind some kind of "obfuscation" law to use all the available UNICODE symbols, actively develop rude, unesthetic tools, and laugh in the face of standards.

Yes, I've been moving from a "blame them" to a "blame us" perspective ;-)

So, my question is: do you use any kind of formal methods in your company? Have you introduced them, or were they pre-requisites? What techniques do you use to clear the fog of mathematics from people's fears and incite them to use formal methods? What do you think current tools are lacking for a more general usage?

Answer 1

Hi

I'm taking a course on 'Specification and Verification'. As part of the course structure we are doing the following- 1. Learning tools like PVS(Prototype Verification System) http://pvs.csl.sri.com/ and SMV(Software Modeling and Verification) http://www.cs.cmu.edu/~modelcheck/smv.html 2. Apart from that we do dissect accidents which happened because of software failures. For e.g. - Failure of Ariane V

I feel formal methods are more applicable to scenarios where the failure cost is more than the design cost. And it seems apt to use them for softwares being used in critical systems. I guess it is used in avionics, chip design etc. and the current automobile industry is also drafting it into practice.

Answer 2

I have tried to get people to embrace formal specification methods a few times (Z and Alloy) and have made the same expirience that you have: Most people, while feeling that they serve a useful purpose, are very uncomfortable using them for actual work.

Funny enough, the same people are more than happy to produce utterly useless UML diagrams in ginormous quantities.

I think there are two main reasons for this:

a.) Many developers are uncomfortable with the level of abstraction required by a formal approach. The fact that most entry-level mathematics education is all calculus and non discrete-mathematics might have to do something with this.

b.) Formal methods require a very bottom up design aproach where you design your core model from the ground up and make it airtight and then connect it up to the actual user requirements by providing an interface on top of it. Since we tend to have requirements drive development efforts, a top-down approach feels more natural although it often leads to inconsistent models. It's like retrofitting a basement underneath your house after it has already been built.

Answer 3

The key to getting people to buy into any methods or methodologies is to show them how it solves problems they are having. If they can see it will make their lives better you have a much improved chance of getting them to adopt the techniques.

And if you can't show them that, perhaps you wanted to adopt the methods based on philosophy rather than practicality. Unless the others share your philosophy then you're not going to get anywhere. And perhaps you shouldn't.

Over the decades there have been a great many methodologies. Newer ones always address the shortcomings of the old ones, yet projects still get in trouble and fail. Why? Because the rock stars that come up with new methodologies are rock stars, and have made a new methodology precisely because they understand the underlying issues and how to apply them. Those who come after tend to blindly follow the recipe, and it doesn't work so well.

So I think the best thing is to teach about the underlying problems and then show how various methods attempt to deal with those problems. The differences in companies, projects, and teams is so great that no one methodology can be applied successfully to all combinations. Learning to choose an appropriate tool and apply it well is crucial.

Answer 4

Working with line of business IT development in an enterprise means having to transfer knowledge about the business from actual business people into the heads of developers. While I myself find abstract maths to be one of the greatest pastimes there is, it's a terrible communications tool. And communications is what it's all about. While I might conceivably have some success convincing IT people to embrace more abstract notations, I basically have no chance with the business people.

While there are some areas where I can see a role for formal methods in an enterprise (math- and logic-heavy specialist software, significant need for provable properties as in safety critical software) they provide little help with getting correct requirements on e.g. how to fulfil a customer order by issuing one or more supply orders to a set of possible external or internal providers.

I think the jury is still out on model based approaches and domain specific languages. I think they will succeed or fail depending on whether they provide quicker feedback from IT to the wishes and needs of the business side, and whether they presume business people will have to do any significant studying.

Technology is easy. Communication is hard. Formal methods may help us do things right, but those I've seen do nothing to help us do the right things. (Yes, these are cliches, but that's because they're inescapably and painfully true.)

Answer 5

Formal methods make no sense in systems where the cost of failure is low.

In a production web application, you've got multiple front-end boxes, multiple back-end boxes, multiple database boxes - if a program on any one of them fails, it's a non-event. Hardware is so cheap that you can build these systems for far less than the cost of formally specifying all your software.

Answer 6

Thank you for all contributions. They are very insightful. Allow me to flame a bit (don't take it personal, though :-)

Most people seem to think that formal methods are just about program verification. Or critical systems. This may be true if we pursue the ultimate cliche: to prove we are doing the program right (v.s. validation, which asks, as a contributor said, if we are doing the right program).

But consider model finding/checking tools, such as Alloy. Learning to use a tool like this takes a negligable ammount of time for anyone used to UML and OO. Still, it can give you immediate insight over your model. It usually takes no more than 10 minutes to find a counter-example over a small enough subset of the model one's trying to use (and that includes describing the model in Alloy in the first place).

Take requirements engineering as an example. One usually draw a lot of UML. Few people use OCL, though, and many business rules are informally annoted in natural language. Why? Time constraints?

Now consider the fact that the majority just uses her/his gut-feeling to prove that a model is satisfiable. Again, why? I can take the same amount of time (probably even less, since I don't need to care about drawing aesthetics) to write that model in Alloy, and just check for satisfiability? And what kind of mathematics do I need to now? "Predicates"? Fancy name for IFs and booleans ;-) Quantifiers? Fancy names for ForEachs()...

What about big information systems? They don't need to be critical... Just try to analyze in your head a conceptual (not implementation!) diagram with over 600 classes. I see many people banging their head in the wall with easy-to-make model mistakes because they missed some constraint, or the model allows stupid things to happen.

The fact is, one does not need to use formal approaches from head to tail. Granted, I could prove a whole application in Coq, and certify that it is 100% compliant with some specification. This may be the Computer Scientist/Mathematician approach.

Still, with a GTD philisophy, why can't I delegate some tasks for the computer and allow it to help improving my development? Is it really a matter of "time", or plain, simple lack of technical abilities and will to learn/inovate?