Certified C compilers for safety-critical embedded systems - Page 7

Do you have a question? Post it now! No Registration Necessary

Translate This Thread From English to

Threaded View
Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it
[...]
Quoted text here. Click to load it

I'd thought about that, but I remembered my instructors discouraging
functions with side effects.  I'm not sure why now, other than they'd
been teaching us FORTRAN the previous quarter.  Certainly after 20
years of programming in C, it seems almost second nature today.

Though one thing bugs me.  In C, nextkey would be written something
like

   int nextkey(int *key_ptr)
   {
      *key_ptr = get_key();
      return *key_ptr != EXIT_KEY;
   }

and would be called like

   while ( nextkey(&key) ) process(key);

Note the address operator at the call.  It makes it obvious (at the
point the function is used) that nextkey modifies its parameter (or at
least it _could_).  In Pascal, the only way to know that is to look at
the function definition.  In C++, the parameter is likely to be a
reference, and have the same problem (IMHO) as Pascal.

Oh, and I never did like Pascal's cutesy way of returning a value from
a function...  But that's just syntax.  Until you try to use the
function name as a temporary -- then all recursive heck breaks out.

Quoted text here. Click to load it

Nor I.  One recent small (PIC) project has 26 function definitions
(including main).  Since most of these are called from one place
(each), the compiler is smart enough to "inline" them so that worst
case return stack usage (including interrupt) is 3.

Regards,

                               -=Dave
--
Change is inevitable, progress is not.

Re: Certified C compilers for safety-critical embedded systems
:   while ( nextkey(&key) ) process(key);
:
: Note the address operator at the call.  It makes it obvious (at the
: point the function is used) that nextkey modifies its parameter (or at
: least it _could_).  In Pascal, the only way to know that is to look at
: the function definition.  In C++, the parameter is likely to be a
: reference, and have the same problem (IMHO) as Pascal.

Ada solution that addresses both & and the while(1) issue:

procedure p is

   function next_key (key_filled: access Character) return Boolean is separate;

   procedure process (the_key: in out Character) is separate;


   key: aliased Character;

begin

   while next_key (key'access) loop
      process(key);

   end loop;

end p;


-- Georg

Re: Certified C compilers for safety-critical embedded systems
: On Wed, 31 Dec 2003 14:27:08 +0000 (UTC), Georg Bauhaus
:
:
: Note: I'm reading from comp.arch.embedded.  Just so you know where I'm
: coming from...

Sorry. I need to adjust my reader software.

: Is the "'access" tag (or whatever you call it)

It's an attribute, like 'address, 'size, 'range, etc.

: Is the "'access" tag (or whatever you call it) _required_ on the call
: if a function is going to modify the parameter?  I like it even better
: if that's true.

Yes, as Stephen has explained. Let me add that if you want a variable
to be modifiably through some pointer you will have to say so.
You declare the variable aliased (using the "aliased" keyword
in the declaration), and point to it using 'access values.

There is also an 'unchecked_access attribute which allows pointers to
aliased local objects to be passed around. The intention is to remind
the programmer/maintainer of the pointer validity check that cannot
in general be done by the compiler as in the following example:

   type Reg16_Ptr is access all Interfaces.Unsigned_16;
   --  pointer to a 16 bit register


   function trig_reg return Reg16_Ptr is
      
      v: aliased Interfaces.Unsigned_16;
      --  16 bits from the toaster's eject trigger, v is local to function
      
      pragma Import(Ada, v);
      --  do not initialise v
      
      for v'address use System.Storage_Elements.To_Address(16#A022#);
      --  hardware address
   begin
      return v'unchecked_access;
      --  points to local v which is really a register, not a value on the
      -- stack
   end trig_reg;


-- Georg

Re: Certified C compilers for safety-critical embedded systems
"safety critical C" is an oxymoron if I ever heard one.



Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it

Ariane 5! Ariane 5! Nyah nyah! Nyah nyah!


Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

In every group that I participated in that ever discussed issues of code
reuse from a systems perspective, the fact that an M1A1 tank was not an
M1 tank was discussed.  (Substitute F-15 and F-15E for Air Force
sponsored groups and so on.) The result, of course is that you may be
able to reuse much of the code, but you CANNOT reuse the requirements
analysis.  And if the requirements change, then the testing has to
change. So even if you can reuse 100% of the code, that only saves 15%
of the overall software costs.  Library reuse works on the other hand,
but you have to invest in building the library independent of an
particular development project.  If a reuse library contains software
that matches your requirements, then you have a component that solves
part of your problem and does not require a new test plan, test suite,
and testing.  (You still need to perform system test however.)

Arianne 501 crashed because the bean counters tried to do software reuse
without repeating the requirements analysis, and later cut out all
system testing.  Oops!  Incidently the subsequent Arianne 5 failures
followed almost identical fault trees, but they did not involve Ada code.


--
                                           Robert I. Eachus

"The war on terror is a different kind of war, waged capture by capture,
We've slightly trimmed the long signature. Click to see the full one.
Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it

Yes, I know. But I'm also pretty sure that there's lots of
safety-critical code that's written in C. If someone is
going to mouth off with ignorant comments about C, I want
to make sure that I mouth off with ignorant comments about
Ada.


Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it

Neither of which is very helpful.  You might do well to recognize
that Ada has been designed to detect Stupid Human Tricks as far as
practicable, while C is designed to allow SHTs anywhere that they
are not demonstrably and immediately fatal.  At the same time I
expect Scott Moore has more experience with strongly typed and
relatively safe languages than you do.  I may be wrong.

Given a choice of two airline pilots, would you choose the one
whose sole experience has been stunt-flying and racing, or the one
who has been captaining an airliner without incident for a similar
length of time?  Would you alter your choice if

 a) You want to get there in one piece or
 b) You have to get there yesterday to prevent disaster or
 c) Only one is available.

