4 ms·

What is high assurance in the context of RTOS for microcontrollers?

snvzz 8y ago
Guaranteeing things like worst case timing, complete with formal proofs. Without formal proofs, no hard realtime is possible; What you've got is soft realtime instead, the relaxed version where there's no guarantees.
- nickpsecurity 8y ago
  Hard real-time without formal proofs is not only possible: it's the norm for almost all hard, real-time systems out there. It's mostly about careful coding and time analysis. Recent ones have had stronger isolation with formal verification of a few. It's not necessary to get them working most of the time, though. Matter of fact, regulators for safety-critical fields are just starting to accept formal verification as evidence. CompCert is only tool I know of that's qualified to just one standard. If in those fields, using formal verification instead of whatever evaluators are used to can get something rejected. It can aid the development or be supplementary evidence at best.
  - snvzz 8y ago
    You're right in that this insanity is not uncommon. Without formal verification, there's no guarantee deadlines will not be missed, hard realtime will not fail and people will not die. Sometimes failure is cheap; Other times it is not. A lot of systems out there make outrageous claims of fitness with no formal basis. What a sad state the industry is in.
    - patacongo 8y ago
      Ultimately, an RTOS can only provide you with the tools to create a hard real-time system. The RTOS cannot guarantee that your application can meet any deadlines. That requires the proper use of those tools by the application. If you improperly prioritize tasks or use semaphore locks improperly or keep interrupts disabled too long, then your application will not be real-time. NOTE: NuttX does provide tools to measure interrupt latencies, response times, and critical section times. Those are helps in creating a real-time system. So, it is not a meaningful to ask if the RTOS has been certified in some way to always meet deadlines. You should ask rather, does the OS provide the tools that you need and does your overall application meets its deadlines.
      - snvzz 8y ago
        >So, it is not a meaningful to ask if the RTOS has been certified in some way to always meet deadlines. It is meaningful. If the system doesn't offer these guarantees, no matter how good you are and how much effort you put into what's within your scope to implement, you won't be able to offer any guarantees. This is ok if you can afford to fail. Just don't use it e.g. where human lives would be put at risk.

Guaranteeing things like worst case timing, complete with formal proofs. Without formal proofs, no hard realtime is possible; What you've got is soft realtime instead, the relaxed version where there's no guarantees.

nickpsecurity 8y ago
Hard real-time without formal proofs is not only possible: it's the norm for almost all hard, real-time systems out there. It's mostly about careful coding and time analysis. Recent ones have had stronger isolation with formal verification of a few. It's not necessary to get them working most of the time, though. Matter of fact, regulators for safety-critical fields are just starting to accept formal verification as evidence. CompCert is only tool I know of that's qualified to just one standard. If in those fields, using formal verification instead of whatever evaluators are used to can get something rejected. It can aid the development or be supplementary evidence at best.
- snvzz 8y ago
  You're right in that this insanity is not uncommon. Without formal verification, there's no guarantee deadlines will not be missed, hard realtime will not fail and people will not die. Sometimes failure is cheap; Other times it is not. A lot of systems out there make outrageous claims of fitness with no formal basis. What a sad state the industry is in.
  - patacongo 8y ago
    Ultimately, an RTOS can only provide you with the tools to create a hard real-time system. The RTOS cannot guarantee that your application can meet any deadlines. That requires the proper use of those tools by the application. If you improperly prioritize tasks or use semaphore locks improperly or keep interrupts disabled too long, then your application will not be real-time. NOTE: NuttX does provide tools to measure interrupt latencies, response times, and critical section times. Those are helps in creating a real-time system. So, it is not a meaningful to ask if the RTOS has been certified in some way to always meet deadlines. You should ask rather, does the OS provide the tools that you need and does your overall application meets its deadlines.
    - snvzz 8y ago
      >So, it is not a meaningful to ask if the RTOS has been certified in some way to always meet deadlines. It is meaningful. If the system doesn't offer these guarantees, no matter how good you are and how much effort you put into what's within your scope to implement, you won't be able to offer any guarantees. This is ok if you can afford to fail. Just don't use it e.g. where human lives would be put at risk.