Search

We study a weakening of the notion of logical relations, called prelogical relations, that has many of the features that make logical relations so useful as well as further algebraic properties including composability. The basic idea is simply to require the reverse implication in the definition of logical relations to hold only for pairs of functions that are expressible by the same lambda term. Prelogical relations are the minimal weakening of logical relations that gives composability for extensional structures and simultaneously the most liberal definition that gives the Basic Lemma. Prelogical predicates (i.e., unary prelogical relations) coincide with sets that are invariant under Kripke logical relations with varying arity as introduced by Jung and Tiuryn, and prelogical relations are the closure under projection and intersection of logical relations. These conceptually independent characterizations of prelogical relations suggest that the concept is rather intrinsic and robust. The use of prelogical relations gives an improved version of Mitchell's representation independence theorem which characterizes observational equivalence for all signatures rather than just for first-order signatures. Prelogical relations can be used in place of logical relations to give an account of data refinement where the fact that prelogical relations compose explains why stepwise refinement is sound.

Implementations of abstract data types are defined via an enrichment of the target type. We suggest to use an extended typed λ-calculus for such an enrichment in order to meet the conceptual requirement that an implementation has to bring us closer to a (functional) program. Composability of implementations is investigated, the main theorem being that composition of correct implementations is correct if terminating programs are implemented by terminating programs. Moreover we provide syntactical criteria to guarantee correctness of composition.

implementations should compose because, in practice, concrete implementations do compose. Therefore, an implementation, to be considered correct, should be composab!e. Then, what we have obtained are (semantical) characterizations of properties that should be achieved by implementations. Although this characterization applies only to EKMP's approach, similar results could be obtained for other approaches (in ORE82, results are presented for IR-implementations, viz. EHR82, EK82) . However, for those approaches not considering the enrichment step, the characterization would be difficult because of its hiding of the problem (see the remark after counter-example 2.3). EKMP do also present some results about composition of implementations. However, instead of studying composability as a property that should be achieved by implementations, they have been dealing, mainly, with the problem of studying under which circumstances may we compose two implementations in order to obtain a new correct implementation. In this sense, they have obtained some sufficient conditions to guarantee the correctness of composition. It is my feel~ng that this is not the correct approach. We may see the reason by looking at the problem of iterated composition: suppose we have to compose implementations If,... ..,In, using their approach we would have to check composition of Ii with I(2,...,n) . But, first of all, this is something against the spirit of design by stepwise refinement: at once, we would have to check

We study the issue of sound multi-agent design trying to keep a system engineering perspective; that is, both when analyzing a problem and when synthesizing a solution the focus is kept on the whole, large-scale structure of the software artifact that is to be realized. The formal tool we evaluate to provide effective assistance to the sound design of multi-agent systems (MASs) applies (labeled) transition systems to the description of software interactive behavior [3], as elaborated and promoted in the field of concurrency theory. When specifying a transition system semantics for an agent, a number of rules are given that describe in a quite declarative way the dynamics of its inner machinery, also providing insights on its internal architecture – expressed at a given level of abstraction. We believe that this formalism is fit for design because of its calculus-like nature, which combines the description of a system with the prescription of its possible evolutions; this property buys designers some generativity, while remaining in a well grounded mathematical landscape. Moreover, transition systems allow us to address both composability and extensibility. An agent model is divided into several LTS specifications that we call tiers, capturing different aspects of an agent design. A partial specification of an agent can be further detailed by adding new tiers, with a technique known as grey-boxing [4, 5]. As a use case for our approach we consider ParADE [2], a development environment exploiting the formal semantics of a FIPA-like Agent Communication Language (ACL) to gain agents semantic interoperability, and providing interaction laws as a design mechanism to specify the agent social role.

