Sites Inria

English version

Equipe de recherche TEA

Publications de l'équipe TEA

2019

Thèse

titre
Parallelism and modular proof in differential dynamic logic
auteur
Simon Lunel
article
Artificial Intelligence [cs.AI]. Université Rennes 1, 2019. English. ⟨NNT : 2019REN1S005⟩
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-02102687/file/LUNEL_Simon.pdf BibTex

2018

Article dans une revue

titre
Guest Editorial: Special Issue of ACM TECS on the ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2017)
auteur
Patricia Derler, Klaus Schneider, Jean-Pierre Talpin
article
ACM Transactions on Embedded Computing Systems (TECS), ACM, 2018, pp.1-2
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01926923/file/TECS%20SI.pdf BibTex
titre
Polychronous Automata and their Use for Formal Validation of AADL Models
auteur
Thierry Gautier, Clément Guy, Alexandre Honorat, Paul Le Guernic, Jean-Pierre Talpin, Loïc Besnard
article
Frontiers of Computer Science, Springer Verlag, 2018, ⟨10.1007/s11704-017-6134-5⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01411257/file/extended_tase15.pdf BibTex

Communication dans un congrès

titre
Refinement types for system design (abstract)
auteur
Jean-Pierre Talpin
article
FDL 2018 - Forum on specification and Design Languages, Sep 2018, Munich, Germany
Accès au bibtex
BibTex
titre
Toward Efficient Many-core Scheduling of Partial Expansion Graphs
auteur
Hai Nam Tran, Shuvra Bhattacharyya, Jean-Pierre Talpin, Thierry Gautier
article
SCOPES 2018 - 21st International Workshop on Software and Compilers for Embedded Systems, May 2018, Saint Goar, Germany. pp.1-4, ⟨10.1145/3207719.3207734⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01926955/file/scopes18.pdf BibTex

Cours

titre
The Signal synchronous language: the principles beyond the language and how to exploit and extend them
auteur
Albert Benveniste, Thierry Gautier
article
École thématique. France. 2018, pp.1-68
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01929567/file/SignalAndBeyond_2018_pdf.pdf BibTex

2017

Article dans une revue

titre
面向同步规范的并行代码自动生成
auteur
Kai Hu, Teng Zhang, Lihong Shang, Zhibing Yang, Jean-Pierre Talpin
article
Journal of Software, Science in China Press, 2017, 28, pp.1-15. ⟨10.13328/j.cnki.jos.005056⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01644290/file/create_pdf.aspx.pdf BibTex

Communication dans un congrès

titre
Compositional methods for CPS design (keynote abstract)
auteur
Jean-Pierre Talpin
article
3rd Symposium on Dependable Software Engineering: Theories, Tools and Applications, Oct 2017, Changsha, China
Accès au bibtex
BibTex
titre
ADFG: a scheduling synthesis tool for dataflow graphs in real-time systems
auteur
Alexandre Honorat, Hai Nam Tran, Loïc Besnard, Thierry Gautier, Jean-Pierre Talpin, Adnan Bouakaz
article
International Conference on Real-Time Networks and Systems , Oct 2017, Grenoble, France. pp.1-10, ⟨10.1145/3139258.3139267⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01615142/file/rnts17.pdf BibTex
titre
Compositional proofs in differential dynamic logic dL
auteur
Simon Lunel, Benoît Boyer, Jean-Pierre Talpin
article
17th International Conference on Application of Concurrency to System Design, Jun 2017, Zaragoza, Spain
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01615140/file/acsd17.pdf BibTex
titre
An Abstraction Technique For Parameterized Model Checking of Leader Election Protocols: Application to FTSP
auteur
Ocan Sankur, Jean-Pierre Talpin
article
23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Apr 2017, Uppsala, Sweden. pp.23-40
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01431472/file/formal.pdf BibTex

Chapitre d'ouvrage

titre
Formal Semantics of Behavior Specifications in the Architecture Analysis and Design Language Standard
auteur
Loic Besnard, Thierry Gautier, Paul Le Guernic, Clément Guy, Jean-Pierre Talpin, Brian Larson, Etienne Borde
article
Cyber-Physical System Design from an Architecture Analysis Viewpoint, Springer, 2017, Cyber-Physical System Design from an Architecture Analysis Viewpoint, ⟨10.1007/978-981-10-4436-6_3⟩
Accès au bibtex
BibTex

