Publications de l'équipe VERTECS

2012

Articles dans des revues avec comité de lecture

Titre

Petri Net Reachability Graphs: Decidability Status of First Order Properties

Auteurs

Philippe Darondeau; Stephane Demri; Roland Meyer; Christophe Morvan

Détail

Logical Methods in Computer Science, International Federation of Computational Logic, 2012, 8 (4:9), pp. 1-28

Accès au texte intégral et bibtex

Titre

Off-line Test Selection with Test Purposes for Non-Deterministic Timed Automata

Auteurs

Nathalie Bertrand; Thierry Jéron; Amélie Stainer ; Moez Krichen

Détail

Logical Methods in Computer Science, IfCoLog (International Federation of Computational Logic), 2012, 8 (4:8), pp. 1-33

Accès au texte intégral et bibtex

Titre

Synthesis of opaque systems with static and dynamic masks

Auteurs

Franck Cassez; Jérémy Dubreil; Hervé Marchand

Détail

Formal Methods in System Design, Springer, 2012, 40 (1), pp. 88-115

Accès au texte intégral et bibtex

Titre

Probabilistic omega-automata

Auteurs

Christel Baier; Nathalie Bertrand; Marcus Groesser

Détail

Journal of the Association for Computing Machinery, ACM, 2012, 59 (1), pp. 1:1-1:52

Accès au bibtex

Titre

More testable properties

Auteurs

Yliès Falcone; Jean-Claude Fernandez; Thierry Jéron; Hervé Marchand ; Laurent Mounier

Détail

International Journal on Software Tools for Technology Transfer, springer, 2012, 14 (4), pp. 407-437

Accès au texte intégral et bibtex

Titre

Modal event-clock specifications for timed component-based design

Auteurs

Nathalie Bertrand; Axel Legay; Sophie Pinchinat; Jean-Baptiste Raclet

Détail

Science of Computer Programming, Elsevier, 2012, 77, pp. 1212-1234

Accès au bibtex

Titre

Symbolic Supervisory Control of Infinite Transition Systems under Partial Observation using Abstract Interpretation

Auteurs

Gabriel Kalyon; Tristan Le Gall; Hervé Marchand; Thierry Massart

Détail

Discrete Event Dynamic Systems, Springer, 2012, 22 (2), pp. 121-161

Accès au texte intégral et bibtex

Communications avec actes

Titre

Analysis of partially observed recursive tile systems

Auteurs

Sébastien Chédor; Christophe Morvan ; Sophie Pinchinat; Hervé Marchand

Détail

11th Int. Workshop on Discrete Event Systems, Oct 2012, Guadalajara, Mexico. pp. 265-271

Accès au texte intégral et bibtex

Titre

Runtime Enforcement of Timed Properties

Auteurs

Srinivas Pinisetty; Yliès Falcone; Thierry Jéron; Hervé Marchand ; Antoine Rollet; Omer Landry Nguena Timo

Détail

3rd International Conference on Runtime Verification, Sep 2012, Istanbul, Turkey.

Accès au texte intégral et bibtex

Titre

Frequencies in Forgetful Timed Automata

Auteurs

Amélie Stainer

Détail

M. Jurdzinski and D. Nickovic. Formal Modeling and Analysis of Timed Systems, Sep 2012, London, United Kingdom. Springer, 7595, pp. 236-251, Lecture notes in computer science

Accès au texte intégral et bibtex

Titre

Playing Optimally on Timed Automata with Random Delays

Auteurs

Nathalie Bertrand; Sven Schewe

Détail

Formats - 10th International Conference on Formal Modeling and Analysis of Timed Systems - 2012, Sep 2012, London, United Kingdom. 7595, pp. 43-58, Lecture Notes in Computer Science

Accès au bibtex

Titre

Test generation from recursive tiles systems

Auteurs

Sébastien Chédor; Thierry Jéron; Christophe Morvan

Détail

Achim D. Brucker and Jacques Julliand. TAP - 6th International Conference on Tests & Proofs - 2012, May 2012, Prague, Czech Republic. Springer, 7305, pp. 99-114, LNCS

Accès au texte intégral et bibtex

Titre

Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic

Auteurs

Peter Bulychev; Alexandre David; Kim G. Larsen; Axel Legay; Guangyuan Li; Danny Bogsten Poulsen; Amélie Stainer

Détail

Nikolaj Bjørner, Andrei Voronkov. Logic for Programming, Artificial Intelligence, and Reasoning, Mar 2012, Merida, Venezuela, Bolivarian Republic Of. Springer, 7180, pp. 168-182, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

Bounded Satisfiability for PCTL

Auteurs

Nathalie Bertrand; John Fearnley; Sven Schewe

Détail

CSL - 21st EACSL Annual Conferences on Computer Science Logic - 2012, Sep 2012, Fontainebleau, France. LIPIcs, 16, pp. 92-106

Accès au bibtex

Titre

On the Decidability Status of Reachability and Coverability in Graph Transformation Systems

Auteurs

Nathalie Bertrand; Giorgio Delzanno; Barbara König; Arnaud Sangnier ; Jan Stückrath

Détail

RTA - 23rd International Conference on Rewriting Techniques and Applications - 2012, 2012, Nagoya, Japan. 15, pp. 101-116, LIPIcs

Accès au bibtex

Rapports

Titre

Frequencies in forgetful timed automata

Auteurs

Amélie Stainer

Détail

[Report], 2012. RR-8009

Accès au texte intégral et bibtex

Documents sans référence de publication

Titre

Reachability of Communicating Timed Processes

Auteurs

Lorenzo Clemente; Frédéric Herbreteau; Amélie Stainer; Grégoire Sutre

Détail

Oct. 2012. Extended version

Accès au bibtex

2011

Articles dans des revues avec comité de lecture

Titre

What can you verify and Enforce at Runtime?

Auteurs

Yliès Falcone; Jean-Claude Fernandez; Laurent Mounier

Détail

Sotfware Tools for Technology Transfer, 2011, pp. Online First

Accès au texte intégral et bibtex

Titre

Runtime Enforcement Monitors: composition, synthesis, and enforcement abilities

Auteurs

Yliès Falcone; Laurent Mounier; Jean-Claude Fernandez; Jean-Luc Richier