We present Abstract (ABortable STate mAChine replicaTion), a new abstraction for designing and reconfiguring generalized replicated state machines that are, unlike traditional state machines, allowed to abort executing a client’s request if “something goes wrong.” Abstract can be used to considerably simplify the incremental development of efficient Byzantine fault-tolerant state machine replication ( BFT ) protocols that are notorious for being difficult to develop. In short, we treat a BFT protocol as a composition of Abstract instances. Each instance is developed and analyzed independently and optimized for specific system conditions. We illustrate the power of Abstract through several interesting examples. We first show how Abstract can yield benefits of a state-of-the-art BFT protocol in a less painful and error-prone manner. Namely, we develop AZyzzyva , a new protocol that mimics the celebrated best-case behavior of Zyzzyva using less than 35% of the Zyzzyva code. To cover worst-case situations, our abstraction enables one to use in AZyzzyva any existing BFT protocol. We then present Aliph , a new BFT protocol that outperforms previous BFT protocols in terms of both latency (by up to 360%) and throughput (by up to 30%). Finally, we present R-Aliph , an implementation of Aliph that is robust , that is, whose performance degrades gracefully in the presence of Byzantine replicas and Byzantine clients.

Architectures are common means for organising coordination between components in order to build complex systems and to make them manageable. They allow thinking on a higher plane and avoiding low-level mistakes. Architectures provide means for ensuring correctness-by-construction by enforcing global properties characterising the coordination between components. In this work, we consider the following questions of architecture modelling: 1) how to model architectures; 2) how to compose them if several properties enforced by different architectures are required; 3) how to specify architectures styles that generalise the notion of architectures and represent families of architectures satisfying the same property. An architecture can be considered as an operator that, applied to a set of components, builds a composite component meeting a characteristic property. The underlying concepts of components and their interaction originate from the BIP framework. This thesis is structured in two parts. In the first part, we study the expressiveness of glue operators in the BIP framework. We provide results for classical BIP glue and for several modifications obtained by relaxing the constraints imposed on priority models. We also study an alternative semantics of BIP glue based on the offer predicate. It meets fundamental properties required from component-based frameworks, namely compositionality, incrementality, flattening and modularity. We provide the comparison with the classical BIP semantics and the algorithm for the synthesis of connectors from the interaction logic used to describe coordination constraints. In the second part, we define architectures and propose an architecture composition operator. We study their properties and prove that the composition operator preserves safety properties of its operands. The alternative glue semantics presented in the first part of the thesis allows to extend architectures with priorities. For the specification of architecture styles, we propose configuration logics. We provide a sound and complete axiomatisation of the propositional configuration logic as well as decision procedures for checking that an architecture satisfies a given logical specification. To allow genericity of specifications, we study higher-order extensions of the propositional configuration logic. We illustrate with examples the specification of various architecture styles. We provide an experimental evaluation using the Maude rewriting system to implement the decision procedure for configuration logics. Additionally, we study the relation between the architecture composition operator and the composition of configuration logic formulas.

Linearizability is a key design methodology for reasoning about implementations of concurrent abstract data types in both shared memory and message passing systems. It provides the illusion that operations execute sequentially and fault-free, despite the asynchrony and faults inherent to a concurrent system, especially a distributed one. A key property of linearizability is inter-object composability: a system composed of linearizable objects is itself linearizable. However, devising linearizable objects is very difficult, requiring complex algorithms to work correctly under general circumstances, and often resulting in bad average-case behavior. Concurrent algorithm designers therefore resort to speculation: optimizing algorithms to handle common scenarios more efficiently. The outcome are even more complex protocols, for which it is no longer tractable to prove their correctness. To simplify the design of efficient yet robust linearizable protocols, we propose a new notion: speculative linearizability . This property is as general as linearizability, yet it allows intra-object composability: the correctness of independent protocol phases implies the correctness of their composition. In particular, it allows the designer to focus solely on the proof of an optimization and derive the correctness of the overall protocol from the correctness of the existing, non-optimized one. Our notion of protocol phases allows processes to independently switch from one phase to another, without requiring them to reach agreement to determine the change of a phase. To illustrate the applicability of our methodology, we show how examples of speculative algorithms for shared memory and asynchronous message passing naturally fit into our framework. We rigorously define speculative linearizability and prove our intra-object composition theorem in a trace-based as well as an automaton-based model. To obtain a further degree of confidence, we also formalize and mechanically check the theorem in the automaton-based model, using the I/O automata framework within the Isabelle interactive proof assistant. We expect our framework to enable, for the first time, scalable specifications and mechanical proofs of speculative implementations of linearizable objects.

