Search

Number of sources in the bibliography: 147 Thesis (Ph. D.) -- University of Cyprus, Faculty of Pure and Applied Sciences, Department of Computer Science, 2020. The University of Cyprus Library holds the printed form of the thesis Ο αναστρέψιμος υπολογισμός είναι μια μη συμβατική μορφή υπολογισμού που επεκτείνει τον τυπικό τρόπο υπολογισμού με τη δυνατότητα αντίστροφης εκτέλεσηs λειτουργιών. Η αναστρεψιμότητα προσέλκυσε πρόσφατα αυξανόμενη προσοχή σε διάφορες ερευνητικές κοινότητες καθώς από τη μία υπόσχεται υπολογισμούς χαμηλής ισχύος και, από την άλλη, είναι εφαρμόσιμη σε μια ποικιλία εφαρμογών. Η διερεύνηση της αναστρεψιμότητας μέσω τυπικών μοντέλων καθορίζει τα θεωρητικά θεμέλια για το τι είναι η αναστρεψιμότητα, ποιο σκοπό εξυπηρετεί, και πως ωφελεί τα φυσικά και τεχνητά συστήματα. Ως εκ τούτου, προτείνουμε μια αναστρέψιμη προσέγγιση για τα δίκτυα Πέτρι, εισάγοντας μηχανισμούς και σχετική λειτουργική σημασιολογία για την αντιμετώπιση των προκλήσεων που έχουν οι κύριες μορφές αναστρεψιμότητας. Τα δίκτυα Πέτρι είναι μια μαθηματική γλώσσα για μοντελοποίηση και συλλογισμό κατανεμημένων συστημάτων. Η πρόταση μας αφορά μία παραλλαγή των δικτύων Πέτρι, που ονομάζεται Αναστρέψιμα Δίκτυα Πέτρι, όπου τα διακριτικά ενός δικτύου ξεχωρίζουν μεταξύ τους με μοναδικές ταυτότητες. Δείχνουμε τη δυνατότητα εφαρμογής της προσέγγισής μας σε ένα μοντέλο μεταβολικής διαδρομής και ένα σύστημα επεξεργασίας συναλλαγών όπου και τα δύο εκδηλώνουν αναστρέψιμη συμπεριφορά. Μια άμεση επέκταση του αρχικού μοντέλου συμπεριλαμβάνει την παροχή πολλαπλών διακριτικών που εκπροσωπούν τον ίδιο τύπο. Μία τέτοια επέκταση σε ένα μοντέλο όπως τα δίκτυα Πέτρι, έχει ως αποτέλεσμα αντίστροφες συγκρούσεις όπου ένα διακριτικό μπορεί να έχει τοποθετηθεί σε μία θέση από διαφορετικές μεταβάσεις. Προτείνουμε λοιπόν μια επέκταση των αναστρέψιμων δικτύων Πέτρι που επιτρέπει πολλαπλά διακριτικά του ίδιου τύπου σε ένα μοντέλο, ενώ παράλληλα διασφαλίζεται ο ντετερμινισμός κατά την αντιστροφή. Συγκεκριμένα, στην προσέγγιση την οποία διερευνούμε, διαφορετικά διακριτικά που βρίσκονται στην ίδια θέση μπορούν να διακριθούν με βάση την πορεία που έχουν ακολουθήσει στο δίκτυο. Αποδεικνύουμε ότι η εκφραστική ισχύς των αναστρέψιμων δικτύων Πέτρι με πολλαπλά διακριτικά είναι ισοδύναμη με εκείνη των αναστρέψιμων δικτύων Πέτρι με μοναδικά διακριτικά. Προτείνουμε επίσης την αντίθετη προσέγγιση, η οποία θεωρεί ότι όλα τα διακριτικά ενός συγκεκριμένου τύπου είναι πανομοιότυπα, αγνοώντας την πορεία που ακολούθησαν κατά την εκτέλεση του δικτύου. Δείχνουμε την ευρωστία αυτής της προσέγγισης ως τεχνική μοντελοποίησης συστημάτων που αφορούν πόρους μέσω ενός παραδείγματος από τη βιοχημεία, γνωστό ως αυτοπροτόλυση του νερού. Και τα δύο προτεινόμενα μοντέλα αναστρέψιμων δικτύων Πέτρι (με μοναδικά ή πολλαπλά διακριτικά) επιτρέπουν την αντιστροφή μεταβάσεων χωρίς περιορισμούς ως προς το πότε και αν θα αντιστραφεί η εκτέλεση ή όχι. Με στόχο να περιορίσουμε την αναστρεψιμότητα, επεκτείνουμε τη σημασιολογία μας συσχετίζοντας τις μεταβάσεις με συνθήκες των οποίων η ικανοποίηση επιτρέπει την εκτέλεση μεταβάσεων προς τα εμπρός/πίσω. Καταλήγοντας, για να διευκολύνουμε την ανάλυση της συμπεριφοράς μοντέλων αναστρέψιμου υπολογισμού διατυπώνουμε στο πλαίσιο μας βασικές ιδιότητες όπως η ασφάλεια και η προσβασημότητα όταν εφαρμόζονται διαφορετικές στρατηγικές αναστρεψιμότητας. Απεικονίζουμε το πλαίσιο μαζί με τις σχετικές ιδιότητες με ένα μοντέλο ενός καινοτόμου, κατανεμημένου αλγορίθμου που επιλέγει κεραίες σε κατανεμημένες σειρές κεραιών. Reversible computation is an unconventional form of computing that extends the standard forward-only mode of computation with the ability to execute a sequence of operations in reverse at any point during computation. Reversibility has recently been attracting increasing attention in various research communities, as on the one hand it promises low-power computation, and on the other hand it is inherent or of interest in a variety of applications. Exploring reversibility through formal models formulates the theoretical foundations of what reversibility is, what purpose it serves, and how it benefits natural and artificial systems. As such, in this thesis we propose a reversible approach to Petri nets by introducing machinery and associated operational semantics to tackle the challenges of the main forms of reversibility. Petri nets are a mathematical language for modelling and reasoning about distributed systems. Our proposal concerns a variation of cyclic Petri nets, called Reversing Petri Nets (RPNs) where tokens are persistent and distinguished from each other by an identity. We demonstrate the applicability of our approach with a model of the ERK signalling pathway and an example of a transaction-processing system both featuring reversible behaviour. An immediate extension of the original model includes allowing multiple tokens of the same base/type to occur in a model. The addition of token multiplicity into a model like Petri nets results in various backward conflicts where a token can be generated in a place because of different transition firings. We therefore propose an extension of reversing Petri nets that allows multiple tokens of the same base/type to occur in a model while still ensuring backward determinism. Specifically, we explore the individual token interpretation where one distinguishes different tokens residing in the same place by keeping track of where they come from. We prove that the expressive power of RPNs with multi tokens is equivalent to that of RPNs with single tokens, and we measure the expressiveness in terms of Labelled Transition Systems (LTSs) up to isomorphism of reachable parts that can be denoted by nets of the respective RPN models. We also propose the collective token interpretation, as the opposite approach to token ambiguity, which considers all tokens of a certain type to be identical, disregarding their history during execution. We show the robustness of this approach as a modelling technique for resource-aware systems by modelling an example from biochemistry, known as the autoprotolysis of water. Both of the proposed models of RPNs (with single or multi tokens) implement the notion of uncontrolled reversibility, meaning that it specifies how to reverse an execution and allows to do so freely, yet it places no restrictions as to when and whether to prefer backward execution over forward execution or vice versa. In this respect, a further aim is to control reversibility by extending our formal semantics where transitions are associated with conditions whose satisfaction allows the execution of transitions in the forward/reversed direction. Finally, in order to facilitate the analysis of the behaviour of reversible models, we formulate the basic properties of our framework such as safety, reachability, precedence and exception when different notions and strategies of reversibility are applied. We illustrate the framework along with the associated properties with a model of a novel, distributed algorithm for antenna selection in distributed antenna arrays.

