Search

Logical Execution Time (LET) is a timed programming abstraction, which features predictable and composable timing. It has recently gained considerable attention in the automotive industry, where it was successfully applied to master the distribution of software applications on multi-core electronic control units. However, the LET abstraction in its conventional form is only valid within the scope of a single component. With the recent introduction of System-level Logical Execution Time (SL LET), the concept could be transferred to a system-wide scope. This article improves over a first paper on SL LET, by providing matured definitions and an extensive discussion of the concept. It also features a comprehensive evaluation exploring the impacts of SL LET with regard to design, verification, performance, and implementability. The evaluation goes far beyond the contexts in which LET was originally applied. Indeed, SL LET allows us to address many open challenges in the design and verification of complex embedded hardware/software systems addressing predictability, synchronization, composability, and extensibility. Furthermore, we investigate performance trade-offs, and we quantify implementation costs by providing an analysis of the additionally required buffers.

International audience; The probing security model is widely used to formally prove the security of masking schemes. Whenever a masked implementation can be proven secure in this model with a reasonable \emph{leakage rate}, it is also provably secure in a realistic leakage model known as the \emph{noisy leakage model}. This paper introduces a new framework for the composition of probing-secure circuits. We introduce the security notion of \emph{input-output separation} (IOS) for a refresh gadget. From this notion, one can easily compose gadgets satisfying the classical probing security notion --which does not ensure composability on its own-- to obtain a \emph{region probing secure} circuit. Such a circuit is secure against an adversary placing up to $t$ probes in each gadget composing the circuit, which ensures a tight reduction to the more realistic noisy leakage model. After introducing the notion and proving our composition theorem, we compare our approach to the composition approaches obtained with the (Strong) Non-Interference (S/NI) notions as well as the Probe-Isolating Non-Interference (PINI) notion. We further show that any uniform SNI gadget achieves the IOS security notion, while the converse is not true. We further describe a refresh gadget achieving the IOS property for any linear sharing with a quasilinear complexity $\Theta(n \log n)$ and a $O(1/\log n)$ leakage rate (for an $n$-size sharing). This refresh gadget is a simplified version of the quasilinear SNI refresh gadget proposed by Battistello, Coron, Prouff, and Zeitoun (ePrint~2016). As an application of our composition framework, we revisit the quasilinear-complexity masking scheme of Goudarzi, Joux and Rivain (Asiacrypt~2018). We improve this scheme by generalizing it to any base field (whereas the original proposal only applies to field with $n$th powers of unity) and by taking advantage of our composition approach. We further patch a flaw in the original security proof and extend it from the random probing model to the stronger region probing model. Finally, we present some application of this extended quasilinear masking scheme to AES and MiMC and compare the obtained performances.

International audience; Component-based software engineering is a paradigm that fosters software flexibility and emphasizes composability and reuse of software components. These are runtime units that provide services and, in turn, may require other services to operate. Assembling components consists in binding compo-nents' required services to provided ones to deliver composite services with added value. Building a composite service is a challenging task as it requires identifying components and services that are compatible, binding them to implement the service, and describe it for discovery. For that, the vocabulary used to describe component-based services (i.e., services offered by components or assemblies) must support the description of required services, and descriptions must be combinable in order to automatically generate composite service descriptions. However, existing solutions are limited to the description and composition of provided (and not required) services. In this paper, we consider ontologies to describe component-based services implemented by component assemblies. After comparing existing service ontologies, we present an extension of OWLS called Comp-O. Through a proof-of-concept, we demonstrate how the added semantics can be handled to automatically build composite service descriptions.

Power and electromagnetic based side-channel attacks are serious threats against the security of cryptographic embedded devices. In order to mitigate these attacks, implementations use countermeasures, among which masking is currently the most investigated and deployed choice. Unfortunately, commonly studied forms of masking rely on underlying assumptions that are difficult to satisfy in practice. This is due to physical defaults, such as glitches or transitions, which can recombine the masked data in a way that concretely reduces an implementation’s security.

International audience; Power and electromagnetic based side-channel attacks are serious threats against the security of cryptographic embedded devices. In order to mitigate these attacks, implementations use countermeasures, among which masking is currently the most investigated and deployed choice. Unfortunately, commonly studied forms of masking rely on underlying assumptions that are difficult to satisfy in practice. This is due to physical defaults, such as glitches or transitions, which can recombine the masked data in a way that concretely reduces an implementation's security. We develop and implement an automated approach for verifying security of masked implementations in presence of physical defaults (glitches or transitions). Our approach helps to recover the main strengths of masking: rigorous foundations, composability guarantees, automated verification under more realistic assumptions. Our work follows the approach of (Barthe et al, EUROCRYPT 2015) and thus contributes to demonstrate the benefits of language-based approaches (specifically probabilistic information flow) for masking.

