Fundamental Approaches to Software Engineering

Service oriented computing (SOC) and service oriented architectures introduce a model for distributed software components. Full inter-component interoperability, based on Web services standards, is a core assumption of the SOC model. SOC, as a platform independent approach to software development and management, is not limited to a particular distributed computing stack (Web services), since the benefits of a distributed component model extend to legacy protocols and platforms as well. Web services has successfully stressed the notion that implementation characteristics should be decoupled from interoperability concerns, and has focused on defining an XML based interoperability stack. SOC is directly concerned with the implementation and management of service oriented applications and stresses the ability to incorporate multiple runtimes and programming models into an architecture of distributed software components.

Software has been evolving from pre-defined, monolithic, centralized architectures to increasingly decentralized, distributed, dynamically composed federations of components. Software processes have been evolving along similar lines, from pre-specified sequential work- flows to decentralized and multi-organization endeavors. The organizations to which software solutions are targeted have also been evolving from highly structured corporates to agile and networked enterprises. All this is affecting the way software is engineered (i.e., conceived, architected, and produced). New difficult challenges arise, while old fundamental problems are still with us. The talk surveys this evolution and tries to identify achievements, challenges, and research directions.

At present, there is a dichotomy of approaches to supporting web service implementation: extending mainstream programming languages with libraries and metadata notations vs. designing new languages. While the former approach has proven suitable for interconnecting services on a simple point-to-point fashion, it turns to be unsuitable for coding concurrent, multi-party, and interrelated interactions requiring extensive XML manipulation. As a result, various web service programming languages have been proposed, most notably (WS-)BPEL. However, these languages still do not meet the needs of highly concurrent and dynamic interactions due to their bias towards statically-bounded concurrency. In this paper we introduce a new web service programming language with a set of features designed to address this gap. We describe the implementations in this language of non-trivial scenarios of service interaction and contrast them to the corresponding BPEL implementations. We also define a formal semantics for the language by translation to the join calculus. A compiler for the language has been implemented based on this semantics.

We develop a formal approach to event-based architectures that serves two main purposes: to characterise the modularisation properties that result from the algebraic structures induced on systems by this discipline of coordination; and to further validate and extend the CommUnity approach to architectural modelling with “implicit invocation”, or “publish/subscribe” interactions. This is a first step towards a formal integration of architectural styles.

Security violations occur in systems even if security design is carried out or security tools are deployed. Social engineering attacks, vulnerabilities that can not be captured in the relatively abstract design model (as buffer-overflows), or unclear security requirements are only some examples of such unpredictable or unexpected vulnerabilities. One of the aims of autonomous systems is to react to these unexpected events through the system itself. Subsequently, this goal demands further research about how such behavior can be designed and sufficiently supported throughout the software development process. We present an approach to engineer self-protection rules for autonomous systems that is integrated into a model-driven software engineering process and provides concepts to formally verify that a given intrusion response model satisfies certain security requirements.

As XML diffusion keeps increasing, it is today common practice for most developers to deal with XML parsing and transformation. XML is used as format to e.g. render data, query documents, deal with Web services, generate code from a model or perform model transformation. Nowadays XSLT is the most common language for XML transformation. But, although meant to be simple, coding in XSLT can become quite a challenge, if the coding approach does not only depend on the structure of the source document, but the order of template application is also dictated by target document structure. This is the case especially when dealing with transformations between visual models. We propose to use a graph-based approach to simplify the transformation definition process where graphs representing documents are transformed in a rule-based manner, as in XSLT. The differences to XSLT are mainly that rules can be developed visually, are more abstract (since the order of execution does not depend on the target document), IDREFs are dealt with much more naturally, and due to typed transformations, the output document is guaranteed to be valid with respect to the target schema. Moreover, graph-based transformation definitions can be automatically reversed in most cases. This is especially useful in model transformation (e.g. in OMG’s MDA approach).

Modern software codebases are frequently large, heterogeneous, and constantly evolving. The languages and tools for software construction, including code builds and configuration management, have not been well-studied. Developers are often faced with using 1) older tools (like make) that do not scale well, 2) custom build scripts that tend to be fragile, or 3) proprietary tools that are not portable.

