Slashdot Mirror

Welcome to Formal Verification!

We wrote lots of tests. (How else would we know it has bugs in it?)

You'd model it and apply LTL to check for certain classes of bugs.

Back when I was at Bell Labs, the convention for names to put on technical papers was to use initials and last name. I don't know how long that had been going on, but it was viewed as allowing work to be seen without the filter of gender (plus it was unambiguous about whether to use your nickname vs. formal name, for those of us like me who are only addressed with our formal first name by bureaucrats who are pretending to be familiar but don't actually know us...)

On the other hand, there were fewer applications using avatars in those days, and the default avatar was usually a Peter Weinberger logo-face.

http://www.sciamdigital.com/index.cfm?fa=Products.ViewIssuePreview&ARTICLEID_CHAR=253EE806-FA7B-4693-8F1D-BDBB1E68AAF is an article i wrote many moons ago for scientific american on these optical telegraph networks more info still, in this book: http://spinroot.com/gerard/hist.html

Well, yeah, that is a problem. FDR is free for academic use, IIRC. But they charge for commercial use. Although, as the Formal Systems Europe folks point out, exactly how much debugging time do they need to save to justify the cost of FDR.

If FDR is too pricey for you (perhaps you're an open source developer), there are a few other options. In the free category is LTSA. LTSA accepts a language called FSP, which is similar (but not identical) to CSP. The tool itself is not as powerful as FDR from what I can tell, can potentially still very useful. And there's an Eclipse plugin :-) In the open source category is SPIN. SPIN's process modeling language, Promela, is more C-like than CSP-like, but does have CSP-like semantics. The tool itself is free, open source, very powerful, and has an active community of users. Definitely worth a try if you're looking for something capable of industrial-strength model-checking.

Anyone who has ever used a tool like Spin should be familiar the idea of a model checker finding counterexamples. That's what they are there for after all ... to exhaustively explore the space and prove conclusively that your protocol is valid. What I (and Cory) find interesting here is the idea of applying this kind of technology outside of the programming domain.

The idea of color-coded data types is also not new - Charles Moore's Color Forth does that and the whole idea there seems one step away from the established practice of using syntax highlighting. But using this as an explicit tool to help amateurs come to terms with a complex concept is new. Another example: anyone that has ever used a profiler, code-coverage or automated testing tool would be familar with some of the "Poison" and "Rehersal" concepts you mention, but I would be suprised if anyone outside the CS discipline had a clue about this sort of thing.

I guess the $64 question is: where will this all end up?

My feeling is that it ultimately may prove to be less useful for story tellers and more useful to people whose everyday job is to construct and take apart hypothesis: criminologists. Imagine feeding in all the facts into a storytron and having it tell you: the butler did it!

>I'll bet the folks in Redmond are looking at these numbers and wondering just how to get IE's numbers that low.

Not really. They've had similar tools internally for years. They aren't a magic bullet.

Nice troll, though. I'm sure you'll be modded to +5.

Finding all POSSIBLE bugs in a software program means traversing all possible paths in the code with all possible inputs. That's a HUGE problem. You can "model" the code using Logic Equations and that helps some but any errors in the conversion from code to logic equations invalidate results. The DoD and NASA have spent many millions on solving this problem over the last 10-12 yrs. When I was at NASA we used several different tools (CodeSurfer, Purify, Lint, Polyspace as I recall) as each tool was better at one thing (i.e memory leaks vs null pointer dereferences). A The complete process took a couple of days to weeks and then human eyes and expertise were still needed to remove false positives. A good site for all the tools out there, old & new is http://spinroot.com/static/. Looks like Coverty might be a good one to look into, as the best I had seen was CodeSurfer. All the good tools I have seen are commercial (NOT open Source) and EXPENSIVE!! I'd love to see a decent open source tool to run as a first pass before applying the other tools. Another point is that these tools are STATIC analysis. Run-Time Analysis is a whole 'nother animal but that area is improving with tools like DTRACE in Solaris.

