Background: Individual fairness testing aims to identify individual discriminatory instances (IDIs) to improve the fairness of machine learning classifiers through retraining. While prior studies have primarily evaluated fairness testing algorithms based on efficiency and retraining performance, emerging metrics such as the diversity of identified IDIs have recently been proposed. However, these alternative metrics have not yet been established as standard evaluation criteria. Aims: This study investigates the significance of IDI diversity as a metric for evaluating fairness testing algorithms. Specifically, we aim to validate its utility as a core evaluation metric by examining its correlation with both fairness improvement and accuracy degradation in retrained classifiers. Method: We conduct an empirical study using a newly developed framework called Redi. This framework generates multiple IDI sets with controlled variations in diversity, enabling systematic evaluation of their impact on retrained classifiers. We apply Redi to analyze the correlations between IDI diversity and retraining outcomes. The validity of the framework is further supported through auxiliary empirical analyses. Results: Our experiments confirm that IDI diversity exhibits a moderate correlation with fairness improvement, while showing only a weak correlation with accuracy degradation. Additionally, our regression analysis indicates that the actual impact of diversity on fairness improvement is substantial, whereas its impact on accuracy degradation is relatively negligible. Conclusions: These results show that higher IDI diversity substantially enhances fairness with minimal accuracy loss, suggesting that it should be adopted as a meaningful proxy metric for evaluating fairness testing algorithms, complementing the established metrics.

Individual fairness testing (Ift) is a framework to find discriminatory instances within a given classifier. In this paper, we show our idea of a Ift framework, that integrates the notion of data validity, termed "Individual Fairness Testing with Data Validity (Ift-v)". We develop a solid foundation of Ift-v and demonstrate the feasibility of Ift-v. Our preliminary evaluation with Ift-v reveals the possibility that many of discriminatory instances detected by state-of-the-art Ift algorithms are considered invalid. These findings prompt a re-think of the current Ift framework, suggesting a transition from solely focusing on the discovery of discriminatory instances to the consideration of valid ones.

As machine learning (ML) systems are increasingly used in various fields, including tasks with high social impact, concerns about their fairness are growing. To address these concerns, individual fairness testing (IFT) has been introduced to identify individual discriminatory instances (IDIs) that indicate the violation of individual fairness in a given ML classifier. In this paper, we propose a black-box testing algorithm for IFT, named Aft (short for Approximation-guided Fairness Testing). Aft constructs approximate models based on decision trees, and generates test cases by sampling paths of the decision trees. Our evaluation by experiments confirms that Aft outperforms the state-of-the-art black-box IFT algorithm ExpGA both in efficiency (by 3.42 times) and diversity of IDIs identified by algorithms (by 1.16 times).

With the increasing use of machine learning software in our daily life, software fairness has become a growing concern.In this paper, we propose an individual fairness testing technique called KOSEI.Individual fairness is one of the central concepts in software fairness.Testing individual fairness aims to detect individual discriminations included in the software.KOSEI is based on AEQUITAS by Udeshi et al., a landmark fairness testing technique featuring a two-step search strategy of global and local search.KOSEI improves the local search part of AEQUITAS, based on our insight to overcome the limitations of the local search of AEQUITAS.Our experiments show that KOSEI outperforms AEQUITAS by orders of magnitude.KOSEI, on average, detects 5,084.8%more discriminations than AEQUITAS, in just 7.5% of the execution time.

Summary In this paper, we extend work on model‐based testing for Apache ZooKeeper, to handle watchers (triggers) and improve scalability. In a distributed asynchronous shared storage like ZooKeeper, watchers deliver notifications on state changes. They are difficult to test because watcher notifications involve an initial action that sets the watcher, followed by another action that changes the previously seen state. We show how to generate test cases for concurrent client sessions executing against ZooKeeper with the tool Modbat. The tests are verified against an oracle that takes into account all possible timings of network communication. The oracle has to verify that there exists a chain of events that triggers both the initial callback and the subsequent watcher notification. We show in detail how the oracle computes whether watch triggers are correct and how the model was adapted and improved to handle these features. Together with a new search improvement that increases both speed and accuracy, we are able to verify large test setups and confirm several defects with our model.

In Software Product Line (SPL) development, one of promising techniques for core asset testing is to test a subset of SPL as representative products. SPL pairwise testing is a such technique in which each product corresponds to a possible feature configuration in the feature model (FM) and representative products are selected so as to all possible feature pairs are included. It is also important to prioritize representative products, because it could improve the effectiveness of core asset testing especially when the testing resource is limited. In this paper, we propose a prioritization method for SPL pairwise testing based on user profiles. A user profile is a set of user groups and their occurrence probabilities such as the percentages of user groups in a market that use specific devices, applications or services. These profiles are used as the probabilities of feature choices at decision points such as optional features and alternative features in a FM. Based on that, we calculate the probability for obtaining a feature pairs (PFP for short), and generate representative products with priority. Most researches relate to the probabilities about FM handle the probability for obtaining a single feature (PSF for short). Based on PSF, we could estimate PFP. However, this estimation is not appropriate for the prioritization especially when conditional probabilities appear in user profiles. In our method, we directly calculate PFP and determine the priorities. We evaluate the method to show advantages of prioritizations using PFP over those using PSF, and also analyze the characteristics of the method.

Apache ZooKeeper is a distributed data storage that is highly concurrent and asynchronous due to network communication, testing such a system is very challenging. Our solution using the tool "Modbat" generates test cases for concurrent client sessions, and processes results from synchronous and asynchronous callbacks. We use an embedded model checker to compute the test oracle for non-deterministic outcomes, the oracle model evolves dynamically with each new test step. Our work has detected multiple previously unknown defects in ZooKeeper. Finally, a thorough coverage evaluation of the core classes show how code and branch coverage strongly relate to feature coverage in the model, and hence modeling effort.