The Levels of Conceptual Interoperability Model LCIM has been developed to provide both a metric of the degree of conceptual representation that exists between interoperating systems and also as a guide showing what is necessary to accommodate a targeted degree of conceptual representation between systems. The model was originally developed to support the interoperability of simulation systems, but has been shown to be useful for other domain areas. The model is stratified into seven general levels, and these are introduced and defined. Implied within the model is that the information and processes of one system should be described and that description is then made available to another system. This description of information and processes can take many forms, but is generally an ontological representation. The components of an ontological representation are defined in form and also as elements for the various layers of the LCIM.

The efficient solution of discretisations of coupled systems of partial differential equations (PDEs) is at the core of much of numerical simulation. Significant effort has been expended on scalable algorithms to precondition Krylov iterations for the linear systems that arise. With few exceptions, the reported numerical implementation of such solution strategies is specific to a particular model setup, and intimately ties the solver strategy to the discretisation and PDE, especially when the preconditioner requires auxiliary operators. In this paper, we present recent improvements in the Firedrake finite element library that allow for straightforward development of the building blocks of extensible, composable preconditioners that decouple the solver from the model formulation. Our implementation extends the algebraic composability of linear solvers offered by the PETSc library by augmenting operators, and hence preconditioners, with the ability to provide any necessary auxiliary operators. Rather than specifying up front the full solver configuration, tied to the model, solvers can be developed independently of model formulation and configured at runtime. We illustrate with examples from incompressible fluids and temperature-driven convection.

Massive exploitation of next-generation sequencing technologies requires dealing with both: huge amounts of data and complex bioinformatics pipelines. Computing architectures have evolved to deal with these problems, enabling approaches that were unfeasible years ago: accelerators and Non-Volatile Memories (NVM) are becoming widely used to enhance the most demanding workloads. However, bioinformatics workloads are usually part of bigger pipelines with different and dynamic needs in terms of resources. The introduction of Software Defined Infrastructures (SDI) for data centers provides roots to dramatically increase the efficiency in the management of infrastructures. SDI enables new ways to structure hardware resources through disaggregation, and provides new hardware composability and sharing mechanisms to deploy workloads in more flexible ways. In this paper we study a state-of-the-art genomics application, SMUFIN, aiming to address the challenges of future HPC facilities., Partially funded by European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (grant agreement No 639595) - HiEST Project Published Euro-Par 2018: Euro-Par 2018: Parallel Processing Workshops pp 613-625

We study a methodology for constructing scheduled systems by restricting successively the behavior of the processes to be scheduled. Restriction is used to guarantee the satisfaction of two types of constraints: schedulability constraints characterizing timing properties of the processes, and constraints characterizing particular scheduling algorithms including process priorities, non-idling, and preemption. The methodology is based on a controller synthesis paradigm. The main results deal with the characterization of scheduling policies as safety constraints and the simplification of the synthesis process by applying a composability principle.

This paper presents new optimization approaches aiming at reducing the impact of memory accesses on the performance of dataflow programs. The approach is based on introducing a high level management of composite data types in dynamic dataflow programming language for the memory processing of data tokens. It does not require essential changes to the model of computation (MOC) or to the dataflow program itself. The objective of the approach is to remove the unnecessary constraints of memory isolations without introducing limitations to the scalability and composability properties of the dataflow paradigm. Thus the identified optimizations allow to keep the same design and programming philosophy of dataflow, whereas aiming at improving the performance of the specific configuration implementation. The different optimizations can be integrated into the current RVC-CAL design flows and synthesis tools and can be applied to different sub-networks partitions of the dataflow program. The paper introduces the context, the definition of the optimization problem and describes how it can be applied to dataflow designs. Some examples of the optimizations are provided.

