SYSTEMS, METHODS, AND MEDIA FOR FAULT LOCALIZATION IN DECLARATIVE SPECIFICATION LANGUAGES

In accordance with some embodiments, systems, methods, and media for fault localization in declarative specification languages are provided. In some embodiments, a method comprises: receiving a model in a declarative specification language; querying an automated analysis of the declarative specification language for a counterexample, wherein the counterexample is an instance of the model that does not satisfy a property; using a partial max satisfiability solver to find an instance that satisfies the property; determining one or more differences in an expression from the model between the counterexample and the satisfying instance; analyzing the differences between the counterexample and the satisfying instance; determining a suspicion score for the expression in the model; and causing the suspicion score to be presented.

STATEMENT REGARDING FEDERALLY SPONSORED RESEARCH

BACKGROUND

Fault localization techniques help developers to identify code locations that might cause bugs in a program. Most existing fault localization techniques are designed for imperative programs (e.g. C and Java) and rely on analyzing correct and incorrect executions of the program to identify suspicious statements.

Existing fault localization techniques designed for declarative specification languages rely on unit tests, mutation testing, and statistical debugging techniques. However, such techniques are slow and inaccurate. Therefore, existing fault localization techniques for declarative specification languages limit confidence in the modeled results, as well as feasibility for analyzing large complex models.

Accordingly, new systems, methods, and media for fault localization in declarative specification languages are desirable.

SUMMARY

In accordance with some embodiments of the present disclosure, systems, methods, and media for fault localization in declarative specification languages are provided.

In accordance with some embodiments of the present disclosure, a method for fault localization is provided, the method comprising: receiving a model in a declarative specification language; querying an automated analysis of the declarative specification language for a counterexample, wherein the counterexample is an instance of the model that does not satisfy a property; using a partial max satisfiability solver to find an instance that satisfies the property; determining one or more differences in an expression from the model between the counterexample and the satisfying instance; analyzing the one or more differences between the counterexample and the satisfying instance to compute a suspicion score for the expression in the model; and causing the suspicion score to be presented.

In some embodiments, the declarative specification language is Alloy.

In some embodiments, the expression comprises one or more relations and one or more atoms.

In some embodiments, the method further comprises: determining, for each of a plurality of expressions in the model, a suspicion score of a respective plurality of suspicion scores; and causing the plurality of suspicion scores to be presented.

In some embodiments, the model models a positioning of one or more surgical robots.

In some embodiments, the model models permissions on one or more electronic devices.

In accordance with some embodiments of the present disclosure, a system for fault localization is provided, the system comprising: at least one processor that is programmed to: receive a model in a declarative specification language; query an automated analysis of the declarative specification language for a counterexample, wherein the counterexample is an instance of the model that does not satisfy a property; use a partial max satisfiability solver to find an instance that satisfies the property; determine one or more differences in an expression from the model between the counterexample and the satisfying instance; analyze the one or more differences between the counterexample and the satisfying instance; determine a suspicion score for the expression in the model; and cause the suspicion score to be presented.

In accordance with some embodiments of the present disclosure, a non-transitory computer readable medium containing computer executable instructions that, when executed by a processor, cause the processor to perform a method for fault localization is provided, the method comprising: receiving a model in a declarative specification language; querying an automated analysis of the declarative specification language for a counterexample, wherein the counterexample is an instance of the model that does not satisfy a property; using a partial max satisfiability solver to find an instance that satisfies the property; determining one or more differences in an expression from the model between the counterexample and the satisfying instance; analyzing the one or more differences between the counterexample and the satisfying instance; determining a suspicion score for the expression in the model; and causing the suspicion score to be presented.

DETAILED DESCRIPTION

In accordance with various embodiments, mechanisms (which can, for example, include systems, methods, and media) for fault localization in declarative specification languages are provided.

Declarative specification languages and the corresponding formally precise analysis engines have long been utilized to solve various software engineering problems. The Alloy specification language relies on first-order relational logic, and has been used in a wide range of applications, such as program verification, test case generation, software design, network security, security analysis of emerging platforms (e.g., such as IoT and Android), and design tradeoff analysis.

Similar to developing programs in an imperative language, such as C or Java, developers can make subtle mistakes when using a declarative specification language, such as Alloy, in modeling system specifications. Avoiding such mistakes can be especially difficult when developing programs that capture complex systems with non-trivial behaviors, rendering debugging thereof even more arduous. These challenges call for debugging assistant mechanisms, such as fault localization techniques, that support declarative specification languages.

Conventional fault localization techniques for declarative specification languages rely on unit testing to locate suspicious expressions. For such techniques, it is unclear how many test cases are needed for the unit tests, and further how detailed the tests must be. Therefore, existing fault localization techniques are relatively slow and inaccurate.

In some embodiments, mechanisms described herein can be used to localize faults more quickly and/or more accurately than conventional techniques. For example, in some embodiments, mechanisms described herein can query an underlying automated analysis of a declarative specification language for a counterexample that does not satisfy a property of a model written in a declarative specification language. As another example, mechanisms described herein can use a partial max satisfiability solver to find an instance that satisfies the property and is relatively close (e.g., as close as possible) to the counterexample. In such examples, mechanisms described herein can then compare differences in expressions from the model between the counterexample and the satisfying instance to compute suspicion scores for the expressions in the model. As disclosed further herein, mechanisms (which can, for example, include systems, methods, and media) for fault localization in declarative specification languages according to the embodiments of the present disclosure are faster and more accurate than conventional techniques, which is of particular importance as models in declarative specification languages continue to grow larger and increasingly complex for a variety of applications.

