While researchers have been investigating the Requirements Engineering (RE) discipline with many empirical studies, attempts to systematically derive an empirically-based theory are recent. We aim at providing an empirical and valid foundation for a theory of RE. We designed a survey instrument and theory that has been replicated in 10 countries world-wide. We evaluate the propositions of the theory with bootstrapped confidence intervals and derive potential explanations for the propositions. We report on the underlying theory and the full results obtained from the replication studies with participants from 228 organisations. Our results give insights into current practices with RE processes. The results reveal, for example, that there are no strong differences between organisations in different countries and regions, that interviews, facilitated meetings and prototyping are the most used elicitation techniques, that requirements are often documented textually, requirements specifications themselves are rarely changed and that requirements engineering improvement endeavours are mostly intrinsically motivated. The theory can be used as starting point for many further studies for more detailed investigations. Practitioners can use the results as theory-supported guidance on selecting suitable RE methods and techniques.

Java reflection has been increasingly used in a wide range of software. It allows a software system to inspect and/or modify the behaviour of its classes, interfaces, methods and fields at runtime, enabling the software to adapt to dynamically changing runtime environments. However, this dynamic language feature imposes significant challenges to static analysis. Existing static analysis tools either ignore reflection or handle it partially, resulting in missed, important behaviours. This paper makes two contributions: we provide a comprehensive understanding of Java reflection through examining its underlying concept, API and real-world usage, and, building on this, we introduce a new static approach to resolving Java reflection effectively in practice. We have implemented our analysis in an open-source tool, called Solar, and evaluated its effectiveness extensively with large Java programs and libraries. Our results demonstrate that Solar is able to (1) resolve reflection more soundly than the state-of-the-art reflection analysis; (2) automatically and accurately identify the parts of the program where reflection is resolved unsoundly or imprecisely; and (3) guide users to iteratively refine the analysis results by using lightweight annotations until their specific requirements are satisfied.

By a domain we shall understand \rationally describable segment of a human assisted reality, i.e., of the world, its physical parts, and living species. These are endurants (``still''), existing in space, as well as perdurants (``alive''), existing also in time. Emphasis is placed on human-assistedness, that is, that there is at least one (man-made) artifact and that humans are a primary cause for change of endurant states as well as perdurant behaviours. Domain science & engineering marks a new area of computing science. Just as we are formalizing the syntax and semantics of programming languages, so we are formalizing the syntax and semantics of human-assisted domains. Just as physicists are studying Nature, endowing it with mathematical models, so we, computing scientists, are studying these domains, endowing them with mathematical models, A difference between the endeavour of physicists and ours lies in the models: the physics models are based on classical mathematics, differential equations and integrals, etc., our models are based on mathematical logic, set theory, and algebra.

Verilog is a hardware description language (HDL) that has been standardized and widely used in industry. MDESL is a Verilog-like language, which is a multithreaded discrete event simulation language. It contains interesting features such as event-driven computation and shared-variable concurrency. This paper considers how the algebraic semantics links with the operational semantics for MDESL. Our approach is from both the theoretical and practical aspects. The link is proceeded by deriving the operational semantics from the algebraic semantics. Firstly, we present the algebraic semantics for MDESL. We introduce the concept of head normal form. Secondly we present the strategy of deriving operational semantics from algebraic semantics. We also investigate the soundness and completeness of the derived operational semantics with respect to the derivation strategy. Our theoretical approach is complemented by a practical one, we use the theorem proof assistant Coq to formalize the algebraic laws and the derived operational semantics. Meanwhile, the soundness and completeness of the derived operational semantics is also verified via the mechanical approach in Coq. Our approach is a novel way to formalize and verify the correctness and equivalence of different semantics for MDESL in both a theoretical approach and a practical approach.

This article reports a controlled experiment with 116 participants on the understandability of representative graphical and textual pattern-based behavioral constraint representations from the viewpoint of novice software designers. Particularly, graphical and textual behavioral constraint patterns present in the declarative business process language Declare and textual behavioral constraints based on Property Specification Patterns are subject of this study. In addition to measuring the understandability construct, this study assesses subjective aspect such as perceived difficulties regarding learning and application of the tested approaches. An interesting finding of this study is the overall low achieved correctness in the experimental tasks which seems to indicate that pattern-based behavioral constraint representations are hard to understand for novice software designer in the absence of additional supportive measures. The results of the descriptive statistics regarding achieved correctness are slightly in favor of the textual representations, but the inference statistics do not indicate any significant differences in terms of understandability between graphical and textual behavioral constraint representations.

Watchdog timers are devices that are commonly used to monitor the health of safety-critical hardware and software systems. Their primary function is to raise an alarm if the monitored systems fail to emit periodic heartbeats that signal their well-being. In this paper we design and verify a molecular watchdog timer for monitoring the health of programmed molecular nanosystems. This raises new challenges because our molecular watchdog timer and the system that it monitors both operate in the probabilistic environment of chemical kinetics, where many failures are certain to occur and it is especially hard to detect the absence of a signal. Our molecular watchdog timer is the result of an incremental design process that uses goal-oriented requirements engineering, simulation, stochastic analysis, and software verification tools. We demonstrate the molecular watchdogs functionality by having it monitor a molecular oscillator. Both the molecular watchdog timer and the oscillator are implemented as chemical reaction networks, which are the current programming language of choice for many molecular programming applications.

In a mobile system, mobility refers to a change in position of a mobile object with respect to time and its reference point, whereas isolation means the isolation relationship of mobile objects under some scheduling policies. Following event-based formal model and the ambient calculus, we propose first two types of special events, entering and exiting an ambient, as movement events to model and analyze mobility. Based on mobility, we then introduce the notion of the isolation of mobile objects for ambients. To ensure the isolation, a priority policy needs to be used to schedule the movement of mobile objects. However, traditional scheduling policies focus on task scheduling and depend on the main assumption: the scheduled tasks are independentthat is, the scheduled tasks do not aect each other. In a practical mobile system, mobile objects and ambients interact with each other. It is dicult to separate a mobile system into independent tasks.We finally present an automatic approach for generating a priority scheduling policy without considering the preceding assumption. The approach can guarantee the isolation of the mobile objects for ambients in a mobile system. Experiments demonstrate these results.