Part 2: Short and “Journal First” Papers; International audience; Computational fields have been proposed as an effective abstraction to fill the gap between the macro-level of distributed systems (specifying a system’s collective behaviour) and the micro-level (individual devices’ actions of computation and interaction to implement that collective specification), thereby providing a basis to better facilitate the engineering of collective APIs and complex systems at higher levels of abstraction. This approach is particularly suited to complex large-scale distributed systems, like the Internet-of-Things and Cyber-Physical Systems, where new mechanisms are needed to address composability and reusability of collective adaptive behaviour. This work introduces a full formal foundation for field computations, in terms of a core calculus equipped with typing, denotational, and operational semantics. Critically, we apply techniques for formal programming languages to collective adaptive systems: we provide formal establishment of a link between the micro- and macro-levels of collective adaptive systems, via a result of computational adequacy and abstraction for the (aggregate) denotational semantics with respect to the (per-device) operational semantics.

The logical execution time (LET) programming model has been applied in the automotive industry to master multicore programming of large task systems with complex dependencies. Recent developments in electric powertrains and autonomous vehicle functions raise parallel programming from the multicore level to the vehicle level where the requirements for LET application do not hold any more. This paper introduces System Level LET (SL LET), an extension of LET with relaxed synchronization requirements. While related extensions have been proposed for specific scheduling and communication models before, SL LET can be used with a variety of scheduling algorithms and communication semantics. Furthermore, it can be applied to systems with combinations of LET and other programming models. Yet, SL LET allows end-to-end timing guarantees and preserves essential LET properties required for automotive systems. For illustration, we apply the model to an electric vehicle use case.

International audience; As the computation power of modern high performance architectures increases, their heterogeneity and complexity also become more important. One of the big challenges of exascale is to reach programming models that give access to high performance computing (HPC) to many scientists and not only to a few HPC specialists. One relevant solution to ease parallel programming for scientists is domain specific language (DSL). However, one problem to avoid with DSLs is to mutualize existing codes and libraries instead of implementing each solution from scratch. For example, this phenomenon occurs for stencil-based numerical simulations, for which a large number of languages has been proposed without code reuse between them. The Multi-Stencil Framework (MSF) presented in this paper combines a new DSL to component-based programming models to enhance code reuse and separation of concerns in the specific case of stencils. MSF can easily choose one parallelization technique or another, one optimization or another, as well as one back-end implementation or another. It is shown that MSF can reach same performances than a non component-based MPI implementation over 16,384 cores. Finally, the performance model of the framework for hybrid parallelization is validated by evaluations.

A major goal of synthetic biology is to reprogram living organisms to solve pressing challenges in manufacturing, environmental remediation, or healthcare. While many types of genetic logic gates have been engineered, their scalability remains limited. Previous work demonstrated that Distributed Multicellular Computation (DMC) enables the implementation of complex logic within cellular consortia. However, current DMC systems require spatial separation of cellular subpopulation to be scalable to N-inputs, and need cell-cell communication channels to operate. Here we present scalable composition frameworks for the systematic design of multicellular consortia performing recombinase-based Boolean or history-dependent logic, and integrating an arbitrary number of inputs. The theoretical designs for both Boolean and history-dependent logic are based on reduced sets of computational modules implemented into specific cellular subpopulations which can then be combined in various manners to implement all logic functions. Our systems mark a departure from previous DMC architectures as they do not require either cell-cell communication nor spatial separation, greatly facilitating their implementation and making them fully autonomous. Due to their scalability and composability, we anticipate that the design strategies presented here will help researchers and engineers to reprogram cellular behavior for various applications in a streamlined manner. We provide an online tool for automated design of DNA architectures allowing the implementation of multicellular N-inputs logic functions at: http://synbio.cbs.cnrs.fr/calin.

International audience; Modularity and composability are essential properties to facilitate and scale the design of cyber-physical systems from the specification of hybrid, discrete and continuous, components. Modularity is essential to break down a system model into comprehensible and manageable component specifications. Composability is essential to design a system from component models while preserving their verified properties, expressed as assume-guarantee contracts. In this paper, we address the specification of hybrid system using Platzer's differential dynamic logic (dL). Our contribution is threefold: (1) We define a new composition operator in dL and prove that it is associative and commutative (AC). Prior notions of composition in dL were not associative. (2) We provide a theorem which characterizes necessary conditions to automate the proof that composed components satisfy the composition of their individual contracts, enabling modular and compositional verification. (3) We case-study our AC composition operator by considering the modular and detailed specification of a cruise controller in KeYmaera X, the latest implementation of dL, to demonstrate the proof automation capability of our contribution and exemplify a compositional design methodology.

International audience; In this paper a passive integrator dedicated to input/output Hamiltonian systems approximation is presented. In a first step, a discrete Hamiltonian framework endowed with a Lie derivative-like formula is introduced. It is shown that the discrete dynamics encodes energy conservation and passivity. Addition- ally, the characterization of the discrete dynamics in terms of Dirac structure is shown to be invariant by interconnection. The class is thus composable: networked systems belong to the class. In a second step, the discrete dynamics is considered as a one-step integration method. The method is shown to be convergent and provides a discrete-time approximation of an input/output Hamiltonian system. Accordingly, the discrete dynamics inherits intrinsic energetic characteristics (storage function and dissipation rate) from the original system. The method is thus tagged as passive integrator. As an illustration, the closed-loop behavior of interconnected subsystems and the stabilization of a rigid body spinning around its center of mass are presented.