In this paper, we study the build issue as a domain-specific programming problem. There are a number of challenges that are unique to the domain of build systems. We argue that a central goal is compositionality—that is, it should be possible to specify a software component in isolation and add it to a project with an assurance that the global specification will not be compromised. The next important goal is to cover the full range of complexity—from allowing very concise specifications for the most common cases to providing the flexibility to encompass projects with unusual needs. Dependency analysis, which is a prerequisite for incremental builds, must be automated in order to achieve compositionality an reliability; it also spans the full range of complexity.

We develop a language for describing software builds and configuration. We also develop an implementation (called

OMake

), that addresses all the above challenges efficiently and portably. It also provides a number of features that help streamline the edit/compile development cycle.

OMake

is freely available under the GNU General Public License, and is actively being used in several large projects.

Recent complicated software functions have made it difficult for end users to operate them. Thus, it becomes important to learn how to operate them easily and effectively. Employing a tutorial system is the most suitable approach for learning how to operate software functions. A tutorial system demonstrates the how to operate using the actual software. As a result, end users can learn the usage as if they were actually using the software. However, development of tutorial systems requires much time and costs. Therefore, we propose a method of generating tutorial systems based on use case diagrams, sequence diagrams and test cases. In our method, a generated tutorial system shows function names extracted from use case diagrams, the how to operate along with sequence diagrams, and text string input and item selection using data from test cases. The generated tutorial system is then added to the source code for use in AOP (aspect-oriented programming).

Software project managers use a variety of informal methods to track the progress of development and refine project schedules. Previous formal techniques have generally assumed a constant implementation pace. This is at odds with the experience and intuition of many project managers. We present a simple model for charting the pace of software development and helping managers understand the changing implementation pace of a project. The model was validated against data collected from the implementation of several large projects.

Techniques for inferring a regular language, in the form of a finite automaton, from a sufficiently large sample of accepted and nonaccepted input words, have been employed to construct models of software and hardware systems, for use, e.g., in test case generation. We intend to adapt these techniques to construct state machine models of entities of communication protocols. The alphabet of such state machines can be very large, since a symbol typically consists of a protocol data unit type with a number of parameters, each of which can assume many values. In typical algorithms for regular inference, the number of needed input words grows with the size of the alphabet and the size of the minimal DFA accepting the language. We therefore modify such an algorithm (Angluin’s algorithm) so that its complexity grows not with the size of the alphabet, but only with the size of a certain symbolic representation of the DFA. The main new idea is to infer, for each state, a partitioning of input symbols into equivalence classes, under the hypothesis that all input symbols in an equivalence class have the same effect on the state machine. Whenever such a hypothesis is disproved, equivalence classes are refined. We show that our modification retains the good properties of Angluin’s original algorithm, but that its complexity grows with the size of our symbolic DFA representation rather than with the size of the alphabet. We have implemented the algorithm; experiments on synthesized examples are consistent with these complexity results.

Programmers understand a piece of software by building simplified mental models of it. Aspects of these models lend themselves naturally to formalization – e.g., structural relationships can be partly captured by module dependency graphs. Automated support for generating and analyzing such structural models has proven useful. For event-driven systems, behavioral models, which capture temporal and causal relationships between events, are important and deserve similar methodological and tool support. In this paper, we describe such a technique. Our method supports building and elaboration of behavioral models, as well as maintaining such models as systems evolve. The method is based on model-checking and witness generation, using strategies to create goal-driven simulation traces. We illustrate it on a two-lift/three-floor elevator system, and describe our tool, Sawblade, which provides automated support for the method.

Software containers present an effective mechanism for decoupling cross-cutting concerns in software. System-wide concerns such as persistence, transaction management, security, fault masking, etc., are implemented as container services. While a lot of effort has been expended in developing effective container implementations, specifications for software containers are largely presented in informal natural language, which hampers predictable reasoning about the behavior of components deployed within containers. In this paper, we present a formal model for reasoning about the behavior of software containers. Our model allows developers to reason precisely about how the behaviors of software components deployed within a container are modified by the container. We further present the specifications of a few examples of container services that are found in different container implementations, and use our formal model to prove the correctness of the behavioral transformations that these services cause.

Our research explores the combination of synchronous and asynchronous collaboration tools for global software development. In this paper we assess the impact of tool-mediated inspections to improve requirements negotiation meetings with stakeholders spread over different continents. We present the design of our investigation in an educational environment, in a course where the clients and developers in a software project were in geographically distributed locations. In particular, we studied the usefulness of asynchronous discussions in IBIS tool in enabling more effective requirements negotiations meetings. Our findings indicate that the requirements negotiations were more effective when the groups conducted asynchronous discussions prior to the synchronous negotiation meetings.

