Showing 1–13 of 13 results for author: Bliudze, S

Adaptable TeaStore

Authors: Simon Bliudze, Giuseppe De Palma, Saverio Giallorenzo, Ivan Lanese, Gianluigi Zavattaro, Brice Arleon Zemtsop Ndadji

Abstract: Adaptability is a fundamental requirement for modern Cloud software architectures to ensure robust performance in the face of diverse known and unforeseen events inherent to distributed systems. State-of-the-art Cloud systems frequently adopt microservices or serverless architectures. Among these, TeaStore is a recognised microservice reference architecture that offers a benchmarking framework for… ▽ More Adaptability is a fundamental requirement for modern Cloud software architectures to ensure robust performance in the face of diverse known and unforeseen events inherent to distributed systems. State-of-the-art Cloud systems frequently adopt microservices or serverless architectures. Among these, TeaStore is a recognised microservice reference architecture that offers a benchmarking framework for modelling and resource management techniques. However, TeaStore's original configuration lacks the flexibility necessary to address the varied scenarios encountered in real-world applications. To overcome this limitation, we propose an enhanced variant of TeaStore that distinguishes between mandatory and optional services while incorporating third-party service integration. Core services such as WebUI, Image Provider, and Persistence are designated as mandatory to maintain essential functionality, whereas optional services, such as Recommender and Auth, extend the architecture's feature set. We outline the design and configuration possibilities of this adaptable TeaStore variant, aimed at enabling a broader spectrum of configurability and operational resilience. △ Less

Submitted 20 December, 2024; originally announced December 2024.

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

Authors: Larisa Safina, Simon Bliudze

Abstract: 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 byte… ▽ More 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. △ Less

Submitted 8 November, 2023; v1 submitted 30 May, 2022; originally announced May 2022.

Robust Software Development for University-Built Satellites

Authors: Anton B. Ivanov, Simon Bliudze

Abstract: 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 satellit… ▽ More 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. △ Less

Submitted 4 October, 2020; originally announced October 2020.

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

Authors: Simon Bliudze, Saddek Bensalem

Abstract: 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 iterati… ▽ More 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. △ Less

Submitted 25 June, 2018; originally announced June 2018.

Journal ref: EPTCS 272, 2018

Coordination of Dynamic Software Components with JavaBIP

Authors: Anastasia Mavridou, Valentin Rutz, Simon Bliudze

Abstract: 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 coord… ▽ More 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. △ Less

Submitted 15 August, 2017; v1 submitted 31 July, 2017; originally announced July 2017.

Comments: Technical report that accompanies the paper accepted at the 14th International Conference on Formal Aspects of Component Software

Architecture Diagrams: A Graphical Language for Architecture Style Specification

Authors: Anastasia Mavridou, Eduard Baranov, Simon Bliudze, Joseph Sifakis

Abstract: 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… ▽ More 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. △ Less

Submitted 10 August, 2016; originally announced August 2016.

Comments: In Proceedings ICE 2016, arXiv:1608.03131

ACM Class: D2.2; D.2.11; D.2.13

Journal ref: EPTCS 223, 2016, pp. 83-97

A Note on the Expressiveness of BIP

Authors: Eduard Baranov, Simon Bliudze

Abstract: 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 d… ▽ More 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. △ Less

Submitted 10 August, 2016; originally announced August 2016.

Comments: In Proceedings EXPRESS/SOS 2016, arXiv:1608.02692

Journal ref: EPTCS 222, 2016, pp. 1-14

Relating BIP and Reo

Authors: Kasper Dokter, Sung-Shik Jongmans, Farhad Arbab, Simon Bliudze

Abstract: 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 mod… ▽ More 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. △ Less

Submitted 19 August, 2015; originally announced August 2015.

Comments: In Proceedings ICE 2015, arXiv:1508.04595

ACM Class: D.3.1

Journal ref: EPTCS 189, 2015, pp. 3-20

Extended Connectors: Structuring Glue Operators in BIP

Authors: Eduard Baranov, Simon Bliudze

Abstract: 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 axiomatisati… ▽ More 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. △ Less

Submitted 16 October, 2013; originally announced October 2013.

Comments: In Proceedings ICE 2013, arXiv:1310.4019

Journal ref: EPTCS 131, 2013, pp. 20-35

Towards a Theory of Glue

Authors: Simon Bliudze

Abstract: 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 Coa… ▽ More 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. △ Less

Submitted 16 December, 2012; originally announced December 2012.

Comments: In Proceedings ICE 2012, arXiv:1212.3458

ACM Class: F.3.2

Journal ref: EPTCS 104, 2012, pp. 48-66

Proceedings Fourth Interaction and Concurrency Experience

Authors: Alexandra Silva, Simon Bliudze, Roberto Bruni, Marco Carbone

Abstract: 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 cert… ▽ More 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. △ Less

Submitted 31 July, 2011; originally announced August 2011.

Journal ref: EPTCS 59, 2011

Proceedings Third Interaction and Concurrency Experience: Guaranteed Interaction

Authors: Simon Bliudze, Roberto Bruni, Davide Grohmann, Alexandra Silva

Abstract: 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 sat… ▽ More 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. △ Less

Submitted 25 October, 2010; originally announced October 2010.

Journal ref: EPTCS 38, 2010

Symbolic Implementation of Connectors in BIP

Authors: Mohamad Jaber, Ananda Basu, Simon Bliudze

Abstract: 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, pri… ▽ More 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. △ Less

Submitted 29 November, 2009; originally announced November 2009.

Journal ref: EPTCS 12, 2009, pp. 41-55