To implement a linearizable shared memory in synchronous message-passing systems it is necessary to wait for a time linear to the uncertainty in the latency of the network for both read and write operations. Waiting only for one of them suffices for sequential consistency. This paper extends this result to crash-prone asynchronous systems, proposing a distributed algorithm building a sequentially consistent shared snapshot memory on top of an asynchronous message-passing system where less than half of the processes may crash. We prove that waiting is needed only when a process invokes a read/snapshot right after a write. We also show that sequential consistency is composable in some cases commonly encountered: 1) objects that would be linearizable if they were implemented on top of a linearizable memory become sequentially consistent when implemented on top of a sequential memory while remaining composable and 2) in round-based algorithms, where each object is only accessed within one round., in 30th International Symposium on Distributed Computing, Sep 2016, Paris, France

GDD_HCERES2020; It has been proved that to implement a linearizable shared memory in synchronous message-passing systems it is necessary to wait for a time proportional to the uncertainty in the latency of the network for both read and write operations, while waiting during read or during write operations is sufficient for sequential consistency. This paper extends this result to crash-prone asynchronous systems. We propose a distributed algorithm that builds a sequentially consistent shared memory abstraction with snapshot on top of an asynchronous message-passing system where less than half of the processes may crash. We prove that it is only necessary to wait when a read/snapshot is immediately preceded by a write on the same process. We also show that sequential consistency is composable in some cases commonly encountered: 1) objects that would be linearizable if they were implemented on top of a linearizable memory become sequentially consistent when implemented on top of a sequential memory while remaining composable and 2) in round-based algorithms, where each object is only accessed within one round.

This paper introduces Atomic Object Factory (AOF), a novel implementation of the distributed object paradigm. AOF allows client applications to transparently manipulate and share remotely-stored objects, while providing strong guarantees on dependability, consistency and persistence. It leverages the support of a listenable key-value store (LKVS), a novel NoSQL storage abstraction that we introduce in this paper. AOF offers integrated language support at the application-facing interface tier. Its middle tier implements the distributed object functionalities atop the LKVS, including coordinated replication. AOF does not rely on a mapping phase and deals with objects end-to-end. It allows the composition of these objects and provide efficient access to their methods. In particular, AOF guarantees disjoint access parallelism: operations on distinct distribued objects make use of distinct LKVS components and execute in parallel. We assess the benefits of our approach in practice by comparing the implementation of a personal cloud storage service using AOF, to an implementation of the same application with a state-of-the-art object-relational mapping over a sharded PostgreSQL database. Our results show that AOF offers a simpler programming framework both in terms of learning time and lines of code, while performing better on average and being more scalable.

International audience; The amount of data that human activities generate poses a challenge to current computer systems. Big data processing techniques are evolving to address this challenge, with analysis increasingly being performed using cloud-based systems. Emerging services, however, require additional enhancements in order to ensure their applicability to highly dynamic and heterogeneous environments and facilitate their use by Small & Medium-sized Enterprises (SMEs). Observing this landscape in emerging computing system development, this work presents Small & Medium-sized Enterprise Data Analytic in Real Time (SMART) for addressing some of the issues in providing compute service solutions for SMEs. SMART offers a framework for efficient development of Big Data analysis services suitable to small and medium-sized organizations, considering very heterogeneous data sources, from wireless sensor networks to data warehouses, focusing on service composability for a number of domains. This paper presents the basis of this proposal and preliminary results on exploring application deployment on hybrid infrastructure.

This paper proposes a system architecture and case study for a heterogeneous moving-object trajectory metamodel using generic sensors. In order to provide a unified metamodel and powerful framework for trajectory's services and queries, the proposed trajectory's data model has benefited from advantages of both conceptual and ontological space–time. However, it extends the basic data model of trajectory with new patterns as the space–time path to describe activities of the moving object and the composite region of interest. Additionally, the proposed system is distinguished by providing a framework for dealing with moving-object trajectory in an interoperable way, using heterogonous sensors that traditional data model incapable for this purpose. The proposed system architecture for the moving-object trajectory's data model is focused on service composability and data interoperability combining Open Geospatial Consortium (OGC) standards, Service-Oriented Architecture , and streaming technology, to allow applications built using the framework to be scalable and have better performance. The case study presented for tracking travelers at the airport means that passenger locations can be determined with a higher degree of accuracy and precision. Indeed, this system makes it easy to answer complex queries, such as seeing closely where passengers congregate, how much time they spend in stores and restaurants, and where there may be bottlenecks. It will also enable airport retailers to communicate with travelers directly.

International audience; The Web offers a great opportunity to share, deploy and use programs without installation difficulties. In this article we explore the idea of freely combining/composing real-time audio applications deployed on the Web using Faust audio DSP language.

