Slashdot Mirror
Tools To Automate Checking of Software Design
heck writes "Scientific American describes some of the work to develop tools for examining the design of software for logical inconsistencies. The article is by one of the developers of Alloy, but the article does reference other tools (open and closed source) in development. The author admits that widespread usage of the tools are years away, but it is interesting reading the approach they are taking regarding validation of design."
Back in the mid-80s I attended a seminar in Atlanta, it was about automated software engineering... and tools and workbenches that would take as input specifications and design parameters and would crank out entire suites of software/applications. (Heck, there was even a new acronym for it, can't remember what it was, but it was a hot, hot, hot button for a few years.) We were pretty much warned our careers were over, automation was here to generate what we as professionals had studied years to create.
It never happened. It never came close to happening. We are as far away today or further from tools that can generate applications transcendentally.
I was skeptical then, I'm skeptical now. Tools like the ones described are useful, but they're not foolproof, and they hardly supplant the intuition and "art" that is programming.
At best tools are an adjunct to the software development process, not to be a replacement for common sense testing and design and code walkthroughs. I could construct many scenarios that logically would be consistent but have no relationship to the desired end of the application, i.e., a logic consistency tool would not detect a problem. Any poorly designed system with these "new" tools applied will merely be rigorously poor systems.
As for the prime example (in the Scientific American article) of the Denver International Airport baggage handling debacle, I doubt logic analysis tools would have had much impact on the success or failure of that effort. I knew people involved in the project, and "logic consistency" in their software was the least of their problems. (I would have loved to been on a team to design and develop that system -- I think it was a cool concept, and ultimately VERY feasible... )
I did get one benefit from the Atlanta Seminar -- I got a football signed by Fran Tarkenton (he was CEO of one of the startup companies fielding a software generating workbench).
For members of IEEE with a subscription to IEEE Computer Society's Transactions on Software Engineering, the last issue (April) has a very interesting article related to this stuff titled: Interactive Fault Localization Techniques in a Spreadsheet Environment. Basically, the article explains how they have worked to develop and test techniques that allow "end-user programmers" (people who create formulas in spreadsheets and such) to use automated fault localization testing tools to help debug their "applications" (spreadsheets) at runtime. Pretty interesting stuff that they found in their analysis. (It's easier for you to just go read it than for me to attempt to summarize it at the end of my work week. ;)
From what I'm reading it looks like these programs preform all sorts of different executions, thats great and all, but they probably dont behve like real people do. The average user isn't going to create a file and then (in the middle of that) start running the delete file interface. Also I doubt these tests include other common user issues (like clicking the same function over and over again if it doesn't respond immedietly). Maybe I'm just not understanding what these do... but if I'm even half right, real world tests are the way to go.
Shots: A Populist Parable
It was a very interesting piece. It talked about the problems of locking (more locks makes deadlocks easier, but they get harder to track down) and the way the code went about finding problems. Basically it remember when any lock was taken or released, which locks were open before that, etc. Through this it can produce warnings. For example if lock B needs lock A, but there is a situation where lock B is taken without A being taken it will flag that.
The article has MUCH better descriptions. But through the use of this the software can find locking bugs that may not be triggered on a normal system under normal loads. Here is summary bit:
"So, even though a particular deadlock might only happen as the result of unfortunate timing caused by a specific combination of strange hardware, a rare set of configuration options, 220V power, a slightly flaky video controller, Mars transiting through Leo, an old version of gcc, an application which severely stresses the system (yum, say), and an especially bad Darl McBride hair day, the validator has a good chance of catching it. So this code should result in a whole class of bugs being eliminated from the kernel code base; that can only be a good thing."
It was a piece of code from Ingo Molnar, you should be able to find it on the kernel mailing-list and read about it.
Kudos, by the way, to LWN for the great article.
Comment forecast: Bits of genius surrounded by a sea of mediocrity.
None of those tools have ever been demonstrated to be cost-effective means of making software more dependable. It's an article of faith that adding a complex notation and another complex set of tools to the development process makes the product any better.
This reminds me of my previous job. One day the owner of the company came up with a brilliant idea. He had just watched the movie "Finding Nemo" and asked me, "have you ever seen finding nemo? You know those little silver fish? I think we should design a system based on those little silver fish. If we get enough small components they can be combined into any piece of software. Eventually we wouldn't need any more components and thus no more software developers. All of our software would be made by sales guys who could just combine these components into any software we need." I remember thinking to myself that we could just start with quarks and we could build everything in the universe. But I didn't say anything and was just happy to not be chosen to be on the team creating the silver fish.
6 years later, dozens of programmers, and millions of dollars, the finding nemo architecture has been a bust. The owner of the company refuses to give up on the idea. They currently have created components of "and" and "or" gates and use "wires" to put them together. It reminds me of entry level electrical engineering. Back before they tell you that writing software on flash is usually easier and cheaper than wiring together dozens of IC's. In any case, I eventually did get sucked into the project and promptly left the company.
These types of algorithmic testing tools are useful for small, truly critical functionality that has to work perfectly. It's not cost effective to try to model typical complex software in a manner that supports testing as described in the article. Most programming is not about designing the next great single algorithm, it's about integrating data, interacting with users, and providing all the logic to handle the myriad special cases that make up user requirements. Rarely is such a testing tool going to cover all the possibilities without a gargantuan effort to model the software -- which effort will most likely not be able to keep up with the actual development anyway. These tools won't be widely accepted until they can automatically read source code and create a software's model without programmer input.
--- JurassicPizza
Sounds like some producer wants a magic-bullet program to replace some bad-performing designer. Even in the case of a 'useful' tool to apply to projects, this is likely to become an excuse for when an inconsistency is found later on by QA- "the program said it was good!"
It's not going to find everything, let alone fix it. See Turing: the halting problem.
Yes, we understand these tags always apply: fud, dupe, typo, slashdotted, topic name
If they're checking the software design for inconsistencies, then they're too late. What is needed is some way to formally specify user requirements, so that they can be checked for completeness and consistency. Use cases are nice, but they're not sufficiently rigorous to capture absolutely all the requirements. I know there have been some schemes tossed around for requirements validation, but none that I've seen have really been general-purpose enough for the average project.
Just junk food for thought...
Making a tool to check most programs for errors sounds extremely complicated, but wouldn't it be possible to make a more simple tool that checks the security of a PHP/MySQL website?
A good design correctly models the concept of what it is you're trying to achive with the program. Ultimately this means the programming interfaces (APIs) for each concept are correct [1]. Don't design interfaces around procedures. Don't design interfaces around the physical world. Design to *concepts* and *ideas*. This is superior because you will never discover at a later time that the code is fundamentally flawed and needs to be totally re-written. If the interface correctly models the concept, by definition, it CANNOT be wrong. If it is wrong then you simply didn't understand the concept well enough or you failed to translate that concept into a suitable interface and you just need to think more and type less. If you do get things right you'll find that major peices dovetail together perfectly [2]. The implementation can be wrong and may need to be re-written but if the interface correctly represents the concept the re-write will be localized to one library or part of a library. That is a much more straight forward matter than using a bad design and finding half way through a project that the required changes transcend the whole system.
And thus you cannot validate a design because that would require representing a concept and determining if an interface suitably models it. That is HARD. If that were possible you would effectively have a thinking, rationalizing, brain (Artifical Intelligence) in which case you wouldn't be dorking around with validating programs, you would be dynamically generating them.
[1] Frequently people advocate that interfaces are "well defined". That just means there are no holes in the logic of it's use. Personally I think a well defined interface is useless if it does not correctly model a concept. You can always go back and fill in the holes later.
[2] Although this is also when you discover that you didn't get the concept right and need to adjust the interface (hopefully not by much)
It's basically a nifty, graphical declarative programming language. Anyone familiar with Prolog and set theory will breeze through the docs, only to ask "Why?" at the end.
One of the tutorials, for example, is a way to get Alloy to create a set of actions for the river crossing problem, and list them. Thus, alloy has saved the poor farmer's chicken. It's actually quite a cool set of toys for set theory, and it generates all possible permutations of a system with rules and facts based on how many total entities there are in the system, and checks the system for consistency. There are doubtless uses for this, but software development is, at the moment, not one of them.
The other tutorial is about how to set up the concept of a file system. The tutorial sets up a false assertion (assertion = something for Alloy to test), which fails. Here is the reasoning, with summary to follow for disinterested:
Basically this says that in a 2-node scenario, i.e. a root directory with one subdirectory, they delete the subdirectory with their delete function. The way they defined the delete function basically meant that the 'deleted' node could, in theory, be the root of the file system after the deletion operation occured, since there was no constraint on which node of the file system was root after the change. They basically said under these constraints, it was possible to define a 'delete' function that deletes the subdirectory in a 2-node filesystem and then makes that same subdirectory the root of the filesystem.
Good thing we built a model, indeed! A bug in the programming of your model is by no means a valid use for spending a significant amount of effort modeling a concept in set theory. The best part is that all of your effort amounts to mental masturbation--there are no tools for turning this into a programming contract, test cases, or anything. Some projects are in the works in the links area, but they aren't there yet, and only for Java. I don't see how the amount of effort that would be required to model a large scale, realistic project in this obtuse set notation would be worth it for absolutely no concrete programming payoff. Writing HR's latest payroll widget, or even their entire payroll system, is just not going to get any benefit from this.
All that aside, it's concievable that this sort of model programming could find use in complicated systems in which high reliability is paramount. The usual suspects, such as satellites, space, deep sea robots or whatever come to mind--this system could prove, for example, that a given system for firmware upgrades cannot leave a robot in mars in an inoperable state, unable to download new, non-buggy firmware.
But it still can't prove the implementation works. *slaps forehead*
nobody
Microsoft sells collaboration software and project management software. And its products are not shipping any faster.
These guys are touting alloy and tools, sounds like a old CASE wine in new bottle. Did they use these tools to design the tools? Atleast would they use these tools and alloy to create the next version? Could they demonstrate that these tools can handle a project of that complexity? And produce provably better code with no bugs?
Please forgive me if I am underwhlemed.
sed -e 's/Chuck Norris/Rajnikant/g' joke > fact
The point of these tools, is to simply verify the consistency of a design, not to execute or examine existing source code. The steps involved are:
1) Come up with software design
2) Implement software design in one of these tools (model it in Z, or as a state machine using fsp/ltsa)
3) Use said tool to verify the consistency of the design.
Now, this activity, of course, takes a lot of time, and is unlikely to ever be of any use to your average J2EE/Ajax/Enterprise application. Areas where they CAN be of use are in things such as life-critical systems. For instance medical devices, or air plane control systems. Using something like FSP/LTSA you can model, check, and verify that your design does not every allow the system to enter into an invalid state. Now, remember, this says nothing about the final code, there is a separate issue of the code not matching the design, but it is possible to verify that the design does not ever lead to invalid states.
...science of abstraction physics.
yes the software industry is still playing with magic potients and introductary alchemy.
Why is a simple answer to give.
money, job security and social status.
Someone posted that they were warned that their jobs would become extinct upon automated software development.
but the fact is.... who but those who have their job to risk....are in a position to employ such tools?
snake oil software development is a self supported dependancy... far from genuine computer software science (of which we haven't really seen since the US government held the money carrot up for code breakers during WWII.
Alloy is a cool tool, if it does something you want done. But nobody should be fooled into thinking that you can just run Alloy and suddenly your code is perfect. Alloy just helps you check out a model based on set theory, etc... it's a long distance from models like that to the actual code.
- David A. Wheeler (see my Secure Programming HOWTO)