That might be the reason why the JPL coding standard says:
"All loops shall have a statically determinable upper-bound on the
maximum number of loop iterations. It shall be possible for a static
compliance checking tool to affirm the existence of the bound. An
exception is allowed for the use of a single non-terminating loop per task
or thread where requests are received and processed. Such a server loop
shall be annotated with the C comment: /* @non-terminating@ */."
Is there a tech stack or language that allows us to write formally proven and real-time (bounded-time tasks) for embedded systems?
What if we can be lenient on these conditions (like soft real time, 500ms bounds)?
I'm looking for something like shell scripting (easy and functional) + busybox set of utilities + language built-ins to write concurrent applications. Like an OS with a specialized shell scripting language. Does something like this exist?
I am currently playing around with Dafny and it is very promising. I have use it to generate proven correct high-performance C# code without too much efforts. It’s great fun actually. Like a really cool puzzle game.
"All loops shall have a statically determinable upper-bound on the maximum number of loop iterations. It shall be possible for a static compliance checking tool to affirm the existence of the bound. An exception is allowed for the use of a single non-terminating loop per task or thread where requests are received and processed. Such a server loop shall be annotated with the C comment: /* @non-terminating@ */."