FIG.1shows an example100of a system for fault localization in declarative specification languages in accordance with some embodiments of the present disclosure. As shown inFIG.1, a computing device110can receive model data from a model data source102. In some embodiments, computing device110can execute at least a portion of a fault localization system104to locate buggy expressions.

In some embodiments, computing device110can execute at least a portion of fault localization system104to compare satisfying and unsatisfying instances of a model to compute suspicion scores for expressions in the model with relatively high accuracy using mechanisms described herein (e.g., compared to time consuming or unreliable conventional techniques that rely on unit testing, mutation testing, or static analysis for effects of testing).

Additionally or alternatively, in some embodiments, computing device110can communicate data received from model data source102to a server120over a communication network108, which can execute at least a portion of fault localization system104. In such embodiments, server120can return information to computing device110(and/or any other suitable computing device) indicative of an output of a fault localization process. In some embodiments, fault localization system104can execute one or more portions of process1000described below in connection withFIG.15.

In some embodiments, computing device110and/or server120can be any suitable computing device or combination of devices, such as a desktop computer, a laptop computer, a smartphone, a tablet computer, a wearable computer, a server computer, a virtual machine being executed by a physical computing device, etc.

In some embodiments, model data source102can be any suitable source of model data (e.g., data modeled using a declarative specification language, or data modeled using a first-order logic tool that relies on sets of atoms and relations for expressions) and/or other data that can be used to locate buggy expressions in models. In a more particular example, model data source102can include memory storing modeling data (e.g., local memory of computing device110, local memory of server120, cloud storage, portable memory connected to computing device110, portable memory connected to server120, etc.). In another more particular example, model data source102can include an application configured to generate model data (e.g., a fault localization application being executed by computing device110, server120, and/or any other suitable computing device).

In some embodiments, model data source102can be local to computing device110. For example, model data source102can be incorporated with computing device110(e.g., computing device110can include memory that stores model data, and/or can execute a program that generates model data). As another example, model data source102can be connected to computing device110by a cable, a direct wireless link, etc. Additionally or alternatively, in some embodiments, model data source102can be located locally and/or remotely from computing device110, and can communicate model data to computing device110(and/or server120) via a communication network (e.g., communication network108).

In some embodiments, communication network108can be any suitable communication network or combination of communication networks. For example, communication network108can include a Wi-Fi network (which can include one or more wireless routers, one or more switches, etc.), a peer-to-peer network (e.g., a Bluetooth network), a cellular network (e.g., a 3G network, a 4G network, a 5G network, etc., complying with any suitable standard, such as CDMA, GSM, LTE, LTE Advanced, NR, etc.), a wired network, etc. In some embodiments, communication network108can be a local area network (LAN), a wide area network (WAN), a public network (e.g., the Internet), a private or semi-private network (e.g., a corporate or university intranet), any other suitable type of network, or any suitable combination of networks. Communications links shown inFIG.1can each be any suitable communications link or combination of communications links, such as wired links, fiber optic links, Wi-Fi links, Bluetooth links, cellular links, etc.

FIG.2shows an example200of hardware that can be used to implement computing device110and/or server120in accordance with some embodiments of the present disclosure. As shown inFIG.2, in some embodiments, computing device110can include a processor202, a display204, one or more inputs206, one or more communication systems208, and/or memory210. In some embodiments, processor202can be any suitable hardware processor or combination of processors, such as a central processing unit (CPU), a graphics processing unit (GPU), an application specific integrated circuit (ASIC), a field-programmable gate array (FPGA), etc. In some embodiments, display204can include any suitable display devices, such as a computer monitor, a touchscreen, a television, etc. In some embodiments, inputs206can include any suitable input devices and/or sensors that can be used to receive user input, such as a keyboard, a mouse, a touchscreen, a microphone, etc.

In some embodiments, memory210can include any suitable storage device or devices that can be used to store instructions, values, etc., that can be used, for example, by processor202to perform a computer vision task, to present content using display204, to communicate with server120via communications system(s)208, etc. Memory210can include any suitable volatile memory, non-volatile memory, storage, or any suitable combination thereof. For example, memory210can include random access memory (RAM), read-only memory (ROM), electronically-erasable programmable read-only memory (EEPROM), one or more flash drives, one or more hard disks, one or more solid state drives, one or more optical drives, etc. In some embodiments, memory210can have encoded thereon a computer program for controlling operation of computing device110. For example, in such embodiments, processor202can execute at least a portion of the computer program to transmit model data to server120, receive model data from server120, analyze differences between a counterexample and a satisfying instance for a property of an expression, and/or present results related to suspicion scores for a location of a buggy expression. As another example, processor202can execute at least a portion of the computer program to implement fault localization system104. As yet another example, processor202can execute at least a portion of process1000described below in connection withFIG.15.

In some embodiments, server120can include a processor212, a display214, one or more inputs216, one or more communications systems218, and/or memory220. In some embodiments, processor212can be any suitable hardware processor or combination of processors, such as a CPU, a GPU, an ASIC, an FPGA, etc. In some embodiments, display214can include any suitable display devices, such as a computer monitor, a touchscreen, a television, etc. In some embodiments, inputs216can include any suitable input devices and/or sensors that can be used to receive user input, such as a keyboard, a mouse, a touchscreen, a microphone, etc.