Ouvrage (y compris édition critique et traduction)

titre
Cyber-Physical System Design from an Architecture Analysis Viewpoint
auteur
Shin Nakajima, Jean-Pierre Talpin, Masumo Toyoshima, Huafeng Yu
article
Springer, 2017, Communications of NII Shonan Meetings, 978-981-10-4435-9. ⟨10.1007/978-981-10-4436-6⟩
Accès au bibtex
BibTex

2016

Article dans une revue

titre
Using Runtime Systems Tools to Implement Efficient Preconditioners for Heterogeneous Architectures
auteur
Adrien Roussel, Jean-Marc Gratien, Thierry Gautier
article
Oil & Gas Science and Technology - Revue d'IFP Energies nouvelles, Institut Français du Pétrole, 2016, 71 (6), pp.65:1-13. ⟨10.2516/ogst/2016020⟩
Accès au texte intégral et bibtex
https://hal-ifp.archives-ouvertes.fr/hal-01396153/file/ogst150225.pdf BibTex

Communication dans un congrès

titre
Formal semantics of behavior specifications in the architecture analysis and design language standard
auteur
Loïc Besnard, Thierry Gautier, Clément Guy, Paul Le Guernic, Jean-Pierre Talpin, Brian Larson, Etienne Borde
article
HLDVT 2016 - 18th IEEE International High-Level Design Validation and Test Workshop, Oct 2016, Santa Cruz, United States. pp.30-39, ⟨10.1109/HLDVT.2016.7748252⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01419968/file/hldvt16.pdf BibTex
titre
Flexible Runtime Verification Based On Logical Clock Constraints
auteur
Daian Yue, Vania Joloboff, Frédéric Mallet
article
FDL 2016 - Forum on specification & Design Languages, ECSI, Sep 2016, Bremen, Germany
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01421890/file/yue.pdf BibTex
titre
A Sequent Calculus for a Modal Logic on Finite Data Trees
auteur
David Baelde, Simon Lunel, Sylvain Schmitz
article
CSL 2016, Sep 2016, Marseille, France. pp.1--16, ⟨10.4230/LIPIcs.CSL.2016.32⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01191172/file/main.pdf BibTex
titre
PSCV: A Runtime Verification Tool for Probabilistic SystemC Models
auteur
Van Ngo, Axel Legay, Vania Joloboff
article
CAV 2016 - 28th International Conference on Computer Aided Verification, Jul 2016, Toronto, Canada. pp.84 - 91, ⟨10.1007/978-3-319-41528-4_5⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01406488/file/c177.pdf BibTex
titre
A Stencil DSEL for Single Code Accelerated Computing with SYCL
auteur
Olivier Aumage, Denis Barthou, Alexandre Honorat
article
SYCL 2016 1st SYCL Programming Workshop during the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, Mar 2016, Barcelone, Spain
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01290099/file/main.pdf BibTex
titre
Integration of polychrony and QGen model compiler
auteur
Christophe Junke, Thierry Gautier, Jean-Pierre Talpin, Loic Besnard
article
ERTS'16 - European Congress on Embeddd Real-Rime Software and Systems, Jan 2016, Toulouse, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01241808/file/erts2016.pdf BibTex

Rapport

titre
TRAP: A Platform For Flexible Runtime Verification of Temporal Properties
auteur
Daian Yue
article
[Research Report] RR-9006, INRIA. 2016, pp.46
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01417075/file/RR-9006%20%281%29.pdf BibTex
titre
Formal semantics of behavior specifications in the architecture analysis and design language standard
auteur
Loïc Besnard, Thierry Gautier, Paul Le Guernic, Clément Guy, Jean-Pierre Talpin, Brian Larson, Etienne Borde
article
[Research Report] RR-8950, INRIA. 2016, pp.30 - 39
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01419973/file/RR-8950.pdf BibTex

2015

Article dans une revue

