Personne

Simon Bliudze

Cette personne n’est plus à l’EPFL

Publications associées (36)

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 es ...

2015

Offer semantics: Achieving compositionality, flattening and full expressiveness for the glue operators in BIP

Simon Bliudze, Eduard Baranov

Based on a concise but comprehensive overview of some fundamental properties required from component-based frameworks, namely compositionality, incrementality, flattening, modularity and expressiveness, we review three modifications of the semantics of glu ...

Elsevier2015

A Theory Agenda for Component-Based Design

Simon Bliudze, Joseph Sifakis

The aim of the paper is to present a theory agenda for component-based design based on results that motivated the development of the BIP component framework, to identify open problems and discuss further research directions. The focus is on proposing a sem ...

Springer International Publishing2015

Automatic Fault Localization for BIP

Simon Bliudze, Qiang Wang

This paper presents a novel idea of automatic fault localization by exploiting counterexamples generated by a model checker. The key insight is that, if a candidate statement is faulty, it is possible to modify (i.e. correct) this statement so that the cou ...

Springer2015

Verification of Component-based Systems via Predicate Abstraction and Simultaneous Set Reduction

Simon Bliudze, Qiang Wang

This paper presents a novel safety property verification approach for component-based systems modelled in BIP (Behaviour, Interaction and Priority), encompassing multiparty synchronisation with data transfer and priority. Our contributions consist of: (1 ...

Springer2015

SeBip: a symbolic executor for BIP

Simon Bliudze, Qiang Wang

This paper presents SeBip, the first symbolic executor for component-based systems modelled in BIP (Be- haviour, Interaction and Priority). To tackle the path explosion problem, SeBip combines partial order reduction technique to reduce the number of inter ...

IEEE Computer Society2015

Formal verification of infinite-state BIP models

Simon Bliudze, Wajeb Saab

We propose two expressive and complementary techniques for the verification of safety properties of infinite-state BIP models. Both our techniques deal with the full BIP specification, while the existing approaches impose con- siderable restrictions: they ...

Springer2015

Configuration Logics: Modelling Architecture Styles

Simon Bliudze, Joseph Sifakis, Anastasia Mavridou, Eduard Baranov

We study a framework for the specification of architecture styles as families of architectures involving a common set of types of components and coordination mechanisms. The framework combines two logics: 1) interaction logics for the specification of arch ...

Springer Int Publishing Ag2015

Applying model checking to industrial-sized PLC programs

Simon Bliudze, Jean-Charles Tournier, Borja Fernandez Adiego

Programmable Logic Controllers (PLCs) are embedded computers widely used in industrial control systems. Ensuring that a PLC software complies with its specification is a challenging task. Formal verification has become a recommended practice to ensure the ...

Institute of Electrical and Electronics Engineers2015

Coordination of software components with BIP: application to OSGi

Radoslaw Szymanek, Simon Bliudze, Alina Zolotukhina, Anastasia Mavridou

ACM Press2014

A General Framework for Architecture Composability

Simon Bliudze, Joseph Sifakis, Eduard Baranov

Architectures depict design principles: paradigms that can be understood by all, allow thinking on a higher plane and avoiding low-level mistakes. They provide means for ensuring correctness by construction by enforcing global properties characterizing the ...

Springer International Publishing2014

Reduction and Abstraction Techniques for BIP

Simon Bliudze, Mohammad Noureddine

Reduction and abstraction techniques have been proposed to address the state space explosion problem in verification. In this paper, we present reduction and abstraction techniques for component-based systems modeled in BIP (Behavior, Interaction and Prior ...

Springer2014

Architecture Internalisation in BIP

Simon Bliudze, Joseph Sifakis

We consider two approaches for building component-based systems, which we call respectively architecture-based and architecture-agnostic. The former consists in describing coordination constraints in a purely declarative manner through parameterizable glue ...

ACM2014

Model-based automated testing of critical PLC programs

Simon Bliudze, Jean-Charles Tournier

Testing of critical PLC (Programmable Logic Controller) programs remains a challenging task for control system engineers as it can rarely be automated. This paper proposes a model-based approach which uses the BIP (Behavior, Interactions and Priorities) fr ...

IEEE2013

Extended Connectors: Structuring Glue Operators in BIP

Simon Bliudze, Eduard Baranov

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 ...

2013

Towards a Theory of Glue

Simon Bliudze

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-base ...

2012