In some embodiments, memory220can include any suitable storage device or devices that can be used to store instructions, values, etc., that can be used, for example, by processor212to present content using display214, to communicate with one or more computing devices110, etc. Memory220can include any suitable volatile memory, non-volatile memory, storage, or any suitable combination thereof. For example, memory220can include RAM, ROM, EEPROM, one or more flash drives, one or more hard disks, one or more solid state drives, one or more optical drives, etc. In some embodiments, memory220can have encoded thereon a server program for controlling operation of server120. For example, in such embodiments, processor212can receive model data from computing device110, transmit model data to computing device110, analyze differences between a counterexample and a satisfying instance for a property of an expression, transmit results related to suspicion scores for a location of a buggy expression to computing device110, and/or cause results related to the simulation to be presented (e.g., by computing device110). As another example, processor212can execute at least a portion of the computer program to implement fault localization system104. As yet another example, processor212can execute at least a portion of process1000described below in connection withFIG.15.

FIG.3shows an example Alloy specification300of a buggy finite state machine (FSM) model. Alloy specification300defines two type signatures, State and FSM, along with associated fields (lines1-5). Specification300contains three fact paragraphs, expressing constraints, detailed as follows. (1) If a start (or a stop) state exists, there is only one of them (fact OneStartAndStop); (2) the start state is not a subset of the stop state; no transition terminates at the start state; and no transition leaves a stop state (fact ValidStartAndStop); (3) every state is reachable from the start state, and the stop state is reachable from any state (fact Reachability). Each assertion specifies a property that is expected to hold in all instances of the model. For example the assertion NoStopTransition checks that a stop state behaves as a sink. An automated analyzer of a declarative specification language, such as Alloy Analyzer, may disprove the assertion NoStopTransition by producing a counterexample (e.g., as shown inFIG.5, panel (a)), in which a stop state labeled State3 transitions to State1. Thus, the FSM model does not behave as expected in at least one situation, which can be an example of a “bug” in the model causing an assertion violation.

Analysis of the model ofFIG.3and the generated counterexample (shown inFIG.5, panel (a)) generated in accordance with some embodiments of the present disclosure can reveal that a fault or bug is in the expression on line19. Instead of stating that a stop state does not have any transition to any state, the expression states that any state not having a transition to anywhere is a stop state—a subtle logical error that is difficult for a human or inaccurate fault localization system to identify. There are two potential resolutions to the subtle logical error: (i) reverse the expression (e.g., to: s in FSM. stop=>s.transition=none), or (ii) replace the implication operator (=>) to logical equivalence (<=>), which strengthens the intended requirement. Thus, mechanisms described herein can be used to identify buggy expressions that may be otherwise missed, and can be used to automatically identify such expressions, such that buggy expressions can be more easily resolved.

FIG.4shows results obtained from the example model inFIG.3using mechanisms described herein. The results shown inFIG.4were generated using mechanisms described herein implemented in accordance with some embodiments based on an analysis of the model shown inFIG.3. The results were generated relatively quickly (e.g., within one second). As shown inFIG.4, the results include four suspicious expressions identified in the model shown inFIG.3, with the expression on line 19 ranked first (e.g., as the most suspicious). Moreover, the results indicate that the operator => is likely the issue in the expression. Such a level of granularity can significantly help a developer understand and fix a problem with a model, such as the example model inFIG.3. For example, as described below in connection withFIG.12, implementations of mechanisms described herein can consistently rank an expression that includes at least one bug within the top 5 suspicious expressions in less than a duration of one second.

FIG.5shows a counterexample and a corresponding satisfying instance in accordance with some embodiments of the present disclosure. In some embodiments, a fault localization system implemented in accordance with some embodiments of the present disclosure can be used to analyze differences between instances of an input model that do not satisfy an assertion (sometimes referred to herein as counterexamples) and instances that do satisfy the assertion to find suspicious expressions in the input model. With regard to the model inFIG.3, the fault localization system can check the assertion NoStopTransition in the model using an Alloy Analyzer, which can return the counterexample shown in panel (a) ofFIG.5. Next, the fault localization system can generate a satisfyinginstance (sometimes referred to herein as a sat instance) that is as minimal and similar to the counterexample as possible. Differences between the counterexample and the satisfying instance can be used to effectively localize one or more faults in the model.

To obtain a satisfying instance similar to the counterexample, a fault localization system implemented in accordance with some embodiments of the present disclosure can transform an input model into a logical formula representing hard constraints and the information from the counterexample into a formula representing soft constraints. For example, such a fault localization system can convert an instance finding problem into a partial-max SAT (PMAX) problem, and then use a known solver (such as, for example, a Pardinus solver) to find a solution that satisfies all of the hard constraints, and as many of the soft constraints as possible. The result can be an instance of the model that is similar to the counterexample, but satisfies the assertion. In a more particular example,FIG.5, panel (b), shows a satisfying instance produced by a Pardinus solver (e.g., made available from the High-Assurance Software Laboratory (HASLab)), considering the counterexample shown inFIG.5, panel (a). The satisfying instance inFIG.5, panel (b), is similar to the counterexample inFIG.5, panel (a), except for the edge from State3 to State1. In some embodiments, a fault localization system implemented in accordance with some embodiments of the present disclosure can analyze differences between counterexamples and satisfying instances—e.g., inFIG.5, the transition from State3 to State1, which only appears in the counterexample, but not the satisfying instance—to identify relations that are likely to be causing an issue.

