Atif Mashkoor

Usman Ashraf, Christoph Mayr-Dorn, Atif Mashkoor et al.

Studies over the past decade demonstrated that developers contributing to open source software systems tend to self-organize in "emerging" communities. This latent community structure has a significant impact on software quality. While several approaches address the analysis of developer interaction networks, the question of whether these emerging communities align with the developer teams working on various subsystems remains unanswered. Work on socio-technical congruence implies that people that work on the same task or artifact need to coordinate and thus communicate, potentially forming stronger interaction ties. Our empirical study of 10 open source projects revealed that developer communities change considerably across a project's lifetime (hence implying that relevant relations between developers change) and that their alignment with subsystem developer teams is mostly low. However, subsystems teams tend to remain more stable. These insights are useful for practitioners and researchers to better understand developer interaction structure of open source systems.

Sebastian Stock, Jannik Dunkelau, Atif Mashkoor

Context: With artificial intelligence (AI) being well established within the daily lives of research communities, we turn our gaze toward formal methods (FM). FM aim to provide sound and verifiable reasoning about problems in computer science. Objective: We conduct a systematic mapping study to overview the current landscape of research publications that apply AI to FM. We aim to identify how FM can benefit from AI techniques and highlight areas for further research. Our focus lies on the previous five years (2019-2023) of research. Method: Following the proposed guidelines for systematic mapping studies, we searched for relevant publications in four major databases, defined inclusion and exclusion criteria, and applied extensive snowballing to uncover potential additional sources. Results: This investigation results in 189 entries which we explored to find current trends and highlight research gaps. We find a strong focus on AI in the area of theorem proving while other subfields of FM are less represented. Conclusions: The mapping study provides a quantitative overview of the modern state of AI application in FM. The current trend of the field is yet to mature. Many primary studies focus on practical application, yet we identify a lack of theoretical groundwork, standard benchmarks, or case studies. Further, we identify issues regarding shared training data sets and standard benchmarks.

Michael Alexander Tröls, Atif Mashkoor, Alexander Egyed

Consistency checking of interdependent heterogeneous engineering artifacts, such as requirements, specifications, and code, is a challenging task in large-scale engineering projects. The lack of team-oriented solutions allowing a multitude of project stakeholders to collaborate in a consistent manner is thus becoming a critical problem. In this context, this work proposes an approach for team-oriented consistency checking of collaboratively developed heterogeneous engineering artifacts.

Saad Shafiq, Atif Mashkoor, Christoph Mayr-Dorn et al.

In this paper, we propose a recommendation approach -- TaskAllocator -- in order to predict the assignment of incoming tasks to potential befitting roles. The proposed approach, identifying team roles rather than individual persons, allows project managers to perform better tasks allocation in case the individual developers are over-utilized or moved on to different roles/projects. We evaluated our approach on ten agile case study projects obtained from the Taiga.io repository. In order to determine the TaskAllocator's performance, we have conducted a benchmark study by comparing it with contemporary machine learning models. The applicability of the TaskAllocator was assessed through a plugin that can be integrated with JIRA and provides recommendations about suitable roles whenever a new task is added to the project. Lastly, the source code of the plugin and the dataset employed have been made public.

Atif Mashkoor, Michael Leuschel, Alexander Egyed

Traditionally, practitioners use formal methods pre-dominately for one half of the quality-assurance process: verification (do we build the software right?). The other half -- validation (do we build the right software?) -- has been given comparatively little attention. While verification is the core of refinement-based formal methods, where each new refinement step must preserve all properties of its abstract model, validation is usually postponed until the latest stages of the development, when models can be automatically executed. Thus mistakes in requirements or in their interpretation are caught too late: usually at the end of the development process. In this paper, we present a novel approach to check compliance between requirements and their formal refinement-based specification during the earlier stages of development. Our proposed approach -- "validation obligations" -- is based on the simple idea that both verification and validation are an integral part of all refinement steps of a system.

Saad Shafiq, Atif Mashkoor, Christoph Mayr-Dorn et al.

Context: The software development industry is rapidly adopting machine learning for transitioning modern day software systems towards highly intelligent and self-learning systems. However, the full potential of machine learning for improving the software engineering life cycle itself is yet to be discovered, i.e., up to what extent machine learning can help reducing the effort/complexity of software engineering and improving the quality of resulting software systems. To date, no comprehensive study exists that explores the current state-of-the-art on the adoption of machine learning across software engineering life cycle stages. Objective: This article addresses the aforementioned problem and aims to present a state-of-the-art on the growing number of uses of machine learning in software engineering. Method: We conduct a systematic mapping study on applications of machine learning to software engineering following the standard guidelines and principles of empirical software engineering. Results: This study introduces a machine learning for software engineering (MLSE) taxonomy classifying the state-of-the-art machine learning techniques according to their applicability to various software engineering life cycle stages. Overall, 227 articles were rigorously selected and analyzed as a result of this study. Conclusion: From the selected articles, we explore a variety of aspects that should be helpful to academics and practitioners alike in understanding the potential of adopting machine learning techniques during software engineering projects.

Atif Mashkoor, Alexander Egyed, Robert Wille

This paper presents a systematic mapping study on the model-driven engineering of safety and security concerns in systems. Integrated modeling and development of both safety and security concerns is an emerging field of research. Our mapping study provides an overview of the current state-of-the-art in this field. Through a rigorous and systematic process, this study carefully selected 95 publications out of 17,927 relevant papers published between 1992 and 2018. This paper then proposes and answers several relevant research questions about frequently used methods, development stages where these concerns are typically investigated in, or application domains. Additionally, we identify the community's preference for publication venues and trends.

Andreea Buga, Sorana Tania Nemes, Atif Mashkoor

Cloud-enabled large-scale distributed systems orchestrate resources and services from various providers in order to deliver high-quality software solutions to the end users. The space and structure created by such technological advancements are immense sources of information and impose a high complexity and heterogeneity, which might lead to unexpected failures. In this chapter, we present a model that coordinates the multi-cloud interaction through the specification, validation, and verification of a middle-ware exploiting monitoring and adaptation processes. The monitoring processes handle collecting meaningful data and assessing the state of components, while the adaptation processes restore the system as dictated by the evolution needs and sudden changes in the operating environment conditions. We employ Abstract State Machines to specify the models and we further make use of the ASMETA framework to simulate and validate them. Desired properties of the system are defined and analysed with the aid of the Computation Tree Logic.

Atif Mashkoor

Advanced medical devices exploit the advantages of embedded software whose development is subject to compliance with stringent requirements of standardization and certification regimes due to the critical nature of such systems. This paper presents initial results and lessons learned from an ongoing project focusing on the development of a formal model of a subsystem of a software-controlled safety-critical Active Medical Device (AMD) responsible for renal replacement therapy. The use of formal approaches for the development of AMDs is highly recommended by standards and regulations, and motivates the recent advancement of the state of the art of related methods and tools including Event-B and Rodin applied in this paper. It is expected that the presented model development approach and the specification of a high-confidence medical system will contribute to the still sparse experience base available at the disposal of the scientific and practitioner community of formal methods and software engineering.

Atif Mashkoor, Miklos Biro

The use of embedded software is advancing in modern medical devices, so does its capabilities and complexity. This paradigm shift brings many challenges such as an increased rate of medical device failures due to software faults. In this letter, we present a rigorous correct by construction approach for the trustworthy development of hemodialysis machines, a sub-class of active medical devices. We show how informal requirements of hemodialysis machines are modeled and analyzed through a rigorous process and suggest a generalization to a larger class of active medical devices.