Whenever software components process personal or private data, appropriate data protection mechanisms are mandatory. An essential factor in achieving trust and transparency is not to give preference to a single party but to make it possible to audit the data usage in an unbiased way. The scenario in mind for this contribution contains (i) users bringing in sensitive data they want to be safe, (ii) service developers building software-based services whose Intellectual Properties (IPs) they desire to protect, and (iii) platform providers wanting to be trusted and to be able to rely on the component developers integrity. The authors see these interests as an insufficiently solved field of tension that can be relaxed by a suitable level of transparently represented software components to give insights without exposing every detail.

Christian Schindler

Institute for Enterprise Systems, University of Mannheim

Formal specifications in \textsf{Alloy} are organized around user-defined data domains, associated with \emph{signatures}, with almost no support for built-in datatypes. This minimality in the built-in datatypes provided by the language is one of its main features, as it contributes to the automated analyzability of models. One of the few built-in datatypes available in Alloy specifications are integers, whose SAT-based treatment allows only for small bit-widths. In many contexts, where relational datatypes dominate, the use of integers may be auxiliary, e.g., in the use of cardinality constraints and other features. However, as the applications of \textsf{Alloy} are increased, e.g., with the use of the language and its tool support as backend engine for different analysis tasks, the provision of efficient support for numerical datatypes becomes a need. In this work, we present our current preliminary approach to providing an efficient, scalable and user-friendly extension to \textsf{Alloy}, with arithmetic support for numerical datatypes. Our implementation allows for arithmetic with varying precisions, and is implemented via standard \textsf{Alloy} constructions, thus resorting to SAT solving for resolving arithmetic constraints in models.

Cesar Cornejo

University of Rio Cuarto and CONICET

Argentina

Given that creating an in-house test lab is expensive and time-consuming to maintain, companies and app developers often use device clouds to test their apps. To ensure that this service is functional, cloud organizations need to use management software to control test executions and perform frequent system updates to patch possible issues with the devices. In this paper, we present a preliminary study investigating issues and highlighting research opportunities for managing and maintaining device clouds. In the study, we analyzed more than 12 million test executions on 110 devices. We found that the management software of the cloud infrastructure we considered affected some test executions, and almost all the cloud devices had at least one security-related issue.

Mattia Fazzini

University of Minnesota

United States

Alessandro Orso

Georgia Tech

United States

The design and development of production-grade microservice backends is a tedious and error-prone task. In particular, they must be capable of handling all Functional Requirements (FRs) and all Non-Functional Requirements (NFRs) (like security) including all operational requirements (like monitoring). This becomes even more difficult if there are many clients with different roles, linked to diverse (non-)functional requirements and many existing services are involved, which have to consider these in a consistent way. In this paper, we present a model-driven approach that automatically generates client-specific production-grade backends by incorporating previously expressed architectural knowledge out of an interpretable specification of the targeted APIs and the NFRs.

Nils Wieber

Institute for Enterprise Systems (InES), University of Mannheim

Software reliability is a primary concern in the construction of software, and thus a fundamental component in the definition of software quality. Analyzing software reliability requires a \emph{specification} of the intended behavior of the software under analysis. Unfortunately, software many times lacks such specifications. This issue seriously diminishes the analyzability of software with respect to its reliability. Thus, finding novel techniques to capture the intended software behavior in the form of specifications would allow us to exploit them for automated reliability analysis.

Our research focuses on the application of learning techniques to automatically distinguish correct from incorrect software behavior. The aim here is to decrease the developer’s effort in specifying oracles, and instead \emph{generating} them from actual software behaviors.

Facundo Molina

University of Río Cuarto

Argentina