FIG.6shows a text representation of the counterexample inFIG.5, panel (a). The transition relation involves the tuple State3−>State1 and the stop relation involves State3. Thus, in some embodiments, a fault localization system can identify that two relations of transition and stop may cause differences between two models. While the illustrated example ofFIG.5shows a single counterexample and one corresponding satisfying instance, some embodiments of the present disclosure can also support analyzing multiple pairs of counterexamples and satisfying instances (e.g., in tandem).

In some embodiments, a fault localization system implemented in accordance with some embodiments of the present disclosure can slice an input model to contain only expressions affecting both relations “transition” and “FSM. stop.” This can result in two expressions: (1) all s: State|FSM.stop in s.*transition (line25inFIG.3), and (2) all s: State|s.transition=none=>s in FSM. stop (line19inFIG.3). At this point, the fault localization system can stop and return these two expressions, one of which is the buggy expression on line19inFIG.3. While some conventional fault localization techniques (e.g., Tarantula, and Ochiai) purport to produce this level of “statement” granularity, mechanisms described herein can be used to achieve a finer-grained granularity level (e.g., by also considering the Boolean and relational subexpressions, as described herein).

Referring again toFIG.3, the expressions on lines25and19have four Boolean nodes or expressions: (a) FSM. stop in s.*transition, (b) s.transition=none, (c) s in FSM.stop, and (d) s.transition=none=>s in FSM. stop. Mechanisms described herein can be used to instantiate each of the four Boolean nodes with State1 and State3, the values that differentiate the counterexample and satisfying instance. For example, node (a) can be instantiated as FSM.stop in S1.*transition and FSM.stop in S3.*transition. Further, mechanisms described herein can be used to evaluate such instantiations using the counterexamples and satisfying instance, and can be used to assign a higher suspicion score to those with inconsistent evaluation results. For example, the instantiations FSM.stop in S1.*transition and FSM.stop in S3.*transition of node (a) evaluate to True in both the counterexample and satisfying instance, so node (a) is given a score of 0 (i.e., no changes). Node (b) is assigned a score of 1 because State3.transition=none evaluates to False in the counterexample, but to True in the satisfying instance (i.e. there is 1 change), and State1.transition=none evaluates to False in both the counterexample and the satisfying instance (i.e. there is no change). Overall, with the example model shown inFIG.3, mechanisms described herein may obtains the scores 0, 1, 0, 1 for nodes (a), (b), (c), (d), respectively. Thus, mechanisms described herein can be used to determine that nodes (b) s.transition=none and (d) s.transition=none=>s in FSM.stop are the two most suspicious Boolean subexpressions within the expression on line19ofFIG.3. Again, this level of granularity in analyzing Boolean and relational subexpressions can provide more accurate and/or more detailed results than some conventional fault localization techniques.

Still referring toFIGS.3-6, while expression (d) contains an error, it receives the same score as expression (a), which does not contain an error. To achieve more accurate results, mechanisms described herein can be used to further analyze relations between the expressions. Referring to the example model ofFIG.3, mechanisms described herein can be used to instantiate the expressions with State1 and State3, assess them in the context of the counterexample and satisfying instance, and assign scores based on evaluations. For example, node (d) s.transition=none=>s in FSM.stop includes 3 relations: (1) s.transition, (2) s, and (3) FSM.stop. Instantiating these relations with State3 and evaluating them using the counterexample can be performed as follows: (1) becomes {State1}, (2) {State3}, and (3) {State3}. Thus, for the counterexample, (d) involves both State1 and State3, and mechanisms described herein can give (d) a score of 1. Next, mechanisms described herein can be used to evaluate the instantiations using the satisfying instance as follows: (1) becomes {}, (2) {State3}, and (3) {State3}. In this example, (d) does not include State1 and therefore has a score of 0. In such an example, mechanisms described herein can assign (d) an average score of 0.5 (for the instantiations of State3). Performing a similar computation for the instantiation of State1 obtains a score of 2/3 for (d) as the evaluation for the counterexample and satisfying instance involves both State1 and State3 (differentiated values) and State2 (regular value). Thus, (d) has a score of 0.58 (i.e. the average of 0.5 and 2/3). Overall, for the example model inFIG.3, mechanisms described herein can obtain the scores 0.5, 0.25, 0.5, 0.58 for (a), (b), (c), and (d), respectively. In this analysis, node (d) is ranked higher than node (a), as desired.

In some embodiments, mechanisms described herein can be used to compute a suspicion score of a node as a sum of the Boolean and relational scores of the node, as described above. For example, the node (d) s.transition=none=>s in FSM. stop in the expression on line19ofFIG.3has the highest suspicion score of 1.58 (seeFIG.4).FIG.4shows suspicion scores of the expressions in a ranked list that can be generated and presented using mechanisms described herein. Further, in some embodiments, mechanisms described herein can be used to analyze (non-atomic) nodes containing (Boolean) connectors and can report connectors that connect sub-nodes with different scores. For example, a fault localization system implemented in accordance with some embodiments of the present disclosure can suggest that the operator =>in line19ofFIG.3is likely responsible for the error in node (d) because the two subexpressions s.transition=none, and s in FSM. stop have different suspicion scores (e.g., as shown inFIG.4). In the example shown inFIGS.3and4, the assertion violation is entirely due to the => operator (a potential fix would be strengthening the model ofFIG.3to <=>, or switching the two subexpressions).

