Yes, McConnell is a Microsoft guy, but this book is completely operating-system and programming-language agnostic (even though examples are in C, Fortran, and Pascal, IIRC). It is an excellent guide to software construction, covering every aspect from design, over coding practice, style issues, to project management. I highly recommend it.
(I work in an academic context, so take the following with a grain of salt.)
First you should understand the difference between testing and verification. With testing, you rule out a certain number of bugs, but you can never guarantee the absence of bugs. The latter is only possible with software verification, where you prove that the software contains no bugs and fulfills its specification.
Unfortunately, software verification is very expensive. Also, software verification is still a subject of research, and AFAIK it has not been tried for large software projects so far. (My current research project aims at verifying a complete operating-system kernel -- check out the VFiasco project.)
So in most cases, verification is too expensive, and you need to ensure robustness by other means like a good programming standard and testing. (I believe that is what you are looking for, despite the title of your question including the word ``verification.'')
If your shop uses C, I recommend the following book: Les Hatton, Safer C. It explains what a good programming standard should contain, and advocates automatic enforcability. (It also explains what the standard should not contain -- in particular, issues of style such as indentation and variable naming.)
One example of such a programming standard for C are the Guidelines for the Use of the C Language in Vehicle Based Software, which should be particularly relevant to you as you also work in the automotive industry.
Testing is another important aspect. In safety-related environments such as yours, a high test coverage for your code is desirable. This requirements suggests automated testing on the unit level. Automated unit testing is practical only if the code is designed to be testable, and there are a number of strategies which provide this property, such as avoiding dependency cycles (for C and C++, John Lakos' Large-Scale C++ Software Design
still is the ultimate guide), or creating the unit test before the program (the Extreme Programming way). I also liked
Testing Object-Oriented Systems: Models, Patterns, and Tools by Robert Binder - a huge and thorough guide to all imaginable kinds of testing, especially for object-oriented systems.
In this paper, we measured
``worst-case'' interrupt delays of two real-time systems:
RTLinux and
L4RTL,
a reimplementation of the RTLinux API on top
of Fiasco
(a real-time L4-compatible
microkernel) and
L4Linux.
In comparison to RTLinux, L4RTL sports address spaces for real-time tasks.
The simulated worst-case load was a
combination of a heavy time-sharing load and a
cache flooder.
On a 800-MHz Pentium III, the worst-case latency for
RTLinux was 68 s. For L4RTL, it was 85 s.
Note that 68 s is considerably higher than what
other sources quote as RTLinux's worst-case delay (in this thread, someone said 30--50 s). We believe that other researchers forget to
take into account caching effects.
Anyway, it looks like both systems would be adequate
for your application.
[...] in order to be illegal, a monopoly must be harmful to its consumers, and the DoJ failed to dig up enough evidence to that, choosing instead to focus on the damage done to other companies (particularly Netscape).
I just want to remind you all that this trial did not try to prove that Microsoft's monopoly in the OS market is illegal or bad for consumers.
I wonder why Microsoft always said that their doing was actually beneficial for costumers. They missed the point just as you guys are missing it: Nobody in the trial actually debated that.
Being a monopoly is perfectly legal in the US. This case is about something different: It is illegal to use your monopoly in one market in order to establish a monopoly in another market. In this case, the court found Microsoft guilty of (among a few other things) using their monopoly in the OS market be built a monopoly in the browser market. For example, they illegally bundled the OS with a browser, making it impossible to buy the OS without their browser. Saying that this bunding was actually benefitting for consumers is just obfusication.
As owning a monopoly is not illegal, you should not complain that the court's decision to split up Microsoft does not actually take the OS monopoly away from them (or the OS company that will emerge from them). Instead, the decision deals with the bundling issue I mentioned.
I am speculating here, but my guess is that MacOS X's kernel is a descendant (at least in spirit) of the old NeXT OS (NeXTStep?) which was a Mach-2.5-based BSD system. When Apple bought NeXT, they probably decided to use NeXT's existing OS technology and talent to build their own new OS; I guess that is about the only reason why Darwin (the BSD OS core MacOS X uses) today is Mach-based.
So why did NeXT use Mach in the first place? I'm speculating again. I guess they started out from OSF/1, and the OSF/1 developers had your goals (a) and (b) in mind.
Remember: The Open Software Foundation (OSF, now a merged with the Open Group) was a group of vendors that wanted to develop an Unix platform independent from then-AT&T's UNIX. OSF/1 was to be their kernel. DEC used it to build DEC OSF/1 (now Compaq Tru64 UNIX or whatever it is called this week), and I guess that NeXT took it to build NeXTStep.
The first version of OSF/1 (the one out of which vendors made successful products) was a BSD single server on top of Mach 2.5. At the time it was developed, it was not yet well established that Mach-based systems are slow. In fact, the Mach-2.5-based OSF/1 probably was not that slow: Mach 2.5 had considerably less bloat than Mach 3.0, and it was not really a microkernel-based system as it was closely integrated with a BSD kernel - that is, the microkernel and the BSD server shared the kernel address space (this is sometimes called ``colocation''; the OSF recently rediscovered this technique to speed up MkLinux on top of Mach 3.0). Only with the advent of Mach 3.0, the first ``real'' microkernel, people started to notice that there is something wrong with Mach's original approach.
That said, it does not necessarily follow that microkernel-based system, or even Mach-based systems in particular, need to be slow. I do microkernel-related research myself, and my group has shown with L4Linux that a Unix single server can be implemented with very reasonable overhead on top of a ``real,'' second-generation microkernel - in this case, L4 (macrobenchmarks indicate that L4Linux has an overhead of about 2% to 3% when compared to the original monolithic Linux kernel).
I do not really know MacOS X's architecture well enough to give a well-informed statement, but my guess is that they have enough talent to avoid the most stupid mistakes.
Slashdot Mirror
Yes, McConnell is a Microsoft guy, but this book is completely operating-system and programming-language agnostic (even though examples are in C, Fortran, and Pascal, IIRC). It is an excellent guide to software construction, covering every aspect from design, over coding practice, style issues, to project management. I highly recommend it.
First you should understand the difference between testing and verification. With testing, you rule out a certain number of bugs, but you can never guarantee the absence of bugs. The latter is only possible with software verification, where you prove that the software contains no bugs and fulfills its specification.
Unfortunately, software verification is very expensive. Also, software verification is still a subject of research, and AFAIK it has not been tried for large software projects so far. (My current research project aims at verifying a complete operating-system kernel -- check out the VFiasco project.)
So in most cases, verification is too expensive, and you need to ensure robustness by other means like a good programming standard and testing. (I believe that is what you are looking for, despite the title of your question including the word ``verification.'')
If your shop uses C, I recommend the following book: Les Hatton, Safer C . It explains what a good programming standard should contain, and advocates automatic enforcability. (It also explains what the standard should not contain -- in particular, issues of style such as indentation and variable naming.) One example of such a programming standard for C are the Guidelines for the Use of the C Language in Vehicle Based Software, which should be particularly relevant to you as you also work in the automotive industry.
Testing is another important aspect. In safety-related environments such as yours, a high test coverage for your code is desirable. This requirements suggests automated testing on the unit level. Automated unit testing is practical only if the code is designed to be testable, and there are a number of strategies which provide this property, such as avoiding dependency cycles (for C and C++, John Lakos' Large-Scale C++ Software Design still is the ultimate guide), or creating the unit test before the program (the Extreme Programming way). I also liked Testing Object-Oriented Systems: Models, Patterns, and Tools by Robert Binder - a huge and thorough guide to all imaginable kinds of testing, especially for object-oriented systems.
In this paper, we measured ``worst-case'' interrupt delays of two real-time systems:
- RTLinux and
- L4RTL,
a reimplementation of the RTLinux API on top
of Fiasco
(a real-time L4-compatible
microkernel) and
L4Linux.
In comparison to RTLinux, L4RTL sports address spaces for real-time tasks.
The simulated worst-case load was a combination of a heavy time-sharing load and a cache flooder.On a 800-MHz Pentium III, the worst-case latency for RTLinux was 68 s. For L4RTL, it was 85 s.
Note that 68 s is considerably higher than what other sources quote as RTLinux's worst-case delay (in this thread, someone said 30--50 s). We believe that other researchers forget to take into account caching effects.
Anyway, it looks like both systems would be adequate for your application.
I just want to remind you all that this trial did not try to prove that Microsoft's monopoly in the OS market is illegal or bad for consumers.
I wonder why Microsoft always said that their doing was actually beneficial for costumers. They missed the point just as you guys are missing it: Nobody in the trial actually debated that.
Being a monopoly is perfectly legal in the US. This case is about something different: It is illegal to use your monopoly in one market in order to establish a monopoly in another market. In this case, the court found Microsoft guilty of (among a few other things) using their monopoly in the OS market be built a monopoly in the browser market. For example, they illegally bundled the OS with a browser, making it impossible to buy the OS without their browser. Saying that this bunding was actually benefitting for consumers is just obfusication.
As owning a monopoly is not illegal, you should not complain that the court's decision to split up Microsoft does not actually take the OS monopoly away from them (or the OS company that will emerge from them). Instead, the decision deals with the bundling issue I mentioned.
So why did NeXT use Mach in the first place? I'm speculating again. I guess they started out from OSF/1, and the OSF/1 developers had your goals (a) and (b) in mind.
Remember: The Open Software Foundation (OSF, now a merged with the Open Group) was a group of vendors that wanted to develop an Unix platform independent from then-AT&T's UNIX. OSF/1 was to be their kernel. DEC used it to build DEC OSF/1 (now Compaq Tru64 UNIX or whatever it is called this week), and I guess that NeXT took it to build NeXTStep.
The first version of OSF/1 (the one out of which vendors made successful products) was a BSD single server on top of Mach 2.5. At the time it was developed, it was not yet well established that Mach-based systems are slow. In fact, the Mach-2.5-based OSF/1 probably was not that slow: Mach 2.5 had considerably less bloat than Mach 3.0, and it was not really a microkernel-based system as it was closely integrated with a BSD kernel - that is, the microkernel and the BSD server shared the kernel address space (this is sometimes called ``colocation''; the OSF recently rediscovered this technique to speed up MkLinux on top of Mach 3.0). Only with the advent of Mach 3.0, the first ``real'' microkernel, people started to notice that there is something wrong with Mach's original approach.
That said, it does not necessarily follow that microkernel-based system, or even Mach-based systems in particular, need to be slow. I do microkernel-related research myself, and my group has shown with L4Linux that a Unix single server can be implemented with very reasonable overhead on top of a ``real,'' second-generation microkernel - in this case, L4 (macrobenchmarks indicate that L4Linux has an overhead of about 2% to 3% when compared to the original monolithic Linux kernel).
I do not really know MacOS X's architecture well enough to give a well-informed statement, but my guess is that they have enough talent to avoid the most stupid mistakes.