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, and 4-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 three Terminal Disclaimers filed on July 21, 2025, the Double Patenting rejections are withdrawn.
Applicant's arguments with respect to the 35 USC 101 rejections 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 prior art rejections have been considered, but 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, “method for verifying a software component of an automated driving function, wherein native program code of the software component to be verified is limited to a set of operations of a programming language used that are defined as permissible, the method comprising the following steps: translating the native program code into a model checker representation of the software component to be verified; and analyzing the model checker representation of the software component to be verified using a model checking method; wherein the native program code is converted into a finite automaton (FA), states and state transitions of which can be uniquely assigned to a code structure of the native program code, and the model checker representation is generated based on the finite automaton such that the code structure of the native program code is substantially retained when the native program code 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 “the programming language of the native program code … such as C++, Python, and Java.”2 Furthermore, it is commonly understood that finite state models are often represented as bubbles or blocks (states) and arrows (transitions), which may be easily drawn by hand. 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 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 that the claim limitations provide several technological improvements.4 However, the corresponding claim limitations that allegedly provide these benefits are part of the identified abstract idea (see above) and are not additional elements to be evaluated under Step 2 Prong 2 to determine whether they integrate the identified mental process into a practical application. Applicant’s argument is therefore unpersuasive.
Prior Art Arguments – Rejections
Applicant’s arguments 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 does not disclose “wherein the native program code is converted into a finite automaton (FA), wherein states and state transitions of the FA are at least one of: uniquely assigned to a code structure of the native program code and not uniquely assigned to the code structure of the native program code, and the model checker representation is generated based on the finite automaton such that the code structure of the native program code is at least partially retained upon the translating of the native program code into the model checker representation.”5 To support this argument, Applicant asserts that the “Patent Office improperly equates converting mechanism quoted above to extracting a finite state model from Java source code … The Patent Office assumes that the automatic extraction performed by Bandera would have been understood in the art as the claimed converting of native program code into an FA, but that assumption is belied by the denial in Corbett itself that translation (expressed as translation in the claim) and extraction are synonymous … Corbett explains that ‘our tool-set should go beyond simple translation and instead be structured like an optimizing compiler.’ … To be sure, Corbett discloses that ‘Bandera front-end translates Java to a high-level intermediate language called Jimple,’ but translation/conversion to Jimple is not the same as translation/conversion to an FA, as recited in the claim.”6 Examiner respectfully disagrees for several reasons. First, 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. Second, to the extent that Applicant argues that “translation/conversion to Jimple is not the same as translation/conversion to an FA,” 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 automaton,” 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’s argument is therefore unpersuasive.
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.”7 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.”8 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.”9 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. Applicant’s argument is therefore unpersuasive.
Furthermore, to the extent that Applicant also references the above arguments to support withdrawal of the 35 USC 103 rejections, this is not persuasive for the reasons set forth above.
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 non-transitory computer-readable medium and falls within the statutory category of articles of manufacture; claim 10 is directed to a computer-implemented system and falls within the statutory category of machines. Therefore, “Are the claims to a process, machine, manufacture or composition of matter?” Yes.
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, wherein native program code of the software component to be verified is limited to a set of operations of a programming language used that are defined as permissible, 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 the native program code is converted into a finite automaton (FA), wherein states and state transitions of the FA are at least one of: uniquely assigned to a code structure of the native program code and not uniquely assigned to the code structure of the native program code, and the model checker representation is generated based on the finite automaton such that the code structure of the native program code is at least partially retained upon the translating of the native program code into the model checker representation”, 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 non-transitory computer-readable medium on which is stored a computer program,” “A computer-implemented system … the system comprising: one or more processors and a memory that stores instructions that are executed by the one or more processors to:,” 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 claim 2, the limitations merely provide details for detecting, assigning, and embedding structures in code, which could also be performed in the human mind with no more than pencil and paper. Thus, the claim is directed to the judicial exception and does not have elements amounting to significantly more that the abstract idea itself. Therefore, claim 2 does not recite patent eligible subject matter under 35 U.S.C. §101.
With respect to claims to 3-7, the limitations provide additional details of the “intermediate representation” and “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 do not have elements amounting to significantly more that the abstract idea itself. Therefore, claims 3-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 optimizing code, which could also be performed in the human mind with no more than pencil and paper. Thus, the claim is directed to the judicial exception and does not have elements amounting to significantly more that the abstract idea itself. Therefore, claim 8 does not recite patent eligible subject matter under 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-3 and 8-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, wherein native program code of the software component to be verified is limited to a set of operations of a programming language used that are defined as permissible (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) [component to be verified is limited to a set of operations of a programming language used that are defined as permissible] 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 the native program code is converted into a finite automaton (FA), wherein states and state transitions of the FA are at least one of: uniquely assigned to a code structure of the native program code and not uniquely assigned to the code structure of the native program code, and the model checker representation is generated based on the finite automaton such that the code structure of the native program code is at least partially retained upon the translating of the native program code 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 [FA] 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 automaton such that the code structure of the native program code is at least partially retained upon the translating of the native program code 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; 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 automaton such that the code structure of the native program code is at least partially retained upon the translating of the native program code into the model checker representation] … BIR is a guarded command language for describing state transition systems.).
With respect to claim 9, Corbett discloses A non-transitory computer-readable medium on which is stored a computer program for verifying a software component of an automated driving function, wherein native program code of the software component to be verified is limited to a set of operations of a programming language used that are defined as permissible, the computer program, when executed by a computer, causing the computer to perform the following steps (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) [component to be verified is limited to a set of operations of a programming language used that are defined as permissible] to a non-trivial program.):
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 the native program code is converted into a finite automaton (FA), states and state transitions of the FA are least one of: uniquely assigned to a code structure of the native program code and not uniquely assigned to the code of structure of the native program code, and the model checker representation is generated based on the finite automaton such that the code structure of the native program code is at least partially retained upon the translating of the native program code 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 [FA] 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 automaton such that the code structure of the native program code is at least partially retained upon the translating of the native program code 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; 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 automaton such that the code structure of the native program code is at least partially retained upon the translating of the native program code 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 for verifying a software component of an automated driving function, wherein native program code of the software component to be verified is limited to a set of operations of a programming language used that are defined as permissible, the system comprising one or more processors and a memory that stores instructions that are executed by the one or more processors to (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) [component to be verified is limited to a set of operations of a programming language used that are defined as permissible] to a non-trivial program.):
translate 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 [translate 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.);
analyze 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 [analyze 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 the native program code is converted into a finite automaton (FA), wherein states and state transitions of the FA are at least one of: uniquely assigned to a code structure of the native program code and not uniquely assigned to the code structure of the native program code, and the model checker representation is generated based on the finite automaton such that the code structure of the native program code is at least partially retained upon the translating of the native program code 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 [FA] 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 automaton such that the code structure of the native program code is at least partially retained upon the translating of the native program code 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; 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 automaton such that the code structure of the native program code is at least partially retained upon the translating of the native program code 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, in at least one first step, structures are detected in the native program code, in that corresponding FA states and FA state transitions are assigned to the structures, and in that an intermediate representation of the native program code is generated which has a structure of the finite automaton (FA segments), in which remaining parts of the native program code are embedded (Fig. 1 and associated text, e.g., 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 [intermediate representation].… BIR is a guarded command language for describing state transition systems …. BIRC translates a subset of Jimple to BIR. Java locals and instance variables are mapped onto BIR state variables and record fields; p. 442, The Bandera front-end translates Java to a high-level intermediate language called Jimple; the Bandera back-end generates model-checker inputs from a low-level intermediate language of guarded commands called BIR (Bandera Intermediate Representation) [structures are detected in the native program code, in that corresponding FA states and FA state transitions are assigned to the structures, and in that an intermediate representation of the native program code is generated which has a structure of the finite automaton, in which remaining parts of the native program code are embedded]; see also Abstract, p. 440-442.).
With respect to claim 3, Corbett also discloses wherein, in at least one further step, at least one code segment of the intermediate representation is converted into FA segments (e.g., Fig. 1 and associated text, e.g., 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 [code segment of the intermediate representation is converted into FA segments].).
With respect to claim 8, Corbett also discloses wherein the native program code of the software component to be verified is optimized before being converted into a finite automaton in order to simplify a program structure of the native program code (e.g., Fig. 1 and associated text, e.g., p. 441, One of the primary goals of Bandera is to provide automated support for the model-construction and error trace interpretation techniques outlined in the previous section. Specifically, Bandera uses slicing to automate irrelevant component elimination, abstract interpretation to support data abstraction [wherein the native program code of the software component to be verified is optimized before being converted into a finite automaton in order to simplify the program structure of the native program code], and a model-generator that allows significant flexibility in setting bounds for various system components. Bandera also includes a collection of data structures for automatically mapping model-checker error traces back to the source level as well as facilities for graphical navigation of these traces; see also p. 442.).
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 4-6 are rejected under 35 U.S.C. 103 as being unpatentable over Corbett in view of Drumm et al. 20080300838 (hereinafter Drumm).
With respect to claim 4, Corbett also discloses wherein structures in a form of [“switch case”] instructions are detected and a separate FA state and at least one state transition between FA states are assigned to each [“case”] component of a detected [“switch case”] instruction (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 [FA] 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. 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; p. 442, The Bandera front-end translates Java to a high-level intermediate language called Jimple; the Bandera back-end generates model-checker inputs from a low-level intermediate language of guarded commands called BIR (Bandera Intermediate Representation); 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 and produces BIR..… BIR is a guarded command language for describing state transition systems.).
Corbett does not appear to disclose “switch case” and “case.” However, this is taught in analogous art, Drumm (e.g., Figs. 1-7 and associated text, e.g., [0048], intermediate states and paths in the state diagram may be identified when there is branching in the process (for example… switch; [0087], The sequence activity is the easier to represent in TLA+ from both, as its child activities will translate into a sequence of state transitions and states; [0098], consider flow control activities. Flow control activities are these which lead to branching and introduction of new paths in the state diagram. These include … switch/case; [0100], The switch/case activity may be replaced by its child activities including the cases and otherwise clauses (in the case of if structure, this structure will be replaced by if, else and the set of else if clauses); see also [0051] and [008-97].).
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 Drumm such that switch statements are verified by a model checker because software requiring verification often includes switch statements because they provide a clean way to implement multiple conditions.
With respect to claim 5, Corbett also discloses wherein, based on at least one [“switch case”] instruction of the native program code, an intermediate representation having a structure of the finite automaton is generated, in which remaining parts of the native program code are embedded (Fig. 1 and associated text, e.g., 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 [intermediate representation].… BIR is a guarded command language for describing state transition systems …. BIRC translates a subset of Jimple to BIR. Java locals and instance variables are mapped onto BIR state variables and record fields; p. 442, The Bandera front-end translates Java to a high-level intermediate language called Jimple; the Bandera back-end generates model-checker inputs from a low-level intermediate language of guarded commands called BIR (Bandera Intermediate Representation) [an intermediate representation having a structure of the finite automaton is generated, in which remaining parts of the native program code are embedded]; see also Abstract, p. 440-442.) and Drumm discloses “switch case” (e.g., Figs. 1-7 and associated text, e.g., [0048], intermediate states and paths in the state diagram may be identified when there is branching in the process (for example… switch; [0087], The sequence activity is the easier to represent in TLA+ from both, as its child activities will translate into a sequence of state transitions and states; [0098], consider flow control activities. Flow control activities are these which lead to branching and introduction of new paths in the state diagram. These include … switch/case; [0100], The switch/case activity may be replaced by its child activities including the cases and otherwise clauses (in the case of if structure, this structure will be replaced by if, else and the set of else if clauses); see also [0051] and [008-97].).
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 Drumm for the same reason set forth above.
With respect to claim 6, Corbett also discloses wherein at least one [“case”] component includes the native program code, which is retained during the conversion into an intermediate representation (Fig. 1 and associated text, e.g., 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 [intermediate representation].… BIR is a guarded command language for describing state transition systems …. BIRC translates a subset of Jimple to BIR. Java locals and instance variables are mapped onto BIR state variables and record fields; p. 442, The Bandera front-end translates Java to a high-level intermediate language called Jimple; the Bandera back-end generates model-checker inputs from a low-level intermediate language of guarded commands called BIR (Bandera Intermediate Representation); see also Abstract, p. 440-442.) and Drumm discloses “case” (e.g., Figs. 1-7 and associated text, e.g., [0048], intermediate states and paths in the state diagram may be identified when there is branching in the process (for example… switch; [0087], The sequence activity is the easier to represent in TLA+ from both, as its child activities will translate into a sequence of state transitions and states; [0098], consider flow control activities. Flow control activities are these which lead to branching and introduction of new paths in the state diagram. These include … switch/case; [0100], The switch/case activity may be replaced by its child activities including the cases and otherwise clauses (in the case of if structure, this structure will be replaced by if, else and the set of else if clauses); see also [0051] and [008-97].).
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 Drumm for the same reason set forth above.
Claims 7 is rejected under 35 U.S.C. 103 as being unpatentable over Corbett in view of Lucco et al. 20080071802 (hereinafter Lucco).
With respect to claim 7, Corbett does not appear to disclose wherein the entire native program code of the software component to be verified comprises an entire native program code, and wherein the entire native program code is assigned to a single FA state. However, this is taught in analogous art, Lucco (e.g., [0141], An FSM with only one state is called a combinatorial FSM and uses only input actions.).
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 combinatorial FSM invention of Lucco because it is “useful in cases where a number of FSM are required to work together, and where it is convenient to consider a purely combinatorial part as a form of FSM to suit the design tools,” as suggested by Lucco (see [0141]).
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 system, call 800-786-9199 (IN USA OR CANADA) or 571-272-1000.
/STEPHEN D BERMAN/Examiner, Art Unit 2192
/S. SOUGH/SPE, AU 2192
1 Although claims 1, 9, and 10 have been amended, the substance of these limitations has not changed as they have been amended consistent with the 35 USC 112(b) interpretation provided by Examiner in the Non-Final Office Action.
2 See Applicant’s specification at p. 5 at lines 11-14
3 See Remarks at pp. 8-9.
4 See Remarks at pp. 11-12.
5 See Remarks at p. 13.
6 See Remarks at p. 13.
7 See Remarks at p. 14.
8 See Remarks at pp. 13-14.
9 See p. 442, right column, 1st full paragraph; see also p. 441, right column, last full paragraph, “Bandera also includes a collection of data structures for automatically mapping model-checker error traces back to the source level ….”