Artificial intelligence (AI) assistants such as GitHub Copilot and ChatGPT, built on large language models like GPT-4, are revolutionizing how programming tasks are performed, raising questions about whether code is authored by generative AI models. Such questions are of particular interest to educators, who worry that these tools enable a new form of academic dishonesty, in which students submit AI-generated code as their work. Our research explores the viability of using code stylometry and machine learning to distinguish between GPT-4 generated and human-authored code. Our dataset comprises human-authored solutions from CodeChef and AI-authored solutions generated by GPT-4. Our classifier outperforms baselines, with an F1-score and AUC-ROC score of 0.91. A variant of our classifier that excludes gameable features (e.g., empty lines, whitespace) still performs well with an F1-score and AUC-ROC score of 0.89. We also evaluated our classifier on the difficulty of the programming problem and found that there was almost no difference between easier and intermediate problems, and the classifier performed only slightly worse on harder problems. Our study shows that code stylometry is a promising approach for distinguishing between GPT-4 generated code and human-authored code.

Analyses of a software product line (SPL) model typically report variable results annotated with logical expressions to indicate the set of products for which each result holds. These expressions can be complicated and difficult to reason about when the SPL has lots of features and derivable products. In previous work, we introduced Neo4j Browser, a visualizer for graphical analysis results that highlights the results that apply to specific products. In this paper, we report on a controlled user study that evaluates the visualizer's effectiveness in helping the user (1) understand variable analysis results and (2) compare the analysis results of multiple products. Our findings suggest significant improvements in efficiency (30%), and correctness (22%), and significant reductions in cognitive load (42%).

Test cases use assertions to check program behaviour. While these assertions may not be complex, they are themselves code that must be written correctly in order to determine whether a test case should pass or fail. We claim that most test assertions are relatively repetitive and straight-forward, making their construction well suited to automation and that this automation can reduce developer effort while improving assertion quality. Examining 33,873 assertions from 105 projects revealed that developer-written assertions fall into twelve high-level categories, confirming that the vast majority ($>$90%) of test assertions are fairly simple in practice. We created AutoAssert, a human-in-the-loop tool to fit naturally into a developer's test-writing workflow by automatically generating assertions for JavaScript and TypeScript test cases. A developer invokes AutoAssert by identifying the variable they want validated; AutoAssert uses dynamic analysis to generate assertions relevant for this variable and its runtime values, injecting the assertions into the test case for the developer to accept, modify, delete. Comparing AutoAssert's assertions to those written by developers, we found that the assertions generated by AutoAssert are the same kind of assertion as was written by developers 84% of the time in a sample of over 1,000 assertions. Additionally we validated the utility of AutoAssert-generated assertions with 17 developers who found the majority of generated assertions to be useful and expressed considerable interest in using such a tool for their own projects.

Software Product Lines (SPLs) are families of related software products developed from a common set of artifacts. Most existing analysis tools can be applied to a single product at a time, but not to an entire SPL. Some tools have been redesigned/re-implemented to support the kind of variability exhibited in SPLs, but this usually takes a lot of effort, and is error-prone. Declarative analyses written in languages like Datalog have been collectively lifted to SPLs in prior work [1], which makes the process of applying an existing declarative analysis to a product line more straightforward. In this paper, we take an existing declarative analysis (behaviour alteration) and apply it to a set of automotive software product lines from General Motors. We discuss the design of the analysis pipeline used in this process, present its scalability results, and provide a means to visualize the analysis results for a subset of products filtered by feature expression. We also reflect on some of the lessons learned throughout this project.

There is a large body of research on extracting models from code-related artifacts to enable model-based analyses of large software systems. However, engineers do not always have access to the entire code base of a system: some components may be procured from third-party suppliers based on a Model specification or their code may be generated automatically from Models.

Model-Driven Engineering has been proposed to increase the productivity of developing a software system. Despite its benefits, it has not been fully adopted in the software industry. Research has shown that modelling tools are amongst the top barriers for the adoption of MDE by industry. Recently, researchers have conducted empirical studies to identify the most-severe cognitive difficulties of modellers when using UML model editors. Their analyses show that users' prominent challenges are in remembering the contextual information when performing a particular modelling task; and locating, understanding, and fixing errors in the models. To alleviate these difficulties, we propose two Focus+Context user interfaces that provide enhanced cognitive support and automation in the user's interaction with a model editor. Moreover, we conducted two empirical studies to assess the effectiveness of our interfaces on human users. Our results reveal that our interfaces help users 1) improve their ability to successfully fulfil their tasks, 2) avoid unnecessary switches among diagrams, 3) produce more error-free models, 4) remember contextual information, and 5) reduce time on tasks.

