| |||||||||||||
|
| |||||||||||||
Green Hills Software strikes againGreen Hills Software strikes againPosted May 4, 2004 18:59 UTC (Tue) by rriggs (subscriber, #11598)In reply to: Green Hills Software strikes again by jpb105 Parent article: Green Hills Software strikes again I read that quote to mean that these formal methods must be used in the certification process, not necessarily in the development process. Isn't that really the case here?
(Log in to post comments)
Formal Methods Posted May 4, 2004 23:26 UTC (Tue) by jpb105 (guest, #21364) [Link] All I know about Formal Methods is based on two undergraduate courses, but yes I think it is required for certification and optional for development, however if a system has not been developed with formal methods it is often harder to certify.This is a interesting article linked to from Green Hill's site, it states " [Green Hill's CEO] O'Dowd cited Green Hills' Integrity real-time operating system, along with LynuxWorks' LynxOS-178 and Wind River Systems' VxWorks AE653 RTOSes, as secure solutions." LynuxWorks produces GPL Real-Time Linux Distributions for use in defence and aviation systems. So one of my past posts was wrong (too limited vision and too much FUD) - You can have 'Fly by Linux' systems! They have a response to anti-Linux claims Here. I guess LynuxWorks must drastically simplify the standard Linux kernel. LynuxWorks is a member of the Embedded Linux Consortium and Wind River Systems has supported it!
Formal Methods Posted Sep 5, 2005 18:27 UTC (Mon) by speedplane (guest, #32280) [Link] The formal methods you are talking about basiclly mean documenting every single line of soure code. Every single loop, if statement, and function call has to be checked and rechecked. I've heard that the certification process costs about $1000 per line of source!
The result is software that is rock solid. Linux may be a good operating system for the desktop, but its in a different category alltogether when it comes to defence and extremly critical situations.
There are other benefit to their opertaing system too. Its a real-time operating system which means that the interrupt latency is small and bounded. (Interrupt latency is the time it takes for the computer to respond to something from the outside ie sensors, networks, and human input devices) Linux can't provide that and changing the code to lower interrupt latency would be an extremly difficult endeavor. Real-time is a commendable effort but it is still an order of magnitude different from a true real-time operating system.
Finally there's security. A process running in integrity cannot effect any other process unless it is specifcally allowed. That goes for hardware too. That means that if there is one 'bad' process running on the OS, that process can only do damage to itself and nothing else on the system. Linux has some protections like this but nothing near the detail of integrity.
|
|
||||||||||||