Verified inference engine for autonomy

• US 10,095,230 B1
• Filed: 09/13/2016
• Issued: 10/09/2018
• Est. Priority Date: 09/13/2016
• Status: Active Grant

• Current Assignee: Rockwell Collins, Inc. (Raytheon Technologies Corporation d/b/a RTX)
• Original Assignee: Rockwell Collins, Inc. (Raytheon Technologies Corporation d/b/a RTX)
• Inventors: Hardin, David S.
• Primary Examiner(s): CHEUNG, CALVIN K
• Application Number:
  US15/264,587
• Time in Patent Office: 756 Days
• CPC Class Codes: G05D 1/0088 characterized by the autonomous decision making process, e.g. artificial intelligence, predefined behaviours using knowledge based models G06N5/00
• CPC Class Codes: G06N 3/02 Neural networks
• CPC Class Codes: G06N 5/046 Forward inferencing; Production systems

Abstract

An autonomous vehicle system includes one or more output devices, one or more input sources, and a controller. In some embodiments, a verified inference engine is used by the controller to generate outputs for the output devices from inputs received from the input sources. The inference engine may be verified to be mathematically correct with an automated theorem proving tool. The automated theorem proving tool may verify that the inference engine meets the design requirements of standards such as DO-178C Level A and/or EAL-7. The controller is configured to validate the inputs received from the input sources, store the validated inputs in a fact base, generate outputs from the validated inputs, validate the one or more outputs, and provide the one or more validated outputs to the output devices.

Claims

1. An autonomous vehicle system, comprising:

one or more autonomous vehicle actuators configured to control movement of an autonomous vehicle;

one or more input sources of the autonomous vehicle; and

a controller coupled to a non-transitory storage medium and a processing circuit, the processing circuit configured to;

validate one or more rules generated by a production rule source by determining that the one or more rules generated by the production rule source are consistent;

store the one or more validated rules in a rule base;

validate one or more inputs from the one or more input sources by determining that the one or more inputs are reliable;

store the one or more validated inputs in a fact base;

determine one or more outputs by selecting one or more applicable rules in the rule base and firing the one or more applicable rules with information stored in the fact base as parameters for the applicable rules;

validate the one or more outputs by determining that the one or more outputs are inside a defined range; and

provide the one or more validated outputs to the one or more autonomous vehicle actuators.

2. The system of claim 1, wherein the processing circuit is further configured to execute verified code stored in the non-transitory storage medium, the verified code being verified by:

translating code stored on the non-transitory storage medium into a format for an automated theorem proving tool;

determining a mathematical correctness level for the code using the automated theorem proving tool; and

determining that the mathematical correctness level is above a threshold.

3. The system of claim 1, wherein the processing circuit is configured to determine that the one or more rules generated by the production rule source are consistent by using at least one of an automated theorem proving tool and a model checker.

4. The system of claim 1, wherein the processing circuit is configured to determine that the one or more inputs are reliable by performing at least one of:

determining that the inputs from the input sources are within an expected range;

determining that redundant inputs are within an acceptable offset from one another; and

using an artificial neural network to determine that input data is reliable.

5. The system of claim 1, wherein the input sources comprise at least one of:

a pitch sensor;

an altitude sensor;

a heading sensor;

a roll sensor;

a global positioning system;

a yaw sensor;

an accelerometer; and

a velocity sensor.

6. The system of claim 5, wherein the input sources further comprise at least one of:

a light detection and ranging (LIDAR) input source;

a stereo vision input source;

a radio detection and ranging (RADAR) input source;

an infrared vision input source;

an obstacle proximity input source;

a radio beacon or other direction-finding source; and

a sound navigation and ranging (SONAR) input source.

7. The system of claim 1, wherein the autonomous vehicle actuators comprise at least one of:

land vehicle actuators;

surface ship actuators;

underwater vehicle actuators;

spacecraft actuators; and

airborne vehicle actuators.

8. The system of claim 1, wherein the processing circuit is further configured to disable the one or more outputs and provide a manual output to the one or more autonomous vehicle actuators in response to a command to enable manual control of the one or more autonomous vehicle actuators.

