Tools To Automate Checking of Software Design 128
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."
too hard. (Score:5, Insightful)
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).
Re:too hard. (Score:2)
Re:too hard. (Score:2)
Re:too hard. (Score:2)
True, but the fallout's been useful. Ever used Rational XDE? I see Sun has something similar in the latest Sun Studio 8 Enterprise, but I haven't used it. Basically, it's a round-trip UML modeler: lay out your class diagram, and XDE will generate the code for it. Update the generated skeleton with "real" code, and XDE will update your model from the changes. It's much nicer than trying to do things with Ratio
Re:too hard. (Score:2)
You have a realistic view on Rational Rose and that makes me want t
Re:too hard. (Score:2)
Tools are getting smarter. We need to leverage them to help us write the code, check the code, and maintain the code. They are, however, just tools -- not panaceas.
Re:too hard. (Score:3, Insightful)
I vaguely recall that fad as well. A lot of executives were jazzed about the idea, as they seemed to assume that software was rote and procedural anyway. They viewed programmers as simple translators, not realizing that program code doesn't just facilitate the resulting software, but was the software. Regardless of how many tools you devise to commoditize the basic functions
Re:too hard. (Score:2)
If you state your intentions in a language that the code checker understands (preferrably a language designed to be expressive when it comes to mak
Re:too hard-Intentions. (Score:2)
Tools Have Been Successful (Score:1)
OLTP business applications tend to be the best fit because there are many many forms/transactions to create and they tend to be relatively simple (mostly data validation, some calculations, database update, etc.). The work that is being automated is not creative problem solving but rather the application of a solution multiple times t
AD/Cycle (Score:2)
The thing is, on an abstract level, "Designing Code from Logically-Proven Constructs" (the title of a book by James Martin) makes total sense: If the base elements are logically proven, and if the complex elements are constructed of base elements, then the output will have no un-proven output. However, the design of the programs needs to be at a meta-level to the operation. (Thanks, Goedel!) I coul
Re:too hard. (Score:1)
Bingo! In fact, unless you are working at the very cutting edge of science and/or technology, going where no man has gone before, the really hard part of program design is figuring out just what the heck that desired end really is.
The rest is just a programming exercise.
Computers may be able to prove a program correct, logically consistent and even generate algorithms, but t
Re:too hard. (Score:1)
Let's say that I would say that it is the meat of design.
I've seen computers come up with quite novel design solutions.
There are an infinate number of novel solutions to any given problem. Only a few of them are interesting. Even fewer are suitable. Novelty is the meat of art, not applied mathematics.
It is, of course, up to you what role you assign to art in your design.
KFG
"That's Incredible!" (Score:1)
"That's Incredible!"
(Boy am I showing my age...)
--
It's Better to Have It and Not Need It
Re:"That's Incredible!" (Score:2)
Dijkstra Sceptical too. (Score:1)
Re:Dijkstra Sceptical too. (Score:1, Interesting)
Re:too hard. (Score:2)
I once studied "Z", a specification language that was supposed to eventually be able to feed automatic correctness checkers. I realized how bad the language was when one of the canonical examples required that the design of the code itself be contaminated by the constraints of the specification language.
For some very narrowly defi
Re:too hard. (Score:1)
If the only tool that you have is a hammer, then every problem becomes a nail.
Re:too hard. (Score:1)
Of course, we should remember that the original FORTRAN 0 manual stated that the use of the language would elimate coding errors and the
Re:too hard. (Score:5, Insightful)
Re:too hard. (Score:5, Insightful)
When I was young, stupid and without real-world experience, I also thought UML was crap. However, once you realize that the point of UML is not helping to design, but helping to communicate the design to other developers, it becomes useful (not ground-breaking, not amazing, not neccessary, just useful).
It's like that: when you design a piece of software alone, you can use whatever system you want to model it (keep it all in your memory, write class-structure as pseudo-code etc.). If you need to communicate your design to others, it's good to have a system with defined semantics to formulate the design (visualization is not even the issue here), and one such system is UML; surely not the best, but one that a sufficient number of developers (software engineers, not programmers) are trained to understand.
Lacking such a system of communication, you would first have to explain the meta-model (explain how the description of your design is to be understood) instead of just explaining the design-model itself.
Re:too hard. (Score:2)
I also agree with you about code generation - it is a very minor feature of UML tools. What isn't so minor however is reverse engineering. Taking a legacy project and generating
Blaming your tools? (Score:2)
There are environments that have had great success implementing UML in their design process. My favorite example is from Nokia:
http://www.powells.com/biblio?isbn=0521645301 [powells.com]
I had trouble wrapping my head around UML until I read Jaaksi's books (there's more than one), and I've been using Rational Rose since 1996. I never found or developed a clear system for making it work until I read his books.
A book that clearly describes the case for code generation (and the limits) is t
Re:too hard. (Score:4, Insightful)
at absolute best, it saves you 5 minutes of typing boilerplate class skeletons
The code generation from UML is only supposed to be the class skeletons, and I've got to ask... have you never written an application with more than a handful of classes? The time spent just building the skeletons for some of the applications I've written over the years has taken a helluva lot longer than 5 minutes.
I personally find class diagrams darned useful. I also find use case diagrams useful not because they help the programmer, but because they help to make sure that we correctly understand what the user is asking for.
From reading your post, though, I'm not entirely certain you have actually bothered to learn UML before you started to slam it. You say:
it just doesn't, and never can, portray all the information that text can
Anybody who knows UML knows that an incredible amount of the work is done in text. Sure, you can create state and activity diagrams for your use cases... or you can just attach textual documentation that is typically easier to create and much smaller than state or activity diagrams. This is what you are typically ENCOURAGED to do for anything but the most convoluted process... and when you have a very convoluted process, even text fails.
There are times that it is very useful to have pictures with circles and arrows and a paragraph on the back of each one.
UML is not the best solution for every development project, for very large projects with lots of developers involved, it can certainly make life easier.
Re:too hard. (Score:2)
- Diagrams are useful in design
- Common syntax and standards are useful in technical artifacts (e.g.: code, documents)
Ergo:
- Designing in diagrams using an effective, standard syntax is a joke.
Complaining about UML being insufficient for a complete design is like complaining that CGI is not enough to create a movie. It is both obviously true and obviously besides the point.
Like any decent tool, it serves a particular task for which the alternatives are inferior or more cost
More than class skeletons... (Score:1)
Re:too hard. (Score:2)
False.
I have written a series of XML-based code-generators over the past five or six years, and found them increasingly useful. I started out with a big dream: represent an application as a narrative [supersaturated.com] and tie the document structure (DTD) to the program structure in a deep and powerful way.
Like a lot of big dreams, it didn't survive contact with reality (or with other developers).
Bugs (Score:2)
Well, yeah... (Score:2)
You then want the automated tool to map out the paths through the code, substituting every variable for an equivalent expression consisting of the inputs that would go into producing that variable, for each path. (This works for loops, so
IEEE CS:ToSE talks about this in their last issue (Score:3, Interesting)
Duh! Must be a memeber to read article! (Score:2)
Mike
Re:Duh! Must be a memeber to read article! (Score:2)
I'm not surprised... (Score:2)
Their "Computer" magazine tends stay away from actual programming techniques and sadly focuses only on (human) management. It's crap.
I see one problem with this. (Score:2, Insightful)
Re:I see one problem with this. (Score:2)
Thank you! (Score:1, Insightful)
Tools that make sure programs are self-consistent are good!
What's the point of having testing and real world trials if you're programming doesn't even agree with itself?
Re:I see one problem with this. (Score:2)
LWN - Lock Checker (Score:4, Interesting)
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.
Re:LWN - Lock Checker (Score:1)
No problem, just right click the login-box and select "Login with BugMeNot".
You need Firefox and the BugMeNot-extension, though. Firefox can be found in your favorite repository or at http://www.mozilla.com/firefox/ [mozilla.com].
The BugMeNot extension is here: http://extensions.roachfiend.com/bugmenot.xpi [roachfiend.com]
Re:LWN - Lock Checker (Score:2)
SECOND, how kind of you to encourage people to steal from such a great website. LWN is the only one I subscribe to because I like them so much. They aren't a "pay us or you won't see anything" site (like most science journals). They aren't a "pay us and we won't put large flash ads between each page" site (their only
Re:LWN - Lock Checker (Score:2)
It's a real subscriber account. It's the HP group account.
Please, DON'T use that login. Support LWN.
I've reported the link to both BugMeNot and LWN.
Re:LWN - Lock Checker (Score:1)
software snake oil (Score:4, Insightful)
Re:software snake oil (Score:1)
Ooo... and throw in lots of beurocratic layers in your organization, too!
Lord knows software can't be high-quality without at least 10 separate management rubber-stamps on it.
Re:software snake oil (Score:1)
Your choice of word ordering is interesting. The article is not about making software more dependable; it's about making more dependable software!
Re:software snake oil (Score:2)
Re:software snake oil (Score:1)
You're absolutely right. Unfortunately, that also applies to pretty much every other software engineering tool, including ones that are currently being used. There are very few tools and techniques that have been experimentally validated (inspections ar
Finding Nemo Architecture (Score:5, Interesting)
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.
Re:Finding Nemo Architecture (Score:2)
Re:Finding Nemo Architecture (Score:5, Interesting)
When I worked for IBM in the 90's the CEO made the pronouncement: "All code has been written, it just needs to be managed". We all thought he was clueless, nevertheless here I am 10yrs later writing "glue code" for somebody else and IBM is still the largest "software as a service" company on the planet.
Re:Finding Nemo Architecture (Score:2)
Re:Finding Nemo Architecture (Score:2)
Re:Finding Nemo Architecture (Score:2, Insightful)
Re:Finding Nemo Architecture (Score:1)
Re:Finding Nemo Architecture (Score:2, Interesting)
When this type of intelligence is directeted toward some more concrete goal, such as getting away from a predator (for fish), it turns out that the average path can be near optimal if the proper heuristics can be chosen.
http://en.wikipedia.org/wiki/Swarm_intelligence [wikipedia.org]
Re:Finding Nemo Architecture (Score:3, Insightful)
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.
the key is that phrase "can be combined" although my second pick is "eventually". your finding nemo system will have to be self-organizing because is too vast to have organization imposed from without. You already have that kind of system today anyway. So if you have a self organizing system, two questions are a) how does it arise and b)
Re:Finding Nemo Architecture (Score:1)
In the news today: Tanenbaum [oreilly.com] charged of subliminally brain-washing people on his microkernel design. People with tin-foil hats [wikipedia.org] live to tell the day!
* lon3st4r *
Re:Finding Nemo Architecture (Score:1)
Re:Finding Nemo Architecture (Score:2)
The idea of sales guys looking at code scares the crap out of me.
It's the combining that's the hard part (Score:2)
Snakeoil/Panacea (Score:1, Interesting)
Software design and coding isn't easy, and beyond the fundamentals (code coverage tools, unit testing frameworks, etc.), I have yet to see automation tools that increase software quality in any real way.
Any person who knows anything about software quality knows that the answer is not to use "a tool that explores billions of possible executions of the system, looking fo
In gaming, it'd work like this.. (Score:2)
Re:In gaming, it'd work like this.. (Score:1)
Re:In gaming, it'd work like this.. (Score:1)
These tools have very limited applicability (Score:2, Insightful)
Re:These tools have very limited applicability (Score:1)
did you RTFA? design first, code later.
there are other tools for analyzing code after it's written. this article is not about those, but there's lots of work
Re:These tools have very limited applicability (Score:2, Interesting)
Crutch for bad developers (Score:3, Insightful)
It's not going to find everything, let alone fix it. See Turing: the halting problem.
Re:Crutch for bad developers (Score:2)
Re:Crutch for bad developers (Score:1)
Turing did not say "you cannot prove a algorithm will terminate" he said "you cannot prove that all arbitrary algorithms will terminate on a turing machine"
First, computers are NOT turing machines. They are bounded in storage (although the bounds are pretty high nowadays).
Second. It is possible to prove that a given algorithm will terminate. Just not all algorithms. Therefore a tool can prove that your algorithm terminates. If it does terminate you are set. If
Detecting too late (Score:3, Interesting)
Re:Detecting too late (Score:2)
Other posters
Compile-time assertions (Score:2)
But why does the specification have to be a one-to-one mapping into the algorithm? Couldn't the specification be of
PHP security checker (Score:3, Funny)
Re:PHP security checker (Score:1)
If this would be a thread about car safety, you would be saying something along the lines of "It's nice that cars are safe and all, but can I have an apple?"
Re:PHP security checker (Score:1)
Good Software Design (Score:5, Insightful)
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)
Re:Good Software Design (Score:2, Insightful)
A well defined interface means that if you build 1 million holes in a plank and I deliver 1 million pegs, when they "meet" they fit.
A square hole and a round hole, one 1 inch in diameter and one 1 foot wide, all of them model the concept, but are utterly useless.
You can always go back and fill in the holes later.
No you cannot, otherwise we would all use Dvorak keyboards, not this stupid Qwerty. And we would have had HDTV 15 years ago. And...
Re:Good Software Design (Score:1)
Also, color TV managed to build on top of black and white. Black and white tvs recieve color signals and display black and white, color tvs do fine with black and white signals.
Qwerty sticks because it is good enough. Dvorak might be better(it isn't as clear as people want it to be), but it really doesn't matter that much, people that hunt and peck don't care what the field looks like, people
URLs in an image? (Score:1, Troll)
If this is reliable, I don't mind unreliability, but at least let me copy and paste!
Generic armchair quarterback sacking (Score:1)
Jackson doesn't claim it'll find everything. What he says is that it carefully synthesizes the two previous approaches to software testing, reducing the amount of time-e
The problems .. (Score:1)
Why is this billed as software help? (Score:3, Interesting)
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
Won't help (Score:2)
If your non-trivial project lacks such a document, it will probably fail.
The only way to overcome a lack of requirements is to have a heroic effort by one or more engineers, and even then you end up with many of the same problems.
The problems will stem from missing a few
Software Design Should Be Like Hardware Design (Score:2)
The problem with this is that algorithmic software does not work like ICs. The only way to solve the crisis is to abandon the algorithmic software model and embrace a non-algorithmic, signal-based, synchronous model. This is the model used in hardwar
Autotest (Score:1)
Did they use these tools in developing them? (Score:2, Interesting)
Microsoft sells collaboration software a
Formal Modeling/Model Checking (Score:5, Informative)
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.
Re:Formal Modeling/Model Checking (Score:1)
"Agile methods" are largely an acknowledgement that mistakes are inevitable and should be planned for. Unit testing helps find mistakes by stating everything twice, once inside(the code) and once outside(the tests) the implementation. Test failures are mistakes
Re:Formal Modeling/Model Checking (Score:2)
This is hardly something that orginated with "Agile methods".
snake oil software design rather than genuine .... (Score:3, Interesting)
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.
For more information... (Score:3, Informative)
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.
in summary (Score:2)
More syntax (Score:1)
Rule Verification (Score:1)
checking, not case tools (Score:1)
Floyd (whose early
Re:Static code analysis? (Score:1)
no. RTFA.
if you already did, then you're just dumb.
Re:Nobody can grasp the idea??? (Score:1)
1 have your program check the the platform is sane before it installs.
(min os version enough memory enough drive space yadda)
2 clean any input more than MAFIA money is (if a form will choke if more than 30 characters are input in a field then drop from character 29)
3 race tickets anybody???
Re:Sorry for the OT(Ptolemy's epicycles), but... (Score:2)