The paper describes an approach, which we developed to assess the expected quality of software for a huge governmental system. The assessment was done on behalf of the customer, and not of the development company, and was performed within two years along with the software development process. Our approach was based on a modification to GQM and was focused on the evaluation of the quality of methods and the deliverables of the project. The paper describes the areas of the quality evaluation, the questions that we stated and the metrics that we used. The statistical metrics defined in ISO 9126 appeared not very helpful within the context of this project.

While multiagent systems have been extolled as dynamically configurable and capable of emergent behavior, these qualities can be a drawback. When the system changes so that it no longer achieves its goals, emergent behavior is undesirable. Giving agents the autonomy to adapt and then expecting them to adapt only in acceptable ways requires rigorous design analyses. In this paper, we propose metrics for determining system flexibility at design time. Our approach is based on organization-based multiagent systems, which allows multiagent systems to adapt within a preset structure. We tailored the Bogor model checker to efficiently analyze the adaptive behaviors of these systems and to determine their properties such as fault-tolerance and cost-efficiency. We develop state-space coverage metrics to allow designers to make informed trade-offs at design-time between computational cost and system flexibility.

Problem frames are a sound and convenient approach to requirements modeling. Nevertheless, they are far less popular than other less rigorous approaches. One reason is that they employ a notation that is neither very appealing nor easy to use. The problem frames notation is sufficiently different from other development languages –especially UML– to create an “impedance mismatch”: using problem frames to describe requirements does not help the transition to the design phase, makes it difficult for programmers to fully comprehend requirements, and does not favor traceability. As a consequence, problem frames are rarely adopted in software development processes employing UML as a design language. UML itself provides a linguistic support for requirements modeling, which however suffers from several limitations, especially as far as precision and formality are concerned.

The goal of this paper is to combine problem frames and UML in order to both improving the linguistic support for problem frames –while preserving the underlying concepts– and to improve the UML development practice by introducing the problem frames approach, making it seamlessly applicable in the context of the familiar UML language.

The benefits of design patterns are well-established. We argue that these benefits can be further amplified across the system lifecycle. We present two contributions. First, we describe an approach to complementing existing informal pattern descriptions with precise pattern specifications. Our specification language captures the properties common across all applications of a pattern, while accommodating the variation that occurs across those applications. Second, we describe an approach to monitoring a system’s runtime behavior to determine whether the appropriate pattern specifications are respected. The monitoring code is generated automatically from the pattern specifications underlying the system’s design. We conclude with a discussion of how our contributions are beneficial across the software lifecycle.

The Life Sequence Chart (LSC) language is a conservative extension of the well-known visual formalism of Message Sequence Charts. An LSC specification formally captures requirements on the inter-object behaviour in a system as a set of scenarios. As with many languages, there are LSCs which are syntactically correct but insatisfiable due to internal contradictions. The authors of the original publication on LSCs avoid this problem by restricting their discussion to well-formed LSCs, i.e. LSCs that induce a partial order on their elements.

This abstract definition is of limited help to authors of LSCs as they need guidelines how to write well-formed LSCs and fast procedures that check for the absence of internal contradictions. To this end we provide an exact characterisation of well-formedness of LSCs in terms of concrete syntax as well as in terms of the semantics-giving automata. We give a fast graph-based algorithm to decide well-formedness. Consequently we can confirm that the results on the complexity of a number of LSC problems recently obtained for the subclass of well-formed LSCs actually hold for the set of all LSCs.

The separation of concerns, as a conceptual tool, enables us to manage the complexity of the software systems that we develop. There have been a number of approaches aimed at modularizing software around the natural boundaries of the various concerns, including subject-oriented programming, composition filters, aspect-oriented programming, and our own view-oriented programming. The growing body of experiences in using these approaches has identified a number of fundamental issues such as what is a concern, what is an aspect, which concerns are inherently separable, and which aspects are composable. To address these issues, we need to focus on the semantics of separation of concerns, as opposed to the mechanics (and semantics) of aspect-oriented software development methods. We propose a conceptual framework based on a transformational view of software development. Our framework affords us a unified view of the different aspect-oriented development techniques which enables us a simple expression for the separability issue.