FIG.7shows a schematic example700of a system for fault localization in declarative specification languages in accordance with some embodiments of the present disclosure, which takes as an input an Alloy model. The Alloy model has a violated assertion and system700can return a ranked list of suspicious expressions that contribute to the violated assertion. In some embodiments, system700can use an Alloy Analyzer to find counterexamples showing the violation of the assertion. Additionally, in some embodiments, system700can use a PMAX-SAT solver to find satisfying instances that are relatively close (e.g., as close as possible) to the counterexamples. In some embodiments, system700can analyze differences between the counterexamples and satisfying instances to find expressions in the Alloy model that likely cause the errors. Additionally, in some embodiments, system700can compute and return a ranked list of suspicious expressions.

In the example ofFIG.7, an alloy specification or model can include various components, such as: (i) Type signatures (sig) that define essential data types, and fields that capture relationships among such data types, (ii) facts, predicates (pred), and assertions (assert) (e.g., formulae defining constraints over data types), and/or (iii) run and check commands to invoke an Alloy Analyzer. The “check” command can be used to find counterexamples that violate some asserted property, and “run” can be used to find satisfying model instances (sat instances). For example, for a model M and a property p, a counterexample can be an instance of M that satisfies MΛ¬p, and a satisfying instance can be one that satisfies M Λ p. In a particular example, the example specification shown inFIG.3defines two signatures (FSM, State), three fields (start, stop, transition), three facts (OneStartStop, ValidStart, ValidStop), and one assertion (NoStopTransition).

In some embodiments, analysis of specifications written in Alloy using mechanisms described herein can be entirely automated, yet bounded up to user-specified scopes on the size of type signatures. For example, to check that p is satisfied by all instances of M (e.g., indicating that p is valid) up to a certain scope, a developer can encode p as an assertion and use the “check” command to validate the assertion (e.g., showing that no counterexample exists within the specified scope, where a counterexample is an instance I such that IMΛ¬p). To check that p is satisfied by some instances of M, a developer can encode p as a predicate and use the “run” command to analyze the predicate, (e.g., searching for a sat instance I such that IMΛp). Referring again to the example inFIG.3, the “check” command can be used to examine the NoStopTransition assertion, and can return a counterexample inFIG.5, panel (a).

Internally, declarative specification languages, such as Alloy can convert tasks of searching for instances into Boolean formulae and can use a SAT solver to check the satisfiability of the formulae. Each value of each relation can be translated to a distinct variable in the Boolean formula. For example, given a scope of 5 in the FSM model inFIG.3, the relation State includes 5 values and can be translated to 5 distinct variables in the Boolean formula, and the transition can be translated to 25 values representing 25 values of combinations of ∥State∥×∥State∥. An instance is an assignment for all variables that makes a formula True. For example, the counterexample inFIG.3, panel (a), is an assignment where all variables corresponding to values inFIG.2are assigned True and all other variables are assigned False. A declarative specification language, such as Alloy, can translates a result from the SAT solver (e.g., an assignment that makes a Boolean formula True, back to an instance of M).

FIG.8shows an example algorithm that can be used to analyze differences between pairs of instances in accordance with some embodiments of the present disclosure. The example algorithm ofFIG.8can take as input an Alloy model M and a property p that is not satisfied by M (as an assertion violation), and the example algorithm ofFIG.8can return a ranked list of expressions that likely contribute to the assertion violation. In some embodiments, an Alloy Analyzer and a PMAX-SAT solver, such as Pardinus, can be used to generate pairs of counterexamples and closely similar satisfying instances. In some embodiments, the example algorithm ofFIG.8can analyze the differences between the counterexample and satisfying instances to locate an error. If no satisfying instance can be generated, mechanisms described herein can be used to inspect the unsatisfying core returned by the Alloy Analyzer to locate an error.

In some embodiments of the present disclosure, a fault localization system (e.g., fault localization system104) can obtain differences between counterexamples and relevant satisfying instances to determine why M does not satisfy p. The differences can lead to the cause of an error. For example, an Alloy Analyzer can be used to generate a satisfying instance directly (e.g., by checking a predicate consisting of p). However, such an instance generated by Alloy is often predominantly different from the counterexample, and thus may not help identify the main difference. For example, the counterexample, shown inFIG.5, panel (a), that violates the assertion NoStopTransition is quite different from the two Alloy-generated satisfying instances shown inFIG.9, which shows two example Alloy-generated satisfying instances. To generate a satisfying instance closely similar to the counterexample, the problem can be reduced to a PMAX-SAT (partial maximum satisfiability) problem.

In some embodiments, the fault localization system can compare generated counterexamples and satisfying instances to obtain differences between the counterexamples and satisfying instances, which can involve atoms, tuples, and relations. For example, the fault localization system can obtain tuples and associated atoms that are different between the counterexamples and satisfying instance (e.g., inFIG.5, the tuple State3−>State1, which has the atoms State1 and State3, is in the counterexample but not in the satisfying instance). As another example, the fault localization system can obtain relations with different tuples between the counterexample and satisfying instance (e.g., the transition relation involves the tuple State3->State1 in the counterexample, but not in the satisfying instance). As yet another example, the fault localization system can obtain relations that can be inferred from the tuples and atoms derived in the previous steps (e.g., the relation FSM.stop involves tuples having the State3 atom). In such examples, for the pair of counterexamples and satisfying instance inFIG.5, the fault localization system can obtain the suspicious relations “transitions” and “stop” and the atoms “State1,” “State3.” In some embodiments, the fault localization system can perform such comparisons for all pairs of satisfying instances and counterexamples and uses the common results.

After obtaining differences in relations and atoms between counterexamples and satisfying instances, the fault localization system can analyze the differences to obtain a ranked list of expressions based on the suspicion level associated with each expression. Higher suspicion scores can be assigned to expressions for which the evaluation(s) depends on the differences (and lower scores can be assigned to expressions for which the evaluation(s) that do not depend on the differences).

