Our author asks: "but how can you actually prove that your design is error-free?"
The answer is it is difficult but possible. It requires the use of technologies people are generally not familiarized with, such as proof assistants -- prominent examples are Coq, Isabelle/HOL, and ACL2.
There exist, at this point, actual formally verified software artifacts of quite substantial complexity -- the seL4 microkernel, the CompCert C compiler, the Quark browser, and a number of others.
Sadly, very few people outside of academia are familiar with the existence of formal verification tools for software, and the documentation for such systems is (to say the least) non-transparent. The best tool at the moment, Coq, practically requires that its users learn quite a bit about Martin-Löf type theory in order to work effectively in it.
That said, such tools are clearly the way to deal with such things going forward.
What are the engineering and design challenges in creating successful IoT devices? These devices are usually small, resource-constrained electronics designed to sense, collect, send, and/or interpret data. Some of the devices need to be smart enough to act upon data in real time, 24/7. Are the design challenges the same as with embedded systems, but with a little developer- and IT-skills added in? What do engineers need to know? Rick Merritt talks with two experts about the tools and best options for designing IoT devices in 2016. Specifically the guests will discuss sensors, security, and lessons from IoT deployments.