# US 2013/0158974 A1 · Modeling and predicting control system behavior through fast-forwarding > Agents: this data is available as JSON from the patentgrep API and MCP server — see https://patentgrep.com/llms.txt - Number: US 2013/0158974 A1 - Document ID: US20130158974A1 - Status: Published application - Kind: A1 - Application number: 13/325,077 - Filed: 2011-12-14 - Published: 2013-06-20 - Earliest claimed: 2011-12-14 - Assignees: Microsoft Corporation - Inventors: Jason Croft; Ratul Mahajan; Madan Musuvathi - Web page: https://patentgrep.com/patent/US20130158974A1 ## CPC - G05B 17/02: electric - G05B: CONTROL OR REGULATING SYSTEMS IN GENERAL; FUNCTIONAL ELEMENTS OF SUCH SYSTEMS; MONITORING OR TESTING ARRANGEMENTS FOR SUCH SYSTEMS OR ELEMENTS (systems for controlling or regulating non-electric variables G05D; systems for regulating electric or magnetic variables G05F; control devices or systems insofar as characterised by mechanical features only G05G) ## Abstract Methods and systems for modeling and predicting control system behavior through fast-forwarding are provided herein. The method includes obtaining sets of equivalent inputs, time zones, and a user-defined stop time. The method also includes taking a primary checkpoint of a main instance of a control system in response to a user input. The method includes fast-forwarding the control system by generating a secondary instance from the main instance at the primary checkpoint and subjecting the secondary instance to each combination of an input from each of the sets of equivalent inputs in each time zone. The method includes taking a secondary checkpoint from the primary checkpoint for each combination. For each secondary checkpoint, the method includes fast-forwarding the control system by generating a tertiary instance from the secondary instance and subjecting the tertiary instance to each combination as long as a time does not exceed the user-defined stop time. ## Claims ### Claim 1 A method for modeling and predicting control system behavior through fast-forwarding, comprising: obtaining sets of equivalent inputs, time zones, and a user-defined stop time within a computing environment; taking a primary checkpoint of a main instance of a control system in response to a user input; fast-forwarding the control system by generating a secondary instance from the main instance at the primary checkpoint and subjecting the secondary instance to each combination of an input from each of the sets of equivalent inputs in each of the time zones; taking a secondary checkpoint from the primary checkpoint for each combination; for each secondary checkpoint, fast-forwarding the control system by generating a tertiary instance from the secondary instance at the secondary checkpoint and subjecting the tertiary instance to each combination as long as a time does not exceed the user-defined stop time. ### Claim 2 (depends on 1) The method of claim 1, comprising: taking an additional checkpoint from the secondary checkpoint for each combination; and for each additional checkpoint, fast-forwarding the control system by generating an additional instance from the tertiary instance and subjecting the additional instance to each combination as long as the time does not exceed the user-defined stop time. ### Claim 3 (depends on 1) The method of claim 1, comprising outputting results from the fast-forwarding of the control system, wherein the results comprise a model of future control system behavior. ### Claim 4 (depends on 1) The method of claim 1, wherein obtaining the sets of equivalent inputs comprises analyzing source code from the control system to infer the sets of equivalent inputs using symbolic execution. ### Claim 5 (depends on 1) The method of claim 1, wherein obtaining the time zones comprises: analyzing source code from the control system to infer virtual clocks and associated constraints; and utilizing the virtual clocks and associated constraints to construct the time zones using symbolic execution and timed automata techniques. ### Claim 6 (depends on 1) The method of claim 1, comprising allowing the main instance of the control system to continue running without interruption. ### Claim 7 (depends on 1) The method of claim 1, wherein subjecting the primary checkpoint and each secondary checkpoint to each combination comprises observing a predicted state of the control system at the input from each of the sets of equivalent inputs in each of the time zones. ### Claim 8 (depends on 1) The method of claim 1, comprising terminating the fast-forwarding of the control system if the time exceeds the user-defined stop time. ### Claim 9 (depends on 1) The method of claim 1, wherein the time comprises a virtual time, a physical time, or a relative time, or any combinations thereof. ### Claim 10 (depends on 1) The method of claim 1, wherein fast-forwarding the control system comprises performing a state space exploration procedure to model a future behavior of the control system. ### Claim 11 A system, comprising: a processor that is adapted to execute stored instructions; and a storage device that stores modules that are executable by the processor, the modules comprising: an offline analysis module configured to analyze source code from a control system to infer sets of equivalent inputs and construct time zones; and a state space exploration module configured to: take a second instance from a main instance of the control system in response to a user's selection of a primary checkpoint; perform state space exploration by subjecting the second instance to an input from each of the sets of equivalent inputs in each of the time zones; take a plurality of additional checkpoints from the primary checkpoint for the input in each of the time zones; and for each additional checkpoint, perform the state space exploration by generating a subsequent instance from the second instance at the additional checkpoints and subjecting the subsequent instance to the input in each of the time zones as long as a time does not exceed a user-defined stop time. ### Claim 12 (depends on 11) The system of claim 11, wherein the offline analysis module is configured to analyze the source code to infer the sets of equivalent inputs using symbolic execution. ### Claim 13 (depends on 11) The system of claim 11, wherein the offline analysis module is configured to: analyze the source code to infer virtual clocks and time constraints; and construct the time zones from the virtual clocks and the time constraints using symbolic execution and timed automata. ### Claim 14 (depends on 11) The system of claim 11, wherein the user-defined stop time comprises a virtual time, a relative time, or a physical time, or any combinations thereof, at which to end the state space exploration of the control system, as specified by a user of the control system. ### Claim 15 (depends on 11) The system of claim 11, wherein the sets of equivalent inputs comprise sets of inputs for which a state of the control system is unchanged. ### Claim 16 (depends on 11) The system of claim 11, wherein the time zones comprise virtual lengths of time, physical lengths of time, or relative lengths of time during which a specific time is irrelevant. ### Claim 17 (depends on 11) The system of claim 11, wherein the state space exploration module is configured to output results of the state space exploration to a user of the control system. ### Claim 18 (depends on 17) The system of claim 17, wherein the results of the state space exploration comprise a prediction or a model of control system behavior. ### Claim 19 (depends on 11) The system of claim 11, wherein the state space exploration of the control system comprises a fast-forwarding of a copy of the main instance of the control system. ### Claim 20 One or more non-transitory, computer-readable storage media for storing computer-readable instructions, the computer-readable instructions providing a system for modeling and predicting control system behavior when executed by one or more processing devices, the computer-readable instructions comprising code configured to: perform state space exploration of a control system as long as a time does not exceed a user-defined stop time by evaluating the control system at multiple checkpoints within each of a plurality of instances of the control system, wherein evaluating the control system at one of the checkpoints within one of the instances comprises subjecting the one instance to an input from each of a plurality of sets of equivalent inputs in each of a plurality of time zones at the one checkpoint, the multiple checkpoints generated by evaluating the control system at a primary checkpoint within a main instance of the control system, wherein evaluating the control system at the primary checkpoint within the main instance comprises subjecting the main instance to the input from each of the sets of equivalent inputs in each of the time zones at the primary checkpoint, a delay being incorporated to transition between the time zones.