Détail

Formal Methods in System Design, 2011, pp. 10.1007/s10703-011-0114-4

Accès au texte intégral et bibtex

Titre

Decentralized Control of Infinite Systems

Auteurs

Gabriel Kalyon; Tristan Le Gall; Hervé Marchand; Thierry Massart

Détail

Discrete Event Dynamic Systems, springer, 2011, 21 (3), pp. 359-393

Accès au texte intégral et bibtex

Communications avec actes

Titre

Runtime Verification of Component-Based Systems

Auteurs

Yliès Falcone ; Mohamad Jaber; Thanh-Hung Nguyen; Marius Bozga; Saddek Bensalem

Détail

Software Engineering and Formal Methods, Nov 2011, Montevideo, Uruguay. pp. 10.1007/978-3-642-24690-6_15

Accès au texte intégral et bibtex

Titre

Polychronous Controller Synthesis from MARTE CCSL Timing Specifications

Auteurs

Huafeng Yu; Jean-Pierre Talpin; Loïc Besnard; Thierry Gautier; Hervé Marchand; Paul Le Guernic

Détail

ACM/IEEE Ninth International Conference on Formal Methods and Models for Codesign (MEMOCODE), Jul 2011, Cambridge, United Kingdom.

Accès au texte intégral et bibtex

Titre

Abstracting Time and Data for Conformance Testing of Real-Time Systems

Auteurs

Wilkerson L. Andrade; Patricia D. L. Machado; Thierry Jéron; Hervé Marchand

Détail

7th Workshop on Advances in Model Based Testing A-MOST 2011, Mar 2011, Berlin, Germany.

Accès au texte intégral et bibtex

Titre

Minimal Disclosure in Partially Observable Markov Decision Processes

Auteurs

Nathalie Bertrand; Blaise Genest

Détail

Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011), 2011, India. pp. 411-422

Accès au texte intégral et bibtex

Titre

Global State Estimates for Distributed Systems

Auteurs

Gabriel Kalyon; Tristan Le Gall; Hervé Marchand; Thierry Massart

Détail

31th IFIP International Conference on FORmal TEchniques for Networked and Distributed Systems., Jun 2011, Reykjavik, Iceland. Springer, 6722, pp. 198-212, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

Synthesis of Communicating Controllers for Distributed Systems

Auteurs

Gabriel Kalyon; Tristan Le Gall; Hervé Marchand; Thierry Massart

Détail

IEEE Conference on Decision and Control and European Control Conference, Dec 2011, Orlando, United States. IEEE, pp. 1803-1810

Accès au texte intégral et bibtex

Titre

Petri Net Reachability Graphs: Decidability Status of FO Properties

Auteurs

Philippe Darondeau; Stephane Demri; Roland Meyer; Christophe Morvan

Détail

Supratik Chakraborty and Amit Kumar. IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Dec 2011, Bombay, India. Dagstuhl Publishing, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Leibniz International Proceedings in Informatics (LIPICS)

Accès au bibtex

Titre

Test Case Generation Using PDA

Auteurs

Puneet Batheja

Détail

IEEE International Conference on Theoretical Aspects of Software Engineering, Aug 2011, Xi'an, China. IEEE

Accès au texte intégral et bibtex

Titre

A Tagging Protocol for Asynchronous Testing

Auteurs

Puneet Batheja

Détail

IEEE International Conference on Theoretical Aspects of Software Engineering, Aug 2011, Xi'an, China. IEEE

Accès au texte intégral et bibtex

Titre

Minimal Disclosure in Partially Observable Markov Decision Processes

Auteurs

Nathalie Bertrand; Blaise Genest

Détail