To face the ever demanding requirements in term of accuracy and speed of scientific simulations, the High Performance community is constantly increasing the demands in term of parallelism, adding thus tremendous value to parallel libraries strongly optimized for highly complex architectures.Enabling HPC applications to perform efficiently when invoking multiple parallel libraries simultaneously is a great challenge. Even if a uniform runtime system is used underneath, scheduling tasks or threads coming from dfferent libraries over the same set of hardware resources introduces many issues, such as resource oversubscription, undesirable cache ushes or memory bus contention.In this thesis, we present an extension of StarPU, a runtime system specifically designed for heterogeneous architectures, that allows multiple parallel codes to run concurrently with minimal interference. Such parallel codes run within scheduling contexts that provide confined executionenvironments which can be used to partition computing resources. Scheduling contexts can be dynamically resized to optimize the allocation of computing resources among concurrently running libraries. We introduced a hypervisor that automatically expands or shrinks contexts using feedback from the runtime system (e.g. resource utilization). We demonstrated the relevance of this approach by extending an existing generic sparse direct solver (qr mumps) to use these mechanisms and introduced a new decomposition method based on proportional mapping that is used to build the scheduling contexts. In order to cope with the very irregular behavior of the application, the hypervisor manages dynamically the allocation of resources. By means of the scheduling contexts and the hypervisor we improved the locality and thus the overall performance of the solver.; Pour répondre aux besoins de précision et d'efficacité des simulations scientifiques, la communauté du Calcul Haute Performance augmente progressivement les demandes en terme de parallélisme, rajoutant ainsi un besoin croissant de réutiliser les bibliothèques parallèles optimisées pour les architectures complexes.L'utilisation simultanée de plusieurs bibliothèques de calcul parallèle au sein d'une application soulève bien souvent des problèmes d 'efficacité. En compétition pour l'obtention des ressources, les routines parallèles, pourtant optimisées, se gênent et l'on voit alors apparaître des phénomènes de surcharge, de contention ou de défaut de cache.Dans cette thèse, nous présentons une technique de cloisonnement de flux de calculs qui permet de limiter les effets de telles interférences. Le cloisonnement est réalisé à l'aide de contextes d'exécution qui partitionnement les unités de calculs voire en partagent certaines. La répartition des ressources entre les contextes peut être modifiée dynamiquement afin d'optimiser le rendement de la machine. A cette fin, nous proposons l'utilisation de certaines métriques par un superviseur pour redistribuer automatiquement les ressources aux contextes. Nous décrivons l'intégration des contextes d'ordonnancement au support d'exécution pour machines hétérogènes StarPU et présentons des résultats d'expériences démontrant la pertinence de notre approche. Dans ce but, nous avons implémenté une extension du solveur direct creux qr mumps dans la quelle nous avons fait appel à ces mécanismes d'allocation de ressources. A travers les contextes d'ordonnancement nous décrivons une nouvelle méthode de décomposition du problème basée sur un algorithme de \proportional mapping". Le superviseur permet de réadapter dynamiquement et automatiquement l'allocation des ressources au parallèlisme irrégulier de l'application. L'utilisation des contextes d'ordonnancement et du superviseur a amélioré la localité et la performance globale du solveur.

To face the ever demanding requirements in term of accuracy and speed of scientific simulations, the High Performance community is constantly increasing the demands in term of parallelism, adding thus tremendous value to parallel libraries strongly optimized for highly complex architectures.Enabling HPC applications to perform efficiently when invoking multiple parallel libraries simultaneously is a great challenge. Even if a uniform runtime system is used underneath, scheduling tasks or threads coming from dfferent libraries over the same set of hardware resources introduces many issues, such as resource oversubscription, undesirable cache ushes or memory bus contention.In this thesis, we present an extension of StarPU, a runtime system specifically designed for heterogeneous architectures, that allows multiple parallel codes to run concurrently with minimal interference. Such parallel codes run within scheduling contexts that provide confined executionenvironments which can be used to partition computing resources. Scheduling contexts can be dynamically resized to optimize the allocation of computing resources among concurrently running libraries. We introduced a hypervisor that automatically expands or shrinks contexts using feedback from the runtime system (e.g. resource utilization). We demonstrated the relevance of this approach by extending an existing generic sparse direct solver (qr mumps) to use these mechanisms and introduced a new decomposition method based on proportional mapping that is used to build the scheduling contexts. In order to cope with the very irregular behavior of the application, the hypervisor manages dynamically the allocation of resources. By means of the scheduling contexts and the hypervisor we improved the locality and thus the overall performance of the solver.; Pour répondre aux besoins de précision et d'efficacité des simulations scientifiques, la communauté du Calcul Haute Performance augmente progressivement les demandes en terme de parallélisme, rajoutant ainsi un besoin croissant de réutiliser les bibliothèques parallèles optimisées pour les architectures complexes.L'utilisation simultanée de plusieurs bibliothèques de calcul parallèle au sein d'une application soulève bien souvent des problèmes d 'efficacité. En compétition pour l'obtention des ressources, les routines parallèles, pourtant optimisées, se gênent et l'on voit alors apparaître des phénomènes de surcharge, de contention ou de défaut de cache.Dans cette thèse, nous présentons une technique de cloisonnement de flux de calculs qui permet de limiter les effets de telles interférences. Le cloisonnement est réalisé à l'aide de contextes d'exécution qui partitionnement les unités de calculs voire en partagent certaines. La répartition des ressources entre les contextes peut être modifiée dynamiquement afin d'optimiser le rendement de la machine. A cette fin, nous proposons l'utilisation de certaines métriques par un superviseur pour redistribuer automatiquement les ressources aux contextes. Nous décrivons l'intégration des contextes d'ordonnancement au support d'exécution pour machines hétérogènes StarPU et présentons des résultats d'expériences démontrant la pertinence de notre approche. Dans ce but, nous avons implémenté une extension du solveur direct creux qr mumps dans la quelle nous avons fait appel à ces mécanismes d'allocation de ressources. A travers les contextes d'ordonnancement nous décrivons une nouvelle méthode de décomposition du problème basée sur un algorithme de \proportional mapping". Le superviseur permet de réadapter dynamiquement et automatiquement l'allocation des ressources au parallèlisme irrégulier de l'application. L'utilisation des contextes d'ordonnancement et du superviseur a amélioré la localité et la performance globale du solveur.