Feature-oriented software development enables rapid software creation and evolution, through incremental and parallel feature development or through product line engineering. However, in practice, features are often not separate concerns. They behave differently in the presence of other features, and they sometimes interfere with each other in surprising ways.

Modern automotive software systems are large, complex, and feature rich; they can contain over 100 million lines of code, comprising hundreds of features distributed across multiple electronic control units (ECUs), all operating in parallel and communicating over a CAN bus. Because they are safety-critical systems, the problem of possible Feature Interactions (FIs) must be addressed seriously; however, traditional detection approaches using dynamic analyses are unlikely to scale to the size of these systems. We are investigating an approach that detects static source-code patterns that are symptomatic of FIs. The tools report Feature-Interaction warnings, which can be investigated further by engineers to determine if they represent true FIs and if those FIs are problematic. In this paper, we present our preliminary toolchain for FI detection. First, we extract a collection of static “facts” from the source code, such as function calls, variable assignments, and messages between features. Next, we perform relational algebra transformations on this factbase to infer additional “facts” that represent more complicated design information about the code, such as potential information flows and data dependencies; then, the full collection of “facts” is matched against a curated set of patterns for FI symptoms. We present a set of five patterns for FIs in automotive software as well a case study in which we applied our tools to the Autonomoose autonomous-driving software, developed at the University of Waterloo. Our approach identified 1,444 possible FIs in this codebase, of which 10% were classified as being probable interactions worthy of further investigation.

Software modelling is a challenging and error-prone task. Existing Model-Driven Engineering (MDE) tools provide modellers with little aid, partly because tool providers have not investigated users' difficulties through empirical investigations such as field studies. This paper presents the results of a two-phase user study to identify the most prominent difficulties that users might face when developing UML Class and State-Machine diagrams using UML modelling tools. In the first phase, we identified the preliminary modelling challenges by analysing 30 Class and State-Machine models that were previously developed by students as a course assignment. The result of the first phase helped us design the second phase of our user study where we empirically investigated different aspects of using modelling tools: the tools' effectiveness, users' efficiency, users' satisfaction, the gap between users' expectation and experience, and users' cognitive difficulties. Our results suggest that users' greatest difficulties are in (1) remembering contextual information and (2) identifying and fixing errors and inconsistencies.

Systems that are assembled from independently developed features suffer from feature interactions, in which features affect one another's behaviour in surprising ways. The Feature Interaction Problem results from trying to implement an appropriate resolution for each interaction within each possible context, because the number of possible contexts to consider increases exponentially with the number of features in the system. Resolution strategies aim to combat the Feature Interaction Problem by offering default strategies that resolve entire classes of interactions, thereby reducing the work needed to resolve lots of interactions. However most such approaches employ coarse-grained resolution strategies (e.g., feature priority) or a centralized arbitrator.

A software product line is a family of software products that share a common set of mandatory features and whose individual products are differentiated by their variable (optional or alternative) features. Family-based analysis of software product lines takes as input a single model of a complete product line and analyzes all its products at the same time. As the number of products in a software product line may be large, this is generally preferable to analyzing each product on its own. Family-based analysis, however, requires that standard algorithms be adapted to accomodate variability.

In this paper, we present a technique for incremental and commutative composition of state-machine models of features, using the Feature House framework. The inputs to Feature House are feature state-machines (or state-machine fragments) modelled in a feature-oriented requirement modelling language called FORML and the outputs are two state-machine models: (1) a model of the whole product line with optional features guarded by presence conditions, this model is suitable for family-based analysis of the product line, and (2) an intermediate model of composition that facilitates incremental composition of future features. We discuss the challenges and benefits of our approach and our implementation in the Feature House.

Product line (PL) engineering promotes the development of families of related products, where individual products are differentiated by which optional features they include. Modelling and analyzing requirements models of PLs allows for early detection and correction of requirements errors -- including unintended feature interactions, which are a serious problem in feature-rich systems. A key challenge in analyzing PL requirements is the efficient verification of the product family, given that the number of products is too large to be verified one at a time. Recently, it has been shown how the high-level design of an entire PL, that includes all possible products, can be compactly represented as a single model in the SMV language, and model checked using the NuSMV tool. The implementation in NuSMV uses BDDs, a method that has been outperformed by SAT-based algorithms. In this paper we develop PL model checking using two leading SAT-based symbolic model checking algorithms: IMC and IC3. We describe the algorithms, prove their correctness, and report on our implementation. Evaluating our methods on three PL models from the literature, we demonstrate an improvement of up to 3 orders of magnitude over the existing BDD-based method.

