Systematic model-driven design and early validation enable engineers to verify that a reactive system does not violate its requirements before actually implementing it. Requirements may come from multiple stakeholders, who are often concerned with different facets – design typically involves different experts having different concerns and views of the system. Engineers start from a specification which may be sourced from some domain model, while validation is often done on state-transition structures that support model checking. Two computationally expensive steps may work against scalability: transformation from specification to state-transition structures, and model checking. We propose a technique that makes the former efficient and also makes the resulting transition systems small enough to be efficiently verified. The technique automatically projects the specification into submodels depending on a property sought to be evaluated, which captures some stakeholder’s viewpoint. The resulting reactive system submodel is then transformed into a state-transition structure and verified. The technique achieves cone-of-influence reduction, by slicing at the specification model level. Submodels are analysis-equivalent to the corresponding full model. If stakeholders propose a change to a submodel based on their own view, changes are automatically propagated to the specification model and other views affected. Automated reflection is achieved thanks to bidirectional model transformations, ensuring correctness. We cast our proposal in the context of graph-based reactive models whose dynamics is described by rewriting rules. We demonstrate our view-based framework in practice on a case study within cyber-physical systems.

Christos Tsigkanos

TU Vienna

Austria

NIANYU LI

Peking University, China

China

Zhi Jin

Peking University

Zhenjiang Hu

Peking University, China

Carlo Ghezzi

Politecnico di Milano

Italy

Signal-based temporal properties (SBTPs) characterize the behavior of a system when its inputs and outputs are signals over time; they are very common for the requirements specification of cyber-physical systems. Although there exist several specification languages for expressing SBTPs, such languages either do not easily allow the specification of important types of properties (such as spike or oscillatory behaviors), or are not supported by (efficient) trace-checking procedures.

In this paper, we propose SB-TemPsy, a novel model-driven trace-checking approach for SBTPs. SB-TemPsy provides (i) SB-TemPsy-DSL, a domain-specific language that allows the specification of SBTPs covering the most frequent requirement types in cyber-physical systems, and (ii) SB-TemPsy-Check, an efficient, model-driven trace-checking procedure. This procedure reduces the problem of checking an SB-TemPsy-DSL property over an execution trace to the problem of evaluating an Object Constraint Language constraint on a model of the execution trace.

We evaluated our contributions by assessing the expressiveness of SB-TemPsy-DSL and the applicability of SB-TemPsy-Check using a representative industrial case study in the satellite domain. SB-TemPsy-DSL could express 97% of the requirements of our case study and SB-TemPsy-Check yielded a trace-checking verdict in 87% of the cases, with an average checking time of 48.7 s. From a practical standpoint and compared to state-of-the-art alternatives, our approach strikes a better trade-off between expressiveness and performance as it supports a large set of property types that can be checked, in most cases, within practical time limits.

Chaima Boufaied

University of Luxembourg

Claudio Menghi

University of Luxembourg, Luxembourg

Domenico Bianculli

University of Luxembourg

Luxembourg

Lionel Briand

SnT Centre/University of Luxembourg

Luxembourg

Yago Isasi Parache

LuxSpace

High-fidelity Graphical User Interface (GUI) prototyping is a well-established and suitable method for enabling fruitful discussions, clarification and refinement of requirements formulated by customers. GUI prototypes can help to reduce misunderstandings between customers and developers, which may occur due to the ambiguity comprised in informal Natural Language (NL). However, a disadvantage of employing high-fidelity GUI prototypes is their time-consuming and expensive development. Common GUI prototyping tools are based on combining individual GUI components or manually crafted templates. In this work, we present GUI2WiRe, a tool that enables users to retrieve GUI prototypes from a semi-automatically created large-scale GUI repository for mobile applications matching user requirements specified in Natural Language (NLR). We extract multiple text segments from the GUI hierarchy data and employ various Information Retrieval (IR) models and Automatic Query Expansion (AQE) techniques to achieve ad-hoc GUI retrieval from NLR. Retrieved GUI prototypes mined from applications can be inserted in the graphical editor of GUI2WiRe to rapidly create wireframes. GUI components are extracted automatically from the GUI screenshots and basic editing functionality is provided to the user. Finally, a preview of the application is created from the wireframe to allow interactive exploration of the current design. We evaluated the applied IR and AQE approaches for their effectiveness in terms of GUI retrieval relevance on a manually annotated collection of NLR and discuss our planned user studies.

Kristian Kolthoff

Institute for Enterprise Systems (InES), University Of Mannheim

Germany

Christian Bartelt

Institute for Software and Systems Engineering, TU Clausthal

Simone Paolo Ponzetto

Data and Web Science Group, University of Mannheim

Mobile operating systems evolve quickly, frequently updating the APIs that app developers use to build their apps. Unfortunately, API updates do not always guarantee backward compatibility, causing apps to not longer work properly or even crash when running with an updated system. This paper presents FILO, a tool that assists Android developers in resolving backward compatibility issues introduced by API upgrades. FILO both suggests the method that needs to be modified in the app in order to adapt the app to an upgraded API, and reports key symptoms observed in the failed execution to facilitate the fixing activity. Results obtained with the analysis of 12 actual upgrade problems and the feedback produced by early tool adopters show that FILO can practically support Android developers. FILO can be downloaded from https://gitlab.com/learnERC/filo, and its video demonstration is available at https://youtu.be/WDvkKj-wnlQ.

Marco Mobilio

University of Milano Bicocca

Italy

Oliviero Riganelli

