Error Reporting LogicCiera JaspanCarnegie Mellon UniversityPittsburgh, PA [email protected] QuanCarnegie Mellon UniversityPittsburgh, PA [email protected] AldrichCarnegie Mellon UniversityPittsburgh, PA [email protected]—When a system fails to meet its specification, it canbe difficult to find the source of the error and determine how tofix it. In this paper, we introduce error reporting logic (ERL),an algorithm and tool that produces succinct explanations forwhy a target system violates a specification expressed in firstorder predicate logic. ERL analyzes the specification to determinewhich parts contributed to the failure, and it displays an errormessage specific to those parts. Additionally, ERL uses a heuristicto determine which object in the target system is responsiblefor the error. Results from a small user study suggest that thecombination of a more focused error message and a responsibleobject for the error helps users to find the failure in the systemmore effectively. The study also yielded insights into how theusers find and fix errors that may guide future research.I. INTRODUCTIONMany specification languages are based upon first-orderpredicate logic. This is a very natural route to take forspecifications; it provides a concise, expressive, and well-understood way for describing system-level details. Examplesof such specification languages in recent literature includeAcme, SCL, and Alloy [1]–[3]. In each of these languages,FOPL-based specifications constrain a system, and a toolproduces errors when there is an inconsistency between thespecifications and the system. The error messages producedby these systems generally fall into three categories:• Specification identifier. Under this mechanism, the toolproduces an error message that states which specificationfailed. The user must read the specification and manuallyanalyze the system to determine which part of the systembroke the specification.• Human generated message. This mechanism attempts toprovide the user with an intuitive understanding of thespecification. The specification writer makes a genericsummary about what the specification is checking, andthis is used as the error message. The user can thenuse this message as a guide to understand the generalproblem.• Hybrid systems. Some tools also hybridize the two mech-anisms; they will use a human generated error messageif it exists, but they will fall back on a specificationidentifier.These mechanisms work very well for specifications that areshort and have an obvious point of failure. However, they donot work well for complex specifications, such as the Acmespecification shown in Figure 1. By Acme standards, this is amedium sized specification. It has 3 levels of quantification, aforall con : ORMConnector in self.CONNECTORS |forall comp : Component in self.COMPONENTS |forall p : Port in comp.ports |(attached(con.caller, p) ->declaresType(comp, Data) anddeclaresType(p, DataPort))Fig. 1. Sample Acme Specificationvery small inner predicate, and it only calls pre-defined atomicpredicates.If the user must read the specification itself, they can quicklybecome lost in the details of the specification. There is no wayto tell which sub-predicates in the specification failed, so theuser must check each one. The user also doesn’t know whichelements in the system caused this failure and so must checkall elements with matching types.Even if the specification writer provided an error message,this would not necessarily help a user. An error message wouldtell us the purpose of the specification, and this might help theuser look for bad patterns of behavior in the system. However,it still does not describe which predicate failed or which objectin the system caused the failure.In Figure 1, the user would have to check the entire systemfor conformance to the specification. What we would preferis an error message that says:myPort must declare the type DataPort sincemyConn.caller is attached to myPortError reporting logic (ERL) provides an automated way forcreating error messages such as the one above. ERL presentseach failing point as a unique error. To do this, it singles outonly the failing predicates and assigns responsibility of theerror to a specific object in the system.In this paper, we will provide four contributions related toerror messages from FOPL-based specifications:• We present a user study that provides several insightsinto how users examine errors to find the root cause of theproblem and how users attempt to fix the error. Primarily,we found that users see an error message as a single taskwhich they must resolve, they only use keywords to findthe problem rather than reading anything in depth, andthey frequently rely on pattern recognition to find and fixerrors. (Section II)• We present ERL, a system for automatically generatingerror messages from a specification based on first-orderFig. 2. The Web System in AcmeStudiopredicate logic. Section III will show how the ERLhandles each of the specifications from the user study,and Section VI shows how the implementation of ERLperforms with MDS, the most complex architecturalspecification built with Acme.• We have implemented ERL as a reusable component andhave integrated it within AcmeStudio [4]. The integrationwas relatively straightforward and required only a smallamount of work to change the error messages. SectionIV provides implementation and integration details.• During the user study, the same participants also usedERL. In section V we describe how the users reacted tothe new error messages. Three of the four participantsbenefited from the ERL error messages. The remainingparticipant did not benefit, but was not hindered, by theerror messages.Throughout this paper, we will use the Acme specifica-tion language (and AcmeStudio, the graphical interface andchecker for Acme) as our example system. AcmeStudio allowsdevelopers to view a graphical representation of an architec-ture. While the developers can access and edit the Acme codebehind the graphical view, it is typically not used. AcmeStudiodisplays the architecture using component-connector diagramswhich can be edited entirely through a user interface. A samplediagram for an architecture is shown in Figure 2.If an architecture fails to meet a specification, a red error tri-angle appears at the place where the specification was defined,as shown in Figure 2. Notice that this is not necessarily thecomponent which is