I’ve been doing a fair amount of AVR work in Ada lately, as well; at some point, I’ll probably switch to using Spark. It’s nice to have strict typing and formal semantics on even these devices.
@angersockSpin is a model-checker i.e. you provide a formal specification of a program (usually a concurrent one) and it is able to prove some properties (i.e. absence of deadlocks), it also features tools to aid you in extracting [formal] models from C programs. I was speculating that Ada should be more friendly with respect to formal model extraction and hence use with Spin.
I’ve been doing a fair amount of AVR work in Ada lately, as well; at some point, I’ll probably switch to using Spark. It’s nice to have strict typing and formal semantics on even these devices.
One of the (many) items on my (ever growing) todo list is to experiment with Ada, SPIN and model-checking embedded-systems software.
What’s SPIN?
That’s a new one to me.
@angersock Spin is a model-checker i.e. you provide a formal specification of a program (usually a concurrent one) and it is able to prove some properties (i.e. absence of deadlocks), it also features tools to aid you in extracting [formal] models from C programs. I was speculating that Ada should be more friendly with respect to formal model extraction and hence use with Spin.
Thanks, I’d never heard of Spark. Do you have much experience with it?
I’ve only just started using it, actually.