Multi-Objective Combinatorial Optimization (MOCO) is fundamental to the development and optimization of software systems. We propose five novel parallel algorithms for solving MOCO problems exactly and efficiently. Our algorithms rely on off-the-shelf solvers to search for exact Pareto-optimal solutions, and they parallelize the search via collaborative communication, divide-and-conquer, or both. We demonstrate the feasibility and performance of our algorithms by experiments on three case studies of software-system designs. A key finding is that one algorithm, which we call FS-GIA, achieves substantial (even super-linear) speedups that scale well up to 64 cores. Furthermore, we analyze the performance bottlenecks and opportunities of our parallel algorithms, which facilitates further research on exact, parallel MOCO.

Systems assembled from independently developed features suffer from feature interactions, in which features affect one another's behaviour in surprising ways. The feature-interaction problem states that the number of potential interactions is exponential in the number of features in a system. Resolution strategies offer general strategies that resolve entire classes of interactions, thereby reducing the work of the developer who is charged with the task of resolving interactions. In this paper, we focus on resolving interactions due to conflict. We present an approach, language, and implementation based on resolution modules in which the developer can specify an appropriate resolution for each variable under conflict. We performed a case study involving 24 automotive features, and found that the number of resolutions to be specified was much smaller than the number of possible feature interactions (6 resolutions for 24 features), that what constitutes an appropriate resolution strategy is different for different variables, and that the subset of situation calculus we used was sufficient to construct nontrivial resolution strategies for six distinct output variables.

A software product line (SPL) is often constructed as a set of features, such that individual products can be assembled from a set of common features and a selection of optional features. Although features are conceptualized, developed, and evolved as separate concerns, it is often the case that, in practice, they interfere with each other -- called a feature interaction. In this paper, we precisely define what it means for one feature to have a behaviour interaction with another feature, where the behaviour of one feature is affected by the presence of another feature. Specifically, we use a form of bisimilarity to define when the behaviour of a feature in isolation differs from its behaviour in the presence of an interacting feature. We also consider the case where features are modelled in a language that allows the specification of intended interactions, and we adapt our use of bisimilarity to provide a formal definition for unintended behaviour interactions.

Models are an important tool in conquering the increasing complexity of modern software systems. Key industries are strategically directing their development environments towards more extensive use of modeling techniques. This workshop sought to understand, through critical analysis, the current and future uses of models in the engineering of software-intensive systems. The MISE-workshop series has proven to be an effective forum for discussing modeling techniques from the MDD and the software engineering perspectives. An important goal of this workshop was to foster exchange between these two communities. The 2013 Modeling in Software Engineering (MiSE) workshop was held at ICSE 2013 in San Francisco, California, during May 18–19, 2013. The focus this year was analysis of successful applications of modeling techniques in specific application domains to determine how experiences can be carried over to other domains. Details are available at: https://sselab.de/lab2/public/wiki/MiSE/index.php.

In this paper, we propose a pattern for decomposing and structuring the model of a feature's behavioural requirements, based on modes of operation (e.g., Active, Inactive, Failed) that are common to features in multiple domains. Interestingly, the highest-level modes of the pattern can serve as a generic behavioural interface for all features that adhere to the pattern. We have applied the pattern in modelling the behavioural requirements of 19 automotive features that were specified in 5 production-grade requirements documents. We found that the pattern was applicable to all 19 features, and that our proposed generic feature interface was applicable to 50 out of 57 inter-feature references.

FMSPLE 2013 is the fourth edition of the FMSPLE workshop series aimed at connecting researchers and practitioners interested in raising the efficiency and the effectiveness of software product line engineering through the application of innovative analysis approaches and formal methods.

In this paper, we present a feature-oriented requirements modelling language (FORML) for modelling the behavioural requirements of a software product line. FORML aims to support feature modularity and precise requirements modelling, and to ease the task of adding new features to a set of existing requirements. In particular, FORML decomposes a product line's requirements into feature modules, and provides language support for specifying tightly-coupled features as model fragments that extend and override existing feature modules. We discuss how decisions in the design of FORML affect the evolvability of requirements models, and explicate the specification of intended interactions among related features. We applied FORML to the specification of two feature sets, automotive and telephony, and we discuss how well the case studies exercised the language and how the requirements models evolved over the course of the case studies.

