Experimental evaluation of a tool for the verification and transformation of source code in event-driven systems

A wafer scanner (Fig. 2) exposes an IC image on rectangular segments of a wafer. Such a segment is called die. During an exposure, the wafer scanner uses a laser beam to scan the image, and uses a lens to project the laser beam onto the die.

Connecting the statechart and the activities consists of two steps: The first step is creating the control calls (see Fig. 1). Harel (1987) refers to this step as “linking activities to states”, which can be explained as follows: Upon entrance to a state, calling a function realizing an activity. Control calls are usually specified while creating the statecharts, which we also did: In Fig. 3, entry: preprocess() and entry: process() are the control calls.

The second step for connecting the statechart and the activities is creating the event calls (see Fig. 1): Stimulating the implementation of the statecharts with the events that occur due to the execution of the non-reactive part (i.e., the activities). In the remainder of this section, we present the details of the second step, which is necessary for understanding the remainder of this article.

The second step requires identifying all the points (i.e., locations) in the implementation (i.e., source code) of the activities where the events occur during execution. For example, the preprocessed event occurs when the preprocessing activity is completed (Section 2.1.4). Note that the preprocessing activity consists of cleaning the reticle if it is dirty, and then measuring the shape imperfections of the wafer (Section 2.1.2). Therefore, the preprocessed event occurs if one of the following sequences of function calls is executed: <..., cleanReticle, ..., measureWafer>, or <..., measureWafer>. By analyzing all possible paths through the implementation of the preprocessing activity (i.e., Listing 1), we can find out whether such sequences exist (note that both of the previously mentioned sequences exist in Listing 1). If such a sequence exists, then we can find the syntactic location in the source code where that sequence terminates (i.e., the location after ‘;’ in Line 7, Listing 1). We call such a location event point, because an event occurs when an execution reaches that point. Now, let us define the term event point more precisely:

Using the definitions of the preprocessing and processing activities (Sections 2.1.2 and 2.1.1), we can identify the event points, as follows: The preprocessed event is mapped to the point located after ‘;’ in Line 7, Listing 1. The processed event is mapped to the point located after ‘}’ in Line 8, Listing 2. Hence, there are two event points:

After the identification of the event points, the implementation of the statechart must be stimulated with the occurrences of the events that are mapped to the event points. For this reason, typically a function that transmits the occurrence of an event to the statecharts is called at each event point. Hence, we call such functions event functions. Listings 3 and 4 show the implementations of the preprocessing and processing activities after inserting calls to the event functions, say preprocessed and processed, at the event points enumerated above.

The definitions of the event functions are typically located in the reactive-part of event-driven software (see Fig. 1). They can be considered as the interface provided by the reactive part to the non-reactive part; event calls (see Fig. 1) are the calls to the event functions. The implementation details of the event functions are not important in this article.

The insertion of the event calls concludes the connection of the statechart and the activities. Consequently, each requirement in Section 2.1.3 is fulfilled by the event-driven software resulting from the connection explained in this section.

Note that the event points of the simplified wafer scanner are at the end of the functions. In the software of the actual wafer scanner, however, there are usually several other function calls between an event point and the end of a function. We identified two typical reasons for this:

We do not illustrate such modularity and concurrency cases in this article, because they would unnecessarily complicate our example application.

In the software of the actual wafer scanner, the following cases exist, too: An event is mapped to multiple points in one function; an event is mapped to multiple points in multiple functions; multiple events are mapped to multiple points in one function. Although we do not illustrate these complicated cases, our solution addresses them, as well.

If the activities evolve, then the ETB may become unsound or incomplete (i.e., defective), as we exemplify in this section. Note that, even if there is only one version of activities (i.e., activities are implemented once and they do not evolve), the ETB should still be sound and complete (i.e., defect-free).

Let us reconsider the case in Section 3.1.1, where we remove the calls to measureWafer and preprocessed in Listing 3. After removing the call to preprocessed, the statechart is no longer stimulated with an occurrence of the preprocessed event. Consequently, the wafer scanner cannot perform the transitions from the PREPROCESSING state to the PROCESSING state, and from the PROCESSING state to the final state. Hence, the requirements R2 and R4 cannot be fulfilled despite the sound and complete ETB. Thus, we can conclude that an occurrence of the preprocessed event is mandatory whenever the preprocess function is executed. Therefore, the call to measureWafer must not be removed, as ‘dictated’ by the requirements (Section 2.1.3) and the statechart in Fig. 3. Otherwise, the preprocessing activity becomes incompatible with the statechart.

