Visible to the public Formal Analysis of Human Machine Interactions for Cyber-Physical Systems