The papers in this special section contain extended versions of selected papers from the 31st ACM/IEEE International Conference on Software Engineering (ICSE), held 20-22 May 2009 in Vancouver, British Columbia, Canada.

The output of a code generator is assumed to be correct and not usually intended to be read or modified; yet programmers are often interested in this, e.g., to monitor a system property. Here, we consider code customization for a family of code generators associated with big-step executable modelling languages (e.g., statecharts). We introduce a customization language that allows us to express customization scenarios for the generated code independently of a specific big-step execution semantics. These customization scenarios are all different forms of runtime monitors, which lend themselves to a principled, uniform implementation for observation and code extension. A monitor is given in terms of the enabledness and execution of the transitions of a model and a reachability relation between two states of the execution of the model during a big step. For each monitor, we generate the aspect code that is incorporated into the output of a code generator to implement the monitor at the generated-code level. Thus, we provide means for code analysis through using the vocabulary of a model, rather than the detail of the generated code. Our technique not only requires the code generators to reveal only limited information about their code generation mechanisms, but also keeps the structure of the generated code intact. We demonstrate how various useful properties of a model, or a language, can be checked using our monitors.

In this paper, we introduce a model-checking-based certification technique called search-carrying code (SCC). SCC is an adaptation of the principles of proof-carrying code, in which program certification is reduced to checking a provided safety proof. In SCC, program certification is an efficient re-examination of a program's state space. A code producer, who offers a program for use, provides a search script that encodes a search of the program's state space. A code consumer, who wants to certify that the program fits her needs, uses the search script to direct how a model checker searches the program's state space.

Software model checking is the process of systematically exploring a program's state space to find hard-to-discover errors. Because of the exponential size of the state space, an exhaustive search of the state space is often impossible given the memory resources. In such cases, an estimate of how much of the state space is covered can help the verifier to decide whether to employ additional computational resources or to use more aggressive abstraction techniques. Our work focuses on coverage estimation for explicit-state model checking of software programs. In this paper, we present an estimation algorithm that is based on Monte Carlo techniques that sample the unexplored portion of the reachability graph. We implemented our algorithm in Java Pathfinder and evaluated our approach on a suite of Java programs, simulating out-of-memory errors after a known percentage of a program's state space had been searched. Our empirical studies show that, on average, our algorithm's coverage estimates differ from the actual coverage by less than 10 percentage points, with a standard deviation of about 5 percentage points - regardless of whether the actual state-space coverage is low (3%) or high (95%).

With the popularity of model-driven methodologies, and the abundance of modelling languages, a major question for a requirements engineer is: which language is suitable for modelling a system under study? We address this question from a semantic point-of-view for big-step modelling languages (BSMLs). BSMLs are a class of popular behavioural modelling languages in which a model can respond to an input by executing multiple, possibly concurrent, transitions. We deconstruct the operational semantics of a large class of BSMLs into high-level, orthogonal semantic aspects, and analyze the relative advantages and disadvantages of the common semantic options for each of these aspects. Our goal is to empower a requirements engineer to compare and choose an appropriate BSML.

This paper is an overview of Software Engineering 2004, the Software Engineering volume of the Computing Curricula 2001 project. We briefly describe the contents of the volume, the process used in developing the volume's guidelines, and how we expect the volume to be used in practice.

Specifiers must be able to understand and compare the specification notations that they use. Traditional means for describing notations' semantics (e.g., operational semantics, logic, natural language) do not help users to identify the essential differences among notations. Previously, we presented a template-based approach defining model-based notations, in which semantics that are common among notations (e.g., the concept of an enabled transition) are captured in the template and a notation's distinct semantics (e.g., which states can enable transitions) are specified as parameters. We demonstrate the template's generality by using it to document the semantics of SCR, SDL, and Petri nets. We also show how the template can be used to compare notation variants. We believe template definitions of notations ease a user's effort in understanding and comparing model-based notations.

