Alexandr Naumchev

Exigences orientées objets dans un cycle de vie continu: L'évolution constante des besoins des clients et des utilisateurs exige une réponse rapide de la part des équipes logicielles. Cela crée une forte demande pour un fonctionnement sans rupture des processus logiciels. L'intégration, la livraison et le déploiement continus, également connus sous le nom de DevOps, ont fait d'énormes progrès en rendant les processus logiciels réactifs au changement. Ces progrès n'ont toutefois eu que peu d'effets sur les exigences en matière de logiciels. Aujourd'hui, la plupart des besoins sont exprimés en langage naturel. Cette approche a un grand pouvoir expressif, mais au détriment d'autres aspects de la qualité des exigences telles que la traçabilité, la réutilisabilité, la vérifiabilité et la compréhensibilité. Le défi est ici d'améliorer ces aspects sans sacrifier l'expressivité. Bertrand Meyer, dans sa méthode multi-exigences, relève ce défi et propose d'exprimer les besoins individuels en trois couches : sous-ensemble déclaratif d'un langage de programmation orienté objet, langage naturel et notation graphique. Cette approche a motive et inspire les travaux de la présente thèse. Alors que l'approche multiexigences se concentre sur la traçabilité et la compréhensibilité, l'approche Seamless Object-Oriented Requirements (SOOR) présentée dans cette thèse prend en compte la vérifiabilité, la réutilisabilité et la compréhensibilité. Cette thèse explore l'hypothèse de Martin Glinz selon laquelle, pour soutenir la continuité, les exigences logicielles devraient être des objets. L'exploration confirme l'hypothèse et aboutit à un ensemble de méthodes basées sur des outils pour spécifier, valider, vérifier et réutiliser les exigences orientées objets. La contribution technique réutilisable la plus importante de cette thèse est une bibliothèque Eiffel prête à l'emploi de patrons de classes, qui capturent les modèles d'exigences logicielles récurrents. Les exigences orientées objets, concrètes et sans rupture, héritent de ces patrons et deviennent des clients du logiciel spécifié. La construction de logiciels orientés objets devient la méthode de spécification, de validation et de réutilisation des exigences ; la conception par contrat devient la méthode de vérification de l'exactitude des implémentations par rapport aux exigences. Cette thèse s'appuie sur plusieurs expériences et montre que la nouvelle approche propose favorise la vérifiabilité, la réutilisabilité et la compréhensibilité des exigences tout en maintenant l'expressivité à un niveau acceptable. Les expérimentations mettent en oeuvre plusieurs exemples, dont certains sont des standards de l'état de l'art de l'ingénierie des exigences. Chaque expérimentation illustre un problème par un exemple, propose une solution générale et montre comment la solution règle le problème. Alors que l'expérimentation s'appuie sur Eiffel et son support d'outils avancés, tels que la preuve et les tests automatisés, chaque idée présentée dans l'approche SOOR s'adapte conceptuellement à tout langage de programmation orienté objet typé statiquement, possédant un mécanisme de généricité et un support élémentaire pour les contrats.

In this study, we propose a novel adaptive algorithm for approximate nearest neighbor (ANN) search, based on the inverted file (IVF) index (cluster-based index) and online query complexity classification. The concept of the classical IVF search implemented in vector databases is as follows: all data vectors are divided into clusters, and each cluster is assigned to its central point (centroid). For an ANN search query, the closest centroids are determined, and the further search continues in the corresponding clusters only. In our study, the complexity of each query is assessed and classified with the use of results of an initial trial search in a limited number of clusters. Based on this classification, the algorithm dynamically determines the presumably sufficient number of clusters which is sufficient to achieve the desired Recall value, thereby improving vector search efficiency. Our experiments show that such a complexity classifier can be built with the use of a single feature, and we propose an algorithm for its training. We studied the impact of various features on the query processing and discovered a strong dependence on the number of clusters that contains at least one nearest neighbor (productive clusters). The new algorithm is designed to be implemented on top of the IVF search which is a well-known algorithm for approximate nearest neighbor search and uses existing IVF indexes that are widely used in the most popular vector database management systems, such as pgvector. The results obtained demonstrate a significant increase in the speed of nearest neighbor search (up to 35%) while maintaining a high Recall rate of 0.99. Additionally, the search algorithm is deterministic, which might be extremely important for tasks where the reproducibility of results plays a crucial role. The developed algorithm has been tested on datasets of varying sizes up to one billion data vectors.