In Model-Driven Engineering, a software development process is a sequence of manipulation tasks that are applied to models, where model transformations play a relevant role. MOMENT (MOdel manageMENT) is a framework that is integrated in the Eclipse platform. MOMENT provides a collection of generic set-oriented operators to manipulate EMF models. In this paper, we present the model transformation mechanism that is embodied by the

ModelGen

operator. This operator uses the term rewriting system Maude as transformation engine and provides support for traceability.

ModelGen

has been defined in an algebraic specification so that we can use formal tools to reason about transformation features, such as termination and confluence. Furthermore, its application to EMF models shows that formal methods can be applied to industrial modeling tools in an efficient way. Finally, we indicate how the

ModelGen

operator provides support for the QVT Relations language in the MOMENT Framework.

Detecting and localizing a fault within a program is a non-trivial and time consuming task. Most of the efforts spent for automating the task have focused on fault detection. In this paper we shift the focus on fault localization. We introduce a resolution calculus that allows for representing the program’s behavior based on correctness assumptions. The fault localization task is reduced to finding consistent assumptions which are represented as a non-monotonic reasoning process where efficient algorithms exist. Finally, we compare our approach with a previous approach to fault localization that is based on trace analysis. As a result we can show that our approach is less sensitive to search assumptions.

Component-Based Development (CBD) is an effective approach to develop software effectively and economically through reuse of software components. Model Driven Architecture (MDA) is a new software development paradigm where software is generated by a series of model transformations. By combing essential features of CBD and MDA, both benefits of software reusability and development automation can be achieved in a single framework. In this paper, we propose a UML profile for specifying component-based design in MDA framework. The profile consists of UML extensions, notations, and related instructions to specify elements of CBD in MDA constructs. Once components are specified with our profile at the level of PIM, they can be automatically transformed into PSM and eventually source code implementation.

Statistical debugging is a powerful technique for identifying bugs that do not violate programming rules or program invariants. Previously known statistical debugging techniques are offline bug isolation (or localization) techniques. In these techniques, the program dumps data during its execution, which is used by offline statistical analysis to discover differences in passing and failing executions. The differences identify potential bug sites. Offline techniques suffer from three limitations: (i) a large number of executions are needed to provide data, (ii) each execution must be labelled as passing or failing, and (iii) they are postmortem techniques and therefore cannot raise an alert at runtime when a bug symptom occurs. In this paper, we present an

online statistical bug detection

tool called Argus. Argus constructs statistics at runtime using a

sliding window

over the program execution, is capable of detecting bugs in a single execution and can raise an alert at runtime when bug symptoms occur. Moreover, it eliminates the requirement for labelling all executions as passing or failing. We present experimental results using the Siemens bug benchmark showing that Argus is effective in detecting 102 out of 130 bugs. We introduce optimization techniques that greatly improve Argus’ detection power and control the false alarm rate when a small number of executions are available. Argus generates more precise bug reports than the best known bug localization techniques.

Fault-based testing is a technique where testers anticipate errors in a system under test in order to assess or generate test cases. The idea is to have enough test cases capable of detecting these anticipated errors. This paper presents a theory and technique for generating fault-based test cases for concurrent systems. The novel idea is to generate test purposes from faults that have been injected into a model of the system under test. Such test purposes form a specification of a more detailed test case that can detect the injected fault. The theory is based on the notion of refinement. The technique is automated using the TGV test case generator and an equivalence checker of the CADP tools. A case study of testing web servers demonstrates the practicability of the approach.

We present an algorithm for automatic testing of distributed programs, such as Unix processes with inter-process communication, Web services, etc. Specifically, we assume that a program consists of a number of asynchronously executing concurrent processes or actors which may take data inputs and communicate using asynchronous messages. Because of the large numbers of possible data inputs as well as the asynchrony in the execution and communication, distributed programs exhibit very large numbers of potential behaviors. Our goal is two fold: to execute all reachable statements of a program, and to detect deadlock states. Specifically, our algorithm uses simultaneous concrete and symbolic execution, or

concolic execution

, to explore all distinct behaviors that may result from a program’s execution given different data inputs and schedules. The key idea is as follows. We use the symbolic execution to generate data inputs that may lead to alternate behaviors. At the same time, we use the concrete execution to determine, at runtime, the partial order of events in the program’s execution. This enables us to improve the efficiency of our algorithm by avoiding many tests which would result in equivalent behaviors. We describe our experience with a prototype tool that we have developed as a part of our Java program testing tool jCUTE.

