-
A Tool for Automated Reasoning About Traces Based on Configurable Formal Semantics
Authors:
Ferhat Erata,
Arda Goknil,
Bedir Tekinerdogan,
Geylani Kardas
Abstract:
We present Tarski, a tool for specifying configurable trace semantics to facilitate automated reasoning about traces. Software development projects require that various types of traces be modeled between and within development artifacts. For any given artifact (e.g., requirements, architecture models and source code), Tarski allows the user to specify new trace types and their configurable semanti…
▽ More
We present Tarski, a tool for specifying configurable trace semantics to facilitate automated reasoning about traces. Software development projects require that various types of traces be modeled between and within development artifacts. For any given artifact (e.g., requirements, architecture models and source code), Tarski allows the user to specify new trace types and their configurable semantics, while, using the semantics, it automatically infers new traces based on existing traces provided by the user, and checks the consistency of traces. It has been evaluated on three industrial case studies in the automotive domain (https://modelwriter.github.io/Tarski/).
△ Less
Submitted 9 March, 2024;
originally announced March 2024.
-
AlloyInEcore: Embedding of First-Order Relational Logic into Meta-Object Facility for Automated Model Reasoning
Authors:
Ferhat Erata,
Arda Goknil,
Ivan Kurtev,
Bedir Tekinerdogan
Abstract:
We present AlloyInEcore, a tool for specifying metamodels with their static semantics to facilitate automated, formal reasoning on models. Software development projects require that software systems be specified in various models (e.g., requirements models, architecture models, test models, and source code). It is crucial to reason about those models to ensure the correct and complete system speci…
▽ More
We present AlloyInEcore, a tool for specifying metamodels with their static semantics to facilitate automated, formal reasoning on models. Software development projects require that software systems be specified in various models (e.g., requirements models, architecture models, test models, and source code). It is crucial to reason about those models to ensure the correct and complete system specifications. AlloyInEcore allows the user to specify metamodels with their static semantics, while, using the semantics, it automatically detects inconsistent models, and completes partial models. It has been evaluated on three industrial case studies in the automotive domain (https://modelwriter.github.io/AlloyInEcore/).
△ Less
Submitted 4 March, 2024;
originally announced March 2024.
-
Metamorphic Testing for Web System Security
Authors:
Nazanin Bayati Chaleshtari,
Fabrizio Pastore,
Arda Goknil,
Lionel C. Briand
Abstract:
Security testing aims at verifying that the software meets its security properties. In modern Web systems, however, this often entails the verification of the outputs generated when exercising the system with a very large set of inputs. Full automation is thus required to lower costs and increase the effectiveness of security testing. Unfortunately, to achieve such automation, in addition to strat…
▽ More
Security testing aims at verifying that the software meets its security properties. In modern Web systems, however, this often entails the verification of the outputs generated when exercising the system with a very large set of inputs. Full automation is thus required to lower costs and increase the effectiveness of security testing. Unfortunately, to achieve such automation, in addition to strategies for automatically deriving test inputs, we need to address the oracle problem, which refers to the challenge, given an input for a system, of distinguishing correct from incorrect behavior. In this paper, we propose Metamorphic Security Testing for Web-interactions (MST-wi), a metamorphic testing approach that integrates test input generation strategies inspired by mutational fuzzing and alleviates the oracle problem in security testing. It enables engineers to specify metamorphic relations (MRs) that capture many security properties of Web systems. To facilitate the specification of such MRs, we provide a domain-specific language accompanied by an Eclipse editor. MST-wi automatically collects the input data and transforms the MRs into executable Java code to automatically perform security testing. It automatically tests Web systems to detect vulnerabilities based on the relations and collected data. We provide a catalog of 76 system-agnostic MRs to automate security testing in Web systems. It covers 39% of the OWASP security testing activities not automated by state-of-the-art techniques; further, our MRs can automatically discover 102 different types of vulnerabilities, which correspond to 45% of the vulnerabilities due to violations of security design principles according to the MITRE CWE database. We also define guidelines that enable test engineers to improve the testability of the system under test with respect to our approach.
△ Less
Submitted 7 March, 2023; v1 submitted 19 August, 2022;
originally announced August 2022.
-
ETAP: Energy-aware Timing Analysis of Intermittent Programs
Authors:
Ferhat Erata,
Arda Goknil,
Eren Yıldız,
Kasım Sinan Yıldırım,
Ruzica Piskac,
Jakub Szefer,
Gökçin Sezgin
Abstract:
Energy harvesting battery-free embedded devices rely only on ambient energy harvesting that enables stand-alone and sustainable IoT applications. These devices execute programs when the harvested ambient energy in their energy reservoir is sufficient to operate and stop execution abruptly (and start charging) otherwise. These intermittent programs have varying timing behavior under different energ…
▽ More
Energy harvesting battery-free embedded devices rely only on ambient energy harvesting that enables stand-alone and sustainable IoT applications. These devices execute programs when the harvested ambient energy in their energy reservoir is sufficient to operate and stop execution abruptly (and start charging) otherwise. These intermittent programs have varying timing behavior under different energy conditions, hardware configurations, and program structures. This paper presents Energy-aware Timing Analysis of intermittent Programs (ETAP), a probabilistic symbolic execution approach that analyzes the timing and energy behavior of intermittent programs at compile time. ETAP symbolically executes the given program while taking time and energy cost models for ambient energy and dynamic energy consumption into account. We evaluated ETAP on several intermittent programs and compared the compile-time analysis results with executions on real hardware. The results show that ETAP's normalized prediction accuracy is 99.5%, and it speeds up the timing analysis by at least two orders of magnitude compared to manual testing.
△ Less
Submitted 3 February, 2022; v1 submitted 27 January, 2022;
originally announced January 2022.
-
Metamorphic Security Testing for Web Systems
Authors:
Phu X. Mai,
Fabrizio Pastore,
Arda Goknil,
Lionel Briand
Abstract:
Security testing verifies that the data and the resources of software systems are protected from attackers. Unfortunately, it suffers from the oracle problem, which refers to the challenge, given an input for a system, of distinguishing correct from incorrect behavior. In many situations where potential vulnerabilities are tested, a test oracle may not exist, or it might be impractical due to the…
▽ More
Security testing verifies that the data and the resources of software systems are protected from attackers. Unfortunately, it suffers from the oracle problem, which refers to the challenge, given an input for a system, of distinguishing correct from incorrect behavior. In many situations where potential vulnerabilities are tested, a test oracle may not exist, or it might be impractical due to the many inputs for which specific oracles have to be defined. In this paper, we propose a metamorphic testing approach that alleviates the oracle problem in security testing. It enables engineers to specify metamorphic relations (MRs) that capture security properties of the system. Such MRs are then used to automate testing and detect vulnerabilities. We provide a catalog of 22 system-agnostic MRs to automate security testing in Web systems. Our approach targets 39% of the OWASP security testing activities not automated by state-of-the-art techniques. It automatically detected 10 out of 12 vulnerabilities affecting two widely used systems, one commercial and the other open source (Jenkins).
△ Less
Submitted 11 December, 2019;
originally announced December 2019.
-
Automatic Generation of Acceptance Test Cases from Use Case Specifications: an NLP-based Approach
Authors:
Chunhui Wang,
Fabrizio Pastore,
Arda Goknil,
Lionel C. Briand
Abstract:
Acceptance testing is a validation activity performed to ensure the conformance of software systems with respect to their functional requirements. In safety critical systems, it plays a crucial role since it is enforced by software standards. Test engineers need to identify all the representative test execution scenarios from requirements, determine the runtime conditions that trigger these scenar…
▽ More
Acceptance testing is a validation activity performed to ensure the conformance of software systems with respect to their functional requirements. In safety critical systems, it plays a crucial role since it is enforced by software standards. Test engineers need to identify all the representative test execution scenarios from requirements, determine the runtime conditions that trigger these scenarios, and finally provide the input data that satisfy these conditions. Given that requirements specifications are typically large and often provided in natural language, the generation of acceptance test cases tends to be expensive and error-prone.
In this paper, we present UMTG, an approach that supports the generation of executable, system-level, acceptance test cases from requirements specifications in natural language, with the goal of reducing the manual effort required to generate test cases and ensuring requirements coverage. More specifically, UMTG automates the generation of acceptance test cases based on use case specifications and a domain model for the system under test, which are commonly produced in many development environments. Unlike existing approaches, it does not impose strong restrictions on the expressiveness of use case specifications. We rely on recent advances in natural language processing to automatically identify test scenarios and to generate formal constraints that capture conditions triggering the execution of the scenarios, thus enabling the generation of test data. In two industrial case studies, UMTG automatically and correctly translated 95% of the use case specification steps into formal constraints required for test data generation; furthermore, it generated test cases that exercise not only all the test scenarios manually implemented by experts, but also some critical scenarios not previously considered.
△ Less
Submitted 18 May, 2020; v1 submitted 19 July, 2019;
originally announced July 2019.
-
Automating System Test Case Classification and Prioritization for Use Case-Driven Testing in Product Lines
Authors:
Ines Hajri,
Arda Goknil,
Fabrizio Pastore,
Lionel C. Briand
Abstract:
Product Line Engineering (PLE) is a crucial practice in many software development environments where software systems are complex and developed for multiple customers with varying needs. At the same time, many development processes are use case-driven and this strongly influences their requirements engineering and system testing practices. In this paper, we propose, apply, and assess an automated…
▽ More
Product Line Engineering (PLE) is a crucial practice in many software development environments where software systems are complex and developed for multiple customers with varying needs. At the same time, many development processes are use case-driven and this strongly influences their requirements engineering and system testing practices. In this paper, we propose, apply, and assess an automated system test case classification and prioritization approach specifically targeting system testing in the context of use case-driven development of product families. Our approach provides: (i) automated support to classify, for a new product in a product family, relevant and valid system test cases associated with previous products, and (ii) automated prioritization of system test cases using multiple risk factors such as fault-proneness of requirements and requirements volatility in a product family. Our evaluation was performed in the context of an industrial product family in the automotive domain. Results provide empirical evidence that we propose a practical and beneficial way to classify and prioritize system test cases for industrial product lines.
△ Less
Submitted 17 June, 2020; v1 submitted 28 May, 2019;
originally announced May 2019.
-
A Rule-Based Change Impact Analysis Approach in Software Architecture for Requirements Changes
Authors:
Arda Goknil,
Ivan Kurtev,
Klaas van den Berg
Abstract:
Software systems usually operate in a dynamic context where their requirements change continuously and new requirements emerge frequently. A single requirement hardly exists in isolation: it is related to other requirements and to the software development artifacts that implement it. When a requirements change is introduced, the requirements engineer may have to manually analyze all requirements a…
▽ More
Software systems usually operate in a dynamic context where their requirements change continuously and new requirements emerge frequently. A single requirement hardly exists in isolation: it is related to other requirements and to the software development artifacts that implement it. When a requirements change is introduced, the requirements engineer may have to manually analyze all requirements and architectural elements for a single change. This may result in neglecting the actual impact of a change. We aim at improving change impact analysis in software architecture for requirements changes by using formal semantics of requirements relations, requirements changes and traces between Requirements & Architecture. In our previous work we presented a technique for change impact analysis in requirements. The technique uses the formal semantics of requirements relations and changes. Its output is a set of candidate requirements for the impact with proposed changes and a propagation path in the requirements model. In this paper we present a complementary technique which propagates requirements changes to software architecture and finds out which architectural elements are impacted by these changes. The formalization of requirements relations, changes and traces between R&A is used to determine candidate architectural elements for the impact of requirements changes in the architecture. The tool support is an extension of our Tool for Requirements Inferencing and Consistency Checking (TRIC). Our approach helps in the elimination of some false positive impacts in change propagation. We illustrate our approach in an industrial example which shows that the formal semantics of requirements relations, changes and traces enables the identification of candidate architectural elements with the reduction of some false positive impacts.
△ Less
Submitted 9 August, 2016;
originally announced August 2016.