Based on the discussion in this section, one can imagine certain constraints on the implementation of activities, such that these constraints are satisfied, if and only if the activities are compatible with the statecharts. For example, the constraint in this case would be “the preprocessed event must occur whenever the preprocess function is executed”. We call such constraints compatibility constraints.

In contrast to the case presented in this section, one can imagine other cases in which the activities remain compatible with the statecharts. For instance, if one or more statements are inserted after ; in Line 5 in Listing 3, then the activity is still compatible with the statechart. In any case, a manual verification of the compatibility in a large-scale software system is a time-consuming and error-prone maintenance task.

Possible human errors during the evolution of activities may cause other defects than those we discussed so far in Section 3. For example, a human error during the evolution of the measureWafer function, which is the implementation of the wafer measuring activity, may lead to incorrect measurements, hence defective ICs. Addressing these kinds of defects is beyond the scope of this article.

Whenever the activities (i.e., the non-reactive part of software) evolve, the compatibility between the activities and the statecharts (i.e., the reactive part of software) has to be verified. If this verification fails, then the compatibility has to be maintained (i.e., one or more compatibility defect has to be repaired). Next, the soundness and completeness of the ETB has to be verified. If this verification fails, then the ETB has to be maintained such that it remains sound and complete (i.e., one or more ETB defects has to be repaired). The problem is that these verification and maintenance tasks are time-consuming and error-prone, if they are manually performed.

To address the problem stated in Section 3.4, we defined the following goals to be reached in this article: In Section 4, we provide an overview of the solution that we developed for reaching the goals stated above.

When software engineers implement the activities for the first time (without event calls), the four stages can be performed to verify that the compatibility constraints are satisfied, and to insert valid event calls, so that a sound and complete ETB is generated.

Whenever software engineers modify the event-call-free implementation of the activities (e.g., Listings 1 and 2) that is in the input folder mentioned in Section 4.1.3, the Stages 3 and 4 can be automatically repeated (a) to re-verify that the compatibility constraints are satisfied, and (b) to re-insert valid event calls; so that (a) a sound and complete ETB is re-generated, and (b) the resulting source code is deposited to the output folder mentioned in Section 4.1.3.⁷ This automatic repetition of the Stages 3 and 4 brings us to the goals stated in Section 3.5.

Now, let us see our solution in more detail. In Section 5, we explain a way of working for deriving and specifying compatibility constraints. This way of working is the first stage of our solution.

The hints for deriving the compatibility constraints are the events whose lack of occurrence indicates an incompatibility exemplified in Section 3.2. We call such events mandatory events, because if such an event does not occur, then some of the requirements are not fulfilled. After the identification of mandatory events, the compatibility constraints can be derived in such a way that the satisfaction of the constraints guarantees the occurrences of the mandatory events.

The developer (see Fig. 4), who knows the requirements, the statecharts, and the implementations of the activities, can identify the mandatory events: she picks an event, say preprocessed, from the statechart in Fig. 3, and imagines what would happen if this event would not occur: the wafer scanner could not perform the transitions from the PREPROCESSING state to the PROCESSING state, and from the PROCESSING state to the final state. Hence, the system could not fulfill the requirements R2 and R4. With this line of reasoning, the developer realizes that the preprocessed event is mandatory. Note that the processed event (see Section 2.1.4) is a mandatory event, too.

If the requirements are formally specified and ‘linked’ to the states and transitions, then automating the identification of the mandatory events becomes possible. However, this automation falls outside the scope of this article.

In this section, we explain how a developer can derive the compatibility constraints whose satisfaction guarantees the occurrence of the mandatory event preprocessed.

These constraints can be derived from the following facts: (a) the preprocessed event occurs when the preprocessing activity is completed, (b) the preprocessing activity is “cleaning the reticle if it is dirty, and then measuring the shape imperfections of the wafer” (Section 2.1.2), (c) the reticle cleaning activity, the wafer measuring activity, and the preprocessing activity are respectively implemented within the cleanReticle, measureWafer, and preprocess functions. Using these facts, the developer can derive the following compatibility constraints:

There are two possible sequences of function calls from the preprocess function in Listing 1: seq ₁ = <cleanReticle, measureWafer>, and seq ₂ = <measureWafer>. With these sequences in mind, note that the preprocess function satisfies both C1 and C2. As a result, the mandatory event preprocessed occurs each time the preprocess function is executed.

In fact, C1 and C2 are stricter than necessary: they enforce that the preprocessed event is mapped to the source code point(s) within the definition of the preprocess function. However, it would equally be fine if the preprocessed event were mapped to the source code point(s) in the definition of another function, say f, such that the event occurs each time f is executed, and f is called each time the preprocess function is executed. In this article, we only present stricter-than-necessary constraints due to a limitation of the current analyzer implementation: the analyzer can reason about function definitions as a single block, but it cannot reason about the nesting of function calls. This is not a fundamental limitation; some of the existing program analysis tools (e.g., CodeSurfer; http://​www.​grammatech.​com) are already capable of reasoning about the nesting of function calls. The current implementation of our analyzer has proven to be useful despite this limitation (Sections 9–12).

The compatibility constraints that are related to the mandatory event processed (i.e., the other event in Fig. 3) are provided in (Güleşir 2008).

After the developer derives the compatibility constraints, she needs to specify them in VisuaL, so that the analyzer (see Fig. 4) can verify the implementations of the activities. In this section, we explain how to specify C1 and C2 in VisuaL, and informally discuss the syntax and semantics of VisuaL, using examples. If the readers are interested in the general syntax and formal semantics of VisuaL, then we kindly request them to see (Güleşir 2008), where an entire chapter is allocated to this topic. Broadly speaking, a VisuaL specification can be considered as a special type of Moore machine (Hopcroft and Ullman 1990).

If the preprocess function (Listing 1) is given to the analyzer as an input, then the analyzer parses the preprocess function, and constructs an abstract syntax tree (Aho et al. 1986) AST _preprocess shown at the top of Fig. 9.

The rectangles labelled with FDef or FCall are the abstract nodes denoting a function definition or a function call, respectively.

We assume that the compatibility constraints and the events can be specified in terms of function calls and the possible flow of control (Fenton and Pfleeger 1998) between the function calls. Based on this assumption, only a part of the information that is in the AST is needed during the analysis. Therefore, the analyzer constructs a model (of the AST) that contains only the function calls and the flow of control between them. We call this model simplified control flow graph (SCFG), which is a ‘lightweight’ version of the traditional control flow graph (Fenton and Pfleeger 1998). A formal definition of a SCFG and its relation to source code are provided in (Güleşir 2008).

A SCFG decouples the analysis algorithm (explained in Section 7.3) from the implementation language of the activities, which is C in this case. Consequently, the implementation of the analysis algorithm does not need to be adapted if the implementation language of the activities is changed to another language in which the flow of control is explicit (i.e., imperative languages). Furthermore, the use of a SCFG enables a simpler implementation of the analysis algorithm, and a higher performance during analysis.

The analyzer traverses AST _preprocess in the depth-first (Cormen et al. 2001) manner to create SCFG _preprocess depicted at the bottom of Fig. 9. The black dot on the left represents the initial node, which denotes the beginning of the preprocess function; The cleanReticle-labelled ellipse represents an internal node that denotes the call to cleanReticle; The measureWafer-labelled ellipse represents an internal node that denotes the call to measureWafer; The circled black dot represents the final node, which denotes the end of the preprocess function; And the arrows between these shapes represent the possible flow of control between the entities denoted by the nodes. As visualized by the dashed arrows, the analyzer maintains a one-to-one mapping from the nodes of SCFG _preprocess to the related nodes of AST _preprocess .

To verify that the preprocess function satisfies the compatibility constraints C1 and C2 presented in Section 5.2, the analyzer has to check whether all possible sequences of function calls from the preprocess function are matched by the pattern depicted in Fig. 8. To generate the function call sequences, the analyzer traverses SCFG _preprocess in a depth-first manner, such that if the analyzer detects a cycle in the SCFG, the analyzer backtracks. As understandable from SCFG _preprocess , there are two possible sequences of function calls: seq ₁ and seq ₂, both of which are already presented in Section 5.2. The analysis of these sequences reveals that each sequence ‘ends in’ q1 (see Fig. 8). Since this rectangle has the < <final> > label, each sequence is matched by the pattern, which means the preprocess function satisfies both C1 and C2. If the constraints were not satisfied, then the analyzer would output a compatibility error containing a sequence that violates the constraint. Such an error is valuable for finding and repairing an inconsistency.

During the analysis of seq ₁, q0 (see Fig. 8) is mapped to the cleanReticle-labelled internal node of SCFG _preprocess , and q1 is mapped to the measureWafer-labelled internal node. During the analysis of seq ₂, q1 is once more mapped to the measureWafer-labelled internal node. Other rectangles (i.e., q2 and q3) are not mapped to any node of SCFG _preprocess . This partial⁹ mapping from the set of the rectangles of the specification to the set of the internal nodes of SCFG _preprocess is the output of the analysis (i.e., Stage 3). As depicted in Fig. 4, this output is the input for the transformation (i.e., Stage 4), which is explained in Section 8.

Statecharts are proposed for expressing the event-driven and continuous (non-terminating) behavior of reactive systems (Harel et al. 1990; Harel and Pnueli 1985; Harel 1987; Harel and Naamad 1996; Harel and Politi 1998). According to this proposal, the activities must terminate upon execution. Hence, the possible sequences of function calls from a function realizing an activity must be finite. Given this fact, the verification algorithm can be explained as follows: Let ptrn denote a pattern that represents a compatibility constraint cns. ptrn can be translated to a Moore machine that accepts a set S _ptrn of finite sequences. Let S _f denote the set of possible sequences of function calls from f. Note that S _f can be computed by traversing SCFG _f . f satisfies cns if and only if \(S_{f} \subseteq S_{ptrn}\). We compute this by finding the intersection of the set of sequences accepted by Moore machines. A mathematical explanation of the analysis algorithm and its asymptotic time complexity (polynomial) are provided in (Güleşir 2008).

The software of the actual wafer scanner consists of around 200 software components, most of which are designed and implemented in the way explained in Section 2. In the past, one of the software teams developing and maintaining such a component informed us about the excessive maintenance time they spend due to the defects explained in Section 3. Therefore, we conducted this research.

The solutions presented in this article were tested within the context of the component mentioned above. This component has 15 statecharts, each having on average ten states and 15 transitions. The component contains 55,000 lines of source code, and 55 events mapped to 102 source code points distributed over 81 function definitions. Hence, the component has 55 event functions, and 102 event calls distributed over 81 functions. Among the 200 components of the actual wafer scanner, this component is a mid-sized one.

After we developed the solution, our purpose was to find answers to these questions: Is VisuaL expressive enough to specify events and compatibility constraints in real-life? Can a professional software developer efficiently use VisuaL? To find preliminary answers to these questions, we trained the domain expert of the component, who is a software developer with 15 years of professional experience. During the 1-h training, we used the material presented in this article. After the training, the developer selected a statechart that has 18 states and 22 transitions, and identified the part of the software component in which the corresponding activities are implemented. This selection and identification was purely based on the existing daily work that the expert had to carry out at that time.

Using the heuristic presented in Section 5.1, the developer identified three mandatory events. Then, the developer created three composite specifications in VisuaL, each of which consists of one compatibility constraint, one event definition, and one event call binding.

In total, the developer worked 8 h under daily conditions: he was interrupted by colleagues, phone calls, lunch and coffee breaks, etc. Using two video cameras, we captured the developer, his screen, and his desk while he was working. The resulting footage enabled us to accurately calculate the net amount of time he spent for creating the specifications, which was 155 min.

The first specification created by the developer contains 11 nodes and 19 edges. To create this specification, and to draw it using Borland Together, the developer spent 80 min in total. In Table 1, the data for each of the three specifications is listed.

Using the data presented in Table 1, one can calculate that the developer spent on the average 160, 83, and 56 s per node or edge while creating Specification1, Specification2, and Specification3, respectively. This calculation indicates that the developer quickly gained speed in creating specifications. To be able to generalize this conclusion to other developers however, we need to repeat this study with more number of software developers.

To create the specifications, the developer had to rigorously analyze the relationship between the implementation, the detailed design, the architecture, and the requirements of the software component. This rigorous analysis enabled him to find one defect, which had to be repaired in the next release, four design anomalies that required restructuring and maintenance, and one undocumented feature. Two weeks earlier, the component in which the developer found these problems had been maintained by himself, and reviewed by two of his colleagues.

The purpose of this experiment is (a) to test whether the analyzer and transformer can reduce the time spent by humans and prevent human errors, while humans are removing incompatibilities and repairing ETB defects in industrial software, and (b) to quantify the time reduction and error prevention.

We conducted this experiment twice. In the first experiment, 21 M.Sc. computer science students from the University of Twente participated. In the second experiment, 23 professional software developers from ASML participated.

During both experiments, the participants worked with three C functions (i.e., implementations of three activities) selected by the domain expert from the component of the wafer scanner software (see Section 9.1), and the corresponding specifications that were created by the expert using VisuaL.

We injected an incompatibility defect, an unsoundness defect, and an incompleteness defect into each function, and then we requested the participants to repair these defects by modifying the functions, such that each function would conform to the corresponding specification.

We formulated the following hypotheses to be tested in the first experiment:

We formulated the following hypotheses to be tested in the second experiment:

We chose 0.01 as the significance level for rejecting the hypothesis above.

In this article, we do not investigate the differences between M.Sc. students and professional developers, because the experiments were executed under different conditions, as we will explain in Section 10.2.

As visible in Table 4, we designed an experiment that has one factor and two treatments. The factor and its levels are already explained in Section 9.4.1. Each level of the factor is a treatment in this experiment.

The participants were randomly assigned to one of the two treatments (i.e., there were two independent groups of participants). We balanced the design by assigning (almost) equal number of participants per treatment. In the remainder of this article, we will use tool-supported participant for referring to a participant treated with the tool support, and manual participant for referring to a participant treated without tool support.

The instruments of this experiment are

Interested readers can request the instruments from us by providing personal details and affiliation. If ASML approves the request, then we can send a non-disclosure agreement (NDA). After the NDA is signed and returned, we can provide the instruments.

We prepared a tutorial for teaching the participants how to (a) interpret the specifications, (b) relate the specifications to the source code, and (c) repair the defects in the source code using the specifications. For the tool-supported participants, the tutorial also included how to use the tools. We presented this tutorial before the experiment as a slide show, and we distributed hard copies of the slides to the participants, after the presentation.

We prepared step-wise instructions for the participants. By following these instructions, a participant could find the source code in the directory structure of the computer, run the tools, etc.

We implemented facilitating software that puts a time stamp on the source code modified by a participant, and logs the source code in a file. The manual participants ran this software twice: once at the beginning of the treatment, and once at the end of the treatment. The facilitating software was integrated with the tool support (i.e., analyzer and transformer). Consequently, the tool-supported participants ran the facilitating software at least twice: once at the beginning of the treatment (i.e., when they initially used the tool to find and understand the defects), once at the end of the treatment (i.e., after they modified the source code), and zero or more times during the treatment (i.e., each additional time they used the tool to see whether they could successfully repair the defects).

We prepared an example treatment for the participants, so that they get used to the tasks they are required to perform. In this way, we aimed at improving the accuracy of our measurements, by decreasing the learning overhead in the actual treatments. The example treatment was the first treatment of each participant.

We conducted preliminary runs of the experiment to test the artifacts explained above. These runs enabled us to improve the instruments of the experiment. The four participants of these preliminary runs were different than the participants of the actual experiment. During the analysis presented in Section 11, we excluded the data of the preliminary runs.

To motivate the students for performing the tasks as carefully and quickly as they can, we rewarded the first, second, and the third best performers in each of the tool-supported and manual groups with 50 EUR, 40 EUR, and 30 EUR, respectively. The ranking criterion was performing the tasks with least number of unrepaired defects in least amount of time, where the number of unrepaired defects had priority over the amount of time. Besides the top three prizes, each student received 10 EUR for his participation. Before the students started the experiment, we informed them about the prizes and the ranking criteria. The results of the students were kept anonymous, and these results did not have any impact on their course grade.

We assumed that the developers were self-motivated, because they volunteered. Therefore, we did not reward them with a prize.

During the experiment, the students worked at the computer laboratories of the university, and they used the computers in the laboratories to modify source code, and to run the tools.

To ensure the independence of the observations, each student participated in the experiment at the same time. This required an instructor to give the tutorial for the tool-supported group in a laboratory, and another instructor to give the tutorial for the manual group in another laboratory. Moreover, the instructors and two additional assistants were present at the laboratories.

The developers participated in the experiment at their offices at ASML, and they participated in the experiment not at the same time but at various dates and times. We could not avoid this due to the busy agendas of the developers. We ensured the independence of observations as good as possible: We kept the participant list secret (note that 23 out of 500 developers participated), and collected the material of the experiment after the participation of each developer. During the experiment, the developers used a computer whose setting was identical to the setting of the computers used by the students in the laboratories.

For practical reasons, each the participant had a time limit of 3 h for performing the tasks of the experiment.

As explained in Section 10.1, each participant ran a facilitating software that logs the source code with a time stamp. The participants were not authorized to modify the clock of the operating system.

To validate the data contained in the files, we compared the latest time stamp in a file with the last modified time of the file. If they were different, this would indicate that the participant had manually modified the file, hence the data is invalid. In this way, we found two invalid log files, and we did not include their data in the analysis.

We informed each participant about his result, and asked whether the result is as he expected; each participant informed us that his result is as he expected. This supports the claim that the participants have understood the instructions, and followed them properly (i.e., this is a positive indication about the validity of data).

Our investigations on the log files revealed that the logged data of one tool-supported and one manual student were manually modified (i.e., corrupted). We understood this by comparing the time stamps in the files with the last modified time of the files. Consequently, we excluded their data from our calculations.

One of the tool-supported students could not finish the treatment within the given amount of time, which was 3 h. Therefore, we excluded his data, too.

For testing the hypotheses stated in Section 9.3, we used the independent-samples t-test provided by SPSS. The assumptions for using the t-test hold in our experiment: each dependent variable is measured in the ratio scale (see Section 9.4.3); each participant is randomly assigned to either the tool-supported or the manual group (see Section 9.6); the observations made during the experiment are independent of each other (see Section 10.2); it is likely that the dependent variables have a normal distribution (see Section 11.2).

This category of threats effect the ability to draw correct conclusion about the relation between the treatment and the outcome of the experiment.

In our experiment, we identified two categories of threats to the conclusion validity: low statistical power, and reliability of treatment implementation (Cook and Campbell 1979).

Internal validity threats are issues that can affect the measurements of the independent variable, without the researcher’s knowledge. Therefore, these kinds of threats may influence the validity of conclusions about a possible causal relationship between a treatment and the corresponding outcome.

In our experiment, we identified and addressed three types of threats to the internal validity: maturation, instrumentation, and diffusion or imitation of treatments (Cook and Campbell 1979).

Threats to construct validity influence the ability to draw correct conclusions about the relation between the results of the experiment and the hypotheses that are being tested using these results. Some of such threats are related to the experimental design, and others are related to social factors.

In our experiment, we identified and addressed three types of threats to the construct validity: confounding constructs and levels of constructs, restricted generalizability across constructs, and experimenter expectancy (Cook and Campbell 1979).

The threats to external validity limit the ability to generalize the results of the experiment.

VisuaL is a graphical language that is suitable for expressing constraints on the behavior of algorithms. Such a constraint is a logical or temporal property that must be satisfied by each possible execution of the corresponding algorithm.

Since an algorithm does not execute indefinitely (otherwise it would not be an algorithm by definition (Linz 2001)), each possible execution of an algorithm is finite. Thus, VisuaL is a language that is suitable for expressing properties of finite executions. For example, the following constraint can be expressed using VisuaL, as shown in Fig. 13.

C3 In each possible sequence of function calls from the function f, there must be at least one call, and the last call must be a call to the function traceOut.

In contrast to the executions of algorithms, the executions of finite-state concurrent systems (Magee and Kramer 1999) or reactive systems (Harel and Pnueli 1985) are often infinite. Therefore, we call such systems non-terminating systems. To express the logical and temporal properties of non-terminating systems, several temporal logic formalisms are available: LTL (Clarke et al. 1999), CTL (Clarke et al. 1999), CTL* (Clarke et al. 1999), FLTL (Giannakopoulou and Magee 2003), (Letier et al. 2005). To be able to express the constraint C3 (see above) using one of these formalisms, one has to first translate the finite executions of the algorithm to infinite executions. For example, if seq = <g, h, traceOut> is a finite sequence of function calls representing an execution of the function f, then seq can be translated into the infinite sequence seq′ = < g, h, traceOut,⊙ , ⊙ , ⊙ , ... >, where ⊙ is a special symbol marking the end of seq. Upon this translation, the infinite sequence seq′ can be checked against the LTL formula eventually(traceOut and (next ⊙)). This LTL formula is semantically different than the VisuaL specification shown in Fig. 13. However, the formula ‘mimics’ the specification, provided that the finite sequences are extended to infinite sequences as explained above. FLTL, CTL, CTL* can also be used for creating formulas similar to the LTL formula stated above.

Event-based systems can be modelled as labelled transition systems (LTS) (Magee and Kramer 1999), and these models can be checked by the LTSA tool (Magee and Kramer 1999), based on the properties specified in FLTL. The nature of the models that our analyzer checks is different from the nature of the models that LTSA tool checks: Our analyzer checks a given SCFG (see Section 7.3), which is not an LTS. However, one can transform a SCFG to an LTS, by labelling each edge with the label of the target node. Upon this transformation, one can also perform the verification using the LTSA tool. Nevertheless, LTSA neither can analyze nor transform source code. The combination of our analyzer and transformer is capable of doing these.

Bandera (Corbett et al. 2000) is an integrated collection of analysis tools. Bandera can (a) automatically extract finite-state models from Java code, for the verification of LTL properties, (b) perform the automatic verification, and (c) automatically map counter-examples to Java code. From this perspective, our analyzer is similar to Bandera: Our analyzer can (a) automatically create the SCFG of a given C function (b) automatically perform the verification, (c) enumerate the function calls along a path that is a counter example. Bandera can analyze Java source code but cannot transform it. The combination of our analyzer and transformer can both analyze and transform C code.

We perform static program analysis to verify source code. There is a substantial body of research in static analysis (Ball and Rajamani 2002; Chen and Wagner 2002; Das et al. 2002; Evans et al. 1994; Ashcraft and Engler 2002; Engler et al. 2000; CodeSurfer, http://​www.​grammatech.​com; CodeSonar, http://​www.​grammatech.​com; CoverityPrevent, http://​www.​coverity.​com). This line of research does not focus on source code transformation. Therefore, static analysis and verification tools do not provide mechanisms for specifying events and binding event calls. Consequently, using existing static analysis tools, one cannot solve the problems presented in Section 3.1, at least in the way we solve them.

Interval logic, which is originally introduced by Schwartz et al. (1983), is a type of temporal logic that is specifically designed for expressing abstract requirements that a program must satisfy. Dillon et al. (1994a, b) have recognized the need for graphical languages for expressing interval logic formulas, and they introduced Graphical Interval Logic. Later, Bates (1995) introduced Event-Based Behavioral Abstraction (EBBA) for debugging heterogenous distributed systems. EBBA provides a textual way to express interval logic expressions.

Rosenblum (1991), presents Task Sequencing Language (TSL), which is designed for expressing design constraints on the behavior of concurrent programs. TSL is later evolved in to the architecture description language Rapide (Luckham and Vera 1995), which provides extensive support for event-based specifications of software architectures.

Hendrickson et al. (2005) propose an approach that aids in understanding, debugging, and visualizing the reactive behavior of event-driven systems. This approach can address the problems due to possible mistakes during the evolution of statecharts, which is mentioned as future work in Section 14.4.

In AOP terms, the ETB of a system is scattered (Kiczales et al. 1997) over and tangled (Kiczales et al. 1997) with the implementations of the activities. Hence, the ETB is a crosscutting concern (Kiczales et al. 1997). The event specifications (e.g., the pattern in Fig. 7) correspond to pointcuts (Kiczales et al. 1997), the event points (e.g., the point located after ‘;’ in Line 7, Listing 1) correspond to joinpoints (Filman et al. 2005), the event calls (e.g., preprocessed();) correspond to advices (Kiczales et al. 1997), and the VisuaL specifications in which an event is specified and an event call is bound (e.g., Fig. 7) correspond to aspects (Kiczales et al. 1997). Thus, part of the solution presented in this article exhibits the fundamental characteristics of the AOP technology. Note that our approach and the tools can be used for weaving not only event calls but also arbitrary advice code.

In Section 9.1, we stated that there are 55 events mapped to 102 source code points in the component using which we tested our the solution. Hence, a full-blown application of our solution requires creation of 55 aspects for weaving 102 calls to 55 event functions at 102 joinpoints. That is, 1 aspect needs to be created per 1.9 joinpoints on the average. This means that the ETB of the system is not highly-replicated, in contrast to the classical examples of crosscutting concerns: tracing, parameter checking, etc. By addressing the problems presented in Section 3.1, we have shown a case in which AOP can be useful for improving the evolvability of a crosscutting concern that is not highly-replicated.

Recent research (Aldrich 2005; Sullivan et al. 2005) has raised awareness about the problems of aspect-oriented systems in the context of software evolution. It is argued that seemingly harmless modifications to base code may break the functionality of aspects, which increases the workload of aspect developers, and sometimes makes it infeasible to realize a working system. To address such problems, on one hand Aldrich (2005) proposed to restrict joinpoint models and advising mechanisms. His proposal has been incorporated to AspectJ (http://​www.​eclipse.​org/​aspectj/​) by Ongkingco et al. (2006). On the other hand, (Sullivan et al. 2005) proposed to constrain the implementation of the base programs, so that the aspects can properly function. Our solution follows the latter approach: The compatibility constraints (Section 5) are interface specifications (Sullivan et al. 2005) (or contracts (Beugnard et al. 1999)) that base code developers implement. The analyzer verifies whether these interface specifications (or contracts) are correctly implemented. According to the four levels of contracts proposed by Beugnard et al. (1999), the compatibility constraints can be classified under the third level: “Constraints on the temporal ordering of system services and method calls.”

In a nutshell, a VisuaL specification is a Moore machine-like automaton that generates output strings from an output alphabet, while recognizing regular patterns of input symbols from an input alphabet. Therefore, using VisuaL one can specify history-sensitive pointcuts that can identify function call joinpoints, based on regular patterns of function calls. Hence, VisuaL is related to some of the existing trace-based and history-sensitive approaches (Allan et al. 2005; Douence et al. 2001, 2002, 2004). In these approaches, the state of the pointcut advances only if the encountered input symbol is in the input alphabet. In VisuaL, however, one always explicitly specifies the next state for the symbols that are not in the input alphabet as well. In this respect, our language is similar to MOPS Chen and Wagner (2002). Using this feature, one can naturally express “Function call c ₁ has to come immediately after function call c ₂”, or “Whenever function call c ₁ comes immediately after function call c ₂, weave advice A”.

VisuaL, enables concisely localizing the information about a mandatory event (see Section 6 and Fig. 8). If the existing trace-based languages (Allan et al. 2005; Douence et al. 2001, 2002, 2004) are used however, it is necessary to create at least one declare error (AJ5, http://​www.​eclipse.​org/​aspectj/​) pointcut for the compatibility constraints (e.g., C1 and C2 in Section 5.2), and another one for the event specification. So, the information about a mandatory event would be distributed over multiple pointcuts, in which case conciseness and locality-of-information would be suboptimal.

The programming technique enabled by VisuaL can be considered as concern-shy programming (Lieberherr and Lorenz 2005). The $-labelled arrows (see Figs. 5, 6, 7, and 8) abstract away from the function calls that are not parts of the concerns represented by the VisuaL specifications. In our case, these concerns are either compatibility constraints, or the events of a system.

Property checking and program queries are other applications of trace-based approaches (Douence et al. 2005; Goldsmith et al. 2005; Martin et al. 2005). In these approaches, one writes queries over execution traces of programs, often for detecting errors, flaws, etc. Hence, weaving is not the purpose of these applications. In contrast, our purpose is both weaving additional behavior, and enforcing design rules Sullivan et al. (2005).