arXiv subjects

Simon Bliudze

Publications and source records attributed to Simon Bliudze.

15 recordsLinked to original sources

arXiv2026

Fancy Some Chips for Your TeaStore? Modeling the Control of an Adaptable Discrete System

When designing new web applications, developers must cope with different kinds of constraints relative to the resources they rely on: software, hardware, network, online micro-services, or any combination of the mentioned entities. Together, these entities form a complex system of communicating interdependent processes, physical or logical. It is very desirable that such system ensures its robustness to provide a good quality of service. In this paper we introduce Chips, a language that aims at facilitating the design of models made of various entwined components. It allows the description of applications in the form of functional blocks. Chips mixes notions from control theory and general purpose programming languages to generate robust component-based models. This paper presents how to use Chips to systematically design, model and analyse a complex system project, using a variation of the Adaptable TeaStore application as running example.

cs.PL↗

arXiv2025

Adaptable TeaStore

Modern cloud-native systems require adapting dynamically to changing operational conditions, including service outages, traffic surges, and evolving user requirements. While existing benchmarks provide valuable testbeds for performance and scalability evaluation, they lack explicit support for studying adaptation mechanisms, reconfiguration strategies, and graceful degradation. These limitations hinder systematic research on self-adaptive architectures in realistic cloud environments. To cover this gap, we introduce Adaptable TeaStore, an extension of the renowned TeaStore architecture that incorporates adaptability as a first-class design concern. Our extension distinguishes between mandatory and optional services, supports multiple component versions -- with varying resource requirements and functionality levels -- considers the outsourcing of functionalities to external providers, and provides local cache mechanisms for performance and resilience. These features enable the systematic exploration of reconfiguration policies across diverse operational scenarios. We discuss a broad catalogue of reference adaptation scenarios centred around Adaptable TeaStore, useful to evaluate the ability of a given adaptation technology to address conditions such as component unavailability, cyberattacks, provider outages, benign/malicious traffic increases, and user-triggered reconfigurations. Moreover, we present an open-source implementation of the architecture with APIs for metrics collection and adaptation triggers, to enable reproducible experiments.

cs.DC↗

arXiv2025

AdaptiFlow: An Extensible Framework for Event-Driven Autonomy in Cloud Microservices

Modern cloud architectures demand self-adaptive capabilities to manage dynamic operational conditions. Yet, existing solutions often impose centralized control models ill-suited to microservices decentralized nature. This paper presents AdaptiFlow, a framework that leverages well-established principles of autonomous computing to provide abstraction layers focused on the Monitor and Execute phases of the MAPE-K loop. By decoupling metrics collection and action execution from adaptation logic, AdaptiFlow enables microservices to evolve into autonomous elements through standardized interfaces, preserving their architectural independence while enabling system-wide adaptability. The framework introduces: (1) Metrics Collectors for unified infrastructure/business metric gathering, (2) Adaptation Actions as declarative actuators for runtime adjustments, and (3) a lightweight Event-Driven and rule-based mechanism for adaptation logic specification. Validation through the enhanced Adaptable TeaStore benchmark demonstrates practical implementation of three adaptation scenarios targeting three levels of autonomy self-healing (database recovery), self-protection (DDoS mitigation), and self-optimization (traffic management) with minimal code modification per service. Key innovations include a workflow for service instrumentation and evidence that decentralized adaptation can emerge from localized decisions without global coordination. The work bridges autonomic computing theory with cloud-native practice, providing both a conceptual framework and concrete tools for building resilient distributed systems. Future work includes integration with formal coordination models and application of adaptation techniques relying on AI agents for proactive adaptation to address complex adaptation scenarios.

cs.SE↗

arXiv2023

SAT-Based Extraction of Behavioural Models for Java Libraries with Collections

Behavioural models are a valuable tool for software verification, testing, monitoring, publishing etc. However, they are rarely provided by the software developers and have to be extracted either from the source or from the compiled code. In the context of Java programs, a number of approaches exist for building behavioural models. Most of these approaches rely on the analysis of the compiled bytecode. Instead, we are looking to extract behavioural models in the form of Finite State Machines (FSMs) from the Java source code to ensure that the obtained FSMs can be easily understood by the software developers and, if necessary, updated or integrated into the original source code, e.g. in the form of annotations. Modern software systems are huge, rely on external libraries and interact with their environment. Hence, extracting useful behavioural models requires abstraction. In this paper, we present an initial approach to this problem by focusing on the extraction of FSMs modelling library APIs. We focus on the analysis of Java code involving the use of collections. To this end, we encode the operational semantics of collection operations using patterns of Boolean predicates. These patterns are instantiated based on the analysis of the source code of API implementation methods to form an encoding of the possible FSM transitions. A SAT solver is then used to determine the enabledness conditions (guards) of these transitions.