Product lines promise to improve software quality and development productivity. A central issue to meet this is systematically dealing with variations within products in a certain domain. Although various techniques are available, their use is constrained by the specific application domain. This paper presents an extractive method for handling variation in the mobile device application domain. Being based on Aspect-Oriented Programming and general program transformation, it oers enhanced configurability and composability. We illustrate the approach with a game product line built with J2ME.

Adaptability and composability have become two of the most important research areas in concurrent object-oriented systems in recent years. Nevertheless, at the present time, COOLs do not provide enough support for the development of true adaptable and composable software because either i) the different aspects that appear in these systems, synchronization and behavior, are mixed in the same component or, ii) if they are properly separated in different components, once these components are woven the resulting executable piece of software is too rigid to be adapted or reconfigured at run-time. Our contention is that this last feature is very important in critical control systems where, due to unexpected environment changes, urgent and not preestablished decisions must be taken at run-time. From security and economic point of views, it is not admissible to stop the application, adapt it to the new environment and re-run it. In this context, under project PRI97C161 of Junta de Extremadura, we have developed the Disguises Model, a model mainly thought for a clear separation of synchronization and behavioral aspects. A new language for the specification of the composition rules between the synchronization and behavioral aspects is provided, allowing synchronization policies to be added, replaced or reconfigured at run-time, which is the main contribution of the proposed model.

International audience; Building a composite application based on Web services has become a real challenge regarding the large and diverse service space nowadays. Especially when considering the various functional and non-functional capabilities that Web services may afford and users may require. In this paper, we propose an approach for facilitating Web service selection according to user requirements. These requirements specify the needed functionality and expected QoS, as well as the composability between each pair of services. The originality of our approach is embodied in the use of Relational Concept Analysis (RCA), an extension of Formal Concept Analysis (FCA). Using RCA, we classify services by their calculated QoS levels and composability modes. We use a real case study of 901 services to show how to accomplish an efficient selection of services satisfying a specified set of functional and non-functional requirements.

The security of key exchange and secure channel protocols, such as TLS, has been studied intensively. However, only few works have considered what happens when the established keys are actuallyused -- to run some protocol securely over the established "channel". We call this a vertical protocol composition, and it is truly commonplace in today's communication with the diversity of VPNs and secure browser sessions. In fact, it is normal that we have several layers of secure channels: For instance, on top of a VPN-connection, a browser may establish another secure channel (possibly with a different end point). Even using the same protocol several times in such a stack of channels is not unusual: An application may very well establish another TLS channel over an established one. We call this self-composition. In fact, there is nothing that tells us that all these compositions are sound, i.e., that the combination cannot introduce attacks that the individual protocols in isolation do not have. In this work, we prove a composability result in the symbolic model that allows for arbitrary vertical composition (including self-composition). It holds for protocols from any suite of channel and application protocols that fulfills a number of sufficient preconditions. These preconditions are satisfied for many practically relevant protocols such as TLS.

We investigate two major limiting factors in the design and implementation of modern dynamics solvers that interfere with their full utilization in versatile, manipulation-driven robotic software architectures. The first limitation originates from the design of those solvers which aims at computational efficiency while neglecting composability. Instead, we advocate to design the solvers in such a way that they exploit linearity in the equations of motion to fully decompose the state of a kinematic chain. This enables a versatile recomposition and more flexible applications. Secondly, we have observed that most implementations follow the programming principle of information hiding. Consequently, the internal state that is used to compute motion control commands is withheld from other parts of the software architecture. We tackle this problem by following a dataflow programming paradigm and separating the software’s dataflow from the control flow. Thereafter, we demonstrate those two simple, yet effective strategies to overcome the limitations along various case studies.

