Modern Integrated Development Environments (IDEs) offer automated refactorings to aid programmers in developing and maintaining software. However, implementing sound automated refactorings is challenging, as refactorings may inadvertently introduce name-binding errors or cause references to resolve to incorrect declarations. To address these issues, previous work by Schäfer et al. proposed replacing concrete references with locked references to separate binding preservation from transformation. Locked references vacuously resolve to a specific declaration, and after transformation must be replaced with concrete references that also resolve to that declaration. Synthesizing these references requires a faithful inverse of the name lookup functions of the underlying language. Manually implementing such inverse lookup functions is challenging due to the complex name-binding features in modern programming languages. Instead, we propose to automatically derive this function from type system specifications written in the Statix meta-DSL. To guide the synthesis of qualified references we use scope graphs , which represent the binding structure of a program, to infer their names and discover their syntactic structure. We evaluate our approach by synthesizing concrete references for locked references in 2528 Java, 196 ChocoPy, and 49 Featherweight Generic Java test programs. Our approach yields a principled languageparametric method for synthesizing references.

For software maintenance and evolution, insight into the codebase is crucial. One way to enhance insight is the application of static analysis to extract and visualize program-specific relations from the code itself, such as call graphs and inheritance trees. Yet, software often contains in-house libraries: unique, domain-specific libraries whose usage is typically scattered throughout the codebase. To provide sufficient insight into the usage of those libraries, the static analysis must be customized with domain-specific information. In this paper, we propose a method to enhance insight into the usage of in-house libraries by producing custom overviews. Furthermore, we describe three exploratory case studies targeting industrial C++ and Ada codebases, in which the method was developed, evolved, and validated. The method prescribes how to create custom overviews using static analysis iteratively, starting from a user-provided, initial specification of proper library usage using code patterns. As a safeguard, the method includes cross-checks to detect code fragments that deviate from proper library usage. Whenever such a deviating library usage is found, the code owners determine whether that deviating library usage should be added to the specification of proper library usage or the code fragment should be made compliant. The latter alternative makes both the codebase more regular and keeps the custom static analysis simpler. The method creates custom overviews that reveal opportunities to improve the usage of the in-house libraries, e.g., the removal of domain-specific redundant code which cannot be detected using generic tools, such as compilers and linters. We observed that industrial codebases are regular enough to create custom overviews using static analysis in the three exploratory case studies. Furthermore, we observed that the cross-checks, which detect deviating library usage, ensure the validity and completeness of the custom overviews. We conclude that producing custom overviews for in-house libraries using the method is valuable and feasible.

In the last couple of years several dynamically-typed, object-oriented programming languages have been equipped with optional static type checkers. This typically requires these languages to be extended with a downcast operator, which is a common operator in statically-typed languages but not in dynamically-typed languages. Our objective is to investigate an approach for static type checking of object-oriented languages that does not require such an additional downcast operator. We systematically weaken the rules for static type checking to avoid reporting errors that can be resolved using downcast operators. This leads to an approach similar to quasi-static typing that enables to make type annotations stricter in a gradual way. These static type checking rules can be applied to dynamically-typed languages by interpreting the dynamic type as the top of the subtype relation. Based on these ideas we have implemented a static type checker for the dynamically-typed, object-oriented language POOSL without introducing a downcast operator. Practical experiences with this type checker indicate that it is useful for early validation.

Over time, software tends to grow more complex, hampering understandability and further development. To reduce accidental complexity, model-based rejuvenation techniques have been proposed. These techniques combine reverse engineering (extracting models) with forward engineering (generating code). Unfortunately, model extraction can be error-prone, and validation can often only be performed at a late stage by testing the generated code. We intend to mitigate the aforementioned challenges, making model-based rejuvenation more controlled. We describe an exploratory case study that aims to rejuvenate an industrial embedded software component implementing a nested state machine. We combine two techniques. First, we develop and apply a series of small, automated, case-specific code refactorings that ensure the code (a) uses well-known programming idioms, and (b) easily maps onto the type of model we intend to extract. Second, we perform model-based rejuvenation focusing on the high-level structure of the code. The above combination of techniques gives ample opportunity for early validation, in the form of code reviews and testing, as each refactoring is performed directly on the existing code. Moreover, aligning the code with the type of model we intend to extract significantly simplifies the extraction, making the process less error-prone. Hence, we consider code refactoring to be a useful stepping stone towards model-based rejuvenation.

When software components are developed iteratively, code frequently evolves in an inductive manner: a unit (class, method, etc.) is created and is then copied and modified many times. Such development often happens when variation points and, hence, proper domain abstractions are initially unclear. As a result, there may be substantial amounts of code duplication, and the code may be difficult to understand and maintain, warranting a redesign. We apply a model-based process to semi-automatically redesign an inductively-evolved industrial adapter component written in C++: we use reverse engineering to obtain models of the component, and generate redesigned code from the models. Based on our experience, we propose to use three models to help recover understanding of inductively-evolved components, and transform the components into redesigned implementations. Guided by a reference design, a component's code is analyzed and a legacy model is extracted that captures the component's functionality in a form close to its original structure. The legacy model is then unfolded, creating a flat model which eliminates design decisions by focusing on functionality in terms of external interfaces. Analyzing the variation points of the flat model yields a redesigned model and fresh domain abstractions to be used in the new design of the component.