Requirements identification in textual documents or extraction is a tedious and error prone task that many researchers suggest automating. We manually annotated the PURE dataset and thus created a new one containing both requirements and non-requirements. Using this dataset, we fine-tuned the BERT model and compare the results with several baselines such as fastText and ELMo. In order to evaluate the model on semantically more complex documents we compare the PURE dataset results with experiments on Request For Information (RFI) documents. The RFIs often include software requirements, but in a less standardized way. The fine-tuned BERT showed promising results on PURE dataset on the binary sentence classification task. Comparing with previous and recent studies dealing with constrained inputs, our approach demonstrates high performance in terms of precision and recall metrics, while being agnostic to the unstructured textual input.

A major determinant of the quality of software systems is the quality of their requirements, which should be both understandable and precise. Most requirements are written in natural language, which is good for understandability but lacks precision. To make requirements precise, researchers have for years advocated the use of mathematics-based notations and methods, known as “formal.” Many exist, differing in their style, scope, and applicability. The present survey discusses some of the main formal approaches and compares them to informal methods. The analysis uses a set of nine complementary criteria, such as level of abstraction, tool availability, and traceability support. It classifies the approaches into five categories based on their principal style for specifying requirements: natural-language, semi-formal, automata/graphs, mathematical, and seamless (programming-language-based). It includes examples from all of these categories, altogether 21 different approaches, including for example SysML, Relax, Eiffel, Event-B, and Alloy. The review discusses a number of open questions, including seamlessness, the role of tools and education, and how to make industrial applications benefit more from the contributions of formal approaches.

The extent of formal verification methods applied to industrial projects has always been limited. The proliferation of distributed ledger systems (DLS), also known as blockchain, is rapidly changing the situation. Since the main area of DLSs' application is the automation of financial transactions, the properties of predictability and reliability are critical for implementing such systems. The actual behavior of the DLS is determined by the chosen consensus protocol, which properties require strict specification and formal verification. Formal specification and verification of the consensus protocol is necessary but not sufficient. It is required to ensure that the software implementation of the DLS nodes complies with this protocol. The verified software implementation of the protocol must run on a fairly reliable operating system. The so-called “smart contracts”, which are an important part of the applied implementations of specific business processes based on DLSs, must be verifiable as well. In this paper, we describe an ongoing industrial project that will result in a DLS verified at least at the four technological levels described above. We then share our experience with the formal specification and verification of HotStuff, a leader-based fault-tolerant protocol that ensures reaching distributed consensus in the presence of Byzantine processes.

This paper presents a case study to examine the affinity of the code review process among young developers in an academic setting. Code review is indispensable considering the positive outcomes it generates. However, it is not an individual activity and requires substantial interaction among stakeholders, deliverance, and acceptance of feedback, timely actions upon feedback as well as the ability to agree on a solution in the wake of diverse viewpoints. Young developers in a classroom setting provide a clear picture of the potential favourable and problematic areas of the code review process. Their feedback suggests that the process has been well received with some points to better the process. This paper can be used as guidelines to perform code reviews in the classroom.

The considerable effort of writing requirements is only worthwhile if the result meets two conditions: the requirements reflect stakeholders' needs, and the implementation satisfies them. In usual approaches, the use of different notations for requirements (often natural language) and implementations (a programming language) makes both conditions elusive. AutoReq, presented in this article, takes a different approach to both the writing of requirements and their verification. Applying the approach to a well-documented example, a landing gear system, allowed for a mechanical proof of consistency and uncovered an error in a published discussion of the problem.