Design Con 2015
Breaking News
Comments
Newest First | Oldest First | Threaded View
<<   <   Page 2 / 3   >   >>
TonyTib
User Rank
CEO
Exactly - how do you verify your specifications?
TonyTib   1/10/2014 12:36:47 PM
NO RATINGS
Even if you can verify your program is a bug-free implementation of your specifications, how do you verify your specifications?


And how do you account for electrical or mechanical "bugs"?  Such as sensors not working correctly, cosmic rays (SEUs, etc), mechanical elements failing, and such.


And then what do you do when the needs (specifications) change?  Often times, it seems like people assume the specs will never change; one of the things I like best about agile development is that they assume the specs will change.  Automated test suites can help (regression testing), but with real world systems that's harder.

There's a reason I like hard-wired (NO SOFTWARE!) E-Stop or EMO systems.

pmetzger
User Rank
Rookie
Re: few ideas
pmetzger   1/10/2014 12:24:06 PM
NO RATINGS
"But it still doesn't prove the widget will do what you actually wanted it to do - only that the two models do the same thing under a (hopefully) more exhaustive set of conditions" -- well, sort of.

It is true that you have to be able to explain in logic what you want the system to do, and the need for such specifications has often been held out as a reason that formal methods can never work. However, I think that's just sour grapes from the days when formal methods were *really* impractical twenty years ago. Not that long ago we *couldn't* actually prove significant systems correct, and so we convinced ourselves that even if we could we would never be able to figure out what properties we wanted proven correct anyway -- just like the fox and the grapes. In practice, I think people often overestimate how troublesome it is to produce a logical statement of the desired behavior vs. implementation.

Consider as a trivial example a sorting routine. The output is supposed to be a permutation of the input in which no element is larger than the next (or smaller than the next depending on sort direction). This is very compact to express in logic -- but there are dozens and dozens of algorithms that will do it, and expressing most of them is substantially more complicated than the correctness condition.

That said, doing things like producing the formal semantics for C to permit the statement of the correctness condition for CompCert was certainly a huge effort, and I don't want to claim that it is not a significant effort in many cases to produce a good statement in formal logic. What I'm trying to claim is that this problem is not, in fact, insurmountable.

Indeed, producing statements about correctness constraints in a safety critical system is often quite straightforward. In particular, the control problem described by the original article has safety conditions that are likely quite compactly described.

bernard.deadman
User Rank
Freelancer
Re: few ideas
bernard.deadman   1/10/2014 12:00:57 PM
NO RATINGS
"you need to produce a statement of what your program is supposed to do in formal logic and then demonstrate that your program actually does it"

But it still doesn't prove the widget will do what you actually wanted it to do - only that the two models do the same thing under a (hopefully) more exhaustive set of conditions.

Which surely is the fundamental argument behind all current verification methodologies?

pmetzger
User Rank
Rookie
Re: few ideas
pmetzger   1/10/2014 9:35:06 AM
NO RATINGS
Spark allows proof, but not (unfortunately) proof of arbitrary properties. You can prove some very limited properties, which is certainly useful, but it is not capable of creating something like seL4.

alex_m1
User Rank
CEO
Re: few ideas
alex_m1   1/10/2014 4:25:08 AM
NO RATINGS
The spark pro site do talk about formal proof. And it was used in a lunar orbiter project.SO maybe there's something usefull inside. 

pmetzger
User Rank
Rookie
Re: few ideas
pmetzger   1/9/2014 8:15:59 PM
NO RATINGS
Languages like Haskell are very cool things, but they're not per se ways of producing formally verified code. To do that, you need to produce a statement of what your program is supposed to do in formal logic and then demonstrate that your program actually does it with something like a proof assistant -- not something Haskell or Spark ADA are designed for. That said, Haskell was used to produce the executable model against which the C code used in the seL4 project was validated.

pmetzger
User Rank
Rookie
Re: Proving a program is error free
pmetzger   1/9/2014 8:13:44 PM
NO RATINGS
I'd recommend Coq at this point, rather than Isabelle.

