3 ms·

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?

by qznc 11y ago

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

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?

by 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