Forums

Formal Verification of Software

Started by MaxMaxfield 2 weeks ago10 replieslatest reply 1 week ago66 views

I'm just trying to get a feel for things here. I'm a hardware design engineer by trade. I'm familiar with the concepts of formal verification with regard to designing hardware. I'm less familiar with formal verification in the context of developing software.

The funny thing is that formal verification was original conceived with software development in mind, but the problem was too unbounded and it was never really practical.

So, my question is, "How many of today's software developers -- both high-level application developers and more firmware-inclined embedded systems developers -- do you think are aware of the concept of formal verification (a) in general and (b) with regard to software?"

Any feedback will be very much appreciated as always :-)

[ - ]
Reply by jmford94July 20, 2021

Hi Max.  I think most are aware of the concept, but I suspect that almost nobody actually does it.  There's an editorial in the July issue of the Communications of the ACM by Moshe Vardi on this very issue(DOI:10.1145/3469113).   He points out that formal verification isn't done for many reasons, but also compares formal verification with Model Checking, which is easier and cheaper.  The main obstacle to formal verification is its cost, according to Vardi.  For hardware designs, where the cost of fixing a defect is very high, it makes sense, whereas for most software, the cost of fixing a defect isn't as high.  At least that's the perception.  Hardware designs are also not as free-form as most large software projects, and formal verification is tractable.

John

[ - ]
Reply by MaxMaxfieldJuly 20, 2021

Hi John -- Thanks so much for your response -- do you mind if I quote your response in a column I'm writing?

[ - ]
Reply by jmford94July 20, 2021

No, I don't mind!  :)


[ - ]
Reply by MaxMaxfieldJuly 20, 2021

Cool Beans -- How would you like to be referred to (name, position, link to LinkedIn)?

[ - ]
Reply by jmford94July 20, 2021

Hi Max.  


I'm John Ford, Principal Engineer at Steward Observatory, University of Arizona.

https://www.linkedin.com/in/john-ford-bb034121/
[ - ]
Reply by MaxMaxfieldJuly 21, 2021

Make sure to keep your eyes open for my column on EEJournal.com thsi coming Thursday :-)

[ - ]
Reply by M65C02AJuly 23, 2021

Post deleted by author

[ - ]
Reply by M65C02AJuly 23, 2021
Hello John: Never heard back from you regarding the multi-channel Asynchronous Receiver that I sent you. Just curious if you were able to make it work in your application?
[ - ]
Reply by jmford94July 26, 2021

No, we were not able to use it, because we needed a 5 megabit per second uart and didn't have enough clock cycles to mux the inputs in.  We ended up with  enough space in the FPGA to do individual UARTs once I got the design completed.

I've got it in my bag of tricks if it's ever needed!


[ - ]
Reply by M65C02AJuly 26, 2021

That’s too bad you weren’t able to use it, but glad that you were successful