This paper describes the application of the Real-Time Maude tool to the formal specification and analysis of the CASH scheduling algorithm and its suggested modifications. The CASH algorithm is a sophisticated state-of-the-art scheduling algorithm with advanced capacity sharing features for reusing unused execution budgets. Because the number of elements in the queue of unused resources can grow beyond any bound, the CASH algorithm poses challenges to its formal specification and analysis. Real-Time Maude extends the rewriting logic tool Maude to support formal specification and analysis of object-based real-time systems. It emphasizes generality of specification and supports a spectrum of analysis methods, including symbolic simulation and (unbounded and time-bounded) reachability analysis and LTL model checking. We show how we have used Real-Time Maude to experiment with different design modifications of the CASH algorithm using both Monte Carlo simulation and reachability analysis. We could quickly and easily specify and analyze these modifications using Real-Time Maude, and discovered subtle behaviors in the modifications that lead to missed deadlines.

We present a tool for verifying temporal properties on Java/ JML classes by generating automatically JML annotations that ensure the verification of the temporal properties.

In this tool demonstration we present the LearnLib, a library for automata learning and experimentation. Its modular structure allows users to configure their tailored learning scenarios, which exploit specific properties of the envisioned applications. As has been shown earlier, exploiting application-specific structural features enables optimizations that may lead to performance gains of several orders of magnitude, a necessary precondition to make automata learning applicable to realistic scenarios.

The demonstration of the LearnLib will include the extrapolation of a behavioral model for a realistic (legacy) system, and the statistical analysis of different variants of automata learning algorithms on the basis of random generated models.

One of the major costs of software development is associated with testing and validation of successive versions of software systems. An important problem encountered in testing and validation is memory aliasing, which involves correlation of variables across program versions. This is useful to ensure that existing invariants are preserved in newer versions and to match program execution histories. Recent work in this area has focused on trace-based techniques to better isolate affected regions. A variation of this general approach considers memory operations to generate more refined impact sets. The utility of such an approach eventually relies on the ability to effectively recognize aliases.

In this paper, we address the general memory aliasing problem and present a probabilistic trace-based technique for correlating memory locations across execution traces, and associated variables in program versions. Our approach is based on computing the

log-odds ratio

, which defines the affinity of locations based on observed patterns. As part of the aliasing process, the traces for initial test inputs are aligned without considering aliasing. From the aligned traces, the log-odds ratio of the memory locations is computed. Subsequently, aliasing is used for alignment of successive traces. Our technique can easily be extended to other applications where detecting aliasing is necessary. As a case study, we implement and use our approach in dynamic impact analysis for detecting variations across program versions. Using detailed experiments on real versions of software systems, we observe significant improvements in detection of affected regions when aliasing occurs.

In this research, we investigate the role of common coupling in evolving software systems. It can be argued that most software developers understand that the use of global data has many harmful side-effects, and thus should be avoided. We are therefore interested in the answer to the following question: if global data does exist within a software project, how does global data usage evolve over a software project’s lifetime? Perhaps the constant refactoring and perfective maintenance eliminates global data usage, or conversely, perhaps the constant addition of features and rapid development introduce an increasing reliance on global data? We are also interested in identifying if global data usage patterns are useful as a software metric that is indicative of an interesting or significant event in the software’s lifetime.

The focus of this research is twofold: first to develop an effective and automatic technique for studying global data usage over the lifetime of large software systems and secondly, to leverage this technique in a case-study of global data usage for several large and evolving software systems in an effort to reach answers to these questions.

Code clones have long been recognized as bad smells in software systems and are considered to cause maintenance problems during evolution. It is broadly assumed that the more clones two files share, the more often they have to be changed together. This relation between clones and change couplings has been postulated but neither demonstrated nor quantified yet. However, given such a relation it would simplify the identification of restructuring candidates and reduce change couplings. In this paper, we examine this relation and discuss if a correlation between code clones and change couplings can be verified. For that, we propose a framework to examine code clones and relate them to change couplings taken from release history analysis. We validated our framework with the open source project Mozilla and the results of the validation show that although the relation is statistically unverifiable it derives a reasonable amount of cases where the relation exists. Therefore, to discover clone candidates for restructuring we additionally propose a set of metrics and a visualization technique. This allows one to spot where a correlation between cloning and change coupling exists and, as a result, which files should be restructured to ease further evolution.