The high-tech industry is faced with ever growing amounts of software to be maintained and extended. To keep the associated costs under control, there is a demand for more human overview and for large-scale code restructurings. Language technology such as parsing can assist in this, but classical restructuring tools are typically not flexible enough to accommodate the needs of specific cases. In our research we investigate ways to make software restructuring tools customizable by software developers at Thermo Fisher Scientific as well as at other high-tech companies. We report on an industry-as-lab project, in which we have collaborated on cleaning up the compilation of COM interfaces of a large industrial software component. As a generic result, we have identified a method that we call model-based software restructuring. The approach taken is to extract high-level models from the code, use these to specify and visualize the restructuring, which is then translated into low-level code transformations. To implement this approach, we integrate generic technology to develop custom solutions. We aim for semiautomation and incrementally automate recurring restructuring patterns. The COM clean-up affected 72 type libraries and 1310 client projects with (one or more) dependencies on these type libraries. We have addressed these one type library at a time, and delivered all changes without blocking regular software development. Software developers in neighboring projects immediately noticed the very low defect rate of our restructuring. Moreover, as a spin-off, we have observed that the developed tools also start to contribute to regular software development.

Abstract A domain specific language (DSL) focuses on the essential concepts in a specific problem domain, and abstracts from low-level implementation details. The development of DSLs usually centers around the meta-model, grammar and code generator, possibly extended with transformations to analysis models. Typically, little attention is given to the formal semantics of the language, whereas this is essential for reasoning about DSL models, and for assessing the correctness of the generated code and analysis models. We argue that the semantics of a DSL should be defined explicitly and independently of any code generator, to avoid all kinds of complexities from low-level implementation details. As the generated analysis models must reflect some of these implementation details, we propose to formalize them separately. To assess the correctness and consistency of the generated code and analysis models in a practical way, we use conformance testing. We extensively illustrate this general approach using specific formalizations for an industrial DSL on collision prevention. We do not aim for a generic semantic model for any DSL, but this specific DSL indicates the potential of a modular semantics to facilitate reuse among DSLs.

Service-oriented computing aims to create complex systems by composing less-complex systems, called services. Since services can be developed independently, the integration of services requires an adaptation mechanism for bridging any incompatibilities. Behavioral adapters aim to adjust the communication between some services to be composed in order to establish proper interaction between them. We present a novel approach for specifying such adapters, based on domain-specific transformation rules that reflect the elementary operations that adapters can perform. We also present a novel way to synthesize complex adapters that adhere to these rules, viz., by consistently separating data and control, and by using existing controller-synthesis algorithms. Our approach has been implemented, and we discuss some example applications, including real business processes in WS-BPEL.

Process mining techniques can be used to effectively discover process models from logs with example behaviour. Cross-correlating a discovered model with information in the log can be used to improve the underlying process. However, existing process discovery techniques have two important drawbacks. The produced models tend to be large and complex, especially in flexible environments where process executions involve multiple alternatives. This “overload” of information is caused by the fact that traditional discovery techniques construct procedural models explicitly showing all possible behaviours. Moreover, existing techniques offer limited possibilities to guide the mining process towards specific properties of interest. These problems can be solved by discovering declarative models. Using a declarative model, the discovered process behaviour is described as a (compact) set of rules. Moreover, the discovery of such models can easily be guided in terms of rule templates. This paper uses DECLARE, a declarative language that provides more flexibility than conventional procedural notations such as BPMN, Petri nets, UML ADs, EPCs and BPEL. We present an approach to automatically discover DECLARE models. This has been implemented in the process mining tool ProM. Our approach and toolset have been applied to a case study provided by the company Thales in the domain of maritime safety and security.

Abstract We explore the applicability of the programming method of Feijen and van Gasteren to the domain of security protocols. This method addresses the derivation of concurrent programs from a formal specification, and it is based on common notions like invariants and pre- and post-conditions. We show that fundamental security concepts like secrecy and authentication can nicely be specified in this way. Using some small extensions, the style of formal reasoning from this method can be applied to the security domain. To demonstrate our approach, we discuss an authentication protocol and a public-key distribution protocol, and we deal with their composition. By focussing on a general setting where agents run the protocols multiple times, the nonce concept turns out to pop-up naturally. Although this work does not contain any new protocols, it does offer a new view on reasoning about security protocols.

Abstract The logic of Owicki and Gries is a well-known logic for verifying safety properties of concurrent programs. Using this logic, Feijen and van Gasteren describe a method for deriving concurrent programs based on safety. In this work, we explore derivation techniques of concurrent programs using progress-based reasoning. We use a framework that combines the safety logic of Owicki and Gries, and the progress logic of UNITY. Our contributions improve the applicability of our earlier techniques by reducing the calculational overhead in the formal proofs and derivations. To demonstrate the effectiveness of our techniques, a derivation of Dekker’s mutual exclusion algorithm is presented. This derivation leads to the discovery of some new and simpler variants of this famous algorithm.