On the Membership and Correctness Problem for State Serializability and Value Opacity - König, Jürgen

On-The-Fly Computing -- Individualized IT-services in dynamic markets - Haake, Claus-Jochen; Meyer auf der Heide, Friedhelm; Platzner, Marco; Wachsmuth, Henning; Wehrheim, Heike
In the proposal for our CRC in 2011, we formulated a vision of markets for IT services that describes an approach to the provision of such services that was novel at that time and, to a large extent, remains so today: „Our vision of on-the-fly computing is that of IT services individually and automatically configured and brought to execution from flexibly combinable services traded on markets. At the same time, we aim at organizing markets whose participants maintain a lively market of services through appropriate entrepreneurial actions.“ Over the last 12 years, we have developed methods and techniques to address problems critical to the convenient, efficient, and secure use of on-the-fly computing. Among other things, we have made the description of services more convenient by allowing natural language input, increased the quality of configured services through (natural language) interaction and more efficient configuration processes and analysis procedures, made the quality of (the products of) providers in the marketplace transparent through reputation systems, and increased the resource efficiency of execution through reconfigurable heterogeneous computing nodes and an integrated treatment of service description and configuration. We have also developed network infrastructures that have a high degree of adaptivity, scalability, efficiency, and reliability, and provide cryptographic guarantees of anonymity and security for market participants and their products and services. To demonstrate the pervasiveness of the OTF computing approach, we have implemented a proof-of-concept for OTF computing that can run typical scenarios of an OTF market. We illustrated the approach using a cutting-edge application scenario – automated machine learning (AutoML). Finally, we have been pushing our work for the perpetuation of On-The-Fly Computing beyond the SFB and sharing the expertise gained in the SFB in events with industry partners as well as transfer projects. This work required a broad spectrum of expertise. Computer scientists and economists with research interests such as computer networks and distributed algorithms, security and cryptography, software engineering and verification, configuration and machine learning, computer engineering and HPC, microeconomics and game theory, business informatics and management have successfully collaborated here.

Composition Analysis in Unknown Contexts - Wehrheim, Heike; Hüllermeier, Eyke; Becker, Steffen; Becker, Matthias; Richter, Cedric; Sharma, Arnab (On-The-Fly Computing -- Individualized IT-services in dynamic markets)

Property-Driven Testing of Black-Box Functions - Sharma, Arnab; Melnikov, Vitaly; Hüllermeier, Eyke; Wehrheim, Heike (Proceedings of the 10th IEEE/ACM International Conference on Formal Methods in Software Engineering (FormaliSE))
Testing is one of the most frequent means of quality assurance for software. Property-based testing aims at generating test suites for checking code against user-defined properties. Test input generation is, however, most often independent of the property to be checked, and is instead based on random or user-defined data generation.In this paper, we present property-driven unit testing of functions with numerical inputs and outputs. Alike property-based testing, it allows users to define the properties to be tested for. Contrary to property-based testing, it also uses the property for a targeted generation of test inputs. Our approach is a form of learning-based testing where we first of all learn a model of a given black-box function using standard machine learning algorithms, and in a second step use model and property for test input generation. This allows us to test both predefined functions as well as machine learned regression models. Our experimental evaluation shows that our property-driven approach is more effective than standard property-based testing techniques.

MLCHECK–Property-Driven Testing of Machine Learning Classifiers - Sharma, Arnab; Demir, Caglar; Ngonga Ngomo, Axel-Cyrille; Wehrheim, Heike (Proceedings of the 20th IEEE International Conference on Machine Learning and Applications (ICMLA))
In recent years, we observe an increasing amount of software with machine learning components being deployed. This poses the question of quality assurance for such components: how can we validate whether specified requirements are fulfilled by a machine learned software? Current testing and verification approaches either focus on a single requirement (e.g., fairness) or specialize on a single type of machine learning model (e.g., neural networks). In this paper, we propose property-driven testing of machine learning models. Our approach MLCheck encompasses (1) a language for property specification, and (2) a technique for systematic test case generation. The specification language is comparable to property-based testing languages. Test case generation employs advanced verification technology for a systematic, property dependent construction of test suites, without additional user supplied generator functions. We evaluate MLCheck using requirements and data sets from three different application areas (software discrimination, learning on knowledge graphs and security). Our evaluation shows that despite its generality MLCheck can even outperform specialised testing approaches while having a comparable runtime

Automatic Fairness Testing of Machine Learning Models - Sharma, Arnab; Wehrheim, Heike (Proceedings of the 32th IFIP International Conference on Testing Software and Systems (ICTSS))

Optimierung von JMCTest beim Testen von Inter Method Contracts - Mayer, Stefan

Higher Income, Larger Loan? Monotonicity Testing of Machine Learning Models - Sharma, Arnab; Wehrheim, Heike (Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA).)

Algorithm Selection for Software Validation Based on Graph Kernels - Richter, Cedric; Hüllermeier, Eyke; Jakobs, Marie-Christine; Wehrheim, Heike (Journal of Automated Software Engineering)

A Case for a New IT Ecosystem: On-The-Fly Computing - Karl, Holger; Kundisch, Dennis; Meyer auf der Heide, Friedhelm; Wehrheim, Heike (Business & Information Systems Engineering)