cs.SE↗

arXiv2020

Robust Software Development for University-Built Satellites

Satellites and other complex systems now become more and more software dependent. Even nanosatellites have complexity that can be compared to scientific instruments launched to Mars. COTS components and subsystems may now be purchased to support payload development. On the contrary, the software has to be adapted to the new payload and, consequently, hardware architecture selected for the satellite. There is not a rigorous and robust way to design software for CubeSats or small satellites yet. In this paper, we will briefly review some existing systems and present our approach, which based on Behaviour-Interaction-Priority (BIP) framework. We will describe our experience in implementing fight software simulation and testing in the Swiss CubETH CubeSat project. We will conclude with lessons learned and future utilization of BIP for hardware testing and simulation.

cs.DC↗

arXiv2018

Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design

This volume contains the proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design (MeTRiD 2018), held on the 15th of April, 2018 in Thessaloniki, Greece as part of ETAPS 2018, the European Joint Conferences on Theory and Practice of Software. The term "Rigorous System Design" (RSD) denotes the design approach that is based on a formal, accountable and iterative process for deriving trustworthy and optimised implementations from models of application software, its execution platform and its external environment. Ideally, a system implementation is derived from a set of appropriate high-level models by applying a sequence of semantics-preserving transformations. The ambition of MeTRiD is to promote the use of formal methods, in general, and the RSD approach, in particular, in the industrial applications and, reciprocally, bring the attention of the formal methods researchers to such industrial applications in order to develop realistic case-studies and guide the evolution of tools. Striving towards this ambitious goal, we have solicited contributions of three types: - regular papers, presenting original research - case study papers, reporting the evaluation of existing modelling, analysis, transformation and code generation formalisms and tools on realistic examples of significant size - tool papers, describing new tool prototypes supporting the RSD flow and enhancements of existing ones We have received 13 submissions (7 regular, 4 tool and 2 case study papers), whereof 8 have been accepted for presentation at the workshop: - 5 regular papers - 2 tool papers - 1 case study paper In this volume, these papers are complemented by an invited paper by Joseph Sifakis.

cs.SE↗

arXiv2017

Coordination of Dynamic Software Components with JavaBIP

JavaBIP allows the coordination of software components by clearly separating the functional and coordination aspects of the system behavior. JavaBIP implements the principles of the BIP component framework rooted in rigorous operational semantics. Recent work both on BIP and JavaBIP allows the coordination of static components defined prior to system deployment, i.e., the architecture of the coordinated system is fixed in terms of its component instances. Nevertheless, modern systems, often make use of components that can register and deregister dynamically during system execution. In this paper, we present an extension of JavaBIP that can handle this type of dynamicity. We use first-order interaction logic to define synchronization constraints based on component types. Additionally, we use directed graphs with edge coloring to model dependencies among components that determine the validity of an online system. We present the software architecture of our implementation, provide and discuss performance evaluation results.

cs.SE↗

arXiv2016

Architecture Diagrams: A Graphical Language for Architecture Style Specification

Architecture styles characterise families of architectures sharing common characteristics. We have recently proposed configuration logics for architecture style specification. In this paper, we study a graphical notation to enhance readability and easiness of expression. We study simple architecture diagrams and a more expressive extension, interval architecture diagrams. For each type of diagrams, we present its semantics, a set of necessary and sufficient consistency conditions and a method that allows to characterise compositionally the specified architectures. We provide several examples illustrating the application of the results. We also present a polynomial-time algorithm for checking that a given architecture conforms to the architecture style specified by a diagram.

cs.SE↗

arXiv2016

A Note on the Expressiveness of BIP

We extend our previous algebraic formalisation of the notion of component-based framework in order to formally define two forms, strong and weak, of the notion of full expressiveness. Our earlier result shows that the BIP (Behaviour-Interaction-Priority) framework does not possess the strong full expressiveness. In this paper, we show that BIP has the weak form of this notion and provide results detailing weak and strong full expressiveness for classical BIP and several modifications, obtained by relaxing the constraints imposed on priority models.

cs.DC↗

arXiv2015

Relating BIP and Reo