FIG.10shows an example algorithm that can be used to analyze differences between pairs of instances in accordance with some embodiments of the present disclosure. The example algorithm ofFIG.10can take as inputs a model “M,” differences “diffs,” and pairs of counterexamples and satisfying instances “pairs” to output a ranked list of suspicious expressions in M. The example algorithm ofFIG.10can be used to identify expressions in M that involve relations in diffs. These expressions can be related to the difference between counterexamples and satisfying instances. For example, in the model inFIG.3, two expressions are identified: all s: State|FSM.stop in s.*transition on line25ofFIG.3, and all s: State|s.transition=none=>s in FSM.stop on line19ofFIG.3, as they involve the relations transition and stop in diffs. The example algorithm ofFIG.10can then recursively compute a suspicion score for each collected expression e, represented as an abstract syntax (AST) tree. If e is a leaf (e.g., a relational expression), the example algorithm instantiates e with atoms from diffs. The example algorithm can then be used to evaluate the instantiated expression for each pair of counterexamples and satisfying instance. If the evaluated result for an instantiated expression contains all atoms involved in diffs, the algorithm can compute the score as the size of diffs divided by the size of evaluated results; otherwise, the score can be 0. For a pair, the score can be the average score of counterexamples and satisfying instance. The score of e can be the average among all pairs. For example, a higher suspicion score can be assigned to a relational subexpression for which an evaluation involves many atoms in diffs. If e is not a leaf node, e's score can be the sum of Boolean and relational scores. If e is a Boolean expression (e.g., an expression that returns True or False), e is instantiated with atoms from diffs and is evaluated on each counterexample and satisfying instance pair. If e has different results between the counterexample and the satisfying instance (e.g., one is True and the other is False), e's score can be increased by 1. Thus, a higher Boolean score can be assigned to expressions for which an evaluation does not match between pairs of the counterexamples and satisfying instances. Then e's relational score can be calculated as the sum of e's children. The final score assigned to each expression can be the sum of the e's Boolean scores and the relational scores of e's children. In some embodiments, all of the expressions ranked by suspicion scores can be returned.

Considering the expression s.transition=none inFIG.3. For the counterexample and satisfying instance pair inFIG.5, diffs contain two atoms State1 and State3. The algorithm ofFIG.10can instantiate the expression under analysis with the atoms mentioned above (e.g., State1 and State3) into two concrete expressions: (1) State1.transition=none and (2) State3.transition=none. The concrete expression (1) can evaluate to False in both the counterexample and satisfying instance, while the concrete expression (2) can evaluate to True in the counterexample and False in the satisfying instance. Thus, the Boolean score for the expression under analysis can be 1 as the aggregation of the values obtained for the concrete expressions (1) and (2). A fault localization system implemented in accordance with some embodiments of the present disclosure can then compute a relational score for the expression under analysis as the sum of the relational scores for its children: s.transition and none, both of which are leaves. To compute the score for s.transition, it can be instantiated to State1.transition and State3.transition. State1.transition can evaluate to State2 in both the counterexample and the satisfying instance. Thus, it gets a score of 0. For State3.transition, in the counterexample, it evaluates to State1 and gets a score of 1 as the size of different values {State3, State1} divided by the size of the instantiated values {State3} and the evaluated values {State1}. In the satisfying instance, it evaluates to an empty set and gets a score of 0. Overall, s.transition gets a relational score of 0.25 as the average of all its instantiated expressions: State1.transition (0) and State3.transition (0.5). Finally, the overall score of 1.25 is assigned to the expression s.transition=none as the aggregation of its Boolean and relational scores.

FIG.11shows an example algorithm that can be used to analyze a set of unsatisfying formulas shows two example Alloy-generated satisfying instances. It is possible that no satisfying instances can be generated for one or more counterexamples, which can indicate that some constraints in the model have conflicts with a property being checked. The example algorithm ofFIG.11can be used to determine why a set of constraints cannot be satisfied by giving a minimal subset of conflicting constraints. Those conflicting constraints can help identify suspicious expressions. The algorithm ofFIG.11can take as input a model M, an unsat core U, and a counterexample c showing that M does not satisfy a property p. The algorithm ofFIG.11can outputs a list of expressions in M that conflict with p. The values M, U, and c, are also referenced above in connection with the algorithm ofFIG.8.

In line1of the algorithm ofFIG.11, a sliced model M1can be produced in which all expressions in the unsat core are omitted from the original model M. Removing the conflicting expressions in the unsat core allows satisfying instances from the new model M1to be obtained to compare with the counterexample. A minimal satisfying instance from M1is generated and compared with the input counterexample to obtain the differences between the counterexample and the satisfying instance. Then, the algorithm ofFIG.11may identify which of the removed expressions conflict with p by evaluating them on obtained differences. If an expression evaluates to True, then adding that expression back to the model can still allow the satisfying instance to be generated (e.g., the expression is not conflicting with p). Thus, expressions that evaluate to False can be identified as conflicting with p and can be returned as suspicious expressions. Similar scores can be assigned to these resulting expressions because they all contribute to the unsatisfiability of the original model and the intended property. For example, if line17is changed in the model shown inFIG.3to all s: State|s.transition !in FSM.start, a declarative specification language, such as Alloy, can find counterexamples, such as the one inFIG.5, but may fail to generate any satisfying instances. This is because the modified line17forces all states to have some transitions, which conflicts with the constraint requiring no transition for stop states. From the unsat core, the example algorithm ofFIG.11can identify four expressions in the model: (a) all start1, start2: FSM.start|start1=start2, (b) some FSM.stop, (c) FSM.start !in FSM.stop and (d) all s: State|s.transition !in FSM.start. After removing these four expressions from the model, the algorithm ofFIG.11can generate the same sat instance inFIG.5, panel (b). As before, the main difference between the counterexample and the satisfying instance involves two values: State1 and State3. Then, the algorithm ofFIG.11can evaluate each expression using these values (e.g., State1 and State 3). Expressions (a), (b), and (c) evaluate to True for both values, while expression (d) evaluates to False for State3. Thus, the algorithm ofFIG.11can correctly identify (d) as a suspicious expression.

