Slashdot Mirror

*Sigh* Every year or two for the past ten years, I get into an argument with some European professor about the qualifications of American graduated students, Usually on their knowlege of engineering of computer programs.

Thanks to this discussion, this year, I am going to have a much harder time defending them, I think.

Safety critical systems is a branch of computer science, routinely taught in the better European universities. The book I first learned it from was Safety Critical Computer Systems http://www.eng.warwick.ac.uk/~neil/safebook.htm

The field really got impetus after the Therac-25 failure http://courses.cs.vt.edu/~cs3604/lib/Therac_25/The rac_1.html
where a group of people got radiated to death because of a minor (in a computer sense) error in some code, thus adding new meaning to the term "execution error".

Its a vast field (google "safety critical") with large numbers of interesting published papers and few good books. I really can't remmend a current book, I haven't seen one I liked in years. I don't think you can learn it fast enough to be useful.

You also need to know a fair amount of higher math to be really competant, or at least even understand whats going on... most of the true experts in the field apparently regard english as a required second language (Math being the first language, not that I can blame them, but often it is overused)

The field seems to have suffered since the recession. and fragmented, but there is a good starting point at http://vl.fmnet.info/safety/

It also seems to be rapidly migrating to India as well, because of the resistance of American "cowboy" programmers. This time, it is possible the game of "cowboy and indians" may end up with the Indian's winning, inasmuch as the techniques are going to be essential to the new multicore programming models. (I heard a rumor Herb Sutter is investigating that, but thats just a rumor. If so, however, he would be the person to talk to about safety critical C/C++)

One of the techniques used in the field is formal verification. McGee and Kramer are coming out with a second edition of thier incredible book, Concurrency, http://www.doc.ic.ac.uk/~jnm/ early this year (last time I emailed them). The book is an gentle introduction to the field of formal verification and model checking, among other things. There are other books (a new one came out on the Spin Model checker, for example) but this is by far the most penetrable.

Much more interesting is the use of model checkers behind UML or BPEL/SOA tools.
Most of the really interesting stuff is still behind university walls, but tools should be appearing soon. I am trying to develop an open source grid based one but it's been slow going due to committments and resources.

You mean like Occam?

A programming method that involves designing an application such that you break each top level logical component/ability down until you a) know that you have to impliment it or b) it is found to have already been done.

That already exists, and the specification is indeed amenable to proof tools (several specification languages use HOL as their proof assistant even!). Check out B-method, HasCASL, SPARK, Extended ML, or even Z and VDM. There are tools like Perfect Developer. There are specification extensions to Java like JML that support extended static checking and proof via other tools.

Uptake has been slow, and the tools associated with this stuff are still maturing (despite the fact that formal specification is a relatively old field - tracing it's way back to Djikstra and Hoare in the late 60's). Doing specification properly tends to require a little more math background, and does take some work. More importantly, for a great many projects, it simply isn't suitable. There is no magic process you can follow that makes everything work, and there is no "final" programming model. There are whatever mix of techniques and models suit the project at hand. Good developers are ones who know lots of models and techniques and adapt them to best fit the problems at hand.

That said, specification is sorely underrated and underused as a programming technique. Too few people are well acquainted with it, and almost all the complaints that often get raised are based on myths and misnomers. It's not right for everything, but there are plenty of places where perhaps it could and should be used. Knowing how to do proper formal specification is simply another weapon in a good developers arsenal, and I wish more people spent the little extra time required to learn something about it.

Jedidiah.

Document your application, requirements, constraints, and system interactions (what the engineer does). Then write the code (what the coder does). What you will quickly learn is that it's better to be the engineer than the coder.

Interestingly there are a number of formal languages to do this, some of them rather similar to programming languages. For example you can use an algebraic specification language like CASL - it provides a structured way to define datatypes, operations on datatypes, and the axioms that the types and operations need to obey for the requirements to be met (For the mathematicians out there: an implementation is then a (many-sorted) universal algebra, and a specification is a presentation). There are things like refinement calculus and theorem provers to help you refine your requirements into an ever more specific specifications. Once that is done the actual programming is pretty much monkey work: there are extremely specific bounds on every datatype, every function, to the point where it is merely a matter just doing what you're told. The interesting part happen with the initial requirements specification and the refinement and design of the specification.

I happen to like CASL, and chose it here because the the syntax is similar to programming languages, but it is far from the only, or even the most popular specification language. You could try Z, or VDM, or B-method, or OBJ3, or any of the myriad other languages out there. Formal specification languages ought to be far more widely used than they apparently are. Isn't it about time more "software engineers" started paying attention to them?

Jedidiah.

Don't exist? Or is it simply that you don't know about them? You might start by looking here. Plenty of different methods for mathematically modeling all sorts of systems (yes, including servers).

Where is the possibility to test a scale model? There's no such thing, anything else than the server itself doesn't guarantee anything.

Try building a more abstract (mathematical) model first. For example, I've developed extremely complex multi-threaded apps (upwards of 1200 threads, all interacting with each other) by doing some intial modeling in CSP to ensure that the interactions between threads wouldn't result in deadlock or other nastiness. Does it result in zero defects? No. Does it radically reduce the number of defects, and shorten the test/debug cycle? YES!

Oh how I hate when people claim that the silver bullet of defect-free software not only does exist, but is available for everyone instantly once they just snap out of the "programmer" mindset and start behaving like an "engineer". The comparable engineering tools are missing, dammit! And there's no guarantee that they are even possible to create (any more than e.g. algorithmic AI).

Oh how I hate it when people claim that anyone is saying there are silver-bullet techniques that guarantee defect-free software. They're not dammit! They're saying that it is possible to do (much) better than we do now. Even "real" engineers produce defective products sometimes (why else do we have product recalls, and spacecraft flying into planets). But a lot fewer than software developers. I also hate it when people claim that comparable engineering tools are missing, apparently without bothering to see if that assertion is actually true.

As an aside, if you think other engineering efforts don't require "invention" every time you undertake the process, then you don't understand the design process at all. There's always more than one way to solve a problem. A large part of the engineering process is examining the available ways (and considering if there are new ways), and selecting the "best" one. By definition if you are engineering a new product, it has not been designed before (otherwise why not just build from the plans for the existing product).

Now you either need:
a) A really intelligent compiler
or
b) A really intelligent programmer

or
(c) A language and corresponding underlying concurrency theory that allows you to design and analyze complex interacting multithreaded systems with ease.

Multithreaded programming is only hard if you use poor tools. If you are trying to write multithreaded programs using ancient concepts of concurrency like mutexes and semaphores then yeah, it'll be hard. If you write software using more modern concepts like CSP, and languages or libraries like occam-pi or JCSP, then multithreading can become extremely easy. I've written reasonably complex multithreaded programs with several hundred "threads" (some nested inside others) running simultaneously and interacting with each other (not just a limited worker thread model) and faced no more debugging difficulties than I would have writing a sequential program of equal complexity.

Roberto Di Cosmo of University of Paris 7 claims that theoretical computer science is particularly strong in France and that its formal methods can be used to manage complex dependencies to create an "integrated, coherent whole."

In different words, people in France are jumping onto the open source bandwagon in order to squeeze out another few years of funding for the same old stuff they have already been doing for 30 years.

If you want to read more about formal methods, look here and here. You can judge for yourself how much relevance you think this is going to have for FOSS. I think its chances are close to nil.