titre
Fast approximately timed simulation
auteur
Vania Joloboff, Shenpeng Wang, Yangdong Deng
article
WIT Transactions on Information and Communication Technologies, WIT Press, 2015, WIT Transactions on Information and Communication Technologies, 978-1-78466-054-3 (68), pp.756. ⟨http://www.witpress.com/⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01081104/file/C029final.pdf BibTex

Communication dans un congrès

titre
Towards Verified Faithful Simulation
auteur
Vania Joloboff, Jean-François Monin, Xiaomu Shi
article
Dependable Software Engineering: Theories, Tools, and Applications, Nov 2015, Nanjing, China
Accès au bibtex
BibTex
titre
Towards refinement types for time-dependent data-flow networks
auteur
Jean-Pierre Talpin, Pierre Jouvelot, Sandeep Kumar Shukla
article
ACM-IEEE Conference on Methods and Models for System Design, Sep 2015, Austin, United States
Accès au bibtex
BibTex
titre
Polychronous Automata
auteur
Paul Le Guernic, Thierry Gautier, Jean-Pierre Talpin, Loïc Besnard
article
TASE 2015, 9th International Symposium on Theoretical Aspects of Software Engineering, Sep 2015, Nanjing, China. pp.95-102, ⟨10.1109/TASE.2015.21⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01240440/file/tase15.pdf BibTex
titre
Model-Based Integration for Automotive Control Software
auteur
Huafeng Yu, Joshi Prashi, Jean-Pierre Talpin, Sandeep Kumar Shukla, Shin'Ichi Shiraishi
article
Digital Automation Conference, ACM, Jun 2015, San Francisco, United States
Accès au bibtex
BibTex
titre
Translation Validation for Synchronous Data-Flow Specification in the SIGNAL Compiler
auteur
Van Chan Ngo, Jean-Pierre Talpin, Thierry Gautier
article
35th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2015, Grenoble, France. pp.66-80, ⟨10.1007/978-3-319-19195-9_5 ⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01767328/file/978-3-319-19195-9_5_Chapter.pdf BibTex
titre
Modular translation validation of a full-sized synchronous compiler using off-the-shelf verification tools (abstract)
auteur
Van Chan Ngo, Jean-Pierre Talpin, Thierry Gautier, Loic Besnard, Paul Le Guernic
article
International Workshop on Software and Compilers for Embedded Systems, ACM, Jun 2015, St Goar, Germany
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01148919/file/scopes15.pdf BibTex
titre
Mapping Functional Behavior onto Architectural Model in a Model Driven Embedded System Design
auteur
Joshi Prashi, Sandeep Kumar Shukla, Jean-Pierre Talpin, Huafeng Yu
article
Symposium On Applied Computing, Apr 2015, Salamanca, Spain
Accès au bibtex
BibTex
titre
Translation Validation for Clock Transformations in a Synchronous Compiler
auteur
Van Chan Ngo, Jean-Pierre Talpin, Thierry Gautier, Paul Le Guernic
article
FASE - ETAPS 2015, Apr 2015, London, United Kingdom
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01087795/file/main.pdf BibTex

Rapport

titre
Liquid Clocks - Refinement Types for Time-Dependent Stream Functions
auteur
Jean-Pierre Talpin, Pierre Jouvelot, Sandeep Kumar Shukla
article
[Research Report] RR-8747, INRIA Rennes - Bretagne Atlantique; INRIA. 2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01166350/file/report.pdf BibTex

2014

Article dans une revue

titre
Constructive Polychronous Systems
auteur
Jean-Pierre Talpin, Jens Brandt, Mike Gemünde, Klaus Schneider, Sandeep Shukla
article
Science of Computer Programming, Elsevier, 2014, Science of Computer Programming, pp.20. ⟨http://www.journals.elsevier.com/science-of-computer-programming⟩
Accès au bibtex
BibTex
titre
From AADL to timed abstract state machine: a certified model transformation
auteur
Zhibin Yang, Kai Hu, Dianfu Ma, Jean-Paul Bodeveix, Lei Pi, Jean-Pierre Talpin
article
Journal of Systems and Software, Elsevier, 2014, Journal of Systems and Software, pp.20
Accès au bibtex
BibTex
titre
Timed behavioural modelling and affine scheduling of embedded software architectures in the AADL using Polychrony
auteur
Loïc Besnard, Adnan Bouakaz, Thierry Gautier, Paul Le Guernic, Yue Ma, Jean-Pierre Talpin, Huafeng Yu
article
Science of Computer Programming, Elsevier, 2014, Science of Computer Programming, pp.20
Accès au bibtex
BibTex
titre
From AADL to Timed Abstract State Machines: A Verified Model Transformation
auteur
Zhibin Yang, Kai Hu, Dianfu Ma, Jean-Paul Bodeveix, Lei Pi, Jean-Pierre Talpin
article
Journal of Systems and Software, Elsevier, 2014, vol. 93, pp. 42-68. ⟨10.1016/j.jss.2014.02.058⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01123837/file/Yang_12950.pdf BibTex