This paper proposes a novel approach to combinatorial test generation, which achieves an increase of not only the number of new combinations but also the distance between test cases. We applied our distance-integrated approach to a state-of-the-art greedy algorithm for traditional combinatorial test generation by using two distance metrics, Hamming distance, and a modified chi-square distance. Experimental results using numerous benchmark models show that combinatorial test suites generated by our approach using both distance metrics can improve interaction coverage for higher interaction strengths with low computational overhead.

Combinatorial testing aims at covering the interactions of parameters in a system under test, while some combinations may be forbidden by given constraints (forbidden tuples). In this paper, we illustrate that such forbidden tuples correspond to unsatisfiable cores, a widely understood notion in the SAT solving community. Based on this observation, we propose a technique to detect forbidden tuples lazily during a greedy test case generation, which significantly reduces the number of required SAT solving calls. We further reduce the amount of time spent in SAT solving by essentially ignoring constraints while constructing each test case, but then “amending” it to obtain a test case that satisfies the constraints, again using unsatisfiable cores. Finally, to complement a disturbance due to ignoring constraints, we implement an efficient approximative SAT checking function in the SAT solver Lingeling. Through experiments we verify that our approach significantly improves the efficiency of constraint handling in our greedy combinatorial testing algorithm.

Combinatorial testing is a widely-used technique to detect system interaction failures. To improve test effectiveness with given priority weights of parameter values in a system under test, prioritized combinatorial testing constructs test suites where highly weighted parameter values appear earlier or more frequently. Such order-focused and frequency-focused combinatorial test generation algorithms have been evaluated using metrics called weight coverage and KL divergence but not sufficiently with fault detection effectiveness so far. We evaluate the fault detection effectiveness on a collection of open source utilities, applying prioritized combinatorial test generation and investigating its correlation with weight coverage and KL divergence.

Priorities (weights) for parameter values can improve the effectiveness of combinatorial testing. Previous approaches have employed weights to derive high-priority test cases either earlier or more frequently. Our approach integrates these order-focused and frequency-focused prioritizations. We show that our priority integration realizes a small test suite providing high-priority test cases early and frequently in a good balance. We also propose two algorithms that apply our priority integration to existing combinatorial test generation algorithms. Experimental results using numerous test models show that our approach improves the existing approaches w.r.t. Order-focused and frequency-focused metrics, while overheads in the size and generation time of test suites are small.

Combinatorial testing aims at reducing the cost of software and system testing by reducing the number of test cases to be executed. We propose an approach for combinatorial testing that generates a set of test cases that is as small as possible, using incremental SAT solving. We present several search-space pruning techniques that further improve our approach. Experiments show a significant improvement of our approach over other SAT-based approaches, and considerable reduction of the number of test cases over other combinatorial testing tools.

Modbat makes testing easier by providing a user-friendly modeling language to describe the behavior of systems, from such a model, test cases are generated and executed. Modbat's domain-specific language is based on Scala, its features include probabilistic and non-deterministic transitions, component models with inheritance, and exceptions. We demonstrate the versatility of Modbat by finding a confirmed defect in the currently latest version of Java, and by testing SAT solvers.

In this paper, we develop a combinatorial testing technique for tree-structured test models. First, we generalize our previous test models for combinatorial testing based on and-xor trees with constraints limited to a syntactic subset of propositional logic, to allow for constraints in full propositional logic. We prove that the generalized test models are strictly more expressive than the limited ones. Then we develop an algorithm for combinatorial testing for the generalized models, and show its correctness and computational complexity. We apply a tool based on our algorithm to an actual ticket gate system that is used by several large transportation companies in Japan. Experimental results show that our technique outperforms existing techniques.

AUTOSAR multicore RTOS is a safety-critical concurrent system, for which high quality is required. A conformance test is important to ensure the quality of the software, but the conventional test is low in coverage and high in cost. In this paper, we present a formal model-based test for multicore RTOS that supports AUTOSAR specifications. First, we developed a formal model. With the model, we developed a test case generator, from which an entire test suite can be extracted. Moreover, we proposed a test program generator, with which optimal executable test programs can be generated fully automatically. Both of the generators are assisted with model checking on the formal model. Bug analysis also becomes easy. Our method demonstrated its advantage over conventional testing by finding 33 test cases for three system service calls, whereas a conventional test carried out by a development team found only 10 test cases. Our method can improve the coverage of the test, clearly saving in cost and development time. It is expected to significantly improve the testing of the AUTOSAR multicore RTOS.

This research aims to develop a formal framework for (1) formal validation for satisfiability of specifications to requirements, and (2) requirements management based on the Jackson's reference model for requirements and specifications, which provides an insight and perspective basis for relationship between requirements and specifications. To develop the framework, we use propositional logic, from which we derive formal discussion and devices for computer assistance. In the framework the validation for satisfiability of specifications to requirements is ascribed to the validity checking of logical formulas. Also within the framework we develop a useful notion of ``weakest adequate specifications'' with its calculating technique. We will demonstrate the usefulness of the framework with practical examples.

We propose a modal logic for modular pi calculus: a logic to specify both temporal and spatial properties for processes in modular pi calculus. Characterization of process equivalence the logic induce is investigated, and it is shown that the distinguishing power of the logic falls between bisimilarity and structural congruence. Then a model checking algorithm for the logic over the finite-control subset of modular pi calculus is presented, and its correctness proved.