METHOD AND SYSTEM FOR VERIFYING SLEEP WAKEUP PROTOCOL BY COMPUTING STATE TRANSITION PATHS

摘要

Disclosed are a method and a system for facilitating verification of program code implementing Sleep Wakeup protocol for a microcontroller. An input handling module is configured to receive metadata from user required for verification of the program code. Identification module is configured to identify abstract syntax tree (AST) nodes corresponding to each program point in the program code. A computation module is configured to compute an actual interrupt protection status (IPS), task lock status (TLS), path entities and shared variables for each program point in the program code. A path analysis module is configured to determine transition paths between program points specified in the metadata, and are computed in terms of the path entities. Also, review information is computed for each of the path entities comprised in the transition paths. Further, a report generation module is configured to generate a report comprising the review information facilitating the user to verify the program code.

主权项

1. A method for facilitating verification of a program code implementing a Sleep Wakeup protocol for a micro-controller, the method performed by at least one processor and comprising:
receiving metadata from a user, wherein the metadata is required for verification of the program code, and wherein the metadata comprises:
a location of a plurality of program points in the program code, each program point of the plurality of program points corresponding to at least one of a start of a Background job, a Sleep operation, and a Wakeup operation in the program code;an initial interrupt protection status (IPS) at the start of the program code;interrupt functions for at least one of enabling and disabling the interrupts; andtask functions for at least one of enabling and disabling task switching; computing for each program point:
an actual IPS based on the initial IPS and calls to the interrupt functions;a task lock status (TLS) based on calls to the task functions;path entities comprising at least one of a conditional statement and a function call point; andshared variables; determining transition paths between the plurality of program points in terms of the path entities; computing review information for each set of path entities based on the actual IPS, the TLS, and the shared variables; and generating a report for the user in a pre-defined format, wherein the report comprises information relating to the transition paths and the review information, and wherein the report facilitates the user to verify the program code.