IoT Event Detector Correctness Verification

A system, comprising:

• one or more processors and corresponding memory configured to implement a correctness checker configured to:
• receive a request to check correctness of a deployable event detector model configured to:
• detect, based on input data from one or more data-producing devices, one or more events;
• or
• to trigger, based on the one or more detected events, one or more actions;
• obtain a definition of the event detector model, wherein the definition comprises statements defining one or more variables, one or more timers, a plurality of states, transitions between the states, or 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, comprising:
• a set of default correctness properties used by default as part of said verify,
• one or more domain-specific correctness properties tailored for correctness checks of detector models of a specific domain,
• 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 compliance of the event detector model with the one or more correctness properties.

A method, comprising:

• performing, by one or more computing devices:
• receiving a request to check correctness of a deployable event detector model, the deployable event detector model to perform:
• detecting, based on input data from one or more of data-producing devices, one or more events, or
• triggering, based on the one or more detected events, one or more actions;
• obtaining a definition of the event detector model, wherein the definition comprises statements defining one or more variables, one or more timers, a plurality of states, transitions between the states, or one or more actions;
• verifying, based on analyzing the definition of the event detector model, whether the event detector model complies with one or more correctness properties, the correctness properties comprising:
• a set of default correctness properties used by default as part of said verifying,
• one or more domain-specific correctness properties tailored for correctness checks of detector models of a specific domain,
• one or more reachability correctness properties that check that respective states or actions are reachable according to the definition of the event detector model, or
• one or more timer-based correctness properties that check correct usage of the one or more timers;
• and
• generating a report that indicates compliance of the event detector model with the one or more correctness properties.

One or more non-transitory computer-readable media storing program instructions executable on or across one or more processors to perform:

• responsive to receipt of a request to check correctness of a deployable event detector model configured to detect, based on input data from one or more data-producing devices, one or more events, or configured to trigger, based on the one or more detected events, one or more actions:
• obtaining a definition of the event detector model, wherein the definition comprises statements defining one or more variables, one or more timers, a plurality of states, transitions between the states, or one or more actions;
• verifying, based on analyzing the definition of the event detector model, whether the event detector model complies with one or more correctness properties, the correctness properties comprising:
• a set of default correctness properties used by default as part of said verifying,
• one or more domain-specific correctness properties tailored for correctness checks of detector models of a specific domain,
• one or more reachability correctness properties that check that respective states or actions are reachable according to the definition of the event detector model, or
• one or more timer-based correctness properties that check correct usage of the one or more timers;
• and
• generating a report that indicates compliance of the event detector model with the one or more correctness properties.