Some of the postings in this thread comparing experienced and inexperienced developers remind me of an article I came across a few years ago by Gerard Holzman titled "The Logic of Bugs". In his article, Holzman states, as one of his first points, the following:

Bugs can adjust to the level of experience of the programmer. One common misconception is that experienced programmers make fewer mistakes than novice programmers. Experienced programmers and novice programmers make roughly the same number of mistakes when writing the same amount of code. The mistakes made by the experienced programmer, however, will be more subtle than those of the novice programmer. The more complex bugs that the experienced programmer can seed into the code are often harder to find than the simpler typos of less experienced colleagues.

Holzman is an extremely distinguished researcher, and I found his comment so counter-intuitive that I approached him and asked if there was any quantitative research behind such a bold statement. He said it was based his many years of observation in the industry.

I googled and found the pdf for Holzman's article at: http://spinroot.com/gerard/pdf/FSE2002.pdf. In the article he also makes the point that developers and writers (say for the New York Times), have similar defect rates in their finished products!

Hehe, do you really believe this ?

I'd recommend you to read Holzmann, "The SPIN model checker".

http://spinroot.com/spin/Doc/Book_extras/

basically, i've got my own improved version of the SPIN model checker, which is a tool people use to verify designs of asycronous systems, such as distributed algorithms, network protocols, and cache-coherence protocols. this is a tool engineers use to find errors in designs. Holzmann, the original author and maintainer, used the tool at Bell Labs to find errors in code for phone switches (among other things). At NASA he has found some bugs in Mars rover code using SPIN on models abstracted from code.

i have made various speed, usability, and flexability enhancements to the program. for details, you'd have to read the papers.

ok, i'll give you that i've seen people get BS and MS degrees in CS at GT who couldn't code their way out of a paper bag, but the highest honors on my BS degree indicates i was setting the curve, not riding it.

also, the terms i use aren't obscure or fancy to the people i work with. they're everyday speak.

granted, my work with Boeing is a result of my advisor sweet-talking Boeing, but what led to my internship with NASA was a paper i wrote contradicting some presumptions made by a big shot working for NASA/JPL. The paper also discusses some hacks for improving speed, and adding flexability without hurting speed.

If discovering and implementing publication-worthy improvements to a piece of software that won an ACM Systems Software Award in 2001 is not enough evidence i can program, i'll just let you assume i'm a "bureaucrat".

hell, i'll assume you're just a mindless code monkey if you don't know any functional languages with static type checking and type inferencing.

ok, i'll give you that i've seen people get BS and MS degrees in CS at GT who couldn't code their way out of a paper bag, but the highest honors on my BS degree indicates i was setting the curve, not riding it.

also, the terms i use aren't obscure or fancy to the people i work with. they're everyday speak.

granted, my work with Boeing is a result of my advisor sweet-talking Boeing, but what led to my internship with NASA was a paper i wrote contradicting some presumptions made by a big shot working for NASA/JPL. The paper also discusses some hacks for improving speed, and adding flexability without hurting speed.

If discovering and implementing publication-worthy improvements to a piece of software that won an ACM Systems Software Award in 2001 is not enough evidence i can program, i'll just let you assume i'm a "bureaucrat".

hell, i'll assume you're just a mindless code monkey if you don't know any functional languages with static type checking and type inferencing.

Having said all of that, I'll agree that formal verification at NASA is in its infancy, and is facing an uphill battle for acceptance (witness how long the Langley group has been trying to push formal methods). It'll be interesting to see what happens with JPL's LaRS.