International audience; The Internet of Things (IoT) advocates for multi-layered platforms from edge devices to Cloud nodes where each layer adopts its own communication standards (media and data formats). While this freedom is optimal for in-layer communication, it puzzles cross-layer integration due to incompatibilities among standards. Also enforcing a unique communication stack within the same IoT platform is not a solution , as it leads to the current phenomenon of IoT islands, where disparate platforms hardly interact with each other. In this paper we tackle the problem of IoT cross-layer and cross-platform integration following a language-based approach. We build on the Jolie programming language, which provides uniform linguistic abstractions to exploit heterogeneous communication stacks, allowing the programmer to specify in a declarative way the desired stack, and to easily change it, even at runtime. Jolie currently supports the main technologies from Service-Oriented Computing, such as TCP/IP, Bluetooth, and RMI at transport level, and HTTP and SOAP at application level. We integrate in Jolie the two most adopted protocols for IoT communication, i.e., CoAP and MQTT. We report our experience on a case study on Cloud-based home automation, and we present high-level concepts valuable both for the general implementation of interoperable systems and for the development of other language-based solutions.

International audience; Behavioral contracts are abstract descriptions of expected communication patterns followed by either clients or servers during their interaction. Behavioral contracts come naturally equipped with a notion of compliance: when a client and a server follow compliant contracts, their interaction is guaranteed to progress or successfully complete. We study two extensions of behavioral contracts, retractable contracts dealing with backtracking and speculative contracts dealing with speculative execution. We show that the two extensions give rise to the same notion of compliance. As a consequence, they also give rise to the same subcontract relation, which determines when one server can be replaced by another preserving compliance. Moreover, compliance and subcontract relation are both decidable in quadratic time. Finally, we study the relationship between retractable contracts and calculi for reversible computing.

