DETAILED ACTION
Remarks
The present application, filed on or after March 16, 2013, is being examined under the first inventor to file provisions of the AIA .
This Office Action is filed in response to Applicant’s arguments and amendment dated July 21, 2025. Claims 1, 2, 5, 6, and 8-10 are currently amended and claims 1-10 remain pending in the application and have been fully considered by Examiner.
The informalities present in the claims have been corrected and the objections are withdrawn.
In view of Applicant’s amendments, the 35 USC 112(b) rejections are withdrawn.
In view of the two Terminal Disclaimers filed on July 21, 2025, the Double Patenting rejections are withdrawn.
Applicant's arguments with respect to the rejections of claims 1-10 under 35 USC 101 as being directed to an abstract idea without significantly more have been considered, but are not persuasive, as detailed below in the 35 USC 101 Argument - Rejections section.
Applicant’s arguments with respect to the rejection of claim 9 under 35 USC 101 as being entirely software and/or data per se is not persuasive, as detailed below in the 35 USC 101 Argument - Rejections section.
In view of Applicant’s amendment to claim 10, the rejection under 35 USC 101 as being entirely software and/or data per se is withdrawn.
Applicant's arguments with respect to the prior art rejections have been considered, but are not persuasive, as detailed below in the Prior Art Argument - Rejections section. To the extent that Applicant has amended these claims, additional clarification has been provided below where necessary to further point out that the prior art of record cited in the previous Office Action discloses the claimed limitations as currently amended.
Examiner Notes
Examiner cites particular columns, paragraphs, figures and line numbers in the references as applied to the claims below for the convenience of the applicant. Although the specified citations are representative of the teachings in the art and are applied to the specific limitations within the individual claim, other passages and figures may apply as well. It is respectfully requested that, in preparing responses, the applicant fully consider the references in their entirety as potentially teaching all or part of the claimed invention, as well as the context of the passage as taught by the prior art or disclosed by the examiner.
35 USC 101 Arguments – Rejections
Applicant’s arguments with respect to the 35 USC 101 rejections have been fully considered, but are not persuasive, as follows:
With respect to claims 1, 9, and 10, Applicant first argues with respect to Step 2 Prong 1 that the claims do not recite a mental process and further that Examiner’s statement to the contrary is merely “conclusory.” Examiner respectfully disagrees. As explained in the original rejection, under the broadest reasonable interpretation, “wherein in the translating, the native program code is converted into a finite-state machine, wherein states and state transitions of the finite state machine are one-to-one assignable to a code structure of the native program code, and the model checker representation is generated based on the finite-state machine, such that the code structure of the native program code is at least partially retained when it is translated into the model checker representation,”1 includes a human translating human-readable source code into a finite-state model and verifying the finite-state model. To further clarify, Applicant’s specification states “native program code - this may also be existing program code. For example: in the programming language C++, Python, or similar.”2 Thus, Examiner has provided a concrete example that could be performed in the mind with no more than pen and paper, which is in direct contrast to the PTAB case cited by Applicant in which the Examiner merely stated “nothing in the claimed invention suggest that the identified abstract idea cannot be performed mentally (or using pen and paper).”3 Furthermore, Applicant even points out at p. 11 of the Remarks that Applicant’s specification states “‘[t]o permit efficient model checking of existing program code (e.g., in C++, Python, etc.), the program code needs to be translated into a format that the model checker is able to use. This step is usually carried out manually by a developer.’” (Emphasis added). For these reasons, the recited elements are a mental process that could be carried out in the human mind with no more than pen and paper. Applicant’s argument is therefore unpersuasive.
Applicant further argues with respect to Prong 2A Prong 2, “the specification establish that the claimed translation mechanism, through its ability to implement a fully automated, programming language--agnostic model checking, represents a technological advance in the field of software verification” and “the Patent Office does not evaluate Prong Two in light of the specification, as it ought to have.”4 Examiner respectfully disagrees, noting that while claims are interpreted in light of the specification, limitations shall not be imported from the specification. Significantly, Applicant has not claimed a “fully automated” translation mechanism and instead merely claims “translating.” Furthermore, as noted above, this is not an additional element to be evaluated under Step 2 Prong 2 to determine whether it integrates the identified mental process into a practical application, but rather it is part of the identified mental process itself for the reasons set forth above, including Applicant express recognition at p. 11 of the Remarks that such translating is “usually carried out manually by a developer.” Applicant’s argument is therefore unpersuasive.
With respect to claim 10, Applicant also argues that the claim has been amended to recite “a processing unit”5 and thus is not software per se. However, the claim as currently amended, merely recites “A software component of an automated driving function, which has been verified by a processing unit configured to perform a method comprising …” and thus the claim is directed to a “software component” that does not actually comprise the “processing unit.” Therefore, under the broadest reasonable interpretation, claim 9 is entirely software and/or data per se, which does not fall within one of the statutory categories identified in 35 U.S.C. 101. Applicant’s argument is therefore unpersuasive.
Prior Art Arguments – Rejections
Applicant’s arguments with respect to the prior art rejections have been fully considered by Examiner, but they are moot and/or not persuasive, as follows:
With respect to claims 1, 9, and 10, Applicant primarily argues that “Corbett fails to disclose ‘wherein in the translating, the native program code is converted into a finite-state machine’ because “the Patent Office improperly equates translating native program code into an FSM as recited in the claims to extracting a finite state model from Java source code.”6 To support this argument, Applicant asserts that “Corbett explains that ‘our tool-set should go beyond simple translation and instead be structured like an optimizing compiler’ (p. 439) because the ‘translation approach often results in larger models, partly because of the mismatch between the semantics of the two languages, and partly because the translation does not consider the property being verified, thus the model cannot be customized for the property.’”7 Examiner respectfully disagrees with Applicant’s argument for several reasons. First, the claims do not recite “translating native program code into an FSM” (emphasis added) as argued by Applicant8. Rather, claim 1 recites “the native program code is converted into a finite-state machine” (emphasis added), with similar limitations recited in claims 9 and 10. Second, while the claims recite the native program code is converted into a finite-state machine, Examiner nonetheless notes that Corbett’s statement that “our tool-set should go beyond simple translation” (emphasis added) simply means that the process does more than “simple translation,” rather than suggesting that it is not translation at all, as argued by Applicant. Third, to the extent that Applicant argues that “translation to Jimple is not the same as translation to an FSM,”9 Examiner has not asserted that the Jimple code corresponds to the claimed FSM. Lastly, Corbett discloses “the native program code is converted into a finite-state machine,” as claimed, because the Bandera tool of Corbett takes a Java code representation and generates corresponding finite-state model code (e.g., Fig. 1 and associated text, Abstract and pp. 440-444).
Applicant additionally states “since the rejection earlier maps the native program code to the Java source code discussed in Corbett, to be consistent with this earlier mapping, the mapping here ought to disclose that ‘the code structure of the [Java source code] is at least partially retained when it is translated into the model checker representation.” Examiner agrees. However, Examiner disagrees with Applicant’s following argument that Corbett does not “disclose any such retention of the Java source code structure when it is translated into the model checker representation.”10 As a threshold matter, Examiner first notes that the claim only requires that the code structure be “at least partially retained when it is translated into the model checker representation,” which means that retention of any amount of code structure reads on the limitation. In view of this, Examiner directs Applicant’s attention to the portion of Corbett that states, with emphasis added, “Given a node in a program’s Jimple representation, JJJC can return the corresponding node in the Java abstract syntax tree (AST) for the program (and vice versa). These bi-directional mappings, together with similar mappings for our other intermediate language BIR, facilitate the mapping of model-checker counter-example traces back to source code traces.”11 It would be impossible to map the model-checker counter-example traces back to the source code traces unless the code structure of the Java source code is at least partially retained when it is translated into the model checker representation.
For the above reasons, Applicant’s arguments are not persuasive.
Claim Interpretation
The following is a quotation of 35 U.S.C. 112(f):
(f) Element in Claim for a Combination. – An element in a claim for a combination may be expressed as a means or step for performing a specified function without the recital of structure, material, or acts in support thereof, and such claim shall be construed to cover the corresponding structure, material, or acts described in the specification and equivalents thereof.
The following is a quotation of pre-AIA 35 U.S.C. 112, sixth paragraph:
An element in a claim for a combination may be expressed as a means or step for performing a specified function without the recital of structure, material, or acts in support thereof, and such claim shall be construed to cover the corresponding structure, material, or acts described in the specification and equivalents thereof.
The claims in this application are given their broadest reasonable interpretation using the plain meaning of the claim language in light of the specification as it would be understood by one of ordinary skill in the art. The broadest reasonable interpretation of a claim element (also commonly referred to as a claim limitation) is limited by the description in the specification when 35 U.S.C. 112(f) or pre-AIA 35 U.S.C. 112, sixth paragraph, is invoked.
As explained in MPEP § 2181, subsection I, claim limitations that meet the following three-prong test will be interpreted under 35 U.S.C. 112(f) or pre-AIA 35 U.S.C. 112, sixth paragraph:
(A) the claim limitation uses the term “means” or “step” or a term used as a substitute for “means” that is a generic placeholder (also called a nonce term or a non-structural term having no specific structural meaning) for performing the claimed function;
(B) the term “means” or “step” or the generic placeholder is modified by functional language, typically, but not always linked by the transition word “for” (e.g., “means for”) or another linking word or phrase, such as “configured to” or “so that”; and
(C) the term “means” or “step” or the generic placeholder is not modified by sufficient structure, material, or acts for performing the claimed function.
Use of the word “means” (or “step”) in a claim with functional language creates a rebuttable presumption that the claim limitation is to be treated in accordance with 35 U.S.C. 112(f) or pre-AIA 35 U.S.C. 112, sixth paragraph. The presumption that the claim limitation is interpreted under 35 U.S.C. 112(f) or pre-AIA 35 U.S.C. 112, sixth paragraph, is rebutted when the claim limitation recites sufficient structure, material, or acts to entirely perform the recited function.
Absence of the word “means” (or “step”) in a claim creates a rebuttable presumption that the claim limitation is not to be treated in accordance with 35 U.S.C. 112(f) or pre-AIA 35 U.S.C. 112, sixth paragraph. The presumption that the claim limitation is not interpreted under 35 U.S.C. 112(f) or pre-AIA 35 U.S.C. 112, sixth paragraph, is rebutted when the claim limitation recites function without reciting sufficient structure, material or acts to entirely perform the recited function.
Claim limitations in this application that use the word “means” (or “step”) are being interpreted under 35 U.S.C. 112(f) or pre-AIA 35 U.S.C. 112, sixth paragraph, except as otherwise indicated in an Office action. Conversely, claim limitations in this application that do not use the word “means” (or “step”) are not being interpreted under 35 U.S.C. 112(f) or pre-AIA 35 U.S.C. 112, sixth paragraph, except as otherwise indicated in an Office action.
This application includes one or more claim limitations that do not use the word “means,” but are nonetheless being interpreted under 35 U.S.C. 112(f) or pre-AIA 35 U.S.C. 112, sixth paragraph, because the claim limitation(s) uses a generic placeholder that is coupled with functional language without reciting sufficient structure to perform the recited function and the generic placeholder is not preceded by a structural modifier. Such claim limitation(s) is/are: “processing unit configured to …” in claims 9 and 10.
Because this/these claim limitation(s) is/are being interpreted under 35 U.S.C. 112(f) or pre-AIA 35 U.S.C. 112, sixth paragraph, it/they is/are being interpreted to cover the corresponding structure described in the specification as performing the claimed function, and equivalents thereof.
If applicant does not intend to have this/these limitation(s) interpreted under 35 U.S.C. 112(f) or pre-AIA 35 U.S.C. 112, sixth paragraph, applicant may: (1) amend the claim limitation(s) to avoid it/them being interpreted under 35 U.S.C. 112(f) or pre-AIA 35 U.S.C. 112, sixth paragraph (e.g., by reciting sufficient structure to perform the claimed function); or (2) present a sufficient showing that the claim limitation(s) recite(s) sufficient structure to perform the claimed function so as to avoid it/them being interpreted under 35 U.S.C. 112(f) or pre-AIA 35 U.S.C. 112, sixth paragraph.
Claim Objections
Claims 1-10 objected to because of the following informalities:
With respect to claims 1, 9, and 10, each recites “the finite state machine,”12 which appears to be a typographical error that should recite “the finite-state machine.” Claims 2-8 inherit the deficiency of claim 1.
Appropriate correction is required.
Claim Rejections - 35 USC § 101
35 U.S.C. 101 reads as follows:
Whoever invents or discovers any new and useful process, machine, manufacture, or composition of matter, or any new and useful improvement thereof, may obtain a patent therefor, subject to the conditions and requirements of this title.
Claims 1-10 are rejected under 35 U.S.C. 101 because the claimed invention recites a judicial exception, is directed to that judicial exception, an abstract idea, as it has not been integrated into practical application and the claims further do not recite significantly more than the judicial exception. Examiner has evaluated the claims under the framework provided in the 2019 Patent Eligibility Guidance published in the Federal Register 01/07/2019 and has provided such analysis below.
Step 1: Claims 1-8 are directed to computer-implemented methods and fall within the statutory category of processes; Claim 9 is directed to a software component of an automated driving function that could be software per se and thus does not fall within one of the four statutory categories; claim 10 is directed to a system that falls within statutory category of machines. Therefore, “Are the claims to a process, machine, manufacture or composition of matter?” Yes as to claims 1-8 and 10 and No as to claim 9 (see section 11 below).
In order to evaluate the Step 2A inquiry “Is the claim directed to a law of nature, a natural phenomenon or an abstract idea?” we must determine, at Step 2A Prong 1, whether the claim recites a law of nature, a natural phenomenon or an abstract idea and further whether the claim recites additional elements that integrate the judicial exception into a practical application.
Step 2A Prong 1:
Claims 1, 9 and 10: The limitations of “method for verifying a software component of an automated driving function, native program code of the software component to be verified being limited to a set of authorized operations of a programming language used, the method comprising the following steps: translating the native program code into a model checker representation of the software component to be verified; analyzing the model checker representation of the software component to be verified using a model checking method; and wherein in the translating, the native program code is converted into a finite-state machine, wherein states and state transitions of the finite state machine are one-to-one assignable to a code structure of the native program code, and the model checker representation is generated based on the finite-state machine, such that the code structure of the native program code is at least partially retained when it is translated into the model checker representation”13, as claimed, is a process that, but for the recitation of generic computing components and under its broadest reasonable interpretation, covers performance of the limitation in the mind with no more than pen and paper. For example, a human could translate human-readable source code into a finite-state model and verify the finite-state model.
Therefore, Yes, claims 1, 9, and 10 recite limitations that fall within the “Mental Processes” grouping of abstract ideas.
The claims have been identified as reciting judicial exceptions, Step 2A Prong 2 will evaluate whether the claims are directed to the judicial exception.
Step 2A Prong 2:
Claims 1, 9, and 10: The judicial exception is not integrated into a practical application. In particular, the claims recite the following additional elements: “computer-implemented,” “A software component of an automated driving function, which has been verified by a processing unit configured to perform a method comprising,” “A computer-implemented system for developing an automated driving function, comprising: a processing unit configured to verify at least one software component,” which are merely recitations of generic computing components and functions merely applying the abstract idea using the generic computing components (see MPEP §2106.05(f)), which does not integrate a judicial exception into a practical application.
Therefore, “Do the claims recite additional elements that integrate the judicial exception into a practical application?” No, these additional elements do not integrate the abstract idea into a practical application and they do not impose any meaningful limits on practicing the abstract idea. The claim is therefore directed to an abstract idea.
After having evaluating the inquires set forth in Steps 2A Prong 1 and 2, it has been concluded that claims 1, 9, and 10 recite a judicial exception and are directed to the judicial exception as the judicial exception has not been integrated into a practical application.
Step 2B:
Claims 1, 9, and 10: The claims do not include additional elements, alone or in combination, that are sufficient to amount to significantly more than the judicial exception. As discussed above with respect to integration of the abstract idea into a practical application, the additional elements amount to no more than generic computing components applying the abstract idea.
Therefore, “Do the claims recite additional elements that amount to significantly more than the judicial exception?” No, these additional elements, alone or in combination, do not amount to significantly more than the judicial exception.
Having concluded analysis within the provided framework, claims 1, 9, and 10 do not recite patent eligible subject matter under 35 U.S.C. §101.
With respect to claims 2-7, the limitations merely provide details for the native program code and converting the native program code, which could also be performed in the human mind with no more than pencil and paper. Thus, the claims are directed to the judicial exception and does not have elements amounting to significantly more that the abstract idea itself. Therefore, claims 2-6 do not recite patent eligible subject matter under 35 U.S.C. §101.
With respect to claim 8, the limitations merely provide details for software component, which could also be performed in the human mind with no more than pencil and paper. Thus, the claims are directed to the judicial exception and does not have elements amounting to significantly more that the abstract idea itself. Therefore, claims 2-6 do not recite patent eligible subject matter under 35 U.S.C. §101.
Claim 9 is rejected under 35 U.S.C. 101 because the claimed invention is directed to non-statutory subject matter. The claims do not fall within at least one of the four categories of patent eligible subject matter
With respect to claim 9, lines 1-2 recite it “A software component of an automated driving function, which has been verified by a processing unit configured to perform a method comprising: ….” Although “processing unit” has been interpreted under 35 USC 112(f) (see above), claim 9 is directed to a “software component” and as the claimed is currently written, “a processing unit” is not actually part of the “software component.” Thus, under the broadest reasonable interpretation, the subject matter of claim 9 is entirely software and/or data per se, which does not fall within one of the statutory categories identified in 35 U.S.C. 101.
Claim Rejections - 35 USC § 102
The following is a quotation of the appropriate paragraphs of 35 U.S.C. 102 that form the basis for the rejections under this section made in this Office action:
A person shall be entitled to a patent unless –
(a)(1) the claimed invention was patented, described in a printed publication, or in public use, on sale or otherwise available to the public before the effective filing date of the claimed invention.
(a)(2) the claimed invention was described in a patent issued under section 151, or in an application for patent published or deemed published under section 122(b), in which the patent or application, as the case may be, names another inventor and was effectively filed before the effective filing date of the claimed invention.
Claims 1-5 and 9-10 are rejected under 35 U.S.C. 102(a)(1) as being anticipated by Corbett et al. “Bandera: Extracting Finite-state Models from Java Source Code” (hereinafter Corbett).
With respect to claim 1, Corbett discloses A computer-implemented method for verifying a software component of an automated driving function, native program code of the software component to be verified being limited to a set of authorized operations of a programming language used (e.g., Fig. 1 and associated text, e.g., Abstract, In this paper, we describe an integrated collection of program analysis and transformation components, called Bandera, that enables the automatic extraction of safe, compact finite-state models from program source code. Bandera takes as input Java source code and generates a program model in the input language of one of several existing verification tools; p. 440, We also describe the application of the current implementation of Bandera (which handles a reasonably large subset of Java) [limited to a set of authorized operations of a programming language] to a non-trivial program.), the method comprising the following steps:
translating the native program code into a model checker representation of the software component to be verified (e.g., Fig. 1 and associated text, e.g., Abstract, Bandera takes as input Java source code and generates a program model in the input language of one of several existing verification tools [translating the native program code into a model checker representation of the software component to be verified]; p. 444, producing verifier-specific representations for targeted verifiers….The Spin translator accepts a BIR representation and produces a Promela model of the system, suitable for input to the Spin model checker.);
analyzing the model checker representation of the software component to be verified using a model checking method (e.g., Figs. 1 and 4 and associated text, e.g., p. 441, a model checking tool algorithmically determines whether all paths through the finite-state transition system satisfy the property [analyzing the model checker representation of the software component to be verified using a model checking method]; p. 446, Table 4 shows data for checking several of the properties described above using Bandera.); and
wherein in the translating, the native program code is converted into a finite-state machine, wherein states and state transitions of the finite state machine are one-to-one assignable to a code structure of the native program code, and the model checker representation is generated based on the finite-state machine, such that the code structure of the native program code is at least partially retained when it is translated into the model checker representation (e.g., Fig. 1 and associated text, e.g., Abstract, we describe an integrated collection of program analysis and transformation components, called Bandera, that enables the automatic extraction of safe, compact finite-state models [finite-state machine] from program source code [native code]. Bandera takes as input Java source code [native code] and generates a program model in the input language of one of several existing verification tools [model checker representation is generated based on the finite-state machine, such that the code structure of the native program code is at least partially retained when it is translated into the model checker representation]; p. 440, The back end of Bandera generates BIR: a low-level intermediate language based on guarded commands that abstracts common model checker input languages. The back end also contains a translator for each model checker supported; p. 441, First, the system (in our case, a Java program) is modeled as a finite-state transition system. Each state represents an abstraction of the program's state and each transition represents the execution of one or more statements transforming this state. … a model checking tool algorithmically determines whether all paths through the finite-state transition system satisfy the property [states and state transitions of the finite state machine are one-to-one assignable to the code structure of the native program code]; p. 444, The Bandera back end is like a code generator, taking the sliced and abstracted program and producing verifier-specific representations for targeted verifiers. The back-end components communicate through BIR, the Bandera Intermediate Representation, an intermediary between compiler-based representations and verifier-based representations. As shown in Figure 1, the back end has one fixed component called BIRC (Bandera Intermediate Representation Constructor) that accepts a restricted form of Jimple and produces BIR. For each supported verifier, there is also a translator component that accepts the program represented in BIR and generates input for that verifier [model checker representation is generated based on the finite-state machine, such that the code structure of the native program code is at least partially retained when it is translated into the model checker representation].… BIR is a guarded command language for describing state transition systems.).
With respect to claim 9, Corbett discloses A software component of an automated driving function, which has been verified by a processing unit configured to perform a method comprising: (e.g., Figs. 1-2 and 4 and associated text, e.g., p. 439, we describe an integrated collection of program analysis and transformation components, called Bandera, that enables the automatic extraction of safe, compact finite-state models from program source code; p. 441, a model checking tool algorithmically determines whether all paths through the finite-state transition system satisfy the property [verified].):
translating the native program code into a model checker representation of the software component to be verified (e.g., Fig. 1 and associated text, e.g., Abstract, Bandera takes as input Java source code and generates a program model in the input language of one of several existing verification tools [translating the native program code into a model checker representation of the software component to be verified]; p. 444, producing verifier-specific representations for targeted verifiers….The Spin translator accepts a BIR representation and produces a Promela model of the system, suitable for input to the Spin model checker.);
analyzing the model checker representation of the software component to be verified using a model checking method (e.g., Figs. 1 and 4 and associated text, e.g., p. 441, a model checking tool algorithmically determines whether all paths through the finite-state transition system satisfy the property [analyzing the model checker representation of the software component to be verified using a model checking method]; p. 446, Table 4 shows data for checking several of the properties described above using Bandera.); and
wherein in the translating, the native program code is converted into a finite-state machine, wherein states and state transitions of the finite state machine are one-to-one assignable to a code structure of the native program code, and the model checker representation is generated based on the finite-state machine, such that the code structure of the native program code is at least partially retained when it is translated into the model checker representation (e.g., Figs. 1 and associated text, e.g., Abstract, we describe an integrated collection of program analysis and transformation components, called Bandera, that enables the automatic extraction of safe, compact finite-state models [finite-state machine] from program source code [native code]. Bandera takes as input Java source code [native code] and generates a program model in the input language of one of several existing verification tools [model checker representation is generated based on the finite-state machine, such that the code structure of the native program code is at least partially retained when it is translated into the model checker representation]; p. 440, The back end of Bandera generates BIR: a low-level intermediate language based on guarded commands that abstracts common model checker input languages. The back end also contains a translator for each model checker supported; p. 441, First, the system (in our case, a Java program) is modeled as a finite-state transition system. Each state represents an abstraction of the program's state and each transition represents the execution of one or more statements transforming this state. … a model checking tool algorithmically determines whether all paths through the finite-state transition system satisfy the property [states and state transitions of the finite state machine are one-to-one assignable to a code structure of the native program code]; p. 444, The Bandera back end is like a code generator, taking the sliced and abstracted program and producing verifier-specific representations for targeted verifiers. The back-end components communicate through BIR, the Bandera Intermediate Representation, an intermediary between compiler-based representations and verifier-based representations. As shown in Figure 1, the back end has one fixed component called BIRC (Bandera Intermediate Representation Constructor) that accepts a restricted form of Jimple and produces BIR. For each supported verifier, there is also a translator component that accepts the program represented in BIR and generates input for that verifier [model checker representation is generated based on the finite-state machine, such that the code structure of the native program code is at least partially retained when it is translated into the model checker representation].… BIR is a guarded command language for describing state transition systems.).
With respect to claim 10, Corbett discloses A computer-implemented system (e.g., Fig. 1.) for developing an automated driving function, comprising:
a processing unit configured to verify at least one software component which has been verified (e.g., Figs. 1-2 and 4 and associated text, e.g., p. 439, we describe an integrated collection of program analysis and transformation components, called Bandera, that enables the automatic extraction of safe, compact finite-state models from program source code; p. 441, a model checking tool algorithmically determines whether all paths through the finite-state transition system satisfy the property [verified].) by:
translating the native program code into a model checker representation of the software component to be verified (e.g., Fig. 1 and associated text, e.g., Abstract, Bandera takes as input Java source code and generates a program model in the input language of one of several existing verification tools [translating the native program code into a model checker representation of the software component to be verified]; p. 444, producing verifier-specific representations for targeted verifiers….The Spin translator accepts a BIR representation and produces a Promela model of the system, suitable for input to the Spin model checker.), and
analyzing the model checker representation of the software component to be verified using a model checking method (e.g., Figs. 1 and 4 and associated text, e.g., p. 441, a model checking tool algorithmically determines whether all paths through the finite-state transition system satisfy the property [analyzing the model checker representation of the software component to be verified using a model checking method]; p. 446, Table 4 shows data for checking several of the properties described above using Bandera.),
wherein in the translating, the native program code is converted into a finite-state machine, wherein states and state transitions of the finite state machine are one-to-one assignable to a code structure of the native program code, and the model checker representation is generated based on the finite-state machine, such that the code structure of the native program code is at least partially retained when it is translated into the model checker representation (e.g., Fig. 1 and associated text, e.g., Abstract, we describe an integrated collection of program analysis and transformation components, called Bandera, that enables the automatic extraction of safe, compact finite-state models [finite-state machine] from program source code [native code]. Bandera takes as input Java source code [native code] and generates a program model in the input language of one of several existing verification tools [model checker representation is generated based on the finite-state machine, such that the code structure of the native program code is at least partially retained when it is translated into the model checker representation]; p. 440, The back end of Bandera generates BIR: a low-level intermediate language based on guarded commands that abstracts common model checker input languages. The back end also contains a translator for each model checker supported; p. 441, First, the system (in our case, a Java program) is modeled as a finite-state transition system. Each state represents an abstraction of the program's state and each transition represents the execution of one or more statements transforming this state. … a model checking tool algorithmically determines whether all paths through the finite-state transition system satisfy the property [states and state transitions of the finite state machine are one-to-one assignable to a code structure of the native program code]; p. 444, The Bandera back end is like a code generator, taking the sliced and abstracted program and producing verifier-specific representations for targeted verifiers. The back-end components communicate through BIR, the Bandera Intermediate Representation, an intermediary between compiler-based representations and verifier-based representations. As shown in Figure 1, the back end has one fixed component called BIRC (Bandera Intermediate Representation Constructor) that accepts a restricted form of Jimple and produces BIR. For each supported verifier, there is also a translator component that accepts the program represented in BIR and generates input for that verifier [model checker representation is generated based on the finite-state machine, such that the code structure of the native program code is at least partially retained when it is translated into the model checker representation].… BIR is a guarded command language for describing state transition systems.).
With respect to claim 2, Corbett also discloses wherein, when the native program code is converted, an intermediate representation is generated which has a structure of the finite-state machine, wherein at least one code part of the native program code is embedded in the intermediate representation (e.g., Fig. 1 and associated text, e.g., p. 442, The Bandera front-end translates Java to a high-level intermediate language called Jimple [when the native program code is converted, an intermediate representation is generated]; the Bandera back-end generates model-checker inputs from a low-level intermediate language of guarded commands called BIR (Bandera Intermediate Representation) [finite-state machine]…. Downstream components such as the slicer and specializer that transform the Jimple representation must be careful to maintain the mappings [intermediate representation is generated which has a structure of the finite-state machine]; p. 444, As shown in Figure 1, the back end has one fixed component called BIRC (Bandera Intermediate Representation Constructor) that accepts a restricted form of Jimple [intermediate representation] and produces BIR…. BIRC translates a subset of Jimple to BIR. Java locals and instance variables are mapped onto BIR state variables and record fields [an intermediate representation is generated which has a structure of the finite-state machine, in which at least one code part of the native program code is embedded in the intermediate representation].).
With respect to claim 3, Corbett also discloses wherein, when the native program code is converted, the at least one code part of the intermediate representation is converted into parts of the finite-state machine (e.g., Fig. 1 and associated text, e.g., p. 442, The Bandera front-end translates Java to a high-level intermediate language called Jimple [intermediate representation]; the Bandera back-end generates model-checker inputs from a low-level intermediate language of guarded commands called BIR (Bandera Intermediate Representation) [finite-state machine]…. Downstream components such as the slicer and specializer that transform the Jimple representation must be careful to maintain the mappings [intermediate representation is generated which has a structure of the finite-state machine]; p. 444, As shown in Figure 1, the back end has one fixed component called BIRC (Bandera Intermediate Representation Constructor) that accepts a restricted form of Jimple [intermediate representation] and produces BIR…. BIRC translates a subset of Jimple to BIR. Java locals and instance variables are mapped onto BIR state variables and record fields [wherein, when the native program code is converted, the at least one code part of the intermediate representation is converted into parts of the finite-state machine].).
With respect to claim 4, Corbett also discloses wherein, when the native program code is converted, at least one operation of the native program code is converted into at least one substate machine including at least two states (e.g., Figs. 1 and 3 along with associated text, e.g., p. 443, When a token flows into the test of a conditional expression [operation] in the abstract program, the specialization engine inserts a flag that informs the downstream model construction components to implement the test as a non-deterministic choice between the true and false branches [operation of the native program code is converted into at least one substate machine including at least two states].).
With respect to claim 5, Corbett also discloses wherein at least one decision operation and/or at least one sequence operation of the native program code is converted into the at least one substate machine including the at least two states (e.g., Figs. 1 and 3 along with associated text, e.g., p. 443, When a token flows into the test of a conditional expression [decision operation] in the abstract program, the specialization engine inserts a flag that informs the downstream model construction components to implement the test as a non-deterministic choice between the true and false branches [converted into at least one substate machine include at least two states].).
Claim Rejections - 35 USC § 103
The following is a quotation of 35 U.S.C. 103 which forms the basis for all obviousness rejections set forth in this Office action:
A patent for a claimed invention may not be obtained, notwithstanding that the claimed invention is not identically disclosed as set forth in section 102 of this title, if the differences between the claimed invention and the prior art are such that the claimed invention as a whole would have been obvious before the effective filing date of the claimed invention to a person having ordinary skill in the art to which the claimed invention pertains. Patentability shall not be negated by the manner in which the invention was made.
Claims 6-7 are rejected under 35 U.S.C. 103 as being unpatentable over Corbett in view of Ivancic et al. 20050166167 (hereinafter Ivancic).
With respect to claim 6, Corbet does not appear to disclose wherein, when the native program code is converted, at least one program counter is assigned to at least one part of the native program code, and the at least one program counter is retained on the translation into the model checker representation. However, this is taught in analogous art, Ivancic (e.g., Fig. 1 and associated text, e.g., [0030], the modeling 120 of the software considers two kinds of logic: control logic 121 and data logic 122. The control logic 121 describes the flow of control that can be represented by a control flow graph of the basic blocks. The data logic 122 describes the assignments of variables given finite ranges. Assuming the software program consists of N basic blocks, each basic block can be represented by a label …. A program counter variable … can be introduced to monitor progress in the graph of the basic blocks [when the native program code is converted, at least one program counter is assigned to at least one part of the native program code]. The control logic defines the transition relation for this program counter variable given the basic block graph and the conditions guarding some of the transitions between the basic blocks. The transitions, thus, model transfer of control within the basic block graph representing the software program. The program counter variable can be used to track progress of allowed executions of the software program during the model checking phase [the at least one program counter is retained on the translation into the model checker representation]. Each basic block of the source code can be replaced by a tight bit-blasted version of the data variables as well as the control logic given the aforementioned program counter variable and the basic block labels; see also [0006] and [0021].).
It would have been obvious to one of ordinary skill in the art before the effective filing date of the claimed invention to combine the invention of Corbett with the invention of Ivancic because it “provides for faster and more efficient operation,” as suggested by Ivancic (see [0010]).
With respect to claim 7, Ivancic further teaches wherein the at least one program counter is assigned only to selected operations of the native program code including statements for setting variables (Id., particularly, [0030], The data logic 122 describes the assignments of variables given finite ranges…. Each basic block of the source code can be replaced by a tight bit-blasted version of the data variables as well as the control logic given the aforementioned program counter variable and the basic block labels; [0006], The state of the system can be defined to contain a location indicating the current active basic block and the evaluation of all variables in scope. Thus, a label can be generated for each basic block and a program counter variable introduced to track progress of allowed executions of the software program during the model checking.).
It would have been obvious to one of ordinary skill in the art before the effective filing date of the claimed invention to combine the invention of Corbett with the invention of Ivancic for the same reason set forth above.
Claim 8 is rejected under 35 U.S.C. 103 as being unpatentable over Corbett in view of Ratiu et al. 20210342250 (hereinafter Ratiu).
With respect to claim 8, Corbett does not appear to disclose wherein the software component of the automated driving function forms an Adaptive Cruise Control (ACC) function for an automated vehicle. However, this is taught in analogous art, Ratiu (e.g., Figs. 1-4 and associated text, e.g., [0019], a method and apparatus are provided to verify a software system in an appropriate state based on a plurality of input values. Typically, the software system includes software components that are responsible for performing one or more functions associated with hardware system. The hardware system may be a vehicle with an adaptive cruise controller.).
It would have been obvious to one of ordinary skill in the art before the effective filing date of the claimed invention to combine the invention of Corbett with the invention of Ratiu because reactive software systems require verification, as suggested by Ratiu (see [0003-4]).
Conclusion
The prior art made of record and not relied upon is considered pertinent to applicant's disclosure. Specifically, Iosif et al. “Translating Java for Multiple Model Checkers: The Bandera Back-End” teaches details of the Bandera Intermediate Representation (BIR), which has been designed to support the translation of Java programs to a variety of model checkers.
Applicant's amendment necessitated the new ground(s) of rejection presented in this Office action. Accordingly, THIS ACTION IS MADE FINAL. See MPEP § 706.07(a). Applicant is reminded of the extension of time policy as set forth in 37 CFR 1.136(a).
A shortened statutory period for reply to this final action is set to expire THREE MONTHS from the mailing date of this action. In the event a first reply is filed within TWO MONTHS of the mailing date of this final action and the advisory action is not mailed until after the end of the THREE-MONTH shortened statutory period, then the shortened statutory period will expire on the date the advisory action is mailed, and any nonprovisional extension fee (37 CFR 1.17(a)) pursuant to 37 CFR 1.136(a) will be calculated from the mailing date of the advisory action. In no event, however, will the statutory period for reply expire later than SIX MONTHS from the mailing date of this final action.
Any inquiry concerning this communication or earlier communications from the examiner should be directed to STEPHEN DAVID BERMAN whose telephone number is (571)272-7206. The examiner can normally be reached on M-F, 9-6 Eastern.
If attempts to reach the examiner by telephone are unsuccessful, the examiner’s supervisor, Hyung S. Sough can be reached on 571-272-6799. The fax phone number for the organization where this application or proceeding is assigned is 571-273-8300.
Information regarding the status of an application may be obtained from the Patent Application Information Retrieval (PAIR) system. Status information for published applications may be obtained from either Private PAIR or Public PAIR. Status information for unpublished applications is available through Private PAIR only. For more information about the PAIR system, see http://pair-direct.uspto.gov. Should you have questions on access to the Private PAIR system, contact the Electronic Business Center (EBC) at 866-217-9197 (toll-free). If you would like assistance from a USPTO Customer Service Representative or access to the automated information