9. The system of claim 1, wherein the processing circuit is configured to provide the one or more validated outputs to the one or more autonomous vehicle actuators by:

sending the one or more outputs to one of the one or more autonomous vehicle actuators in response to a determination that the one or more outputs is in a range of values;

setting the one or more outputs to an upper limit and sending the one or more outputs to the one of the one or more autonomous vehicle actuators in response to a determination that the one or more outputs is above the upper limit; and

setting the one or more outputs to a lower limit and sending the one or more outputs to the one of the one or more autonomous vehicle actuators in response to a determination that the one or more outputs is below the lower limit.

10. An autonomous controller, comprising:

one or more autonomous vehicle actuators configured to control movement of an autonomous vehicle;

one or more input sources of the autonomous vehicle; and

one or more processing circuits configured to;

validate one or more rules generated by a production rule source by determining that the one or more rules generated by the production rule source are consistent;

validate one or more inputs from the one or more input sources by determining that the one or more inputs contain reliable data;

determine one or more outputs by selecting one or more applicable rules in a rule base and firing the one or more rules with information stored in a fact base as parameters for the rules;

validate the one or more outputs by determining that the one or more outputs are inside a defined range; and

control the movement of the autonomous vehicle by providing the one or more validated outputs to the one or more autonomous vehicle actuators.

11. The controller of claim 10, wherein the one or more processing circuits are further configured to execute verified code stored on non-transitory storage medium, the verified code being verified by:

translating the code stored on the non-transitory storage medium into a format for an automated theorem proving tool;

determining a mathematical correctness level for the code using the automated theorem proving tool; and

determining that the mathematical correctness level is above a threshold.

12. The controller of claim 10, wherein the one or more processing circuits are configured to determine that the one or more rules generated by the production rule source are consistent by using at least one of an automated theorem proving tool and a model checker.

13. The controller of claim 10, wherein the one or more processing circuits are configured to determine that the one or more inputs contain reliable data by performing at least one of:

determining that the inputs from the input sources are within an expected range;

determining that redundant inputs are within an acceptable offset from one another; and

using an artificial neural network to determine that input data is reliable.

14. The controller of claim 10, wherein the one or more processing circuits are configured to validate the one or more inputs by performing at least one of:

selecting a midpoint of a plurality of redundant inputs received from the input sources and storing the midpoint in the fact base; and

performing a vote on the plurality of redundant inputs to determine a voted input and store the voted input in the fact base.

15. The controller of claim 10, wherein the one or more processing circuits are further configured to:

send the one or more outputs to an output device in response to a determination that the one or more outputs is in a range of values;

set the one or more outputs to an upper limit and send the one or more outputs to the output device in response to a determination that the one or more outputs is above the upper limit; and

set the one or more outputs to a lower limit and send the one or more outputs to the output device in response to a determination that the one or more outputs is below the lower limit.

16. The controller of claim 10, wherein the one or more processing circuits are configured to select one or more applicable rules in the rule base by performing at least one of a forward-chain search and a backward-chain search.

17. A method for autonomous decision making, the method comprising:

validating one or more rules generated by a production rule source by determining that the one or more rules generated by the production rule source are consistent;

validating one or more inputs from one or more input sources by determining that the one or more inputs contain reliable data;

determining one or more outputs by selecting one or more applicable rules in a rule base and firing the one or more rules with information stored in a fact base as parameters for the rules;

validating the one or more outputs by determining that the one or more outputs are not outside a defined range; and

controlling movement of an autonomous vehicle by providing the one or more validated outputs to one or more autonomous vehicle actuators of the autonomous vehicle.

18. The method of claim 17, wherein determining that one or more rules generated by the production rule source are consistent is done by using at least one of an automated theorem proving tool and a model checker.

19. The method of claim 17, wherein the method further comprises:

translating code stored on a non-transitory stored medium into a format for an automated theorem proving tool;

determining mathematical correctness for the code using the automated theorem proving tool; and

determining that the mathematical correctness is above a threshold.

20. The method of claim 17, wherein selecting one or more applicable rules in the rule base is done by performing at least one of a forward-chain search and a backward-chain search.