International audience; This paper presents a line of research in reversible computing for concurrent systems. This line of research started in 2004 with the definition of the first reversible extensions for concurrent process calculi such as CCS, and is currently heading to the production of practical reversible debuggers for concurrent languages such as Erlang. Main questions that had to be answered during the research include the following. Which is the correct notion of reversibility for concurrent systems? Which history information needs to be stored? How to control the basic reversibility mechanism? How to exploit reversibility for debugging? How to apply reversible debugging to real languages?

[EN] In a reversible language, any forward computation can be undone by a finite sequence of backward steps. Reversible computing has been studied in the context of different programming languages and formalisms, where it has been used for testing and verification, among others. In this paper, we consider a subset of Erlang, a functional and concurrent programming language based on the actor model. We present a formal semantics for reversible computation in this language and prove its main properties, including its causal consistency. We also build on top of it a rollback operator that can be used to undo the actions of a process up to a given checkpoint. (C) 2018 Elsevier Inc. All rights reserved., This work has been partially supported by MINECO/AEI/FEDER (EU) under grants TIN2013-44742-C4-1-R and TIN2016-76843-C4-1-R, by the Generalitat Valenciana under grant PROMETEO-II/2015/013 (SmartLogic), by the COST Action IC1405 on Reversible Computation-extending horizons of computing, and by JSPS KAKENHI Grant Number JP17H01722. Adrian Palacios was partially supported by the EU (FEDER) and the Spanish Ayudas para contratos predoctorales para la formacian de doctores and Ayudas a la movilidad predoctoral para la realtzacion de estancias breves en centros de I+D, MINECO (SEIDI), under FPI grants BES-2014-069749 and EEBB-I-16-11469. Ivan Lanese was partially supported by INdAM as a member of GNCS (Gruppo Nazionale per il Calcolo Scientifico). Part of this research was done while the third and fourth authors were visiting Nagoya and Bologna Universities; they gratefully acknowledge their hospitality. Finally, we thank Salvador Tamarit and the anonymous reviewers for their helpful suggestions and comments.

