From owner-freebsd-hackers Thu Oct 10 3:47: 8 2002 Delivered-To: freebsd-hackers@freebsd.org Received: from mx1.FreeBSD.org (mx1.freebsd.org [216.136.204.125]) by hub.freebsd.org (Postfix) with ESMTP id A5A5D37B401; Thu, 10 Oct 2002 03:47:05 -0700 (PDT) Received: from bulwark.switch.com (bulwark.switch.com [206.181.77.34]) by mx1.FreeBSD.org (Postfix) with ESMTP id 6EBC643EAC; Thu, 10 Oct 2002 03:47:01 -0700 (PDT) (envelope-from tnelson@switch.com) Received: from bulwark.switch.com (root@localhost) by bulwark.switch.com with ESMTP id g9AAl0aR025952; Thu, 10 Oct 2002 06:47:00 -0400 (EDT) Received: from isunix2.switch.com (isunix2.switch.com [199.234.168.6]) by bulwark.switch.com with ESMTP id g9AAl0kt025941; Thu, 10 Oct 2002 06:47:00 -0400 (EDT) Received: from exchptc1.switch.com ([199.234.168.10]) by isunix2.switch.com (PMDF V5.2-32 #37720) with ESMTP id <0H3R00GIXHYBC1@isunix2.switch.com>; Thu, 10 Oct 2002 06:46:59 -0400 (EDT) Received: by exchptc1.switch.com with Internet Mail Service (5.5.2653.19) id <4LCC13MW>; Thu, 10 Oct 2002 06:48:04 -0400 Content-return: allowed Date: Thu, 10 Oct 2002 06:48:03 -0400 From: "Nelson, Trent ." Subject: RE: FreeBSD usage in safety-critical environments To: "'Ted Faber'" , Terry Lambert Cc: "Nelson, Trent ." , "'hackers@freebsd.org'" , "'questions@freebsd.org'" Message-id: <8F329FEDF58BD411BE5200508B10DA7607D71A15@exchptc1.switch.com> MIME-version: 1.0 X-Mailer: Internet Mail Service (5.5.2653.19) Content-type: text/plain; charset="iso-8859-1" Sender: owner-freebsd-hackers@FreeBSD.ORG Precedence: bulk List-ID: List-Archive: (Web Archive) List-Help: (List Instructions) List-Subscribe: List-Unsubscribe: X-Loop: FreeBSD.ORG > -----Original Message----- > From: Ted Faber [mailto:faber@ISI.EDU] > Sent: Wednesday, October 09, 2002 10:59 PM > To: Terry Lambert > Cc: Nelson, Trent .; 'hackers@freebsd.org'; 'questions@freebsd.org' > Subject: Re: FreeBSD usage in safety-critical environments > > On Wed, Oct 09, 2002 at 12:26:14PM -0700, Terry Lambert wrote: > > Life support systems require formal proofs of correctness for code; > > since neither Linux nor FreeBSD is formally correct, in total, you > > would need to be insane to deplaoy either of them as, for example, > > a part of an air traffic control system. > > I suspect that's a bad example, or that you mean an embedded aircraft > control system. Ron Reisman and James Murphy gave a fine invited talk > at USENIX 02 (http://www.usenix.org/events/usenix02/tech/#11am) about > the growing number of UNIX components in the US ATC system. I reject > the conclusion that the FAA is collectively insane for that reason. I'd have to concur. I'm working on a large rail engineering project in the UK that is implementing a two-phased deployment of a Railway Control Centre System. The first phase will be using a combination of Tru64 UNIX and Linux systems, with an investigation being taken place for the second phase to move completely to Linux. There is a huge difference between systems rated at SIL 1 and 2 (which is what ATC/rail CCS would fall under) and those rated at 3 and 4. I was not referring to life-support or life-critical systems, as these will almost certainly be a proprietary hardware/software package that has been certified and accredited to a high level of safety integrity. What I was referring to were systems running on UNIX that control and interface to these safety-critical systems. For railway, Control Centres may suggest an erroneous route that would result in two trains colliding (although such a system will be commissioned on the basis that it wouldn't allow such a route to be suggested), but the 'vital', safety-critical interlocking would prevent such a route being set. The resulting safety-integrity level for the Control Centre would be SIL 2. The analogy between ATCs & embedded aircraft control systems isn't as tight as there isn't a physical interface between the two (well, at least as far as I know). The deployment of FreeBSD, or any BSD variant, (or ANYTHING other than Linux) in environments such as this, is what I was originally getting at. Oh, and Terry, I think you'd be astonished if I informed you of how many rail control systems in the US and around the world use either Linux or some of the commercial variants such as Tru64 UNIX or Solaris. > Ted Faber faber@isi.edu > USC/ISI Computer Scientist http://www.isi.edu/~faber > (310) 448-9190 PGP Keys: http://www.isi.edu/~faber/pubkeys.asc Regards, Trent. To Unsubscribe: send mail to majordomo@FreeBSD.org with "unsubscribe freebsd-hackers" in the body of the message