4 ms·
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
by tralarpa 4y ago
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@ */."
- hajile 4y agoIt took around 5-10 man-years to verify the L4 kernel using a theorem prover and that's just 8700 LOC plus 600 lines of assembly. Without such a theorem solver, it is all just "best practices" then hoping for the best.
- ducktective 4y agoIs 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?
- psd1 4y agocgi-bin
- mbrodersen 4y agoI 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.