31st Annual Conference Foundations on Software Technology and Theoretical Computer Science (FSTTCS'11), Dec 2011, Mumbai, India.

Accès au bibtex

Titre

Intégration de la synthèse de contrôleurs discrets dans un langage de programmation

Auteurs

Gwenaël Delaval; Éric Rutten; Hervé Marchand

Détail

Modélisation des Systèmes Réactifs (MSR'11), Nov 2011, Lille, France.

Accès au texte intégral et bibtex

Titre

Emptiness and Universality Problems in Timed Automata with Positive Frequency.

Auteurs

Nathalie Bertrand; Patricia Bouyer; Thomas Brihaye; Amélie Stainer

Détail

38th International Colloquium on Automata, Languages and Programming (ICALP'11), Jul 2011, Zürich, Switzerland. Springer, 6756, pp. 246-257, LNCS

Accès au bibtex

Titre

Off-line Test Selection with Test Purposes for Non-Deterministic Timed Automata.

Auteurs

Nathalie Bertrand; Thierry Jéron; Amélie Stainer; Moez Krichen

Détail

17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'11), Mar 2011, Saarbrücken, Germany. Springer, 6605, pp. 96-111, LNCS

Accès au bibtex

Titre

A Game Approach to Determinize Timed Automata.

Auteurs

Nathalie Bertrand; Amélie Stainer; Thierry Jéron; Moez Krichen

Détail

14th International Conference on Foundations of Software Science and Computational Structures (FOSSACS'11), Mar 2011, Saarbrücken, Germany. Springer, 6604, pp. 245-259, LNCS

Accès au bibtex

Rapports

Titre

Off-line Test Selection with Test Purposes for Non-Deterministic Timed Automata

Auteurs

Nathalie Bertrand; Thierry Jéron; Amélie Stainer; Moez Krichen

Détail

[Research Report], 2011, pp. 20. RR-7501

Accès au texte intégral et bibtex

2010

Articles dans des revues avec comité de lecture

Titre

Supervisory Control for Opacity

Auteurs

Jérémy Dubreil; Philippe Darondeau; Hervé Marchand

Détail

IEEE Transactions on Automatic Control, IEEE, 2010, 55 (5), pp. 1089-1100

Accès au texte intégral et bibtex

Titre

Equational Approximations for Tree Automata Completion

Auteurs

Thomas Genet; Vlad Rusu

Détail

Journal of Symbolic Computation, Elsevier, 2010, 45(5):574-597, May 2010 (5), pp. 574-597

Accès au texte intégral et bibtex

Titre

Formal executable semantics for conformance in the MDE framework

Auteurs

Marina Egea; Vlad Rusu

Détail

Innovations in Software and Systems Engineering, Springer Verlag, 2010

Accès au texte intégral et bibtex

Communications avec actes

Titre

You Should Better Enforce than Verify

Auteurs

Yliès Falcone

Détail

International Conference on Runtime Verification, Nov 2010, Malta, Malta. pp. 91-108

Accès au texte intégral et bibtex

Titre

Automatic Test Generation for Data-Flow Reactive Systems with time constraints

Auteurs

Omer Landry Nguena Timo; Hervé Marchand; Antoine Rollet

Détail

22nd IFIP International Conference on Testing Software and Systems, Nov 2010, Natal, Brazil.

Accès au bibtex

Titre

Supervisory Control for Modal Specifications of Services

Auteurs

Philippe Darondeau; Jérémy Dubreil; Hervé Marchand

Détail

Workshop on Discrete Event Systems, WODES'10, Aug 2010, Berlin, Germany. pp. 428-435

Accès au texte intégral et bibtex

Titre

More Testable Properties

Auteurs

Yliès Falcone; Jean-Claude Fernandez; Thierry Jéron; Hervé Marchand; Laurent Mounier

Détail

22nd IFIP International Conference on Testing Software and Systems, Nov 2010, Natal, Brazil. Springer, 6435, pp. 30-46, Lectures notes in computer science

Accès au texte intégral et bibtex

Titre

Multicriteria optimal reconfiguration of fault-tolerant real-time tasks

Auteurs

Emil Dumitrescu; Alain Girault; Hervé Marchand; Éric Rutten

Détail

Workshop on Discrete Event Systems, WODES'10, Aug 2010, Berlin, Germany. IFAC, pp. 366-373

Accès au texte intégral et bibtex

Titre

Towards Automatic Integration Of Or-BAC Security Policies Using Aspects

Auteurs

Yliès Falcone; Mohamad Jaber

Détail

International Conference on Software Engineering Research and Practice (SERP 2010), Jul 2010, Las Vegas, Nevada, United States. pp. 5

Accès au texte intégral et bibtex

Titre

Contracts for modular discrete controller synthesis

Auteurs

Gwenaël Delaval; Hervé Marchand; Éric Rutten

Détail

Proceedings of the ACM SIGPLAN/SIGBED 2010 conference on Languages, compilers, and tools for embedded systems, Apr 2010, Stockholm, Sweden. pp. 57-66

Accès au texte intégral et bibtex

Titre

Operational Semantics of the Marte Repetitive Structure Modeling Concepts for Data-Parallel Applications Design

Auteurs

Abdoulaye Gamatié; Vlad Rusu; Éric Rutten

Détail

9th International Symposium on Parallel and Distributed Computing (ISPDC'2010), Jul 2010, Istanbul, Turkey.

Accès au texte intégral et bibtex

Titre

Probabilistic Regular Graphs

Auteurs

Nathalie Bertrand; Christophe Morvan

Détail

Yu-Fang Chen and Ahmed Rezine. Infinity (International Workshop on Verification of Infinite-State Systems), 2010, Singapour, Singapore. EPTCS, Proceedings 12th International Workshop on Verification of Infinite-State Systems (Infinity 2010), 39, pp. 77-90

Accès au texte intégral et bibtex

Titre

Contextual graph grammars characterising Rational Graphs

Auteurs

Christophe Morvan

Détail

Henning Bordihn and Rudolf Freund and Markus Holzer and Martin Kutrib and Friedrich Otto. Workshop on Non-Classical Models for Automata and Applications 2010, 2010, Jena, Germany. Österreichischen Computer Gesellschaft, Second Workshop on Non Classical Models for Automata and Applications 2010, pp. 141-153, book@ocg.at

Accès au texte intégral et bibtex

Titre

Combining theorem proving and narrowing for rewriting-logic specifications

Auteurs

Vlad Rusu

Détail

International Conference on Tests and Proofs, 2010, Malaga, Spain. Springer Verlag

Accès au texte intégral et bibtex

Autres publications

Titre

What can You Verify and Enforce at Runtime?

Auteurs

Yliès Falcone; Jean-Claude Fernandez; Laurent Mounier

Détail

Jan. 2010. Vérimag Technical Report TR-2010-5

Accès au texte intégral et bibtex

Rapports

Titre

A game approach to determinize timed automata

Auteurs

Nathalie Bertrand; Amélie Stainer; Thierry Jéron; Moez Krichen

Détail

[Research Report], 2010. RR-7381

Accès au texte intégral et bibtex

Titre

Various Notions of Opacity Verified and Enforced at Runtime

Auteurs

Yliès Falcone; Hervé Marchand

Détail

[Research Report], 2010. RR-7349

Accès au texte intégral et bibtex

Titre

More Testable Properties

Auteurs

Yliès Falcone; Jean-Claude Fernandez; Thierry Jéron; Hervé Marchand; Laurent Mounier

Détail

[Research Report], 2010, pp. 45. RR-7279

Accès au texte intégral et bibtex

Titre

Supervisory Control for Modal Specifications of Services

Auteurs

Philippe Darondeau; Jérémy Dubreil; Hervé Marchand

Détail

[Research Report], 2010. RR-7247

Accès au texte intégral et bibtex

Documents sans référence de publication

Titre

Automatic Test Generation for Data-Flow Reactive Systems Modeled by Variable Driven Timed Automata

Auteurs

Omer Landry Nguena Timo; Hervé Marchand; Antoine Rollet

Détail

May. 2010

Accès au texte intégral et bibtex

2009

Articles dans des revues avec comité de lecture

Titre

Automatic generation of safe handlers for multi-task systems

Auteurs

Éric Rutten; Hervé Marchand

Détail

Journal of Embedded Computing, IOS Press, 2009, 3 (4), pp. 255-276

Accès au texte intégral et bibtex

Titre

Vérification d'invariants pour des systèmes spécifiés en logique de réécriture

Auteurs

Vlad Rusu; Manuel Clavel

Détail

Studia Informatica Universalis, Hermann, 2009, JFLA 2009, Vingtiemes Journees Francophones des Langages Applicatifs, 7 (2)

Accès au texte intégral et bibtex

Communications avec actes

Titre

Computational Complexity for State-Feedback Controllers with Partial Observation

Auteurs

Gabriel Kalyon; Tristan Le Gall; Hervé Marchand; Thierry Massart

Détail

7th International Conference on Control and Automation, ICCA'09, Dec 2009, Christchurch, New Zealand. IEEE, pp. 435-441

Accès au texte intégral et bibtex

Titre

A Compositional Approach on Modal Specifications for Timed Systems.

Auteurs

Nathalie Bertrand; Axel Legay; Sophie Pinchinat; Jean-Baptiste Raclet

Détail

11th International Conference on Formal Engineering Methods (ICFEM'09), Dec 2009, Rio de Janeiro, Brazil. Springer, 5885, pp. 679-697, LNCS

Accès au bibtex

Titre

Automatic Testing of Access Control for Security Properties

Auteurs

Hervé Marchand; Jérémy Dubreil; Thierry Jéron

Détail

TESTCOM/FATES 2009, Nov 2009, Eindhoven, Netherlands. Springer-Verlag, 5826, pp. 113-128, Lecture notes in computer science

Accès au texte intégral et bibtex

Titre

Contrôle décentralisé de systèmes symboliques infinis sous observation partielle

Auteurs

Gabriel Kalyon; Tristan Le Gall; Hervé Marchand; Thierry Massart

Détail

7ème Colloque Francophone sur la Modélisation des Systèmes Réactifs, Nov 2009, Nantes, France. Hermès, pp. 805-820

Accès au bibtex

Titre

The Effect of Tossing Coins in Omega-Automata

Auteurs

Christel Baier; Nathalie Bertrand; Marcus Größer

Détail

20th International Conference Concurrency Theory (CONCUR 2009), Sep 2009, Bologne, Italy. 5710, pp. 15-29, LNCS

Accès au bibtex

Titre

Qualitative Determinacy and Decidability of Stochastic Games with Signals

Auteurs

Nathalie Bertrand; Blaise Genest; Hugo Gimbert

Détail

LICS'09, IEEE Symposium on logic in computer science, Aug 2009, Los Angeles, United States. pp. 0

Accès au texte intégral et bibtex

Titre

Monitoring Confidentiality by Diagnosis Techniques

Auteurs

Jérémy Dubreil; Thierry Jéron; Hervé Marchand

Détail

European Control Conference, Aug 2009, Budapest, Hungary. pp. 2584-2589

Accès au texte intégral et bibtex

Titre

Control of Infinite Symbolic Transition Systems under Partial Observation

Auteurs

Gabriel Kalyon; Tristan Le Gall; Hervé Marchand; Thierry Massart

Détail

European Control Conference, Aug 2009, Budapest, Hungary. pp. 1456-1462

Accès au texte intégral et bibtex

Titre

When are timed automata determinizable?

Auteurs

Christel Baier; Nathalie Bertrand; Patricia Bouyer; Thomas Brihaye

Détail

36th International Colloquium on Automata, Languages and Programming (ICALP'09), Jul 2009, Rhodes, Greece. Springer, 5556, pp. 43-54, LNCS

Accès au bibtex

Titre

Génération automatique de tests pour des propriétés de sécurité

Auteurs

Hervé Marchand; Jérémy Dubreil; Thierry Jéron

Détail

4ème Conférence sur la Sécurité des Architectures Réseaux et des Systèmes d'Information, Jun 2009, Luchon, France. pp. 157-174

Accès au texte intégral et bibtex

Titre

Opacity and Abstraction

Auteurs

Jérémy Dubreil

Détail

Proceedings of the First International Workshop on Abstractions for Petri Nets and Other Models of Concurrency (APNOC'09), Jun 2009, Paris, France.

Accès au bibtex

Titre

Refinement and Consistency of Timed Modal Specifications.

Auteurs

Nathalie Bertrand; Sophie Pinchinat; Jean-Baptiste Raclet

Détail

3rd International Conference on Language and Automata Theory and Applications (LATA'09), Apr 2009, Tarragona, Spain. Springer, 5457, pp. 152-163, LNCS

Accès au bibtex

Titre

Probabilistic Acceptors for Languages over Infinite Words.

Auteurs

Christel Baier; Nathalie Bertrand; Marcus Größer

Détail

35th Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM'09), Jan 2009, Spindleruv Mlyn, Czech Republic. 5404, pp. 19-33, LNCS

Accès au bibtex

Titre

Dynamic Observers for the Synthesis of Opaque Systems

Auteurs

Franck Cassez; Jérémy Dubreil; Hervé Marchand

Détail

7th International Symposium on Automated Technology for Verification and Analysis (ATVA'09), Oct 2009, Macao SAR, China. Springer-Verlag, 5799, pp. 352-367, Lecture notes in computer science

Accès au texte intégral et bibtex

Titre

On external presentations of infinite graphs

Auteurs

Christophe Morvan

Détail

Axel Legay and Azadeh Farzan. Infinity (International Workshop on Verification of Infinite-State Systems), 2009, Bologne, Italy. EPTCS, 10, pp. 23-35

Accès au texte intégral et bibtex

Titre

Diagnosability of pushdown systems

Auteurs

Christophe Morvan; Sophie Pinchinat

Détail

Kedar Namjoshi and Andreas Zeller. Haifa Verification Conference, 2009, Haifa, Israel. Springer, LNCS

Accès au texte intégral et bibtex

Rapports

Titre

Supervisory Control for Opacity

Auteurs

Jérémy Dubreil; Philippe Darondeau; Hervé Marchand

Détail

[Research Report], 2009, 19 p.. PI 1921

Accès au texte intégral et bibtex

Titre

Contextual graph grammars characterizing context-sensitive languages

Auteurs

Christophe Morvan

Détail

[Research Report], 2009, pp. 19. PI 1926

Accès au texte intégral et bibtex

Titre

Dynamic Observers for the Synthesis of Opaque Systems

Auteurs

Franck Cassez; Jérémy Dubreil; Hervé Marchand

Détail

[Research Report], 2009, pp. 22. PI 1930

Accès au texte intégral et bibtex

Titre

A Compositional Approach on Modal Specifications for Timed Systems

Auteurs

Nathalie Bertrand; Axel Legay; Sophie Pinchinat; Jean-Baptiste Raclet

Détail

[Research Report], 2009. RR-7039

Accès au texte intégral et bibtex

Titre

BZR Contracts for Modular Discrete Controller Synthesis

Auteurs

Gwenaël Delaval; Hervé Marchand; Éric Rutten

Détail

[Research Report], 2009. RR-7111

Accès au texte intégral et bibtex

Thèses

Titre

Vérification et Synthèse de Contrôleur pour des Propriétés de Confidentialité

Auteurs

Jérémy Dubreil

Détail

informatique. Université Rennes 1, Nov. 2009. English

Accès au texte intégral et bibtex

Documents sans référence de publication

Titre

Equational Approximations for Tree Automata Completion

Auteurs

Thomas Genet; Vlad Rusu

Détail

Mar. 2009. 33 pages

Accès au texte intégral et bibtex

2008

Articles dans des revues avec comité de lecture

Titre

Structural Presburger digit vector automata

Auteurs

Jérôme Leroux

Détail

Theoretical Computer Science, 2008, 409 (3), pp. 549-556

Accès au texte intégral et bibtex

Titre

Supervisory Control of Modular Systems with Global Specification Languages

Auteurs

Jan Komenda; Jan Van Schuppen; Benoit Gaudin; Hervé Marchand

Détail

Automatica, Elsevier, 2008, 44, pp. 1127-1134

Accès au bibtex

Communications avec actes

Titre

Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics.

Auteurs

Nathalie Bertrand; Patricia Bouyer; Thomas Brihaye; Nicolas Markey

Détail

5th International Conference on the Quantitative Evaluation of Systems (QEST'08), Sep 2008, Saint Malo, France. IEEE, pp. 55-64

Accès au bibtex

Titre

Predictability of Sequence Patterns in Discrete Event Systems

Auteurs

Thierry Jéron; Hervé Marchand; Sahika Genc; Stéphane Lafortune

Détail

IFAC World Congress, Aug 2008, Seoul, Korea, Republic Of. pp. 537-543

Accès au texte intégral et bibtex

Titre

Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata.

Auteurs

Christel Baier; Nathalie Bertrand; Patricia Bouyer; Thomas Brihaye; Marcus Größer

Détail

23rd Annual IEEE Symposium on Logic in Computer Science (LICS'08), Jun 2008, Pittsburgh, United States. IEEE, pp. 217-226

Accès au bibtex

Titre

On Decision Problems for Probabilistic Büchi Automata.

Auteurs

Christel Baier; Nathalie Bertrand; Marcus Größer

Détail

11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'08), Apr 2008, Budapest, Hungary. Springer, 4962, pp. 287-301, LNCS

Accès au bibtex

Titre

Opacity Enforcing Control Synthesis

Auteurs

Jérémy Dubreil; Philippe Darondeau; Hervé Marchand

Détail

Workshop on Discrete Event Systems, WODES'08, May 2008, Goteborg, Sweden. IEEE, pp. 28-35

Accès au texte intégral et bibtex

Chapitres d'ouvrages scientifiques

Titre

Validation of Reactive Systems

Auteurs

Camille Constant; Thierry Jéron; Hervé Marchand; Vlad Rusu

Détail

S, Merz and N, Navet. Modeling and Verification of Real-TIME Systems - Formalisms and software Tools, Hermès Science, pp. 51-76, Jan. 2008

Accès au bibtex

Rapports

Titre

Opacity Enforcing Control Synthesis

Auteurs

Jérémy Dubreil; Philippe Darondeau; Hervé Marchand

Détail

[Research Report], 2008, pp. 19. PI 1887

Accès au texte intégral et bibtex

Titre

Monitoring Information flow by Diagnosis Techniques

Auteurs

Jérémy Dubreil; Thierry Jéron; Hervé Marchand

Détail

[Research Report], 2008, pp. 15. PI 1901

Accès au texte intégral et bibtex

Titre

Diagnosis of Pushdown Systems

Auteurs

Christophe Morvan; Sophie Pinchinat

Détail

[Research Report], 2008, pp. 19. PI 1904

Accès au texte intégral et bibtex

Thèses

Titre

Génération automatique de tests pour des modèles avec variables ou récursivité.

Auteurs

Camille Constant

Détail

informatique. Université Rennes 1, Nov. 2008. French

Accès au texte intégral et bibtex

Titre

Abstract lattices for the verification of systèmes with stacks and queues

Auteurs

Tristan Le Gall

Détail

informatique. Université Rennes 1, Jul. 2008. English

Accès au texte intégral et bibtex

Documents sans référence de publication

Titre

Determinacy and Decidability of Reachability Games with Partial Observation on Both Sides

Auteurs

Nathalie Bertrand; Blaise Genest; Hugo Gimbert

Détail

Nov. 2008

Accès au texte intégral et bibtex

2007

Articles dans des revues avec comité de lecture

Titre

Integrating Formal Verification and Conformance Testing for Reactive Systems

Auteurs

Camille Constant; Thierry Jéron; Hervé Marchand; Vlad Rusu

Détail

IEEE Transactions on Software Engineering, IEEE Computer Society, 2007, 33 (8), pp. 558-574

Accès au texte intégral et bibtex

Titre

An Efficient Modular Method for the Control of Concurrent Discrete Event Systems: A Language-Based Approach

Auteurs

Benoit Gaudin; Hervé Marchand

Détail

Discrete Event Dynamic Systems, Springer-Verlag, 2007, 17 (2), pp. 179-209

Accès au texte intégral et bibtex

Titre

Test Synthesis from UML Models of Distributed Software

Auteurs

Simon Pickin; Claude Jard; Thierry Jéron; Jean-Marc Jézéquel; Yves Le Traon

Détail

IEEE Transactions on Software Engineering, IEEE, 2007, 33 (4), pp. 252-268

Accès au texte intégral et bibtex

Communications avec actes

Titre

Construction de moniteurs pour la surveillance de propriétés de sécurité

Auteurs

Jérémy Dubreil; Thierry Jéron; Hervé Marchand

Détail

6ème Colloque Francophone sur la Modélisation des Systèmes Réactifs, Oct 2007, Lyon, France. pp. 105-120

Accès au texte intégral et bibtex

Titre

Synthèse optimale de contrôleurs discrets et systèmes répartis tolérants aux fautes

Auteurs

Emil Dumitrescu; Alain Girault; Hervé Marchand; Éric Rutten

Détail

6ème Colloque Francophone sur la Modélisation des Systèmes Réactifs, Oct 2007, Lyon, France. pp. 71-86

Accès au texte intégral et bibtex

Titre

Optimal discrete controller synthesis for modeling fault-tolerant distributed systems

Auteurs

Emil Dumitrescu; Éric Rutten; Alain Girault; Hervé Marchand

Détail

DCDS, Jun 2007, Cachan, France. pp. xxx

Accès au bibtex

Titre

Integrating verification, testing, and learning for cryptographic protocols

Auteurs

Martin Oostidijk; Vlad Rusu; Jan Tretmans; Rene De Vries; Tim Willemse

Détail

Integrated Formal Methods, 2007, Oxford, United Kingdom.

Accès au texte intégral et bibtex

Rapports

Titre

Optimal discrete controller synthesis for the modeling of fault-tolerant distributed systems

Auteurs

Emil Dumitrescu; Alain Girault; Hervé Marchand; Éric Rutten

Détail

[Research Report], 2007, pp. 35. RR-6137

Accès au texte intégral et bibtex

Titre

Predictability of Sequence Patterns in Discrete Event Systems

Auteurs

Thierry Jéron; Hervé Marchand; Sahika Genc; Stéphane Lafortune

Détail

[Research Report], 2007, pp. 17. PI 1834

Accès au texte intégral et bibtex

Titre

Automatic Test Generation from Interprocedural Specifications

Auteurs

Bertrand Jeannet; Thierry Jéron; Camille Constant

Détail

[Research Report], 2007, pp. 19. PI 1835

Accès au texte intégral et bibtex

Titre

Analysis of Communicating Infinite State Machines using Lattice Automata

Auteurs

Tristan Le Gall; Bertrand Jeannet

Détail

[Research Report], 2007, pp. 36

Accès au bibtex

Titre

Analysis of Communicating Infinite State Machines using Lattice Automata

Auteurs

Tristan Le Gall; Bertrand Jeannet

Détail

[Research Report], 2007, pp. 36. PI 1839

Accès au texte intégral et bibtex

Titre

Theorem Proving for Maude's Rewriting Logic

Auteurs

Vlad Rusu; Manuel Clavel

Détail

[Research Report], 2007, pp. 47. PI 1873

Accès au texte intégral et bibtex

2006

Articles dans des revues avec comité de lecture

Titre

Verifying an ATM Protocol Using a Combination of Formal Techniques

Auteurs

Rusu Vlad

Détail

The Computer Journal, Oxford University Press, 2006, 49 (6), pp. 710-730

Accès au bibtex

Titre

Contrôle de systèmes symboliques, discrets ou hybrides

Auteurs

Tristan Le Gall; Bertrand Jeannet; Hervé Marchand

Détail

Revue Technique et Science Informatiques (TSI), Lavoisier, 2006, 35 (3), pp. 293-319

Accès au bibtex

Communications avec actes

Titre

A constructive and modular approach to decentralized supervisory Control problems

Auteurs

Jan Komenda; Hervé Marchand; Sophie Pinchinat

Détail

3rd IFAC Workshop on Discrete-Event System Design, Sep 2006, Rydzyna, Poland.

Accès au texte intégral et bibtex

Titre

Symbolic Determinisation of Extended Automata

Auteurs

Thierry Jéron; Hervé Marchand; Vlad Rusu

Détail

4th IFIP International Conference on Theoretical Computer Science, Aug 2006, Stantiago, Chile, Chile. Springer Science and Business Media, 209/2006, pp. 197-212, IFIP International Federation for Information Processing

Accès au texte intégral et bibtex

Titre

Supervision Patterns in Discrete Event Systems Diagnosis

Auteurs

Thierry Jéron; Hervé Marchand; Sophie Pinchinat; Marie-Odile Cordier

Détail

Workshop on Discrete Event Systems, WODES'06, Jul 2006, Ann-Arbor, United States. IEEE Computer society, pp. 262-268

Accès au texte intégral et bibtex

Titre

Modular and Decentralized Supervisory Control of Concurrent Discrete Event Systems Using Reduced System Models.

Auteurs

Klaus Schmidt; Hervé Marchand; Benoit Gaudin

Détail

Workshop on Discrete Event Systems, WODES'06, Jul 2006, Ann-Arbor, United States. IEEE Computer society, pp. 149-154

Accès au texte intégral et bibtex

Titre

On Rational Trees

Auteurs

Arnaud Carayol; Christophe Morvan

Détail

Ésik Zoltán. 20th International Workshop on Computer Science Logic (CSL'06), Sep 2006, Szeged, Hungary. Springer-Verlag, 4207, pp. 225-239, LNCS

Accès au texte intégral et bibtex

Titre

Motifs de surveillance pour le diagnostic de systèmes à événements discrets

Auteurs

Thierry Jéron; Hervé Marchand; Marie-Odile Cordier

Détail

RFIA 2006 (Congrès Reconnaissance des formes et Intelligence Artificielle), 2006, Tours, France.

Accès au bibtex

Titre

Supervision patterns in discrete event systems

Auteurs

Thierry Jéron; Hervé Marchand; Sophie Pinchinat; Marie-Odile Cordier

Détail

DX'06 (17th International Workshop on Principal of Diagnosis), 2006, Burgos, Spain. pp. 117-124

Accès au bibtex

Titre

A Constructive and Modular Approach to Decentralized Supervisory Control Problems

Auteurs

Jan Komenda; Hervé Marchand; Sophie Pinchinat

Détail

3rd IFAC Workshop on Discrete-Event System Design, DESDes'06, Sep 2006, Rydzyna Castle, Poland.

Accès au bibtex

Titre

Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant

Auteurs

Gilles Barthe; Julien Forest; David Pichardie; Vlad Rusu

Détail

Functional and Logic Programming (FLOPS'06), 2006, Fuji Susono, Japan.

Accès au texte intégral et bibtex

Titre

Model-Based Test Selection for Infinite-State Reactive Systems

Auteurs

Bertrand Jeannet; Thierry Jéron; Vlad Rusu

Détail

Formal Methods for Components and Objects, 2006, Amsterdam, Netherlands.

Accès au texte intégral et bibtex

Chapitres d'ouvrages scientifiques

Titre

Combinaison entre vérification et test pour la validation de systèmes réactifs

Auteurs

Camille Constant; Thierry Jéron; Hervé Marchand; Vlad Rusu

Détail

Nicolas Navet. Traité I2C. Systèmes Temps Réel: Techniques de Description et de Vérification - Théorie et Outils, 1, Hermès Science, pp. 59-88, 2006, Informatique et Systèmes d'information

Accès au bibtex

Rapports

Titre

Symbolic Determinisation of Extended Automata

Auteurs

Thierry Jéron; Hervé Marchand; Vlad Rusu

Détail

[Research Report], 2006. PI 1776

Accès au texte intégral et bibtex

Titre

Supervision Patterns in Discrete Event Systems Diagnosis

Auteurs

Thierry Jéron; Hervé Marchand; Sophie Pinchinat; Marie-Odile Cordier

Détail

[Research Report], 2006, pp. 16. PI 1784

Accès au texte intégral et bibtex

2005

Communications avec actes

Titre

Supervisory Control and Deadlock Avoidance Control Problem for Concurrent Discrete Event Systems

Auteurs

Benoit Gaudin; Hervé Marchand

Détail

44nd IEEE Conference on Decision and Control (CDC'05) and Control and European Control Conference ECC 2005, Dec 2005, Seville, Spain. IEEE, pp. 2763-2768

Accès au texte intégral et bibtex

Titre

Modular supervisory control with general indecomposable specification languages

Auteurs

Jan Komenda; Jan Van Schuppen; Benoit Gaudin; Hervé Marchand

Détail

44nd IEEE Conference on Decision and Control (CDC'05) and Control and European Control Conference ECC 2005, Dec 2005, Seville, Spain. IEEE, pp. 3474-3479

Accès au texte intégral et bibtex

Titre

Supervisory Control of Infinite Symbolic Systems using Abstract Interpretation

Auteurs

Tristan Le Gall; Bertrand Jeannet; Hervé Marchand

Détail

44nd IEEE Conference on Decision and Control (CDC'05) and Control and European Control Conference ECC 2005, Dec 2005, Seville, Spain. pp. 31-35

Accès au texte intégral et bibtex

Titre

Safety Control of Hierarchical Synchronous Discrete Event Systems: A State-Based Approach

Auteurs

Benoit Gaudin; Hervé Marchand

Détail

13th Mediterranean Conference on Control and Automation, Dec 2005, Limassol, Cyprus. IEEE, pp. 889-895

Accès au texte intégral et bibtex

Titre

Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems

Auteurs

Vlad Rusu; Hervé Marchand; Thierry Jéron

Détail

John Fitzgerald, Andrzej Tarlecki, Ian Hayes. Formal Methods 2005 (FM05), Jul 2005, Newcastle, United Kingdom. Springer-Verlag, 3582, pp. 189-204, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

Une approche modulaire pour le contrôle de systèmes à événements discrets concurrents

Auteurs

Benoit Gaudin; Hervé Marchand

Détail

5ième Colloque Francophone sur la Modélisation des Systèmes Réactifs, Oct 2005, Autran, France. Hermès, Modélisation des Systèmes Réactifs, 39, pp. 79-94, Journal Européen des Systèmes Automatisés

Accès au texte intégral et bibtex

Titre

Symbolic Test Selection Based on Approximate Analysis

Auteurs

Bertrand Jeannet; Thierry Jéron; Vlad Rusu; Elena Zinovieva

Détail

TACAS, 2005, Edinburgh, United Kingdom.

Accès au texte intégral et bibtex

Titre

Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems

Auteurs

Vlad Rusu; Hervé Marchand; Thierry Jéron

Détail

Formal Methods, 2005, Newcastle, United Kingdom.

Accès au texte intégral et bibtex

Rapports

Titre

Structural Presburger-definable Digit Vector Automata

Auteurs

Jérôme Leroux

Détail

[Research Report], 2005. PI 1718

Accès au texte intégral et bibtex

Titre

Defining and Reasoning About General Recursive Functions in Type Theory: a Practical Method

Auteurs

David Pichardie; Vlad Rusu

Détail

[Research Report], 2005, pp. 16. PI 1766

Accès au texte intégral et bibtex

Titre

Abstract Interpretation of FIFO channels

Auteurs

Bertrand Jeannet; Thierry Jéron; Tristan Le Gall

Détail

[Research Report], 2005, pp. 25. PI 1767

Accès au texte intégral et bibtex

Titre

Abstract Interpretation of FIFO channels

Auteurs

Bertrand Jeannet; Thierry Jéron; Tristan Le Gall

Détail

[Research Report], 2005, pp. 25. RR-5784

Accès au texte intégral et bibtex

Titre

Contrôle de systèmes symboliques, discrets ou hybrides

Auteurs

Tristan Le Gall; Bertrand Jeannet; Hervé Marchand

Détail

[Research Report], 2005, pp. 30. RR-5474

Accès au texte intégral et bibtex

2004

Articles dans des revues avec comité de lecture

Titre

Supervisory Control of Product and Hierarchical Discrete Event Systems

Auteurs

Benoit Gaudin; Hervé Marchand

Détail

European Journal of Control, hermes, 2004, 10 (2), pp. 131-145

Accès au texte intégral et bibtex

Titre

Ensuring the conformance of reactive discrete-event systems by means of supervisory control

Auteurs

Thierry Jéron; Hervé Marchand; Vlad Rusu; Valérie Tschaen

Détail

International Journal of Production Research, Taylor & Francis, 2004, 42 (14), pp. 2809 – 2826

Accès au texte intégral et bibtex

Titre

Ensuring the conformance of reactive discrete-event systems by means of supervisory control

Auteurs

Thierry Jéron; Hervé Marchand; Vlad Rusu; Valéry Tschaen

Détail

International Journal of Production Research, Taylor & Francis, 2004, 42 (14), pp. 2809-2826

Accès au texte intégral et bibtex

Communications avec actes

Titre

Modular Supervisory Control of a class of Concurrent Discrete Event Systems

Auteurs

Benoit Gaudin; Hervé Marchand

Détail

Workshop on Discrete Event Systems, Sep 2004, Reims, France. IFAC, pp. 181-186

Accès au texte intégral et bibtex

Titre

From Safety Verification to Safety Testing

Auteurs

Vlad Rusu; Hervé Marchand; Valérie Tschaen; Thierry Jéron; Bertrand Jeannet

Détail

R. Groz and R.M. Hierons. Testing of Communicating Systems (Testcom), Mar 2004, Oxford, United Kingdom. Springer, 2978, pp. 160-176, Lecture notes in computer science

Accès au texte intégral et bibtex

Rapports

Titre

Verification and Symbolic Test Generation for Safety Properties

Auteurs

Vlad Rusu; Hervé Marchand; Thierry Jéron

Détail

[Research Report], 2004, pp. 20. RR-5285

Accès au texte intégral et bibtex

Titre

Automatic Generation of Safe Handlers for Multi-Task Systems

Auteurs

Éric Rutten; Hervé Marchand

Détail

[Research Report], 2004. RR-5345

Accès au texte intégral et bibtex

Thèses

Titre

Méthodes symboliques pour la génération de tests de
systèmes réactifs comportant des données.

Auteurs

Elena Leroux (zinovieva)

Détail

informatique. Université Rennes 1, Nov. 2004. English

Accès au texte intégral et bibtex

2003

Communications avec actes

Titre

Ensuring the conformance of reactive discrete-event systems using supervisory control

Auteurs

Thierry Jéron; Hervé Marchand; Vlad Rusu; Valérie Tschaen

Détail

42nd IEEE Conference on Decision and Control, Dec 2003, Hawaii, United States. IEEE, pp. 2692 - 2697

Accès au bibtex

Titre

Synthèse de contrôleurs pour une relation de conformité

Auteurs

Thierry Jéron; Hervé Marchand; Vlad Rusu; Valérie Tschaen

Détail

4ième Colloque Francophone sur la Modélisation des Systèmes Réactifs, Oct 2003, Metz, France. Lavoisier, Modélisation des systèmes réactifs, pp. 523-536

Accès au texte intégral et bibtex

Titre

Contrôle de systèmes à événements discrets hiérarchiques

Auteurs

Benoit Gaudin; Hervé Marchand

Détail

4ième Colloque Francophone sur la Modélisation des Systèmes Réactifs, Oct 2003, Metz, France. Lavoisier, Modélisation des Systèmes Réactifs, pp. 383-397

Accès au texte intégral et bibtex

Titre

Supervisory Control of Asynchronous and Hierarchical Finite State Machines

Auteurs

Benoit Gaudin; Hervé Marchand

Détail

European Control Conference, Sep 2003, Cambridge, United Kingdom.

Accès au texte intégral et bibtex

Communications sans actes

Titre

Automatic State Reaching for Debugging Reactive Programs

Auteurs

Fabien Gaucher; Erwan Jahier; Florence Maraninchi; Bertrand Jeannet

Détail

the Fifth International Workshop on Automated Debugging (AADEBUG 2003), Sep 2003, Ghent, France.

Accès au texte intégral et bibtex

Rapports

Titre

Verifying an ATM Protocol Using a Combination of Formal Techniques

Auteurs

Vlad Rusu

Détail

[Research Report], 2003. RR-5089

Accès au texte intégral et bibtex

Titre

Abstracting Call-Stacks for Interprocedural Verification of Imperative Programs

Auteurs

Bertrand Jeannet; Wendelin Serwe

Détail

[Research Report], 2003. RR-4904

Accès au texte intégral et bibtex

2002

Articles dans des revues avec comité de lecture

Titre

On Optimal Control of a Class of Partially-Observed Discrete Event Systems

Auteurs

Hervé Marchand; Olivier Boivineau; Stéphane Lafortune

Détail

Automatica, Elsevier, 2002, 36 (2)

Accès au texte intégral et bibtex

Communications avec actes

Titre

Supervisory Control Problems of Hierarchical Finite State Machines

Auteurs

Hervé Marchand; Benoit Gaudin

Détail

41th IEEE Conference on Decision and Control, Dec 2002, Las-Vegas, United States. IEEE, pp. 1199-1204

Accès au texte intégral et bibtex

Titre

Managing multi-mode tasks with time cost and quality levels using optimal discrete control synthesis

Auteurs

Hervé Marchand; Éric Rutten

Détail

14th Euromicro Conference on Real-Time Systems (ECRTS'02), Jun 2002, Vienna, Austria. IEEE, pp. 241-248

Accès au texte intégral et bibtex

Titre

A case study in applying discrete control synthesis to excavator operation

Auteurs

Hervé Marchand; Éric Rutten

Détail

IEEE International Conference on Systems, Man and Cybernetics (IEEE SMC), Oct 2002, Hammamet, Tunisia.

Accès au texte intégral et bibtex

Titre

Diagnostic de pannes sur des systèmes à événements discrets : une approche à base de modèles symboliques

Auteurs

Hervé Marchand; Laurence Rozé

Détail

13ème Congrès Francophone AFRIF-AFIA de Reconnaissance des Formes et Intelligence Artificielle, Jan 2002, Angers, France. pp. 191-200

Accès au bibtex

Titre

A Protocol for Loosely Time-Triggered Architectures

Auteurs

Albert Benveniste; Paul Caspi; Paul Le Guernic; Hervé Marchand; Jean-Pierre Talpin; Stavros Tripakis

Détail

Embedded Software Conference (EMSOFT '02), Oct 2002, Grenoble, France. Springer, 2491, pp. 252-265, Lecture notes in computer science

Accès au bibtex

Rapports

Titre

Task-level programming for control systems using discrete control synthesis

Auteurs

Éric Rutten; Hervé Marchand

Détail

[Research Report], 2002. RR-4389

Accès au texte intégral et bibtex

2000

Rapports

Titre

On Rational Graphs

Auteurs

Christophe Morvan

Détail

[Research Report], 2000. RR-3944

Accès au texte intégral et bibtex