This was hard to tag since it is about safety, uses pseudocode, and the formal method was done semi-formally w/ regular conditionals. That plus being a quick slide deck means it’s quite approachable. Most interesting was the use of fault trees. You could also say this uses the pattern from proof assistants and secure compilers of Untrusted Generation of Data/Action followed by Trusted Checker. In such designs, you put as much of the complexity into the Untrusted part with the Trusted part as simple and rigorous as possible. The idea is Trusted part will never fail plus limit damage of Untrusted part.
The system structure with a safety-related, separated, controller supervising simple safety conditions, while another controller does the actual process/machine control, is rather common in industrial control systems. The functional safety standards (IEC 61508 and its industry specific derivates) basically dictate the separation of safety-related functionality from “standard” functionality. If a system were to combine standard and safety functionality running on the same controller, the whole would need to be verified as if safety-critical.
I appreciate the tip. The only problem: Phil Koopman was in my list of stuff to submit this week. You done beat me to posting him! Although, I’ll probably still do it to experiment with submitting his whole, publication list. We normally do it one paper or project at a time. The work he does is pretty similar and focused, though. Might be justifiable. I’ll still do it later in the week.
While I’m at it, @pushcx, what do you think about this as a submission? Most of it is stuff you wouldn’t want to submit individually. A few things are submission worthy. My concept was to submit it tagged appropriately, add “person” maybe, and summarize his research in text field.
This was hard to tag since it is about safety, uses pseudocode, and the formal method was done semi-formally w/ regular conditionals. That plus being a quick slide deck means it’s quite approachable. Most interesting was the use of fault trees. You could also say this uses the pattern from proof assistants and secure compilers of Untrusted Generation of Data/Action followed by Trusted Checker. In such designs, you put as much of the complexity into the Untrusted part with the Trusted part as simple and rigorous as possible. The idea is Trusted part will never fail plus limit damage of Untrusted part.
The system structure with a safety-related, separated, controller supervising simple safety conditions, while another controller does the actual process/machine control, is rather common in industrial control systems. The functional safety standards (IEC 61508 and its industry specific derivates) basically dictate the separation of safety-related functionality from “standard” functionality. If a system were to combine standard and safety functionality running on the same controller, the whole would need to be verified as if safety-critical.
The second author, Phil Koopman, has done a lot of cool work on dependable systems, for example some early work in selecting good polynomials for CRCs in communication systems.
Nice presentation, thanks for posting!
I appreciate the tip. The only problem: Phil Koopman was in my list of stuff to submit this week. You done beat me to posting him! Although, I’ll probably still do it to experiment with submitting his whole, publication list. We normally do it one paper or project at a time. The work he does is pretty similar and focused, though. Might be justifiable. I’ll still do it later in the week.
While I’m at it, @pushcx, what do you think about this as a submission? Most of it is stuff you wouldn’t want to submit individually. A few things are submission worthy. My concept was to submit it tagged appropriately, add “person” maybe, and summarize his research in text field.