[Haskell-cafe] Software correctness in the auto industry and FPLs

Tom Hawkins tomahawkins at gmail.com
Fri Apr 2 18:51:22 EDT 2010


On Fri, Apr 2, 2010 at 2:28 PM, Vasili I. Galchin <vigalchin at gmail.com> wrote:
> Sorry for no "Subject" on the first post. In any case, I meant this
> Wall Street Journal as a challenge to the Haskell community to perhaps
> "step up to the plate" in the auto arena vis-a-vis software
> correctness. I realize that with hard real-time problems and a garbage
> collector that that could be a problem. In any case , enjoy.

Our group at Eaton uses Haskell to program vehicle computers that
control hybrid powertrains for heavy duty trucks -- garbage to be
specific.  Our systems interface with engines, transmissions, brake
controllers, and yes, accelerator pedals.  (It's a good thing garbage
trucks don't have floor mats.)

Haskell and Atom help us maintain correctness in several ways.  For
one, Haskell GADTs ensure type correctness of the generated C code.  I
find it interesting that a type system in one language can prevent
type problems in another.  Another benefit is the type system
distinguishes between stateful and stateless operations.  This helps
manage how state is modified in an embedded control program, which by
its nature tend to be a complex state machine.  For example:

  doSomething :: E Bool -> E Bool -> E Bool  -- Guaranteed not to change state.

versus in C:

  bool doSomething(bool, bool);  // No guarantees what this thing does
under the hood.

One thing specific to Atom is it makes it very easy to create
multi-rate programs without having to partition a lot of code and hook
it up to an RTOS task scheduler, or worse, having to schedule it by
hand.  Often I find myself deep in the design of a feature and
realized I need to perform a task at a faster or slower rate than the
surrounding code.  If it were C, I would have to plumb out all the
communicating variables, create a handful of mutex locks, and bind it
to a task scheduler.  In Atom, I simply specify a different execution
period:

  period 20 $ atom "someTask" $ do ...

But I think the biggest gain is Atom's guarded atomic actions.  There
is something about writing a block of code and knowing it will execute
atomically without anything else getting in the way.  I find it
difficult to explain the benefits of this type of embedded programming
paradigm -- it usually only comes with practice.  In fact, I didn't
fully appreciate Atom until I started using it on a large production
design -- and I'm the one who wrote the library.

Of course, nothing is perfect.  It is still possible to write buggy
programs with Haskell+Atom.  But as Simon PJ stated in a presentation,
"the bugs you can write are far more interesting."  Of course, our
definition of "interesting" is when hardware grinds together and metal
chunks fly through the air.

-Tom


>>
>> By BEN WORTHEN
>>
>> U.S. regulators on Tuesday announced a broad investigation into
>> automotive computer systems and software, which have come under
>> scrutiny because of sudden acceleration and other reports involving
>> some Toyota Motor Corp. cars.
>>
>> An examination of Toyota's problems will be conducted by experts from
>> the National Aeronautics and Space Administration, while the National
>> Academy of Sciences, which advises the government, will undertake a
>> separate, 15-month study into the use of computer technology in cars,
>> U.S. Transportation Secretary Ray LaHood said.
>>
>> Toyota has said there is no evidence that software or electronic
>> systems are responsible for sudden acceleration in its cars. The
>> company "repeatedly and rigorously" tests its software and has
>> subjected it to outside review, a spokesman said.
>>
>> Electronics have led to some of the biggest safety breakthroughs in
>> vehicles, such as antilock brakes and stability control. Software
>> controls an ever-growing variety of functions in cars, including
>> braking and accelerating. Increasingly, cars include software that
>> links these systems to do things like parallel park the vehicle or
>> remember the seat positions, temperatures and radio stations preferred
>> by different drivers.
>>
>> "Ninety percent of all innovation in cars today is driven by
>> software," said Ingolf Krueger, an associate professor of computer
>> science and engineering at the University of California in San Diego.
>>
>> No surprise then that software is sometimes to blame when things go
>> wrong. While Toyota has received most of the attention, other car
>> makers have had software-related incidents.
>>
>> Ford Motor Co.'s 2010 Fusion Hybrid has a high-tech braking system
>> that also recharges its battery through a process called regenerative
>> braking. Software monitors sensors in the car and determines when to
>> engage the conventional braking system instead. Several drivers filed
>> complaints with the National Highway Traffic Safety Administration,
>> the agency responsible for vehicle safety, stating that they depressed
>> the brake pedal as far as possible but the brakes didn't engage.
>>
>> A Ford spokesman said a sensor on the car was set too sensitively and
>> that software interpreted the signal to mean it should skip the
>> regenerative braking step. The company issued a software upgrade that
>> it said would take care of the issue, avoiding a recall.
>>
>> In November 2008, General Motors Co. recalled 12,662 of its 2009 model
>> year Cadillac CTS sedans because a software glitch caused the
>> passenger-side air bag to be turned off when it should have been
>> active.
>>
>> That same year, Volkswagen AG recalled 4,079 2008 Passats because of
>> software that didn't properly control the engine idle while the air
>> conditioning was on. And Toyota in February recalled 2010 Priuses to
>> fix the software in their antilock brakes that some owners said led to
>> delays in the brakes engaging.
>>
>> To date, the National Highway Traffic Safety Administration has
>> evaluated software and electronic systems only as part of other
>> reviews, such as whether an air bag deploys when it is supposed to, a
>> spokeswoman said. The agency doesn't have any software or electronics
>> specialists on staff, she added.
>>
>> Auto software has some distinct characteristics. For one thing, the
>> programs are relatively simple and are designed to be embedded in
>> simple components—typically eight-bit and 16-bit computer chips,
>> compared with more advanced 32-bit and 64-bit microprocessors found in
>> most personal computers.
>>
>> The simplicity is intended to make the software more reliable—the
>> fewer things it is asked to do, the less likely it is to experience a
>> problem.
>>
>> Indeed, Mr. Krueger said automotive software has led to some of the
>> biggest jumps in safety and fuel efficiency. Electronic
>> stability-control systems, which detect when a car is skidding and
>> automatically deploy the brakes, have reduced the number of vehicles
>> that flip over, he said.
>>
>> In an effort to improve the quality of software in vehicles several
>> car makers in 2003 founded the Automotive Open System Architecture
>> group to create standards. These systems have become enormously
>> complex, said Simon Fuerst, a spokesman for the group, all the more so
>> because car makers traditionally use their own proprietary software
>> formats.
>>
>> Raj Rajkumar, professor of electrical and computer engineering at
>> Carnegie Mellon University, has recently been studying the software in
>> a Lexus IS250, a car made by Toyota, that experienced sudden
>> acceleration. His hypothesis is that a software glitch caused the
>> vehicle's fail-safe mode—which typically shuts off or reduces engine
>> power in the event of a system failure—to not to kick in when it
>> should.
>>
>> But he said he isn't certain and his study is made more difficult by
>> the fact he doesn't have access to the software code used in the car.
>>
>> Mr. LaHood on Tuesday said that many members of Congress feel "there's
>> something wrong with the electronics, not only just in Toyotas but in
>> other automobiles, too. We felt that we really needed to look into
>> this."
>> —Josh Mitchell contributed
>> to this article.Printed in The Wall Street Journal, page B1
>>
>> Copyright 2009 Dow Jones & Company, Inc. All Rights Reserved
>>
>> This copy is for your personal, non-commercial use only. Distribution
>> and use of this material are governed by our Subscriber Agreement and
>> by copyright law. For non-personal use or to order multiple copies,
>> please contact Dow Jones Reprints at 1-800-843-0008 or visit
>>


More information about the Haskell-Cafe mailing list