Coordination languages simplify design and development of concurrent systems. Particularly, exogenous coordination languages, like BIP and Reo, enable system designers to express the interactions among components in a system explicitly. In this paper we establish a formal relation between BI(P) (i.e., BIP without the priority layer) and Reo, by defining transformations between their semantic models. We show that these transformations preserve all properties expressible in a common semantics. This formal relation comprises the basis for a solid comparison and consolidation of the fundamental coordination concepts behind these two languages. Moreover, this basis offers translations that enable users of either language to benefit from the toolchains of the other.

cs.PL↗

arXiv2013

Extended Connectors: Structuring Glue Operators in BIP

Based on a variation of the BIP operational semantics using the offer predicate introduced in our previous work, we extend the algebras used to model glue operators in BIP to encompass priorities. This extension uses the Algebra of Causal Interaction Trees, T(P), as a pivot: existing transformations automatically provide the extensions for the Algebra of Connectors. We then extend the axiomatisation of T(P), since the equivalence induced by the new operational semantics is weaker than that induced by the interaction semantics. This extension leads to canonical normal forms for all structures and to a simplification of the algorithm for the synthesis of connectors from Boolean coordination constraints.

cs.LO↗

arXiv2012

Towards a Theory of Glue

We propose and study the notions of behaviour type and composition operator making a first step towards the definition of a formal framework for studying behaviour composition in a setting sufficiently general to provide insight into how the component-based systems should be modelled and compared. We illustrate the proposed notions on classical examples (Traces, Labelled Transition Systems and Coalgebras). Finally, the definition of memoryless glue operators, takes us one step closer to a formal understanding of the separation of concerns principle stipulating that computational aspects of a system should be localised within its atomic components, whereas coordination layer responsible for managing concurrency should be realised by memoryless glue operators.

cs.LO↗

arXiv2011

Proceedings Fourth Interaction and Concurrency Experience

This volume contains the pre-proceedings of ICE'11, the 4th Interaction and Concurrency Experience workshop, which was held in Reykjavik, Iceland on the 9th of June 2011 as a satellite event of DisCoTec'11. The topic of ICE'11 was Reliable and Contract-based Interaction. Reliable interactions are, e.g., those enjoying suitable logical, behavioural, or security properties, or adhering to certain QoS standards. Contract-based interactions are, e.g., those where the interacting entities are committed to give certain guarantees whenever certain assumptions are met by their operating environment. The ICE procedure for paper selection allows for PC members to interact, anonymously, with authors. During the review phase, each submitted paper is published on a Wiki and associated with a discussion forum whose access is restricted to the authors and to all the PC members not declaring a conflict of interests. The PC members post comments and questions that the authors reply to. Each paper was reviewed by four PC members, and altogether 8 papers (out of 12) were accepted for publication. We were proud to host three invited talks by Rocco De Nicola (joint with PACO), Simon Gay and Prakash Panangaden, whose abstracts are included in this volume together with the regular papers.

cs.LO↗

arXiv2010

Proceedings Third Interaction and Concurrency Experience: Guaranteed Interaction

This volume contains the proceedings of the 3rd Interaction and Concurrency Experience (ICE 2010) workshop, which was held in Amsterdam, Netherlands on 10th of June 2010 as a satellite event of DisCoTec'10. Each year, the workshop focuses on a specific topic: the topic of ICE 2010 was Guaranteed Interactions, by which we mean, for example, guaranteeing safety, reactivity, quality of service or satisfaction of analysis hypotheses.

cs.LO↗

arXiv2009

Symbolic Implementation of Connectors in BIP

BIP is a component framework for constructing systems by superposing three layers of modeling: Behavior, Interaction, and Priority. Behavior is represented by labeled transition systems communicating through ports. Interactions are sets of ports. A synchronization between components is possible through the interactions specified by a set of connectors. When several interactions are possible, priorities allow to restrict the non-determinism by choosing an interaction, which is maximal according to some given strict partial order. The BIP component framework has been implemented in a language and a tool-set. The execution of a BIP program is driven by a dedicated engine, which has access to the set of connectors and priority model of the program. A key performance issue is the computation of the set of possible interactions of the BIP program from a given state. Currently, the choice of the interaction to be executed involves a costly exploration of enumerative representations for connectors. This leads to a considerable overhead in execution times. In this paper, we propose a symbolic implementation of the execution model of BIP, which drastically reduces this overhead. The symbolic implementation is based on computing boolean representation for components, connectors, and priorities with an existing BDD package.

cs.SE↗