--
Chuck F ( snipped-for-privacy@yahoo.com) ( snipped-for-privacy@worldnet.att.net)
   Available for consulting/temporary embedded and systems.
We've slightly trimmed the long signature. Click to see the full one.
Re: Certified C compilers for safety-critical embedded systems
 > Ada has been designed...

That does not make safety-critical C an "oxymoron".


Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

Yes, of course.  There's plenty of hyperbole on usenet -- folks say
"X is impossible and Y is perfect" when the truth is,
"Y is better than X for certain purposes".

It's interesting that there are actually *very* few disasters caused by
the malfunction of safety-critical software (in *any* language).  At
least, compared to the number of malfunctions in software I use every
day on my desk.  Language is important, but it is far from the *only*
issue in ensuring safety.  And airplanes are not dropping out of the
sky all the time.

Quoted text here. Click to load it

;-)

This vaguely reminds me of the usenet game of "trolling", where one
tries to trick one's opponents into thinking oneself is a blithering
idiot.  I don't get it -- how can anybody get satisfaction out of that?

At least you said "nyah nyah" to let us know you were being sarcastic.

Sorry, this is getting off topic.  I'll shut up now.

- Bob

Re: Certified C compilers for safety-critical embedded systems
Please, let us not start this Ariane 5 discussion again. There have been at
least 3 threads on this topic, and the later threads have done nothing other
than rehash the arguments from the first thread. There are enough reruns on
television, we don't need them in newsgroups. Unless one of us comes up with
something about Ariane 5 that has not been said here before, can't we just
move on?



Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

From another point of view, they just opened the system testing process
up to the public view :-)

Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

Sorry, no.  If the course of Ariane 501 would have been slightly
different, the launch would have succeeded.  But it would have said
nothing about the likelihood that then next Airiane 5 launch would have
succeeded.  In fact there have been three major failures in less than a
dozen launches, with lots of originally needed testing done after each
failure, and they still don't have a working system.  In the meantime,
Ariane 4 (Remember, the one the software requirements were originally
for?) has had about 100 launches with a very good record.

So the Ariane 5 is almost the poster child for doing reuse without
redoing the systems requirements analysis from the top.   I would hope
that no one would ever make that mistake again.  But the lesson that
keeps being taught about the first Ariane 5 launch is about software
validation.

Similarly the lessons learned in five Airbus 320 crashes are getting
papered over.  It is by now clear to those who study such accidents,
that all five accidents were probably caused by invalid requirements.
For years Airbus has claimed that the software had been proven correct
and couldn't have caused the crashes.  But finally enough has come out
that the accident investigators are pretty sure they know exactly which
requirements error caused which crash.

The Airbus 320 should bury the idea that theorem provers can result in
safe software.  In the case of the Airbus 320 what happened was that the
formal logic used for stating the requirements/theorems was relatively
opaque to experts in the field (read pilots).  So the flaws in the
requirements, and later about 500 people, were buried by that opacity.

--
                                           Robert I. Eachus

"The war on terror is a different kind of war, waged capture by capture,
We've slightly trimmed the long signature. Click to see the full one.
Re: Certified C compilers for safety-critical embedded systems
It would seem intuitively obvious to even the most casual observer that
if you're not sure what a thing is *supposed* to do, you can't possibly
be sure that it does it.  Unfortunately, this lesson is often learned at
great financial (and sometimes human) expense.

MDC

Robert I. Eachus wrote:
Quoted text here. Click to load it


--
======================================================================
Marin David Condic
We've slightly trimmed the long signature. Click to see the full one.
Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it

It's always been my contention that writing the specifications which you
will then prove that a program obeys is exactly as hard as writing the
program itself.

Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it

Well, saying they can't result in safe software would be even wronger,
of course.  So I guess the real idea that has to be buried is that
they _will_ do so, just like that.

Or, in other words: no matter how good your tools, the GIGO principle
(garbage in, garbage out) still holds.

Quoted text here. Click to load it

Which would appear to be one of many special cases of what we used to
call the "lemma on conservation of difficulty" among students here.
In the essence it says: "No truly difficult problems ever go away just
by waving some magical tool at them."

--
Hans-Bernhard Broeker ( snipped-for-privacy@physik.rwth-aachen.de)
Even if all the snow were burnt, ashes would remain.

Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it

Yes and no.

Yes, in that writing rigorous formal specifications is HARD WORK.

No, in that the effort you put into writing those rigorous formal specifications
almost always translates into significantly-reduced effort when writing the code
that implements those specifications, because now you have a SOLID
understanding, where you used to have only a sketchy understanding.



Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

Depends on where you draw the line. I have been on Ada projects where
more that 85% of the effort and budget went into requirements and design
(through to detailed specifcations, which included writing the Ada
package specs).  All of them finished on time and under budget.

If you do the design right, writing, debugging and testing the package
bodies is easy.  But I don't recommend that you contract the coding to
Primate Programmers, Inc. (PPI):
http://www.newtechusa.com/ppi/pressroom.asp#higher ;-)

--
                                           Robert I. Eachus

"The war on terror is a different kind of war, waged capture by capture,
We've slightly trimmed the long signature. Click to see the full one.
Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

Maybe, but nobody showed any better way. Or do you think that XP (eXtreme
Programming) did?

--
Regards,
Dmitry A. Kazakov
We've slightly trimmed the long signature. Click to see the full one.
Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

Not always true---we can specify the Halting problem (for a Turing
Equavilent machine), but we cannot implement it without an oracle.

-CRM



Site Timeline