FIG.12shows example results generated using mechanisms described herein to locate faults in 152 buggy models. The 152 buggy models were collected from 12 Alloy models in AlloyFL. Briefly, the models are addr (address book) and farmer (farmer cross-river puzzle) from Alloy; bempl (bad employer), grade (grade book) and other (access-control specifications) are from Amalgam; and arr (array), bst (balanced search tree), ctree (colored tree), cd (class diagram), dll (doubly linked list), fsm (finite state machine), and ssl (sorted singly linked list) are homework assignments from AlloyFL. For models with assertions (e.g., from Amalgam), those assertions were used to collect results. For models that do not have assertions (e.g., homework assignments), assertions and expected predicates were manually created. Embodiments of the present disclosure deal with models containing multiple violated assertions by analyzing them separately and returning a ranked list for each assertion. For illustration purposes, this is simulated by simply splitting models with separate violations into separate models (e.g., bst2 contains two assertion violations and thus are split into two models bst2, bst2_1). Finally, mechanisms described herein can be highly automatic. For example, a fault localization system implemented in accordance with some embodiments of the present disclosure can have just one user-configurable option: the number of pairs of counterexamples and satisfying instances to be generated (which by default may be set to a particular number, such as 5). For each model,FIG.12lists the name, lines of code, the number of nodes that the example implementation determined to be irrelevant and sliced out, and the number of total AST expression nodes. The last two columns show the resulting ranking of the correct node and its total run time in seconds. The 28 italicized models include predicate violations, while the other 124 models include assertion violations. In some embodiments, mechanisms described herein can be used to automatically determine the violation type and utilize an appropriate technique (e.g., using a comparator for assertion errors and an unsat analyzer for predicate violations). Finally, the models are listed in sorted order based on their ranking results.

In summary,FIG.12shows that an example fault localization system implemented in accordance with some embodiments of the present disclosure was able to rank buggy expressions in the top 1 (e.g., the buggy expression is ranked first) for 91 (60%) of the models, top 2 to 5 for 35 (23%) of the models, top 6 to 10 for 10 (34%) of the models, above top 10 for 6 (4%) of the 152 models. For 10 models, the example fault localization system was not able to identify the cause of the errors (e.g., the buggy expression are not in the ranking list), some of which include assertion errors that are not due to any existing expressions in the model, but rather because the model is “missing” some constraints. Also shown inFIG.12is that the example fault localization system generated results very quickly (e.g., in under one second). As shown inFIG.12, the example fault localization system was able to locate and rank the buggy expressions in 142 out of the 152 models analyzed. Many of the bugs are common errors that are often undetected by humans, such as when a developer fails to consider certain corner cases. For example, stu5 contains the buggy expression all n: This.header.*link|n.elem<=n.link.elem that does not allow any node without link (the fix is changing the buggy expression to all n: This.header.*link|some n.link=>n.elem<=n.link.elem). In some embodiments, mechanisms described herein can be used to successfully recognize the difference that the last node of the list contains a link to itself in the counterexample but not in the satisfying instance, and can rank this expression second. Additionally, the example fault localization system can rank the subexpression n.elem<=n.link.elem first, where the fix is actually needed. The example fault localization system used to generate the results inFIG.12also performed especially well on 28 models with violated predicates by analyzing the unsat cores and correctly ranking the buggy expressions first.

FIG.13shows example results generated using mechanisms described herein to analyze large complex models. For example, a model of surgical robots may be used to verify a critical arm movement safety property: a check that a position of a robot arm is in the same position that a surgeon articulates in a control workspace during a surgery procedure and that the surgeon is notified if the arm is pushed outside of its physical range. This property is formulated as an assertion and checked on 15 models (such as Alloy models) representing 15 types of robot arms using different combinations of hardware and software features. A study found that 5 models violate the property.FIG.13, which has the same format asFIG.12, and lists the results of the study. For each model, an example fault localization system implemented in accordance with some embodiments of the present disclosure ranked the correct buggy expressions in the second place in less than 3 seconds. The example fault localization system returned two suspicious expressions: (1) HapticsDisabled in UsedGeomagicTouch.force, and (2) some notification: GeomagicTouch.force notification=HapticsEnabled. Modifying either expression would fix the issue (e.g., changing Disable to Enabled in (1) or Enabled to Disabled in (2)).

Still referring toFIG.13, and as another example, mechanisms described herein can be used to analyze models for the permissions of one or more electronic devices, such as Android operating systems and applications (sometimes referred to as apps) to find inter-app communication vulnerabilities.FIG.13shows that an example fault localization system was able to locate 4 buggy expressions (the unary modification ranked 2nd, the binary operations ranked 3rd, 9th, and 11th), but did not identify a mutated expression (variable declaration mutations). However, the mutated expression did not contribute to the assertion violation, and accordingly, the example fault localization system was correct in not identifying the mutated expression as a fault.