Specifying and Analyzing Virtual Network Services Using Queuing Petri Nets - Schneider, Stefan Balthasar; Sharma, Arnab; Karl, Holger; Wehrheim, Heike (2019 IFIP/IEEE International Symposium on Integrated Network Management (IM))
For optimal placement and orchestration of network services, it is crucial that their structure and semantics are specified clearly and comprehensively and are available to an orchestrator. Existing specification approaches are either ambiguous or miss important aspects regarding the behavior of virtual network functions (VNFs) forming a service. We propose to formally and unambiguously specify the behavior of these functions and services using Queuing Petri Nets (QPNs). QPNs are an established method that allows to express queuing, synchronization, stochastically distributed processing delays, and changing traffic volume and characteristics at each VNF. With QPNs, multiple VNFs can be connected to complete network services in any structure, even specifying bidirectional network services containing loops. We discuss how management and orchestration systems can benefit from our clear and comprehensive specification approach, leading to better placement of VNFs and improved Quality of Service. Another benefit of formally specifying network services with QPNs are diverse analysis options, which allow valuable insights such as the distribution of end-to-end delay. We propose a tool-based workflow that supports the specification of network services and the automatic generation of corresponding simulation code to enable an in-depth analysis of their behavior and performance.

Testing Balancedness of ML Algorithms - Sharma, Arnab; Wehrheim, Heike (Proceedings of the Software Engineering Conference (SE))

Testing Machine Learning Algorithms for Balanced Data Usage - Sharma, Arnab; Wehrheim, Heike (IEEE International Conference on Software Testing, Verification and Validation (ICST))

Analyzing Data Usage in Array Programs - Haltermann, Jan

Korrektheitsbeweise für Muster von Servicekompositionen - Rautenberg, Kai

On the effectiveness of heuristics for learning nested dichotomies: an empirical analysis - Melnikov, Vitalik; Hüllermeier, Eyke (Machine Learning)
In machine learning, so-called nested dichotomies are utilized as a reduction technique, i.e., to decompose a multi-class classification problem into a set of binary problems, which are solved using a simple binary classifier as a base learner. The performance of the (multi-class) classifier thus produced strongly depends on the structure of the decomposition. In this paper, we conduct an empirical study, in which we compare existing heuristics for selecting a suitable structure in the form of a nested dichotomy. Moreover, we propose two additional heuristics as natural completions. One of them is the Best-of-K heuristic, which picks the (presumably) best among K randomly generated nested dichotomies. Surprisingly, and in spite of its simplicity, it turns out to outperform the state of the art.

JMCTest: Automatically Testing Inter-Method Contracts in Java - Börding, Paul; Haltermann, Jan Frederik; Jakobs, Marie-Christine; Wehrheim, Heike (Proceedings of the IFIP International Conference on Testing Software and Systems (ICTSS 2018))
Over the years, Design by Contract (DbC) has evolved as a powerful concept for program documentation, testing, and verification. Contracts formally specify assertions on (mostly) object-oriented programs: pre- and postconditions of methods, class invariants, allowed call orders, etc. Missing in the long list of properties specifiable by contracts are, however, method correlations: DbC languages fall short on stating assertions relating methods. In this paper, we propose the novel concept of inter-method contract, allowing precisely for expressing method correlations.We present JMC as a language for specifying and JMCTest as a tool for dynamically checking inter-method contracts on Java programs. JMCTest fully automatically generates objects on which the contracted methods are called and the validity of the contract is checked. Using JMCTest, we detected that large Java code bases (e.g. JBoss, Java RT) frequently violate standard inter-method contracts. In comparison to other verification tools inspecting (some) inter-method contracts, JMCTest can find bugs that remain undetected by those tools.

Optimizing the Structure of Nested Dichotomies: A Comparison of Two Heuristics - Melnikov, Vitalik; Hüllermeier, Eyke (Proceedings. 27. Workshop Computational Intelligence, Dortmund, 23. - 24. November 2017)

Testing Java Method Contracts - Börding, Paul

Certiﬁcation Matters for Service Markets - Jakobs, Marie-Christine; Krämer, Julia; van Straaten, Dirk; Lettmann, Theodor (The Ninth International Conferences on Advanced Service Computing (SERVICE COMPUTATION))
Whenever customers have to decide between different instances of the same product, they are interested in buying the best product. In contrast, companies are interested in reducing the construction effort (and usually as a consequence thereof, the quality) to gain profit. The described setting is widely known as opposed preferences in quality of the product and also applies to the context of service-oriented computing. In general, service-oriented computing emphasizes the construction of large software systems out of existing services, where services are small and self-contained pieces of software that adhere to a specified interface. Several implementations of the same interface are considered as several instances of the same service. Thereby, customers are interested in buying the best service implementation for their service composition wrt. to metrics, such as costs, energy, memory consumption, or execution time. One way to ensure the service quality is to employ certificates, which can come in different kinds: Technical certificates proving correctness can be automatically constructed by the service provider and again be automatically checked by the user. Digital certificates allow proof of the integrity of a product. Other certificates might be rolled out if service providers follow a good software construction principle, which is checked in annual audits. Whereas all of these certificates are handled differently in service markets, what they have in common is that they influence the buying decisions of customers. In this paper, we review state-of-the-art developments in certification with respect to service-oriented computing. We not only discuss how certificates are constructed and handled in service-oriented computing but also review the effects of certificates on the market from an economic perspective.