5 ms·

Disregarding that it's not a solution to the DoD's problem as such, does Ada/SPARK have merit for writing embedded software? I am coincidentally researching if

Disregarding that it's not a solution to the DoD's problem as such, does Ada/SPARK have merit for writing embedded software? I am coincidentally researching if I could rewrite parts of a personal project in Ada (from C) to improve reliability, and so far have failed to conclude either way.

qznc 11y ago
Have you considered MISRA C? Ada/SPARK have merit if you really want to do hard real time and formal methods. That seems overkill for a personal project?
- hga 11y ago
  Or if you want to go in the complete opposite direction, formal proofs of your system down to the binary, look at seL4.
  - pgeorgi 11y ago
    So you have a formally verified kernel. And then what? It's possible to run L4 processes written in SPARK on top of seL4.
    - hga 11y ago
      My suggestion of a wildly different approach was to more or less replicate what NICTA et. al. did with seL4 with your own project. There's also the Coq ecosystem, which includes a verified free for non-commercial use C compiler.
      - pgeorgi 11y ago
        That's possible, but incredibly tedious. It may be easier to just generate binary code from assembly in coq (as Microsoft Research has demonstrated: http://research.microsoft.com/en-us/um/people/nick/coqasm.pdf http://research.microsoft.com/en-us/um/people/nick/coqasm.pd...) instead of trying to shoehorn a C compiler into a verified context and then running proofs over that for non-trivial problems. seL4 was a huge project. Once you start reasoning about using L4 APIs, it will only become worse (eg. it's not simple to determine who has access to the pages in any L4 AddressSpace)
- OopsCriticality 11y ago
  A problem there is cost for a personal project: are there any free or low-cost MISRA C static checkers out there? Frama-C might be worth looking into if the goal is improved reliability, and they'd be able to leverage their existing C skillset.
  - hga 11y ago
    Lowest I know of is Gimpel's PC-/FlexLint, single workstation prices are $389 to run on Windows, $998 for obfuscated C source code: http://www.gimpel.com/html/index.htm http://www.gimpel.com/html/index.htm The MISRA documentation is not very expensive and useful by itself, £15 + VAT for an ecopy: http://www.misra.org.uk/?TabId=58 http://www.misra.org.uk/?TabId=58
PinkyThePiggy 11y ago
I would say so, especially considering that is where the majority of Ada/Spark is used currently. Space flight, planes, assembly lines, automotive etc. There is a blog post about rewriting a drones control system in Spark if you were curious: http://blog.adacore.com/how-to-prevent-drone-crashes-using-spark http://blog.adacore.com/how-to-prevent-drone-crashes-using-s... It does exactly what you were planning. Taking C code and rewriting it in Spark in an embedded environment.
noselasd 11y ago
ISRO seem to be quite happy about using Ada on their Mars Orbiter - discussed somewhere in https://www.youtube.com/watch?v=KFJUlVbTXII https://www.youtube.com/watch?v=KFJUlVbTXII

qznc 11y ago

Have you considered MISRA C? Ada/SPARK have merit if you really want to do hard real time and formal methods. That seems overkill for a personal project?

hga 11y ago
Or if you want to go in the complete opposite direction, formal proofs of your system down to the binary, look at seL4.
- pgeorgi 11y ago
  So you have a formally verified kernel. And then what? It's possible to run L4 processes written in SPARK on top of seL4.
  - hga 11y ago
    My suggestion of a wildly different approach was to more or less replicate what NICTA et. al. did with seL4 with your own project. There's also the Coq ecosystem, which includes a verified free for non-commercial use C compiler.
    - pgeorgi 11y ago
      That's possible, but incredibly tedious. It may be easier to just generate binary code from assembly in coq (as Microsoft Research has demonstrated: http://research.microsoft.com/en-us/um/people/nick/coqasm.pdf http://research.microsoft.com/en-us/um/people/nick/coqasm.pd...) instead of trying to shoehorn a C compiler into a verified context and then running proofs over that for non-trivial problems. seL4 was a huge project. Once you start reasoning about using L4 APIs, it will only become worse (eg. it's not simple to determine who has access to the pages in any L4 AddressSpace)
OopsCriticality 11y ago
A problem there is cost for a personal project: are there any free or low-cost MISRA C static checkers out there? Frama-C might be worth looking into if the goal is improved reliability, and they'd be able to leverage their existing C skillset.
- hga 11y ago
  Lowest I know of is Gimpel's PC-/FlexLint, single workstation prices are $389 to run on Windows, $998 for obfuscated C source code: http://www.gimpel.com/html/index.htm http://www.gimpel.com/html/index.htm The MISRA documentation is not very expensive and useful by itself, £15 + VAT for an ecopy: http://www.misra.org.uk/?TabId=58 http://www.misra.org.uk/?TabId=58

PinkyThePiggy 11y ago

I would say so, especially considering that is where the majority of Ada/Spark is used currently. Space flight, planes, assembly lines, automotive etc. There is a blog post about rewriting a drones control system in Spark if you were curious: http://blog.adacore.com/how-to-prevent-drone-crashes-using-spark http://blog.adacore.com/how-to-prevent-drone-crashes-using-s... It does exactly what you were planning. Taking C code and rewriting it in Spark in an embedded environment.

noselasd 11y ago

ISRO seem to be quite happy about using Ada on their Mars Orbiter - discussed somewhere in https://www.youtube.com/watch?v=KFJUlVbTXII https://www.youtube.com/watch?v=KFJUlVbTXII