Search

Your search keyword '"Nathanaël Sensfelder"' showing total 12 results
Start Over Author "Nathanaël Sensfelder"
12 results on '"Nathanaël Sensfelder"'

6. On How to Identify Cache Coherence: Case of the NXP QorIQ T4240

Author

Nathanaël Sensfelder and Julien Brunel and Claire Pagetti, Sensfelder, Nathanaël, Brunel, Julien, Pagetti, Claire, Nathanaël Sensfelder and Julien Brunel and Claire Pagetti, Sensfelder, Nathanaël, Brunel, Julien, and Pagetti, Claire

Abstract

Architectures used in safety critical systems have to pass certain certification standards, which require sufficient proof that they will behave as expected. Multi-core processors make this challenging by featuring complex interactions between the tasks they run. A lot of these interactions are made without explicit instructions from the program designers. Furthermore, they can have strong negative impacts on performance (and potentially affect correctness). One important such source of interactions is cache coherence, which speeds up operations in most cases, but can also lead to unexpected variations in execution time if not fully understood. Architecture documentations often lack details on the implementation of cache coherence. We thus propose a strategy to ascertain that the platform does indeed implement the cache coherence protocol its user believes it to. We also apply this strategy to the NXP QorIQ T4240, resulting in the identification of a protocol (MESIF) other than the one this architecture’s documentation led us to believe it was using (MESI).

Published
2020
Full Text
View/download PDF

7. A Service-Based Modelling Approach to Ease the Certification of Multi-Core COTS Processors

Author

Nathanaël Sensfelder, Kevin Delmas, Claire Pagetti, Thomas Polacsek, Frédéric Boniol, Youcef Bouchebaba, Julien Brunel, ONERA / DTIS, Université de Toulouse [Toulouse], ONERA-PRES Université de Toulouse, Génie Informatique, École Polytechnique de Montréal (EPM)-Centre de Recherche en Informatique (CRI), MINES ParisTech - École nationale supérieure des mines de Paris, Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-MINES ParisTech - École nationale supérieure des mines de Paris, Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL), Réseaux, Mobiles, Embarqués, Sans fil, Satellites (IRIT-RMESS), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), and Université Fédérale Toulouse Midi-Pyrénées

Subjects
CERTIFICATION, Service (systems architecture), Multi-core processor, METHODE FORMELLE, Computer science, 020207 software engineering, 0102 computer and information sciences, 02 engineering and technology, Certification, 01 natural sciences, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], Argumentation theory, 010201 computation theory & mathematics, Salient, MULTI-COEURS, 0202 electrical engineering, electronic engineering, information engineering, Systems engineering, Position paper, Adaptation (computer science), Combinatorial explosion
Abstract

International audience; The Phylog project aims at offering a model-based software-aided certification framework for aeronautical systems based on multi/many-core architectures. Certifying such platforms will entail fulfilling the high level objectives of the MCP-CRI / CAST-32A position paper. Among those, two types of analysis are required: interference and safety analyses. Because of the large size of the platforms and their complexity, those analyses can lead to combinatorial explosion and to some misinterpretation. To tackle these issues, we explore a service-based modelling approach that leads to a simplification of the analyses and to the highlighting of salient properties, making the adaptation of the certification argumentation efficient.

Published
2019
Full Text
View/download PDF

8. Identification of Multi-Core Interference

Author

Claire Pagetti, Frédéric Boniol, Nathanaël Sensfelder, ONERA / DTIS, Université de Toulouse [Toulouse], ONERA-PRES Université de Toulouse, Réseaux, Mobiles, Embarqués, Sans fil, Satellites (IRIT-RMESS), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), and Université Fédérale Toulouse Midi-Pyrénées

Subjects
timing interference, Multi-core processor, certification, business.industry, Computer science, Distributed computing, 02 engineering and technology, Certification, Avionics, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], 020202 computer hardware & architecture, Domain (software engineering), Identification (information), 020303 mechanical engineering & transports, Software, 0203 mechanical engineering, Interference (communication), 0202 electrical engineering, electronic engineering, information engineering, Multi-core, business
Abstract

International audience; The CAST-32A provides some guidelines to help certify multi-core-based systems in the avionics domain. One major requirement is to compute all the potential interference and to provide adequate mitigation means. In this paper, we compare two approaches to identify the interference: the initiator-target and the Phylog models. The latter is more compact and efficient, despite also covering all of the problematic conflictual situations.

Published
2019
Full Text
View/download PDF

9. Modeling Cache Coherence to Expose Interference

Author

Nathanaël Sensfelder and Julien Brunel and Claire Pagetti, Sensfelder, Nathanaël, Brunel, Julien, Pagetti, Claire, Nathanaël Sensfelder and Julien Brunel and Claire Pagetti, Sensfelder, Nathanaël, Brunel, Julien, and Pagetti, Claire