International audience; Over the years, organizations acquired disparate software systems, each answering one specific need. Currently, the desirable outcomes of integrating these systems (higher degrees of automation and better system consistency) are often outbalanced by the complexity of mitigating their discrepancies. These problems are magnified in the decentralized setting (e.g., cross-organizational cases) where the integration is usually dealt with ad-hoc "glue" connectors, each integrating two or more systems. Since the overall logic of the integration is spread among many glue connectors, these solutions are difficult to program correctly (making them prone to misbehaviors and system blocks), maintain, and evolve. In response to these problems, we propose ChIP, an integration process advocating choreographic programs as intermediate artifacts to refine high-level global specifications (e.g., UML Sequence Diagrams), defined by the domain experts of each partner, into concrete, distributed implementations. In ChIP, once the stakeholders agree upon a choreographic integration design, they can automatically generate the respective local connectors, which are guaranteed to faithfully implement the described distributed logic. In the paper, we illustrate ChIP with a pilot from the EU EIT Digital project SMAll, aimed at integrating pre-existing systems from government, university, and transport industry.

International audience; The Internet of Things (IoT) promotes the communication among heterogeneous entities, from small sensors to Cloud systems. However, this is realized using a wide range of communication media and data protocols, usually incompatible with each other. Thus, IoT systems tend to grow as homogeneous isolated platforms, which hardly interact. To achieve a higher degree of interoperability among disparate IoT platforms, we propose a language-based approach for communication technology integration. We build on the Jolie programming language, which allows programmers to easily make the same logic work over disparate communication stacks in a declarative , dynamic way. Jolie currently supports the main technologies from Service-Oriented Computing, such as TCP/IP, Bluetooth, and RMI at transport level, and HTTP and SOAP at application level. As technical result, we integrate in Jolie the two most adopted protocols for IoT communication, i.e., CoAP and MQTT. In this paper, we report our experience and we present high-level concepts valuable both for the general implementation of interoperable systems and for the development of other language-based solutions.

International audience; Programming languages based on the actor model, such as Erlang, avoid some concurrency bugs by design. However, other concurrency bugs, such as message order violations and livelocks, can still show up in programs. These hard-to-find bugs can be more easily detected by using causal-consistent reversible debugging, a debugging technique that allows one to traverse a computation both forward and backward. Most notably, causal consistency implies that, when going backward, an action can only be undone provided that its consequences, if any, have been undone beforehand. To the best of our knowledge, we present the first causal-consistent reversible debugger for Erlang, which may help programmers to detect and fix various kinds of bugs, including message order violations and livelocks.

none 4 no Available online 20 September 2016 Rollback is a fundamental technique for ensuring reliability of systems, allowing one, in case of troubles, to recover a past system state. However, the definition of rollback in a concurrent/distributed scenario is quite tricky. We propose an approach based on the notion of causal-consistent reversibility: any given past action can be undone, provided that all the actions caused by it are undone as well. Given that, we define a rollback as the minimal causal-consistent sequence of backward steps able to undo a given action. We define the semantics of such a rollback operator, and show that it satisfies the above specification. The approach that we present is quite general, but we instantiate it in the case of μKlaim, a formal coordination language based on distributed tuple spaces. We remark that this is the first definition of causal-consistent rollback in a shared-memory setting. We illustrate the use of rollback in μKlaim on a simple, but realistic, application scenario. open Giachino, Elena; Lanese, Ivan; Mezzina, Claudio Antares; Tiezzi, Francesco Giachino, Elena; Lanese, Ivan; Mezzina, Claudio Antares; Tiezzi, Francesco

International audience; Systems need to be updated to last for a long time in a dynamic environment, and to cope with changing requirements. It is important for updates to preserve the desirable properties of the system under update, while possibly enforcing new ones. Here we consider a simple yet general update mechanism, which replaces a component of the system with a new one. The context, i.e., the rest of the system, remains unchanged. We define contexts and components as Constraint Automata interacting via either asynchronous or synchronous communication, and we express properties using Constraint Automata too. Then we build most general updates which preserve specific properties, considering both a single property and all the properties satisfied by the original system, in a given context or in all possible contexts.

Causal-consistent reversibility is the reference notion of reversibility for concurrency. We introduce a modular framework for defining causal-consistent reversible extensions of concurrent models and languages. We show how our framework can be used to define reversible extensions of formalisms as different as CCS and concurrent X-machines. The generality of the approach allows for the reuse of theories and techniques in different settings., In Proceedings ICE 2016, arXiv:1608.03131

