View Full Document


Unformatted text preview:

Error Reporting Logic Ciera Jaspan Trisha Quan Jonathan Aldrich Carnegie Mellon University Pittsburgh PA USA ciera cmu edu Carnegie Mellon University Pittsburgh PA USA tkq andrew cmu edu Carnegie Mellon University Pittsburgh PA USA aldrich cs cmu edu Abstract When a system fails to meet its specification it can be difficult to find the source of the error and determine how to fix it In this paper we introduce error reporting logic ERL an algorithm and tool that produces succinct explanations for why a target system violates a specification expressed in first order predicate logic ERL analyzes the specification to determine which parts contributed to the failure and it displays an error message specific to those parts Additionally ERL uses a heuristic to determine which object in the target system is responsible for the error Results from a small user study suggest that the combination of a more focused error message and a responsible object for the error helps users to find the failure in the system more effectively The study also yielded insights into how the users find and fix errors that may guide future research I I NTRODUCTION Many specification languages are based upon first order predicate logic This is a very natural route to take for specifications it provides a concise expressive and wellunderstood way for describing system level details Examples of such specification languages in recent literature include Acme SCL and Alloy 1 3 In each of these languages FOPL based specifications constrain a system and a tool produces errors when there is an inconsistency between the specifications and the system The error messages produced by these systems generally fall into three categories Specification identifier Under this mechanism the tool produces an error message that states which specification failed The user must read the specification and manually analyze the system to determine which part of the system broke the specification Human generated message This mechanism attempts to provide the user with an intuitive understanding of the specification The specification writer makes a generic summary about what the specification is checking and this is used as the error message The user can then use this message as a guide to understand the general problem Hybrid systems Some tools also hybridize the two mechanisms they will use a human generated error message if it exists but they will fall back on a specification identifier These mechanisms work very well for specifications that are short and have an obvious point of failure However they do not work well for complex specifications such as the Acme specification shown in Figure 1 By Acme standards this is a medium sized specification It has 3 levels of quantification a forall con ORMConnector in self CONNECTORS forall comp Component in self COMPONENTS forall p Port in comp ports attached con caller p declaresType comp Data and declaresType p DataPort Fig 1 Sample Acme Specification very small inner predicate and it only calls pre defined atomic predicates If the user must read the specification itself they can quickly become lost in the details of the specification There is no way to tell which sub predicates in the specification failed so the user must check each one The user also doesn t know which elements in the system caused this failure and so must check all elements with matching types Even if the specification writer provided an error message this would not necessarily help a user An error message would tell us the purpose of the specification and this might help the user look for bad patterns of behavior in the system However it still does not describe which predicate failed or which object in the system caused the failure In Figure 1 the user would have to check the entire system for conformance to the specification What we would prefer is an error message that says myPort must declare the type DataPort since myConn caller is attached to myPort Error reporting logic ERL provides an automated way for creating error messages such as the one above ERL presents each failing point as a unique error To do this it singles out only the failing predicates and assigns responsibility of the error to a specific object in the system In this paper we will provide four contributions related to error messages from FOPL based specifications We present a user study that provides several insights into how users examine errors to find the root cause of the problem and how users attempt to fix the error Primarily we found that users see an error message as a single task which they must resolve they only use keywords to find the problem rather than reading anything in depth and they frequently rely on pattern recognition to find and fix errors Section II We present ERL a system for automatically generating error messages from a specification based on first order TABLE I PARTICIPANTS ID A B C D Configuration 1 Web ERL Web Build ERL Build Configuration 2 Build Build ERL Web Web ERL can only write one message for the entire specification the error message is typically about the general purpose of the specification II H OW Fig 2 The Web System in AcmeStudio predicate logic Section III will show how the ERL handles each of the specifications from the user study and Section VI shows how the implementation of ERL performs with MDS the most complex architectural specification built with Acme We have implemented ERL as a reusable component and have integrated it within AcmeStudio 4 The integration was relatively straightforward and required only a small amount of work to change the error messages Section IV provides implementation and integration details During the user study the same participants also used ERL In section V we describe how the users reacted to the new error messages Three of the four participants benefited from the ERL error messages The remaining participant did not benefit but was not hindered by the error messages Throughout this paper we will use the Acme specification language and AcmeStudio the graphical interface and checker for Acme as our example system AcmeStudio allows developers to view a graphical representation of an architecture While the developers can access and edit the Acme code behind the graphical view it is typically not used AcmeStudio displays the architecture using component connector diagrams which can be edited entirely through a user interface A sample diagram for an architecture is shown in Figure 2 If

Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...

Join to view Error Reporting Logic and access 3M+ class-specific study document.

We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Error Reporting Logic and access 3M+ class-specific study document.


By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?