Model-checking State Machines in the Wild
| Abstract: State machines are a compact representation of complex logical rules. State machines have diverse uses such as watchdog applications to monitor if a critical program has crashed, regular expression matching, and web services such as IFTTT (short for If This Then That) which has 18 million users running over 1 billion state machines. These state machines are often created for ad-hoc purposes with speed of development being a primary goal. But, their correctness is still crucial. For example, consider a watchdog application that should notify you when a critical program crashes. If it is not implemented correctly, you will never be notified causing pain to your downstream users. We have identified five widely applicable property templates that catch real bugs in these state machines. Two of these properties are (1) reachability, i.e. every state in the state machine must be reachable, and, (2) no-uninitialized-variables, i.e. every variable must be set to a value before being used. |
We are verifying these five properties for customers of AWS IoT Events using model-checking. AWS IoT Events helps customers detect events in their IoT devices at scale. In this talk we describe our tool that helps AWS IoT Events customers develop more reliable state machines without requiring any knowledge of automated reasoning.
Vaibhav Sharma is an Applied Scientist at Amazon.com Services LLC. Vaibhav works on applying automated reasoning to secure payments applications at Amazon. Previously, Vaibhav worked on applying automated reasoning to the Internet of Things (IoT) domain at AWS. Prior to AWS, Vaibhav obtained a PhD in Computer Science from the University of Minnesota during which he worked on program synthesis using scalable symbolic execution.