In this paper, we optimize the performances and compare several recent masking schemes in bitslice on 32-bit arm devices, with a focus on multiplication. Our main conclusion is that efficiency (or randomness) gains always come at a cost, either in terms of composability or in terms of resistance against horizontal attacks. Our evaluations should therefore allow a designer to select a masking scheme based on implementation constraints and security requirements. They also highlight the increasing feasibility of (very) high-order masking that are offered by increasingly powerful embedded devices, with new opportunities of high-security devices in various contexts.

One of the objectives of the CTRON interface specifications is to promote software-reutilization for real-time applications by standardizing operating system interfaces. Although this approach does improve reusability by improving portability, means for gaining better composability has to be taken into consideration to achieve more advanced reutilization. Object oriented programming (OOP) which supports encapsulation, polymorphism and inheritance is an appropriate programming paradigm for improving composability of software-modules. The authors describe how they apply OOP to systems based on the CTRON specifications and describe the C++ class libraries they have been designing. They describe how they evaluate the performance, reusability and portability of programs that use the base class libraries. >

Though the advanced manufacturing capabilities offered by additive manufacturing (AM) have been known for several decades, industry adoption of AM technologies has been relatively slow. Recent advances in modeling and simulation of AM processes and materials are providing new insights to help overcome some of the barriers that have hindered adoption. However, these models and simulations are often application specific, and few are developed in an easily reusable manner. Variations are compounded because many models are developed as independent or proprietary efforts, and input and output definitions have not been standardized. To further realize the potential benefits of modeling and simulation advancements, including predictive modeling and closed-loop control, more coordinated efforts must be undertaken. In this paper, we advocate a more harmonized approach to model development, through classification and metamodeling that will support model composability, reusability, and integration. We review several types of AM models and use direct metal powder bed fusion characteristics to provide illustrative examples of the proposed classification and metamodel approach. We describe how a coordinated approach can be used to extend modeling capabilities by promoting model composability. As part of future work, a framework is envisioned to realize a more coherent strategy for model development and deployment.Copyright © 2014 by ASME

In this paper we present a High Level Architecture (HLA) component model, particularly suitable for distributed multiscale simulations. We also present a preliminary implementation of HLA components and the CompoHLA environment that supports setting up and managing multiscale simulations built in the described model. We propose to integrate solutions from High Level Architecture (such as advanced time and data management) with possibilities given by component technologies (such as reusability and composability) and the Grid (such as joining geographically distributed communities of scientists). This approach will allow users working on multiscale applications to more easily exchange and join the simulations already created. The particular focus of this paper is on the design of a HLA component. We show how to insert simulation logic into a component and make it possible to steer from outside its connections with other components. Its functionality is shown through example of multiscale simulation of dense stellar system.

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 coordination between components. An architecture can be considered as an operator A that, applied to a set of components B , builds a composite component A ( B ) meeting a characteristic property Φ . Architecture composability is a basic and common problem faced by system designers. In this paper, we propose a formal and general framework for architecture composability based on an associative, commutative and idempotent architecture composition operator ⊕ . The main result is that if two architectures A 1 and A 2 enforce respectively safety properties Φ 1 and Φ 2 , the architecture A 1 ⊕ A 2 enforces the property Φ 1 ∧ Φ 2 , that is both properties are preserved by architecture composition. We also establish preservation of liveness properties by architecture composition. The presented results are illustrated by a running example and a case study.

Quantum computing has seen tremendous progress in the past years. However, due to limitations in scalability of quantum technologies, it seems that we are far from constructing universal quantum computers for everyday users. A more feasible solution is the delegation of computation to powerful quantum servers on the network. This solution was proposed in previous studies of Blind Quantum Computation, with guarantees for both the secrecy of the input and of the computation being performed. In this work, we further develop this idea of computing over encrypted data, to propose a multiparty delegated quantum computing protocol in the measurement-based quantum computing framework., Comment: 22 pages