University of Milano-Bicocca, Italy

Daniela Micucci

University of Milano-Bicocca, Italy

Italy

Leonardo Mariani

University of Milano Bicocca

Italy

As most smart systems such as smart logistic and smart manufacturing are delay sensitive, the current mainstream cloud computing based system architecture is facing the critical issue of high latency over the Internet. Meanwhile, as huge amount of data is generated by smart devices with limited battery and computing power, the increasing demand for energy-efficient machine learning and secure data communication at the network edge has become a hurdle to the success of smart systems. To address these challenges with using smart UAV (Unmanned Aerial Vehicle) delivery system as an example, we propose EXPRESS, a novel energy-efficient and secure framework based on mobile edge computing and blockchain technologies. We focus on computation and data (resource) management which are two of the most prominent components in this framework. The effectiveness of the EXPRESS framework is demonstrated through the implementation of a real-world UAV delivery system. As an open-source framework, EXPRESS can help researchers implement their own prototypes and test their computation and data management strategies in different smart systems. The demo video can be found at https://youtu.be/r3U1iU8tSmk.

Jia Xu

School of Computer Science and Technology, Anhui University

Xiao Liu

School of Information Technology, Deakin University

Australia

Xuejun Li

School of Computer Science and Technology, Anhui University

Lei Zhang

Antwork Robotics Co., Ltm., Hangzhou, China

Yun Yang

Swinburne University of Technology

Over the last few years, there has been substantial research on automated analysis, testing, and debugging of Ethereum smart contracts. However, it is not trivial to compare and reproduce that research.

To address this, we present SmartBugs, an extendable and easy-to-use execution framework that simplifies the execution of analysis tools on smart contracts written in Solidity, the primary language used in Ethereum.

SmartBugs is currently distributed with support for 10 tools and two datasets of Solidity contracts. The first dataset can be used to evaluate the precision of analysis tools, as it contains 143 annotated vulnerable contracts with 208 tagged vulnerabilities. The second dataset contains 47,518 unique contracts collected through Etherscan.

We discuss how SmartBugs supported the largest experimental setup to date both in the number of tools and in execution time. Moreover, we show how it enables easy integration and comparison of analysis tools by presenting a new extension to the tool Smartcheck that improves substantially the detection of vulnerabilities related to the DASP10 categories Bad Randomness, Time Manipulation, and Access Control (identified vulnerabilities increased from 11% to 24%).

João F. Ferreira

INESC-ID and IST, University of Lisbon

Portugal

Pedro Cruz

IST, University of Lisbon, Portugal

Thomas Durieux

KTH Royal Institute of Technology, Sweden

Sweden

Rui Abreu

Faculty of Engineering, University of Porto, Portugal

Portugal

One the one hand, as a GitHub profile is becoming an essential part of a developer’s resume it becomes increasingly important to enable HR departments to extract someone’s expertise, through automated analysis of his/her contribution to open-source projects. On the other hand, having clear insights on the technologies used in a project can be very beneficial for resource allocation and project maintainability planning. In the literature, one can identify various approaches for identifying expertise on programming languages, based on the projects that developer contributed to. In this paper, we move one step further and introduce an approach (accompanied by a tool) to identify low-level expertise on particular software frameworks and technologies apart, relying solely on GitHub data, using the GitHub API and Natural Language Processing (NLP)—using the Microsoft Language Understanding Intelligent Service (LUIS). In particular, we developed an NLP model in LUIS for named-entity recognition for three (3) .NET technologies and two (2) front-end frameworks. Our analysis is based upon specific commit contents, in terms of the exact code chunks, which the committer added or changed. We evaluate the precision, recall and f-measure for the derived technologies/frameworks, by conducting a batch test in LUIS and report the results. The proposed approach is demonstrated through a fully functional web application named RepoSkillMiner.

Tool Links: Video, Code Repo, Application, Validation Dataset

CCS CONCEPTS • Software and its engineering → Software creation and manage-ment -> Software post-development issues;

KEYWORDS Expertise; Frameworks; GitHub; Natural Language Processing; Soft-ware Project Management;

Efstratios Kourtzanidis

University Of Macedonia

Alexander Chatzigeorgiou

University of Macedonia

Greece

Apostolos Ampatzoglou

University of Macedonia

In this paper, we present Sosed, a tool for discovering similar software projects. We use fastText to compute the embeddings of sub-tokens into a dense space for 120,000 GitHub repositories in 200 languages. Then, we cluster embeddings to identify groups of semantically similar sub-tokens that reflect topics in source code. We use a dataset of 9 million GitHub projects as a reference search base. To identify similar projects, we compare the distributions of clusters among their sub-tokens. The tool receives an arbitrary project as input, extracts sub-tokens in 16 most popular programming languages, computes cluster distribution, and finds projects with the closest distribution in the search base. We labeled sub-token clusters with short descriptions to enable Sosed to produce interpretable output.

Sosed is available at https://github.com/JetBrains-Research/sosed/. The tool demo is available at https://www.youtube.com/watch?v=LYLkztCGRt8. The multi-language extractor of sub-tokens is available separately at https://github.com/JetBrains-Research/identifiers-extractor/.

Egor Bogomolov

JetBrains Research

Yaroslav Golubev

JetBrains Research, ITMO University

Russia

Artyom Lobanov

JetBrains Research

Vladimir Kovalenko

JetBrains Research, JetBrains N.V.

Timofey Bryksin

JetBrains Research, Saint Petersburg State University

Russia