The path to understanding how to use the tool for purposes like this is not, unfortunately, easy. Good examples of projects that have been formally verified using Coq would include CompCert (publications: http://compcert.inria.fr/publi.html ) and Quark ( http://goto.ucsd.edu/quark/ ) -- looking at them may give you some hint of what is possible and how difficult it might be.

Benjamin Pierce's "Software Foundations" ( http://www.cis.upenn.edu/~bcpierce/sf/ ) is probably a good place to get some background while simultaneously learning a bit of Coq. The book Certified Programming with Dependent Types ( http://adam.chlipala.net/cpdt/ ) intends to teach one specifically how to use Coq to write verified programs, but I caution it is not easy going. There is also a book on Coq itself called CoqArt ( http://www.labri.fr/perso/casteran/CoqArt/index.html ) that is not bad.

If this all makes it sound like this is Not An Easy Thing To Learn, that's because it isn't. The state of the art has advanced dramatically in 20 years, from the point where contemplating proving something as big as a compiler correct was impossible to the point where it is feasible for very dedicated PhD students to work on such a thing. However, productizing the work of the innovators in this field is something that has not yet happened. Documentation is sketchy, tools are difficult to use, and the level of complexity remains very high.

That said, it is in fact now feasible for smart people to do this stuff, and the result of formally verified programs is true assurance of correctness.

alex_m1
User Rank
CEO
few ideas
alex_m1   1/9/2014 7:47:19 PM
NO RATINGS
I reas good thing about haskell and spark pro for writing error free code.

http://leepike.wordpress.com/category/haskell/

http://www.adacore.com/sparkpro/

antedeluvian
User Rank
Blogger
Re: Proving a program is error free
antedeluvian   1/9/2014 7:40:46 PM
NO RATINGS
pmetzger

 It requires the use of technologies people are generally not familiarized with, such as proof assistants -- prominent examples are Coq, Isabelle/HOL, and ACL2.



FWIW I did a google search and came up with this book which looks like one place to start. As you say all the references look highly theoretical. Do you know of any practical courses on the subject (perhaps even at EE Live!).

Garcia-Lasheras
User Rank
Blogger
Mission: impossible
Garcia-Lasheras   1/9/2014 7:38:06 PM
NO RATINGS
"Debugging is twice as hard as writing the code in the first place. Therefore, if you write the code as cleverly as possible, you are, by definition, not smart enough to debug it." --Brian Kernighan

Now, add a complex physical system interacting with the code under test and things become even worse... My first reaction is that you can "asymptotically" check the code of a system such as the one you describe, but the coverage will never be perfect -- no matter if you do it by hand or using an automated tool.

<<   <   Page 2 / 3   >   >>


Top Comments of the Week
Flash Poll
Like Us on Facebook

Datasheets.com Parts Search

185 million searchable parts
(please enter a part number or hit search to begin)
EE Life
Frankenstein's Fix, Teardowns, Sideshows, Design Contests, Reader Content & More
Max Maxfield

Want a Voltera Desktop PCB Printer?
Max Maxfield
9 comments
I just received an email from my chum Javi in Spain. "Have you heard about Voltera (VolteraInc.com)? It's a Canadian company that is going to offer desktop-size PCB printers for fast ...

Aubrey Kagan

Have You Ever Been Blindsided by Your Own Design?
Aubrey Kagan
37 comments
I recently read GCHQ: The uncensored story of Britain's most sensitive intelligence agency by Richard J. Aldrich. The Government Communication Headquarters (GCHQ), Britain's equivalent of ...

Martin Rowe

No 2014 Punkin Chunkin, What Will You Do?
Martin Rowe
2 comments
American Thanksgiving is next week, and while some people watch (American) football all day, the real competition on TV has become Punkin Chunkin. But there will be no Punkin Chunkin on TV ...

Rich Quinnell

Making the Grade in Industrial Design
Rich Quinnell
15 comments
As every developer knows, there are the paper specifications for a product design, and then there are the real requirements. The paper specs are dry, bland, and rigidly numeric, making ...

Special Video Section
The LT8640 is a 42V, 5A synchronous step-down regulator ...
The LTC2000 high-speed DAC has low noise and excellent ...
How do you protect the load and ensure output continues to ...
General-purpose DACs have applications in instrumentation, ...
Linear Technology demonstrates its latest measurement ...
10:29
Demos from Maxim Integrated at Electronica 2014 show ...
Bosch CEO Stefan Finkbeiner shows off latest combo and ...
STMicroelectronics demoed this simple gesture control ...
Keysight shows you what signals lurk in real-time at 510MHz ...
TE Connectivity's clear-plastic, full-size model car shows ...
Why culture makes Linear Tech a winner.
Recently formed Architects of Modern Power consortium ...
Specially modified Corvette C7 Stingray responds to ex Indy ...
Avago’s ACPL-K30T is the first solid-state driver qualified ...
NXP launches its line of multi-gate, multifunction, ...
Doug Bailey, VP of marketing at Power Integrations, gives a ...
See how to ease software bring-up with DesignWare IP ...
DesignWare IP Prototyping Kits enable fast software ...
This video explores the LT3086, a new member of our LDO+ ...
In today’s modern electronic systems, the need for power ...