We propose a template-based approach to structuring the semantics of model-based specification notations. The basic computation model is a nonconcurrent, hierarchical state-transition machine (HTS), whose execution semantics are parameterized. Semantics that are common among notations (e.g., the concept of an enabled transition) are captured in the template, and a notation's distinct semantics (e.g., which states can enable transitions) are specified as parameters. The template semantics of composition operators define how multiple HTSs execute concurrently and how they communicate and synchronize with each other by exchanging events and data. The definitions of these operators use the template parameters to preserve notation-specific behavior in composition. Our template is sufficient to capture the semantics of basic transition systems, CSP, CCS, basic LOTOS, a subset of SDL88, and a variety of statecharts notations. We believe that a description of a notation's semantics using our template can be used as input to a tool that automatically generates formal analysis tools.

We propose a unifying framework for model-based specification notations. Our framework captures the execution semantics that are common among model-based notations, and leaves the distinct elements to be defined by a set of parameters. The basic components of a specification are non-concurrent state-transition machines, which are combined by composition operators to form more complex, concurrent specifications. We define the step-semantics of these basic components in terms of an operational semantics template whose parameters specialize both the enabling of transitions and transitions' effects. We also provide the operational semantics of seven composition operators, defining each as the concurrent execution of components, with changes to their shared variables and events to reflect inter-component communication and synchronization; the definitions of these operators use the template parameters to preserve in composition notation-specific behaviour. By separating a notation's step-semantics from its composition and concurrency operators, we simplify the definitions of both. Our framework is sufficient to capture the semantics of basic transition systems, CSP, CCS, basic LOTOS, ESTELLE, a subset of SDL88, and a variety of statecharts notations. We believe that a description of a notation's semantics in our framework can be used as input to a tool that automatically generates formal analysis tools.

One of the accepted techniques for developing and maintaining feature-rich applications is to treat each feature as a separate concern. However, most features are not separate concerns because they override and extend the same basic service. That is, “independent” features are coupled to one another through the system's basic service. As a result, seemingly unrelated features subtly interfere with each other when trying to override the system behaviour in different directions. The problem is how to coordinate features' access to the service's shared variables.

This paper presents a simple logic-model semantics for Software Cost Reduction (SCR) software requirements. Such a semantics enables model-checking of native SCR requirements and obviates the need to transform the requirements for analysis. The paper also proposes modal-logic abbreviations for expressing conditioned events in temporal-logic formulae. The Symbolic Model Verifier (SMV) is used to verify that an SCR requirements specification enforces desired global requirements, expressed as formulae in the enhanced logic. The properties of a small system (an automobile cruise control system) are verified, including an invariant property that could not be verified previously. The paper concludes with a discussion of how other requirements notations for conditioned-event-driven systems could be similarly checked.

Software errors frequently arise from incorrect system requirements. Successful requirements acquisition requires a thorough review process in which both domain experts and implementers can participate. Research groups [6, 10] have developed notations with precise meanings that can be read by both groups of reviewers. In [3], we showed how such requirements, in particular Software Cost Reduction (SCR) requirements, could be analyzed with formal methods. We developed methods for detailing SCR tabular requirements (with information that appears elsewhere in the SCR requirements document), translating the detailed requirements into a finite state machine (representing the system's global reachability graph), and proving safety assertions with a model checker for branching-time temporal logic. In this paper

It is demonstrated how model checking can be used to verify safety properties for event-driven systems. SCR tabular requirements describe required system behavior in a format that is intuitive, easy to read, and scalable to large systems (e.g. the software requirements for the A-7 military aircraft). Model checking of temporal logics has been established as a sound technique for verifying properties of hardware systems. An automated technique for formalizing the semiformal SCR requirements and for transforming the resultant formal specification onto a finite structure that a model checker can analyze has been developed. This technique was effective in uncovering violations of system invariants in both an automobile cruise control system and a water-level monitoring system.>

Abstract This paper describes a language called Nimble that allows designers to declare how the actual parameters in a procedure call are to be transformed at run time. Normally, programmers must edit an application's source in order to adapt it for reuse in some new context where the interfaces fail to match exactly (e.g. the parameters may appear in a different order, data types may not exactly match, and some data may need to be either initialized or masked out when the reusable module is integrated within a new application.) But Nimble allows programmers to adapt the interfaces of existing software without having to operate on the source manually. As a result, existing software may be easily reused in a broader range of applications, and software libraries do not need to store many variants of a component that differ only in how the interfaces are used. Nimble has been implemented on a variety of Unix hosts, and is part of a broader reuse project at the University of Maryland. Our current system is suitable for use either in conjunction with existing module interconnection languages, or stand‐alone with C, Pascal and Ada source programs.