Conference of 2014 8th IEEE International Symposium on Embedded Multicore/Manycore SoCs, MCSoC 2014 ; Conference Date: 23 September 2014 Through 25 September 2014; Conference Code:109143; International audience; This paper presents a first work to bring a consistent Model of Computation (MoC) for real-time applications on embedded many-core systems. Embedded manycores have lots of constraints (power, heterogeneity, memory, etc.) but also lots of promises with regard to harness able applications, i.e. New kinds of applications that could fit embedded systems. Such a MoC would encompass both data movements in Manycore's memories, determinism of execution, composability but also real-time requirements. We build our MoC on a well known base - CycloStatic Data Flow (CSDF) - for its desirable properties (i.e. Determinism and composability), and thank to several case-studies, we extend it to a superset, adding two special data processing filters which preserve these good properties and provide useful features for embedded computing.

Distributed systems are promisingly used in context of cross organizational enterprises. To develop these systems, Web services form an essential and wide accepted technology because they provide a significant level of platform independency and autonomy. Services are generally designed to interact with other services to form larger applications. In order to interact correctly with each other, Web services have to be compatible. This include not only composability of the involved services but also the correct execution of the overall composite service. In this context, we suggest in this paper to study the compatibility of Web services in different aspects and to provide a formal approach to characterize and verify this property. This approach is straightforward since it combines Petri nets and model checking techniques.