This paper presents initial ideas for the design and implementation of a reversible object-oriented language based on extending Janus with object-oriented concepts such as classes that encapsulate behavior and state, inheritance, virtual dispatching, as well as constructors. We show that virtual dispatching is a reversible decision mechanism easily translatable to a standard reversible programming model such as Janus, and we argue that reversible management of state can be accomplished using reversible constructors. The language is implemented in terms of translation to standard Janus programs.

Choreographic Programming is a development methodology for concurrent software that guarantees correctness by construction. The key to this paradigm is to disallow mismatched I/O operations in programs, called choreographies, and then mechanically synthesise distributed implementations in terms of standard process models via a mechanism known as EndPoint Projection (EPP). Despite the promise of choreographic programming, there is still a lack of practical evaluations that illustrate the applicability of choreographies to concrete computational problems with standard concurrent solutions. In this work, we explore the potential of choreographies by using Procedural Choreographies (PC), a model that we recently proposed, to write distributed algorithms for sorting (Quicksort), solving linear equations (Gaussian elimination), and computing Fast Fourier Transform. We discuss the lessons learned from this experiment, giving possible directions for the usage and future improvements of choreography languages.

International audience; The notion of reversible computation is attracting increasing interest because of its applications in diverse fields, in particular the study of programming abstractions for reliable systems. In this paper, we continue the study undertaken by Danos and Krivine on reversible CCS by defining a reversible higher-order π-calculus, called rhoπ. We prove that reversibility in our calculus is causally consistent and that the causal information used to support reversibility in rhoπ is consistent with the one used in the causal semantics of the π-calculus developed by Boreale and Sangiorgi. Finally, we show that one can faithfully encode rhoπ into a variant of higher-order π, substantially improving on the result we obtained in the conference version of this paper.

Choreographic programming is a programming-language design approach that drives error-safe protocol development in distributed systems. Motivated by challenging scenarios in Cyber-Physical Systems (CPS), we study how choreographic programming can cater for dynamic infrastructures where the availability of components may change at runtime. We introduce the Global Quality Calculus (GCq), a process calculus featuring novel operators for multiparty, partial and collective communications; we provide a type discipline that controls how partial communications refer only to available components; and we show that well-typed choreographies enjoy progress.

International audience; Behavioural type systems, usually associated to concurrent or distributed computations, encompass concepts such as interfaces, communication protocols, and contracts, in addition to the traditional input/output operations. The behavioural type of a software component specifies its expected patterns of interaction using expressive type languages, so that types can be used to determine automatically whether the component interacts correctly with other components. Two related important notions of behavioural types are those of session types and behavioural contracts. This paper surveys the main accomplishments of the last twenty years within these two approaches.

International audience; Jolie is an orchestration language conceived during Sensoria, an FP7 European project led by Martin Wirsing in the time frame 2005– 2010. Jolie was designed having in mind both the novel –at project time– concepts related to Service-Oriented Computing and the traditional approach to the modelling of concurrency typical of process calculi. The foundational work done around Jolie during Sensoria has subsequently produced many concrete results. In this paper we focus on two distinct advancements, one aiming at the development of dynamically adaptable orchestrated systems and one focusing on global choreographic specifications. These works, more recently, contributed to the realisation of a framework for programming dynamically evolvable distributed Service-Oriented applications that are correct-by-construction.

This paper presents a compositional approach for schedula-bility analysis of hierarchical systems, which enables to prove more sys-tems schedulable by having richer and more detailed scheduling models.We use a lightweight method (statistical model checking) for design ex-ploration, easily assuring high confidence in the correctness of the model.A satisfactory design can be proved schedulable using the computationcostly method (symbolic model checking). In order to analyze a hierar-chical scheduling system compositionally, we introduce the notion of astochastic supplier modeling the supply of resources in each component.We specifically investigate two different techniques to widen the set ofprovably schedulable systems: 1) a new supplier model; 2) restricting thepotential task offsets. We also provide a way to estimate the minimumresource supply (budget) that a component is required to provide This paper presents a compositional approach for schedulability analysis of hierarchical systems, which enables to prove more systems schedulable by having richer and more detailed scheduling models. We use a lightweight method (statistical model checking) for design exploration, easily assuring high confidence in the correctness of the model. A satisfactory design can be proved schedulable using the computation costly method (symbolic model checking). In order to analyze a hierarchical scheduling system compositionally, we introduce the notion of a stochastic supplier modeling the supply of resources in each component. We specifically investigate two different techniques to widen the set of provably schedulable systems: 1) a new supplier model; 2) restricting the potential task offsets. We also provide a way to estimate the minimum resource supply (budget) that a component is required to provide.

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 Priority). Given a BIP system consisting of several atomic components, we compute the product of two selected atomic components. The product operation often exposes opportunities for constant propagation in the product component that were hidden originally. Moreover, the product operation introduces states that are branching bisimilar. Our method detects and merges those states resulting in a behavior that may overapproximate the original one. The presented method is fully implemented. Our results show a drastic improvement in verifying BIP systems.