Perhaps not surprisingly for anyone who has heard about the management at NASA, C++ was selected for the successors to the Remote Agent on the grounds that it is supposed to be more reliable (this despite the fact that the Remote Agent was originally to be developed in C++, an effort that was abandoned after a year of failure). This caused more than a few people to be upset (including a very personal account by one of the aforementioned designers). Clearly the debugging facilities of Common Lisp are far superior to static systems like C++, something which is very useful in diagnosing unexpected error conditions in spacecraft software (read the first question on p. 3 of the interview to see what pains the JPL staff went through to adapt similar, ad-hoc methods to VxWorks). It's also clear from this interview (question: "How is application programming done for a spacecraft?" Answer:"Much the same as for anything elsesoftware requirements are written, with specifications and test plans, then the software is written and tested, problems are fixed, and eventually its sent off to do its job.") that NASA has in no way tried to adapt formal verification methods for it's software, prefering instead to rely on the "tried and true" (at failing, maybe) poke-and-test development "methods."

Clearly, formal verification methods to eliminate bugs before critical software is deployed, and deployment in a system with advanced debugging facilities is a clear win for spacecraft software, and should be adapted as the standard model of development. Unfortunately, like in many other software development enterprises, inertia keeps outdated, inadequate systems going despite a strong failure correlation rate.

There are some fascinating parts to game of life, but to claim that it has some special place for hackerdom is laughable at best. I can think of one recent good work on GOL worthy of hackerdom brownie points, and that is eppstein's searching for spaceships. Rest of hackerdom's fascination is negligible enough not to warrant the basis for this logo.

Why not the ship from ancient spacewar, which was the reason for Ken's hacking unix? Why not something as imaginative as PJW face from Bell Labs? (oh no, bad suggestion: ESR may decide to deploy his own face as logo...)

Hm. I have been designing logos on and off since 1976. Hacking since 1978. I suppose I have learned a thing or two about both over the years. Here is my somewhat educated assessment: I consider ESR's logo to be unimaginative, poorly balanced, devoid of energy, and not at all representative. In other words, It is really boring, one thing hacking is most certainly not. (one of my friends thought it was a stylized person sitting with his back against the wall, head down)

ESR should have had enough respect to ask the community for input...

(a remedial course on logo design may also help)

nous.

pjw.

It depends on the thread abstractions that are used for synchronisation and thread communication. The most commonly used abstractions today (semaphores, locks, etc) date from the 1970s; there are much better ways to do it!

One way derives from a mathematical notation created by Tony Hoare, called CSP. There is one unit of thread communications and synchronisation, called a channel. It's like a rendezvous point that allows a value to be passed between threads. If one thread tries to send a value on a channel, it will block until another thread tries to read from the channel (also, reading from the channel will block until another thread tries to send on it).

This scheme is incredibly versatile, easy to use and cheap. There are also some tools that can aid in automatic verification of software built in this way. It's true that it's possible to deadlock in concurrent systems, but it's almost always possible to structure the system in such a way that it's deadlock-free by construction. For instance, if my program is structured as a one-way pipeline, it's impossible to deadlock.

Concurrency at this level in a GUI application can greatly enhance the simplicity and maintainability of a program. This is because it's generally much easier to write a straightforward piece of imperative code than encode the same thing as a state machine, e.g.

while (buttons != 0) {
(buttons, point) = <-mouse;
drawat(point)
}


(where <- receives from a channel), versus:


callback(buttons, point) {
if (state == DRAGGING) {
if (buttons != 0)
drawat(point);
else
state = NOTDRAGGING;
}
}

You say:
That would be the case if interaction was a parallel activity, but unfortunately it's not.

But it is! Yes, the user themselves only contributes one thread to the activity, but the program itself is often dealing with multiple activities at the same time; for instance updating itself in response to network activities or updating graphics on a time-step basis.

The most important thing it gives you, in my experience, is the sense of control. As a separate thread, you are free to structure your application in a way directly appropriate to the task being solved. In a callback system, you are at the mercy of the caller; you can't just wait for an event, then do the next thing, you have to encode your current state, return, and wait to be called back, whereupon you have to figure out where you just were!

For a language that exemplifies this, see Limbo, the language of choice in the Inferno environment. No problems with thread unsafe graphics there!