Abstract

To facilitate programming, most multi-core processors feature automated mechanisms maintaining coherence between each core’s cache. These mechanisms introduce interference, that is, delays caused by concurrent access to a shared resource. This type of interference is hard to predict, leading to the mechanisms being shunned by real-time system designers, at the cost of potential benefits in both running time and system complexity. We believe that formal methods can provide the means to ensure that the effects of this interference are properly exposed and mitigated. Consequently, this paper proposes a nascent framework relying on timed automata to model and analyze the interference caused by cache coherence.

Published
2019
Full Text
View/download PDF

10. Modeling Cache Coherence to Expose Interference (Artifact)

Author

Nathanaël Sensfelder and Julien Brunel and Claire Pagetti, Sensfelder, Nathanaël, Brunel, Julien, Pagetti, Claire, Nathanaël Sensfelder and Julien Brunel and Claire Pagetti, Sensfelder, Nathanaël, Brunel, Julien, and Pagetti, Claire

Abstract

To facilitate programming, most multi-core processors feature automated mechanisms maintaining coherence between each core’s cache. These mechanisms introduce interference, that is, delays caused by concurrent access to a shared resource. This type of interference is hard to predict, leading to the mechanisms being shunned by real-time system designers, at the cost of potential benefits in both running time and system complexity. We believe that formal methods can provide the means to ensure that the effects of this interference are properly exposed and mitigated. Consequently, we propose a nascent framework relying on timed automata to model and analyze the interference caused by cache coherence.

Published
2019
Full Text
View/download PDF

11. PHYLOG: A model-based certification framework

Author

Claire Pagetti, Frédéric Boniol, Thomas Polacsek, Julien Brunel, Youcef Bouchebaba, Nathanaël Sensfelder, Kevin Delmas, ONERA / DTIS, Université de Toulouse [Toulouse], ONERA-PRES Université de Toulouse, and André, Cécile

Subjects
[INFO.INFO-AI] Computer Science [cs]/Artificial Intelligence [cs.AI], CERTIFICATION, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Computer science, 020209 energy, MULTI-CORE, 02 engineering and technology, Certification, [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL], [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI], Engineering management, 020303 mechanical engineering & transports, 0203 mechanical engineering, PHYLOG, 0202 electrical engineering, electronic engineering, information engineering
Abstract

International audience; This paper describes PHYLOG, a framework in- tended to help certify the use of a multi-core in an aeronautical context. Specific guidelines for such systems have been published in a document, the MCP-CRI / CAST-32A, which provides a series of objectives to be fulfilled. To justify that an objective is indeed achieved, PHYLOG relies on structured graphical no- tations, recursively refining each objective by solving it using a strategy, itself having its own sub-objectives, until all that remains are evidences found either through the use of formal methods, as part of the design choices, or in external documentation. The PHYLOG framework includes such formal methods, providing the means to model the multi-core and to acquire further evidences through automatic analysis.

Published
2018
Full Text
View/download PDF

12. Inference of Channel Priorities for Asynchronous Communication

Author

Aurélie Hurault, Nathanaël Sensfelder, Philippe Quéinnec, Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, Institut National Polytechnique (Toulouse) (Toulouse INP), Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE), Centre National de la Recherche Scientifique - CNRS (FRANCE), Université Toulouse III - Paul Sabatier - UT3 (FRANCE), Université Toulouse - Jean Jaurès - UT2J (FRANCE), and Université Toulouse 1 Capitole - UT1 (FRANCE)

Subjects
[INFO.INFO-AR]Computer Science [cs]/Hardware Architecture [cs.AR], Property (programming), Computer science, Distributed computing, Inference, User defined, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], 0102 computer and information sciences, Interface homme-machine, 01 natural sciences, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Linear temporal logic, Architectures Matérielles, Génie logiciel, [INFO.INFO-HC]Computer Science [cs]/Human-Computer Interaction [cs.HC], Computer Science::Information Theory, business.industry, Modélisation et simulation, Systèmes embarqués, [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation, Formal verification, 010201 computation theory & mathematics, Order (business), Asynchronous communication, Models of communication, Cryptographie et sécurité, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, business, Computer network, Communication channel
Abstract

International audience; In distributed systems, the order in which the messages are received by the processes is crucial to ensure the expected behavior. This paper presents a communication model which allows for restrictions on the deliveries of a channel depending on the availability of messages in other channels. This corresponds to prioritizing some channels over others. It relies on a framework able to verify if a given system satisfies a user defined LTL (Linear Temporal Logic) property with different priorities. We also propose to automatically infer the channel priorities so that the system does not infringe on this temporal property.

Published
2017
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results