US 12,093,160 B1
IoT event detector correctness verification
Vaibhav Bhushan Sharma, Cupertino, CA (US); Andrew Jude Gacek, Maple Grove, MN (US); Michael William Whalen, Edina, MN (US); Saswat Padhi, Cambridge, MA (US); Andrew Apicelli, Seattle, WA (US); Raveesh Yadav, Redmond, WA (US); Samuel Bayless, Seattle, WA (US); Roman Pruzhanskiy, Kent, WA (US); Rajat Gupta, Seattle, WA (US); Harshil Rajeshkumar Shah, Seattle, WA (US); Fernando Dias Pauer, Lynnwood, WA (US); Ankush Das, San Jose, CA (US); and Dhivashini Jaganathan, Seattle, WA (US)
Assigned to Amazon Technologies, Inc., Seattle, WA (US)
Filed by Amazon Technologies, Inc., Seattle, WA (US)
Filed on Dec. 6, 2021, as Appl. No. 17/543,585.
Int. Cl. G06F 11/00 (2006.01); G06F 11/30 (2006.01); G06F 11/34 (2006.01); G06F 11/36 (2006.01); H04L 67/62 (2022.01)
CPC G06F 11/3447 (2013.01) [G06F 11/3013 (2013.01); G06F 11/3476 (2013.01); G06F 11/3604 (2013.01); H04L 67/62 (2022.05)] 20 Claims
OG exemplary drawing
 
1. A system, comprising:
one or more processors and corresponding memory configured to implement an Internet of things (IOT) service comprising:
an event model builder configured to:
receive input defining an event detector model, wherein the input specifies:
one or more variables to be set based at least in part on IoT input data generated by one or more IoT devices,
a plurality of states,
one or more timers;
transitions between the states, wherein at least some of the transitions are based on at least one of the one or more variables, and
one or more actions to be taken responsive to one or more events detected based at least on the states or transitions; and
generate the event detector model based on the received input such that the event detector model is deployable to:
receive the IoT input data;
detect the one or more events; and
trigger, based on the one or more detected events, respective ones of the one or more actions; and
an event detector model correctness checker configured to:
responsive to receipt of a request to check correctness of the event detector model:
obtain a definition of the event detector model, wherein the definition comprises statements defining the one or more variables, the plurality of states, the one or more timers, the transitions between the states, and the one or more actions;
verify, based on an analysis of the definition of the event detector model, whether the event detector model complies with one or more correctness properties, wherein the one or more correctness properties comprise:
 one or more reachability correctness properties indicating that respective states or actions are reachable according to the definition of the event detector model, or
 one or more timer-based correctness properties indicating correct usage of the one or more timers; and
generate a report indicating the event detector model's compliance with the one or more correctness properties.