We illustrate our approach to develop and verify distributed, adaptive software systems. The cornerstone of our framework is the use of choreography languages, which allow us to obtain correctness by construction. Workflow Patterns are also used as abstract tools to design real systems, while techniques based on abstract interpretation and on dynamic verification are integrated in our framework to reduce the complexity of verification. We develop a methodology for verifying distributed, adaptive software systems.The cornerstone of our framework is the use of choreography languages.We integrate also different techniques based on abstract interpretation and on dynamic verification.

Programming distributed applications free from communication deadlocks and races is complex. Preserving these properties when applications are updated at runtime is even harder. We present DIOC, a language for programming distributed applications that are free from deadlocks and races by construction. A DIOC program describes a whole distributed application as a unique entity (choreography). DIOC allows the programmer to specify which parts of the application can be updated. At runtime, these parts may be replaced by new DIOC fragments from outside the application. DIOC programs are compiled, generating code for each site, in a lower-level language called DPOC. We formalise both DIOC and DPOC semantics as labelled transition systems and prove the correctness of the compilation as a trace equivalence result. As corollaries, DPOC applications are free from communication deadlocks and races, even in presence of runtime updates., Comment: Technical Report

International audience; Causal-consistent reversibility is a natural way of undoing concurrent computations. We study causal-consistent reversibility in the context of µKLAIM, a formal coordination language based on distributed tuple spaces. We consider both uncontrolled reversibility, suitable to study the basic properties of the reversibility mechanism, and controlled reversibility based on a rollback operator, more suitable for programming applications. The causality structure of the language, and thus the definition of its reversible semantics, differs from all the reversible languages in the literature because of its generative communication paradigm. In particular, the reversible behavior of µKLAIM read primitive, reading a tuple without consuming it, cannot be matched using channel-based communication. We illustrate the reversible extensions of µKLAIM on a simple, but realistic, application scenario.

International audience; This paper critically discusses the different choices that have to be made when defining a fault model for an object-oriented programming language. We consider in particular the ABS language, and analyze the interplay between the fault model and the main features of ABS, namely the cooperative concurrency model, based on asynchronous method invocations whose return results via futures, and its emphasis on static analysis based on invariants.

We present AIOCJ, a framework for programming distributed adaptive applications. Applications are programmed using AIOC, a choreographic language suited for expressing patterns of interaction from a global point of view. AIOC allows the programmer to specify which parts of the application can be adapted. Adaptation takes place at runtime by means of rules, which can change during the execution to tackle possibly unforeseen adaptation needs. AIOCJ relies on a solid theory that ensures applications to be deadlock-free by construction also after adaptation. We describe the architecture of AIOCJ, the design of the AIOC language, and an empirical validation of the framework., Comment: Technical Report

Part 2: Track B: Logic, Semantics, Specification and Verification; International audience; We present a (co)algebraic treatment of iteration-free dynamic modal logics such as Propositional Dynamic Logic (PDL) and Game Logic (GL), both without star. The main observation is that the program/game constructs of PDL/GL arise from monad structure, and the axioms of these logics correspond to certain compatibilty requirements between the modalities and this monad structure. Our main contribution is a general soundness and strong completeness result for PDL-like logics for T-coalgebras where T is a monad and the ”program” constructs are given by sequential composition, test, and pointwise extensions of operations of T.

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.