Graph Based Verification of Software Evolution Requirements

Due to market demands and changes in the environment, software systems have to evolve. However, the size and complexity of the current software systems make it time consuming to incorporate changes. During our collaboration with the industry, we observed that the developers spend much time on the following evolution problems: designing runtime reconfigurable software, obeying software design constraints while coping with evolution, reusing old software solutions for new evolution problems. This thesis presents 3 processes and tool suits that aid the developers/designers when tackling these problems. The first process and tool set allow early verification of runtime reconfiguration requirements. Runtime reconfiguration is used for tailoring software systems to the customers' needs and to the available hardware. Runtime reconfigurable systems require special attention during the design phase. Especially during evolution one must think about not violating the reconfiguration requirements of the software. Generally, how the software reconfigures itself has to be modeled explicitly in the architectural model. Usually, the verification of the reconfiguration requirements is realized at the implementation phase increasing the development time. We address these problems with a novel process and a tool set for automating the verification of UML models with respect to runtime reconfiguration requirements. In this process, the UML models are converted into a graph-based model. The execution semantics of UML are modeled by graph transformation rules. Using these graph transformation rules and a graph production tool, the execution of the UML models is simulated. The simulation generates a state-space showing all possible reconfigurations of the models. The runtime reconfiguration requirements are expressed by computational tree logic (CTL) or with a visual state-based language (VSL), which is converted into CTL. The state-space is traversed with a verification algorithm for finding the states that satisfy the CTL formula. We also developed two mechanisms to provide error reports when the verification fails: 1) based on tracing the CTL formula to find the location where the formula evaluates to false. 2) based on a control automaton the execution sequence of the reconfiguration is provided (using VSL) and the simulation tries to generate this execution sequence. We conducted experiments/case studies to evaluate the effectiveness of both mechanisms. The second process and tool set are developed for computer aided detection of static program constraint violations. Software artifacts usually have static program constraints and these constraints should be satisfied in each reuse. In addition to this, the developers are also required to satisfy the coding conventions used by their organization. Because in a complex software system there are too many coding conventions and program constraints to be satisfied, it becomes a cumbersome task to check them all manually. Current tools which have been developed to computerize the program constraint violation checking use code querying and/or extensions to type systems. A limitation of these tools is that they work on abstract-syntax trees (ASTs) and do not provide adequate feedback when constraint violation is detected. The AST is at a different level of abstraction than the source code the developer works on, so constraints on program elements visible on the source code that the developers use and are familiar with cannot be verified. We developed a modeling language called Source Code Modeling Language (SCML) in which program elements from the source code can be represented. In the proposed process for constraint violation detection, the source code is converted into SCML models. The constraint detection is realized by graph transformation rules which are also modeled in SCML; the rules detect the violation and extract information from the SCML model of the source code to provide feedback on the location of the problem. This information can be queried from a querying mechanism that automatically searches the graph. The process has been applied to an industrial software system and to an open source software system. The third process and tool set provide computer aided verification whether a design idiom can be used to implement a change request. The developers tend to implement evolution requests using software structures that are familiar to them; we call these structures design idioms. Implementing the design idioms requires the developer to follow a work-flow, which is a step-by-step description to implementing the design idiom. Each step of this work-flow has invariants that are crucial to the correct operation of the idiom and should be implemented. These invariants, however, have constraints that need to be satisfied before they are implemented. Usually, the applicability of a design idiom to a change request is tested manually. In our process, the work-flow for a change idiom is defined, and the invariants of each step are extracted from the existing source code by experts. Because the invariants are extracted from the source code, they may depend on program elements that are only visible at the source code. In addition, these invariants may include such program elements. The SCML meta-model includes these elements, so in this process the source code is converted to models in SCML. The verification of invariants are done over these models. Graph transformations are used for detecting whether the constraints of the invariants are satisfied or not. If the constraints are satisfied, then the transformation rules add the code which implement the invariants. For a given design idiom and given source files, the work-flow is simulated. If all the steps of the work-flow can be executed, then all invariants of the design idioms are implemented in the resulting SCML model. Thus, the models are converted back to source file. If, on the other hand, a step cannot be executed, then the design idiom cannot be applied and the information about the failing step is presented. The approach has been applied to one open source and one industrial software system to show its applicability