Still referring toFIG.13, and as another example, mechanisms described herein can be used to verify translations of annotated code (TACOs). TACO can automatically convert a Java program annotated with invariants to an Alloy model with an assertion. If the Java program contains a bug that violates the annotated invariant, then checking the assertion in the Alloy model can provide a counterexample. The example fault localization system was tested on three different Alloy models with violated assertions representing three real Java programs from TACO: sll-contains checks if a particular element exists in a linked list; count-nodes counts the number of a list's nodes; and remove-nth removes the nth element of a list. These (machine-generated) models are much larger than typical Alloy models (5000 to 6000 LoC each).FIG.13shows the results of tests run on these three different Alloy models. For ssl-contains, the example fault localization model ranked the buggy expression third within 3 seconds. This expression helps to locate an error in the original Java program that skips the list header. The faulty expressions of remove-nth and count-nodes are ranked 12th and 18th, respectively (which are still beneficial given the large, >5000, number of possible locations). As shown inFIG.13, the example fault localization system worked well on large real-world declarative specification models (such as Alloy models). While developing correct fixes for these models remains nontrivial, mechanisms described herein can help developers (or automatic program repair tools) quickly locate buggy expressions, which in turn helps to understand (and hopefully repair) the actual errors in original models.

FIG.14shows an example comparing performance of mechanisms described herein and another technique locating faults in various models. Row1highlights results for an example fault localization system implemented in accordance with some embodiments of the present disclosure. Row2highlights results for the AlloyFL fault localization system, which is a currently available fault localization system for the declarative specification language Alloy. As described above, mechanisms described herein utilize violated assertions and counterexamples to identify faults, which is different than AlloyFl. As shown inFIG.14, the example fault localization system was more accurate at identifying the top 1 buggy expression than AlloyFL (e.g., 91 models compared to 76 models). On average, buggy expressions in a model rank 2.4 using the example fault localization system, compared to a ranking of 3.1 compared to AlloyFl. Moreover, the example fault localization system was much faster than AlloyFl at identifying buggy expressions. AlloyFl took 32.4 seconds to analyze a specification that was analyzed by the example fault localization system in only 0.2 seconds. Therefore, as models continue to grow more complex for a variety of applications, it is clear that mechanisms described herein can provide improved accuracy and efficiency over conventional techniques for fault localization in declarative specification languages.

FIG.15shows an example1000of a process for fault localization in a model in accordance with some embodiments of the present disclosure. At1002, process1000can receive an original model in a declarative specification language. In some embodiments, the declarative specification language can be Alloy. Further, in some embodiments, the original model can be a model for surgical robots, or Java programs, or permissions on one or more electronic devices (e.g. Android permissions).

In some embodiments, process1000can receive the original model from any suitable source and/or using any suitable technique or combination of techniques. For example, the original model can be received from model data source102(e.g., over communication network108, via a local connection, etc.).

At1004, process1000can query an underlying automated analysis of the declarative specification language for a counterexample using any suitable technique or combination of techniques. In some embodiments, the counterexample can be an instance of the original model that does not satisfy a property. In some embodiments, such as embodiments where the declarative specification language is Alloy, the underlying automated analysis can be an Alloy Analyzer. For example, process1000can query an Alloy Analyzer for at least one counterexample that does not satisfy an assertion associated with the model received at1002(e.g., as described above in connection withFIGS.3-7).

At1006, process1000can use a partial max satisfiability solver (PMAX-SAT) to find an instance that satisfies the property and is a close as possible to the counterexample using any suitable technique or combination of techniques. For example, process1000can transform the input model into a logical formula representing hard constraints, and information from a counterexample into soft constraints, and can use a solver to find a solution that satisfies all of the hard constraints and as many of the soft constraints as possible (e.g., as described above in connection withFIGS.5-9). As a more particular example, process1000can use a Pardinus solver to identify an instance that satisfies the hard constraints and as many soft constraints as possible.

At1008, process1000can determine differences in expressions from the original model between the counterexample and the satisfying instance. The expressions can include relations and atoms, and process1000can determine differences between relations and/or atoms between the counterexample and the satisfying instance. In a particular example, expressions in Alloy can be constrained to use only relations and atoms. In some embodiments, process100can determine differences in the expressions using any suitable technique or combination of techniques. For example, process1000can use techniques described above in connection withFIGS.8,10, and/orFIG.11to determine differences between the counterexample and the satisfying instance.

At1010, process1000can analyze the differences between the counterexample and the satisfying instance to compute suspicion scores for the expressions in the original model using any suitable technique or combination of techniques. For example, process1000can use techniques described above in connection withFIGS.8,10, and/orFIG.11to analyze differences between the counterexample and the satisfying instance.

At1012, process1000can present the suspicion scores using any suitable technique or combination of techniques. For example, process1000can cause a computing device (e.g., computing device110) to present a ranked list of suspicious expressions in the model received at1002.

It should be noted that, as used herein, the term mechanism can encompass hardware, software, firmware, or any suitable combination thereof.

It should be understood that the above-described steps of the processes ofFIGS.8,10,11, and/or15can be executed or performed in any order or sequence not limited to the order and sequence shown and described in the figures. Also, some of the above steps of the processes ofFIGS.8,10,11, and/or15can be executed or performed substantially simultaneously where appropriate or in parallel to reduce latency and processing times.