Abstract Nowadays, cloud‐native software architectures have a significant relevance due to the speed and agility they provide. These properties lead relevant organizations in different industries, like video streaming (Netflix), car‐sharing (Uber, Cabify), banking (BBVA, HSBC), and governmental agencies (NASA, FBI, CERN, ESA) to heavily rely on cloud‐native software to run their business‐critical applications. Additionally, including fault injection actions in the production infrastructure allows companies to have consistent environments, to improve applications dependability against unexpected failures, to provide better user experience, and to improve the overall system quality. Thus, cloud computing technologies allow development teams to rapidly create complex systems and to continuously deploy them, at a global scale. This work describes Pystol, a novel fault injection platform—represented as a Software Product Line—to analyze the effects caused by a wide spectrum of adverse conditions. Pystol is designed to be executed on top of cloud‐native environments, either in private or public clouds. The proposed architecture shows a way for representing feature models based on Unified Model Language (in short, UML) component diagrams. Furthermore, we present a thorough empirical study carried out in real‐world environments, providing promising results.

Software product lines are an excellent mechanism in the development of software. Testing software product lines is an intensive process where selecting the right features where to focus it can be a critical task. Selecting the best combination of features from a software product line is a complex problem addressed in the literature. In this paper, we address the problem of finding the combination of features with the highest probability of being requested from a software product line with probabilities. We use Evolutive Computation techniques to address this problem. Specifically, we use the Ant Colony Optimization algorithm to find the best combination of features. Our results report that our framework overcomes the limitations of the brute force algorithm.

Despite that many real-life contracts include time constraints, for instance explicitly specifying deadlines by when to perform actions, or for how long certain behaviour is prohibited, the literature formalising such notions is surprisingly sparse. Furthermore, one of the major challenges is that compliance is typically computed with respect to timed event traces with event timestamps assumed to be perfect. In this paper we present an approach for evaluating compliance under the effect of imperfect timing information, giving a semantics to analyse contract violation likelihood.

In this paper we develop a general framework to reason about testing. The difficulty of testing is assessed in terms of the amount of tests that must be applied to determine whether the system is correct or not. Based on this criterion, five testability classes are presented and related. We also explore conditions that enable and disable finite testability, and their relation to testing hypotheses is studied. We measure how far incomplete test suites are from being complete, which allows us to compare and select better incomplete test suites. The complexity of finding that measure, as well as the complexity of finding minimum complete test suites, is identified. Furthermore, we address the reduction of testing problems to each other, that is, we study how the problem of finding test suites to test systems of some kind can be reduced to the problem of finding test suites for another kind of systems. This enables to export testing methods. In order to illustrate how general notions are applied to specific cases, many typical examples from the formal testing techniques domain are presented.

We consider the formal representation and analysis of systems with fuzzy-time information. First, we present a formalism to represent specifications. This model exploits the concepts of fuzzy set theory and uses a mathematical framework to get a more flexible approach. As it is usually assumed in industrial case studies, we consider that the original requirements of the specification may change. The implementation is built with respect to these changes but the specification is not upgraded. Thus, it may be outdated. In order to continue using the formal framework, the specification must be adapted with respect to these new requirements. We consider that this update process should be as non-intrusive as possible, that is, without using the source-code of the implementation. We present a novel methodology for self-evolving fuzzy-time systems, without interacting with the source code.

The language RTPA, Real Time Process Algebra, has been created to enable rigorous treatment of knowledge representation and manipulation in terms of to be I to have / to do in a formal and coherent framework. This language has been designed to cope with the three dimensions involved in the problem of software specification: (i) mathematical operations, (ii) event/process timing, and (iii) memory manipulation. In this paper we focus on giving a testing semantics to the second dimension: Process timing dimension. First, we will provide a SOS like operational semantics for the process relations of RTPA. Next, we will define what a test is and we will introduce a relation based on which tests are passed by processes. Finally, we will obtain an operational characterization that can be used as a first step to define a denotational sematics sound and complete with respect the testing semantics.

Due to the use of higher-order functions and laziness, debugging lazy functional programs is not a trivial task. Fortunately, several debuggers have appeared during the last years. However, the difficulty of the debugging process is increased when considering parallel extensions of lazy functional languages. Thus, it is necessary not only to develop practical debuggers, but also to provide a clear semantic environment to understand what the debuggers should do. In this paper we present a formal framework for debugging two different parallel extensions of the lazy functional language Haskell. In order to do that, we define an operational semantics model which allows us to deal with side-effects and parallelism. By doing so, we provide a formalization of a parallel debugger we have already implemented by extending the sequential debugger Hood.

EXercita is a system designed to archive and publish programming exercises. It consists of a repository of structured documents, each describing an exercise, and several tools to manage it. Documents are marked-up with an extension of LaTeX we have designed, called eXercita, and can be automatically published as PostScript files or Web pages. In addition, exercises can be automatically published as a hierarchical Web site that mirrors the structure of the repository.