Communication dans un congrès

titre
Earliest-Deadline First Scheduling of Multiple Independent Dataflow Graphs
auteur
Adnan Bouakaz, Thierry Gautier, Jean-Pierre Talpin
article
2014 IEEE Workshop on Signal Processing Systems (SiPS), Oct 2014, Belfast, United Kingdom
Accès au bibtex
BibTex
titre
Optimized Distribution of Synchronous Programs via a Polychronous Model
auteur
Ke Sun, Loïc Besnard, Thierry Gautier
article
Formal Methods and Models for System Design (MEMOCODE'14), Oct 2014, Lausanne, Switzerland. pp.42 - 51, ⟨10.1109/MEMCOD.2014.6961842⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01088953/file/PAPER2014.pdf https://hal.inria.fr/hal-01088953/file/Optimized%20Distribution%20of%20Synchronous%20Programs%20via%20a%20Polychronous%20Model%20%28MEMOCODE%202014%29.pdf BibTex
titre
An abstraction-refinement framework for priority-driven scheduling of static dataflow graphs
auteur
Adnan Bouakaz, Thierry Gautier
article
International Conference on Formal Methods and Models for System Design, Oct 2014, Lausanne, Switzerland. ⟨10.1109/MEMCOD.2014.6961838⟩
Accès au bibtex
BibTex
titre
Towards an architecture-centric approach dedicated to model-based virtual integration for embedded software systems
auteur
Huafeng Yu, Jean-Pierre Talpin, Sandeep Shukla, Prachi Joshi, Shin'Ichi Shiraishi
article
Workshop on Architecture Centric Virtual Integration, MODELS 2014, Sep 2014, Valencia, Spain
Accès au bibtex
BibTex
titre
A constraint-solving approach to Faust program type checking
auteur
Imré Frotier de La Messelière, Pierre Jouvelot, Jean-Pierre Talpin
article
Constraint Programming meets Verification, The 20th International Conference on Principles and Practice of Constraint Programming, Sep 2014, Lyon, France
Accès au bibtex
BibTex
titre
Precise deadlock detection for polychronous data-flow specifications
auteur
Van Chan Ngo, Jean-Pierre Talpin, Thierry Gautier
article
ESLsyn - DAC 2014, May 2014, San Francisco, United States. ⟨10.1109/ESLsyn.2014.6850379⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01086843/file/ESLSYN14.pdf BibTex

Rapport

titre
Logically timed specifications in the AADL : a synchronous model of computation and communication (recommendations to the SAE committee on AADL)
auteur
Loïc Besnard, Etienne Borde, Pierre Dissaux, Thierry Gautier, Paul Le Guernic, Jean-Pierre Talpin
article
[Technical Report] RT-0446, INRIA. 2014, pp.27
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00970244/file/RT_446.pdf BibTex

Thèse

titre
Formal verification of a synchronous data-flow compiler : from Signal to C
auteur
Van Chan Ngô
article
Software Engineering [cs.SE]. Université Rennes 1, 2014. English. ⟨NNT : 2014REN1S034⟩
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01067477/file/NGO_Van_Chan.pdf BibTex

Pré-publication, Document de travail

titre
Translation Validation for Synchronous Data-flow Specification in the SIGNAL Compiler
auteur
Van Chan Ngo, Jean-Pierre Talpin, Thierry Gautier
article
2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01087801/file/nfm.pdf BibTex

Suivez Inria