International audience; Most computational soundness theorems deal with a limited number of primitives, thereby limiting their applicability. The notion of deduction soundness of Cortier and Warinschi (CCS'11) aims to facilitate soundness theorems for richer frameworks via composition results: deduction soundness can be extended, generically, with asymmetric encryption and public data structures. Unfortunately, that paper also hints at rather serious limitations regarding further composition results: composability with digital signatures seems to be precluded. In this paper we provide techniques for bypassing the perceived limitations of deduction soundness and demonstrate that it enjoys vastly improved composition properties. More precisely, we show that a deduction sound implementation can be modularly extended with all of the five basic cryptographic primitives (symmetric/asymmetric encryption, message authentication codes, digital signatures, and hash functions). We thus obtain the first soundness framework that allows for the joint use of multiple instances of all of the basic primitives. In addition, we show how to overcome an important restriction of the bare deduction soundness framework which forbids sending encrypted secret keys. In turn, this prevents its use for the analysis of a large class of interesting protocols (e.g.~key exchange protocols). We allow for more liberal uses of keys as long as they are hidden in a sense that we also define. All primitives typically used to send secret data (symmetric/asymmetric encryption) satisfy our requirement which we also show to be preserved under composition.

International audience; Modeling and managing variability is a key activity in a growing number of software engineering contexts. Support for composing variability models is arising in many engineering scenarios, for instance, when several subsystems or modeling artifacts, each coming with their own variability and possibly developed by different stakeholders, should be combined together. In this paper, we consider the problem of composing feature models (FMs), a widely used formalism for representing and reasoning about a set of variability choices. We show that several composition operators can actually be defined, depending on both matching/merging strategies and semantic properties expected in the composed FM. We present four alternative forms and their implementations. We discuss their relative trade-offs w.r.t. reasoning, customizability, traceability, composability and quality of the resulting feature diagram. We summarize these findings in a reading grid which is validated by revisiting some relevant existing works. Our contribution should assist developers in choosing and implementing the right composition operators.

This paper proposes a general trajectory's meta-model and its architecture. In order to provide a unified meta-model and a powerful framework for trajectory's services and queries, the proposed trajectory's data-model has benefited from advantages of both conceptual and ontological space-time. However, it extends the basic data-model of trajectory with new patterns as Space Time Path to describe activities of the moving object, and Composite Region of Interest. Additionally, the proposed system is distinguished by providing framework for dealing moving objects trajectory, in an interoperable way, using heterogonous sensors that traditional data model alone are incapable for this purpose. The proposed system architecture for moving object trajectory's data-model is focused on service composability and data interoperability combining OGC standards, Service-Oriented Architecture and streaming technology, to allow applications constructed using the framework have better performance.

International audience; Zero-knowledge proofs have a vast applicability in the domain of cryptography, stemming from the fact that they can be used to force potentially malicious parties to abide by the rules of a protocol, without forcing them to reveal their secrets. $\Sigma$-protocols are a class of zero-knowledge proofs that can be implemented efficiently and that suffice for a great variety of practical applications. This paper presents a first machine-checked formalization of a comprehensive theory of Sigma-protocols. The development includes basic definitions, relations between different security properties that appear in the literature, and general composability theorems. We show its usefulness by formalizing---and proving the security---of concrete instances of several well-known protocols. The formalization builds on CertiCrypt, a framework that provides support to reason about cryptographic systems in the Coq proof assistant, and that has been previously used to formalize security proofs of encryption and signature schemes

This paper gives an overview of the cross-domain component-based architecture GENESYS for embedded systems. The development of this architecture has been driven by key industrial challenges identified within the ARTEMIS Strategic Research Agenda (SRA) such as composability, robustness and integrated resource management. GENESYS is a platform architecture that provides a minimal set of core services and a plurality of optional services that are predominantly implemented as self-contained system components. Choosing a suitable set of these system components that implement optional services, augmented by application specific components, can generate domain-specific instantiations of the architecture (e.g., for automotive, avionic, industrial control, mobile, and consumer electronics applications). Such a cross-domain approach is needed to support the coming Internet of Things, to take full advantage of the economies of scale of the semiconductor industry and to improve productivity.

International audience; This Special Section on “In-Vehicle Embedded Systems” presents four papers that deal with relevant aspects pertaining to the topics highlighted above, covering a spectrum of topics, ranging from schedulability and real-time Quality of Service analysis, thanks to deterministic as well to stochastic approaches, to the composability issues when components provided by different partners are to be integrated or when the designer wants to obtain preliminary results on end-to-end response time during earlier phases of the design process.

INTRODUCTION The Languages of Dynamic System Modeling by Paul A. Fishwick Introduction Dynamic System Modeling Examples Taxonomic Approaches Language Syntax Semantics Pragmatics Summary The Dynamics of the Computational Modeling of Analogy-Making by Robert M. French Introduction Analogy-Making as Sameness Analogy-Making as a Means of "Bootstrapping" Cognition The Necessity of Malleable Representations The Dynamics of Representation-Building in Analogy-Making Context-Dependent Computational Temperature Interaction between Top-Down and Bottom-Up Processes: An Example Computational Models Implementing This Bottom-Up/Top-Down Interaction Architectural Principles How This Type of Program Works: The Details How Tabletop Finds a Reasonable Solution The Issue of Scaling Up The Potential Long-Term Impact of the Mechanisms Presented Conclusions Impact of the Semantic Web on Modeling and Simulation by John A. Miller, Congzhou He, and Julia I. Couto Introduction Semantic Web: Relevant Issues Conceptual Basis for Discrete-Event Simulation Types of Mathematical Models Adding Semantics to Simulation Models Overview of DeSO Overview of DeMO Summary Systems Engineering by Andrew P. Sage Introduction Systems Engineering The Importance of Technical Direction and Systems Management Other Parts of the Story Summary Basic Elements of Mathematical Modeling by Clive L. Dym Principles of Mathematical Modeling Dimensional Consistency and Dimensional Analysis Abstraction and Scale Conservation and Balance Principles The Role of Linearity Conclusions DEVS Formalism for Modeling of Discrete-Event Systems by Tag Gon Kim Introduction System-Theoretic DES Modeling DEVS Formalism for DES Modeling DES Analysis with DEVS Model Simulation of DEVS Model Conclusion MODELING METHODOLOGIES Domain-Specific Modeling by Jeff Gray, Juha-Pekka Tolvanen, Steven Kelly, Anirudda Gokhale, Sandeep Neema, and Jonathan Sprinkle Introduction Essential Components of a Domain-Specific Modeling Environment Case Studies in DSM Overview of Supporting Tools Conclusion Agent-Oriented Modeling in Simulation: Agents for Modeling and Modeling for Agents by Adelinde M. Uhrmacher and Mathias Rohl Introduction Agents for Modeling in Simulation Modeling and Simulation for Agents Conclusion Distributed Modeling by Simon J.E. Taylor Introduction Modeling with COTS Simulation Packages Distributed Simulation CSP-Based Distributed Simulation A Standards-Based Approach Case Study Conclusion Model Execution by Kalyan S. Perumalla Introduction Time-Stepped Execution Discrete-Event Execution Summary Discrete-Event Simulation of Continuous Systems by James Nutaro Introduction Simulating a Single Ordinary Differential Equation Simulating Coupled Ordinary Differential Equations DEVS Representation of Discrete-Event Integrators The Heat Equation Conservation Laws Two-Point Integration Schemes Conclusions MULTIOBJECT AND SYSTEM Toward a Multimodel Hierarchy to Support Multiscale Simulation by Mark S. Shephard, E. Seegyoung Seol, and Benjamin FrantzDale Introduction Functional and Information Hierarchies in Multiscale Simulation Constructing a Multimodel: Design of Functional Components to Support Multiscale Simulations Example Multimodel Simulation Procedures Closing Remarks Finite Elements by Marc Hoit and Gary Consolazio Finite Element Theory Membrane Elements Flat Plate and Shell Elements Solid Elements Dynamics Summary Multimodeling by Minho Park, Paul A. Fishwick, and Jinho Lee Introduction Scene Construction Multimodeling Exchange Language (MXL) Dynamic Exchange Language (DXL) A Boiling Water Example Conclusion Hybrid Dynamic Systems: Modeling and Execution by Pieter J. Mosterman Introduction Hybrid Dynamic Systems Hybrid Dynamic System Behaviors An Implementation Advanced Topics in Hybrid Dynamic System Simulation Pathological Behavior Classes Conclusions Theory and Practice for Simulation Interconnection: Interoperability and Composability in Defense Simulation by Ernest H. Page Introduction The Practice of Simulation Interconnection-Simulation Interoperability The Theory of Simulation Interconnection-Simulation Composability Conclusions MODEL TYPES Ordinary Differential Equations by Francisco Esquembre and Wolfgang Christian Introduction Numerical Solution Taylor Methods Runge-Kutta Methods Implementation Adaptive Step Implementation of Adaptive Step Performance and Other Methods State Events The OSP Library Difference Equations as Discrete Dynamical Systems by Hassan Sedaghat Introduction Basic Concepts First-Order Difference Equations Higher Order Difference Equations Process Algebra by J.C.M. Baeten, D.A. van Beek, and J.E. Rooda Introduction Syntax and Informal Semantics of the ? Process Algebra Algebraic Reasoning and Verification Conclusions Temporal Logic by Antony Galton Propositional Logic Introducing Temporal Logic Syntax and Semantics Models of Time Further Extensions to the Formal Language Illustrative Examples Conclusion Further Reading Modeling Dynamic Systems with Cellular Automata by Peter M.A. Sloot and Altons G. Hoekstra Introduction A Bit of History Cellular Automata to Model Dynamical Systems One-Dimensional CAs Lattice Gas Cellular Automata Models of Fluid Dynamics Spatio-Temporal Connectionist Networks by Stefan C. Kremer Introduction Connectionist Networks (CNs) Spatio-Temporal Connectionist Networks Representational Power Learning Applications Conclusion Modeling Causality with Event Relationship Graphs by Lee Schruben Introduction Background and Definitions Enrichments to Event Relations Graphs Relationships to Other Discrete-Event System Modeling Methods Simulation of Event Relationship Graphs Event Relationship Graph Analysis Experimenting with ERGs Petri Nets for Dynamic Event-Driven System Modeling by Jiacun Wang Introduction Petri Net Definition Transition Firing Modeling Power Petri Net Properties Analysis of Petri Nets Colored Petri Nets Timed Petri Nets Concluding Remark Queueing System Models by Christos G. Cassandras Introduction Specification of Queueing System Models Performance of a Queueing System Queueing System Dynamics Little's Law Simple Markovian Queueing Models Markovian Queueing Networks Non-Markovian Queueing Systems Port-Based Modeling of Engineering Systems in Terms of Bond Graphs by Peter Breedveld Introduction Structured Systems: Physical Components and Interaction Bond Graphs Multiport Generalizations Conclusion System Dynamics Modeling of Environmental Systems by Andrew Ford Introductory Examples Comparison of the Flowers and Sales Models Background on Daisy World The Daisy World Model The Daisy World Management Flight Simulator Dynamic Simulation with Energy Systems Language by Clay L. Montague Introduction Reading an Energy Systems Language Diagram Translating a Diagram to Dynamic Equations Calibration of Model Constants Preparation for Simulation Dynamic Output of the Marsh Sector Model A Brief Comparison with Forrester's Systems Dynamics Approach Conclusions Ecological Modeling and Simulation: From Historical Development to Individual-Based Modeling by David R.C. Hill and P. Coquillard Introduction An Old Story? Determinism or Probability? Modeling Techniques The Use of Models in Ecology Models Are Scientific Instruments Levels of Organization and Methodological Choices Individual-Based Models Applications Conclusion Ontology-Based Simulation in Agriculture and Natural Resources by Howard Beck, Rohit Badal, and Yunchul Jung Introduction Ways in Which Ontologies Can Be Applied to Simulation How to Build an Ontology-Based Simulation-Bioprocessing Example Tools for Ontology-Based Simulation Conclusions Modeling Human Interaction in Organizational Systems by Stewart Robinson Introduction Systems and Human Interaction Why Model Human Interaction? Modeling Human Interaction: Research and Practice The KBI Methodology A Case Study: Modeling Human Decision Making at Ford Motor Company Conclusion Military Modeling by Roger Smith Introduction Applications Representation Dynamics Modeling Approach Military Simulation Systems Conclusion Dynamic Modeling in Management Science by Michael Pidd Introduction An Approach to Dynamic Systems Modeling in Management Science Discrete Event Simulation System Dynamics in Management Science Model Validation Chapter Summary Modeling and Analysis of Manufacturing Systems by E. Lefeber and J.E. Rooda Introduction Preliminaries Analytical Models for Steady-State Analysis Discrete-Event Models Effective Process Times Control of Manufacturing Systems: A Framework Standard Fluid Model and Extensions Flow Models Conclusions Sensor Network Component-Based Simulator by Boleslaw K. Szymanski and Gilbert Gang Chen The Need for a New Sensor Network Simulator Component Simulation Toolkit Wireless Sensor Network Simulation Conclusions CASE STUDIES Multidomain Modeling with Modelica by Martin Otter, Hilding Elmqvist, and Sven Erik Mattsson Modelica Overview Modelica Basics Modelica Libraries Symbolic Processing of Modelica Models Outlook Acknowledgments On Simulation of Simulink(R) Models for Model-Based Design by Rohit Shenoy, Brian McKay, and Pieter J. Mosterman Introduction The Case Study Example Designing with Simulation Obtaining Computational Models The Robotic Arm Model Using Computational Models for Control Design Testing with Model-Based Design Conclusions

International audience; We present a methodology for modeling heterogeneous real-time components. Components are obtained as the superposition of three layers : Behavior, specified as a set of transitions; Interactions between transitions of the behavior; Priorities, used to choose amongst possible interactions. A parameterized binary composition operator is used to compose components layer by layer. We present the BIP language for the description and composition of layered components as well as associated tools for executing and analyzing components on a dedicated platform. The language provides a powerful mechanism for structuring interactions involving rendezvous and broadcast. We show that synchronous and timed systems are particular classes of components. Finally, we provide examples and compare the BIP framework to existing ones for heterogeneous component-based modeling.

Projet POP_ART; We present a framework for the incremental construction of deadlock-free systems meeting given safety properties. The framework borrows concepts and basic results from the controller synthesis paradigm by considering a step in the construction process as a controller synthesis problem. We show that priorities are expressive enough to represent restrictions induced by deadlock-free controllers preserving safety properties. We define a correspondence between such restrictions and priorities and provide compositionality results about the preservation of this correspondence by operations on safety properties and priorities. Finally, we provide an example illustrating an application of the results.

This thesis is concerned with the modelling of real-time systems using Petri nets. We investigate both the problem of time representation, and of preemption (i.e., interruption of the processes of a system) which is often needed for real-time applications.We consider Petri nets without explicit temporal information. The key idea of our approach consists in introducing time through specific sub-nets representing clocks present in the system being modelled. This results in what we refer to as causal time since causality is the only means by which the precedence relationship between event occurrences is specified. For a succinct formulation of the causal time model, we use M-nets which are a class of coloured Petri nets endowed with compositional operators similar to those used by the standard process algebras. We extend the M-nets model in order to allow an efficient representation of asynchronous interprocess communication, and establish a number of theoretical results concerning such an extension. We use the resulting M-nets to model several clocks with varied characteristics, showing how they can be synchronised or kept independent. The suitability of the proposed approach is evaluated using a case study, and it is then used to give a semantics of the parallel programming language B(PN)² extended with real-time constructs.In order to deal with preemption, we propose another extension of the M-nets model supporting operators for process suspension/resuming and abortion. The resulting model is investigated at the theoretical level, and applied to B(PN)² enhanced with exceptions and tasks., Cette thèse traite de la modélisation des systèmes temps-réel à l'aidede réseaux de Petri. Nous considérons séparément la question dereprésentation du temps et celle de la préemption (interruption desprocessus d'un système) qui est d'un usage courant pour lesapplications temps-réel.Nous utilisons des réseaux de Petri sans extension par desinformations concernant le temps. Notre approche consiste alors àintroduire le temps par des sous-réseaux spécifiques représentant leshorloges du système modélisé. Le résultat est appelé tempscausal puisque seule la causalité définit la relation de précédenceentre les occurrences des événements. Afin d'obtenir une formulationélégante de l'approche causale du temps, nous utilisons le modèle desM-nets, une classe de réseaux de Petri colorés composables à lamanière des algèbres de processus. Nous étendons ce modèle de façon àpermettre la représentation efficace des communications asynchronesentre processus et les bases théoriques liées à cette extension sontrevisitées et mises à jour. Nous utilisons les M-nets ainsi étenduspour modéliser plusieurs horloges aux fonctionnalités différentes.Nous montrons comment des systèmes à plusieurs horloges, synchroniséesou non, peuvent être assez simplement obtenus. La pertinence de notreapproche est évaluée par une étude de cas et appliquée à la sémantiqued'une extension d'un langage de programmation parallèle, appeléB(PN)², par des instructions liées au temps.Pour introduire la préemption nous proposons une nouvelle extensiondes M-nets avec des opérations permettant la suspension/reprise etl'avortement. Le modèle obtenu est étudié sur le plan théorique etappliqué à l'extension de la sémantique de B(PN)² par des exceptionset un système de tâches.