Bibliography

Articles in International Peer-Reviewed Journals

• 1C. Canal, J. Cámara, G. Salaün.
  
  Structural Reconfiguration of Systems under Behavioral Adaptation, in: Science of Computer Programming, September 2012, vol. 78, n^o 1, p. 46-64.
  
  http://hal.inria.fr/hal-00734057
• 2J. Cámara, G. Salaün, C. Canal, M. Ouederni.
  
  Interactive specification and verification of behavioral adaptation contracts, in: Information and Software Technology, July 2012, vol. 54, n^o 7, p. 701-723.
  
  http://hal.inria.fr/hal-00694516
• 3F. Durán, M. Ouederni, G. Salaün.
  
  A generic framework for n-protocol compatibility checking, in: Science of Computer Programming, July 2012, vol. 77, n^o 7-8, p. 870-886.
  
  http://hal.inria.fr/hal-00694561
• 4H. Garavel, F. Lang, R. Mateescu, W. Serwe.
  
  CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes, in: International Journal on Software Tools for Technology Transfer, 2012. [ DOI : 10.1007/s10009-012-0244-z ]
  
  http://hal.inria.fr/hal-00715056
• 5E. Lantreibecq, W. Serwe.
  
  Formal Analysis of a Hardware Dynamic Task Dispatcher with CADP, in: Science of Computer Programming, 2013, to appear.
• 6R. Mateescu, P. Poizat, G. Salaün.
  
  Adaptation of Service Protocols using Process Algebra and On-the-Fly Reduction Techniques, in: IEEE Transactions on Software Engineering, 2012. [ DOI : 10.1109/TSE.2011.62 ]
  
  http://hal.inria.fr/hal-00717252
• 7R. Mateescu, W. Serwe.
  
  Model Checking and Performance Evaluation with CADP Illustrated on Shared-Memory Mutual Exclusion Protocols, in: Science of Computer Programming, February 2012. [ DOI : 10.1016/j.scico.2012.01.003 ]
  
  http://hal.inria.fr/hal-00671321
• 8R. Mateescu, A. Wijs.
  
  Sequential and distributed on-the-fly computation of weak tau-confluence, in: Science of Computer Programming, 2012, vol. 77, n^o 10-11, p. 1075-1094. [ DOI : 10.1016/j.scico.2011.07.004 ]
  
  http://hal.inria.fr/hal-00676451
• 9K. H. Rose, R. Bloo, F. Lang.
  
  On Explicit Substitution with Names, in: Journal of Automated Reasoning, August 2012, vol. 49, n^o 2, p. 275-300. [ DOI : 10.1007/s10817-011-9222-5 ]
  
  http://hal.inria.fr/hal-00763399
• 10G. Salaün, T. Bultan, N. Roohi.
  
  Realizability of Choreographies using Process Algebra Encodings, in: IEEE Transactions on Services Computing, August 2012, vol. 5, n^o 3, p. 290-304.
  
  http://hal.inria.fr/hal-00726448

International Conferences with Proceedings

• 11S. Alatartsev, M. Güdemann, F. Ortmeier.
  
  Trajectory Description Conception for Industrial Robots, in: Proceedings of the 7th German Conference on Robotics (ROBOTIK 2012), Munich, Germany, VDE Verlag, May 2012, p. 365-370.
  
  http://hal.inria.fr/hal-00727303
• 12H. Garavel, R. Mateescu, W. Serwe.
  
  Large-Scale Distributed Verification using CADP: Beyond Clusters to Grids, in: 11th International Workshop on Parallel and Distributed Methods in verifiCation, London, United Kingdom, September 2012.
  
  http://hal.inria.fr/hal-00730668
• 13M. Güdemann, M. Lipaczewski, S. Struck, F. Ortmeier.
  
  Unifying Probabilistic and Traditional Formal Model Based Analysis, in: 8. Dagstuhl-Workshop MBEES 2012 - Model-Based Development of Embedded Systems, Dagstuhl, Germany, February 2012.
  
  http://hal.inria.fr/hal-00665607
• 14M. Güdemann, G. Salaün, M. Ouederni.
  
  Counterexample Guided Synthesis of Monitors for Realizability Enforcement, in: Automated Technology for Verification and Analysis - 10th International Symposium, ATVA 2012, India, LNCS, Springer, October 2012, vol. 7561, p. 238-253. [ DOI : 10.1007/978-3-642-33386-6_20 ]
  
  http://hal.inria.fr/hal-00742159
• 15F. Lang, R. Mateescu.
  
  Partial Model Checking using Networks of Labelled Transition Systems and Boolean Equation Systems, in: Tools and Algorithms for the Construction and Analysis of Systems TACAS'2012, Tallinn, Estonia, C. Flanagan, B. König (editors), LNCS, Springer, March 2012, vol. 7214, p. 141-156.
  
  http://hal.inria.fr/hal-00684471
• 16R. Mateescu, G. Salaün.
  
  PIC2LNT: Model Transformation for Model Checking an Applied Pi-Calculus, in: Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2013 (Rome, Italy), N. Piterman, S. Smolka (editors), LNCS, Springer, March 2013, to appear.
• 17P. Poizat, G. Salaün.
  
  Checking the Realizability of BPMN 2.0 Choreographies, in: 27th Symposium On Applied Computing (SAC 2012), Italy, March 2012, p. 1927-1934.
  
  http://hal.inria.fr/hal-00685393
• 18G. Salaün, X. Etchevers, N. De Palma, F. Boyer, T. Coupaye.
  
  Verification of a Self-configuration Protocol for Distributed Applications in the Cloud, in: 27th Symposium On Applied Computing (SAC 2012), Italy, March 2012, p. 1278-1283.
  
  http://hal.inria.fr/hal-00685394
• 19S. Struck, M. Lipaczewski, F. Ortmeier, M. Güdemann.
  
  Multi-Objective Optimization of Formal Specifications, in: Proceedings of the 14th High Assurance System Engineering Symposium (HASE 2012), Omaha, United States, IEEE, October 2012, p. 201-208. [ DOI : 10.1109/HASE.2012.21 ]
  
  http://hal.inria.fr/hal-00735640

Scientific Popularization

• 20H. Garavel, I. Bellin.
  
  La fiabilité des systèmes devient un défi majeur, November 2012, Article series for the 20th anniversary of the Inria research center in Montbonnot.
  
  http://www.inria.fr/centre/grenoble/actualites/la-fiabilite-des-systemes-devient-un-defi-majeur
• 21R. Mateescu.
  
  17th International Workshop on Formal Methods for Industrial Critical Systems, in: ERCIM News, October 2012, vol. 91.
  
  http://ercim-news.ercim.eu/en91/jea/17th-international-workshop-on-formal-methods-for-industrial-critical-systems

Other Publications

• 22A. Dumont.
  
  A LOTOS NT Library for Modeling, Analysis, and Validation of Distributed Systems, Ecole Nationale Supérieure d'Informatiques et Mathématiques Appliquées de Grenoble ENSIMAG, 2012.
• 23H. Garavel, F. Lang, R. Mateescu, G. Salaün, W. Serwe.
  
  CADP : une boîte à outils pour la conception et l'analyse de systèmes distribués, January 2012, This tutorial was presented at 11èmes Journées Francophones sur les Approches Formelles dans l'Assistance au Développement de Logiciels AFADL'2012 (Grenoble, France), January 11-13, 2012..
  
  http://hal.inria.fr/hal-00667288
• 24H. Garavel, F. Lang, R. Mateescu, W. Serwe.
  
  CADP Tutorial, 2012, This tutorial was presented at the 18th International Symposium on Formal Methods FM'2012 (Paris, France), August 27-31, 2012..
  
  http://hal.inria.fr/hal-00764932

• 25AMBA AXI and ACE Protocol Specification, ARM IHI 0022D (ID102711), ARM, October 22 2011.
• 26F. Aarts, F. Heidarian, H. Kuppens, P. Olsen, F. W. Vaandrager.
  
  Automata Learning through Counterexample Guided Abstraction Refinement, in: Proceedings of the 18th International Symposium on Formal Methods FM'2012 (Paris, France), D. Giannakopoulou, D. Méry (editors), LNCS, Springer, August 2012, vol. 7436, p. 10–27.
• 27F. Aarts, H. Kuppens, J. Tretmans, F. W. Vaandrager, S. Verwer.
  
  Learning and Testing the Bounded Retransmission Protocol, in: Proceedings of the 11th International Conference on Grammatical Inference ICGI'2012 (College Park, Maryland, USA), S. Ossowski, P. Lecca (editors), JMLR Workshop and Conference Proceedings (Open Access), March 2012, vol. 21, p. 4–18.
• 28B. Aichernig, F. Lorber, S. Tiran.
  
  Integrating Model-Based Testing and Analysis Tools via Test Case Exchange, in: Proceedings of the 6th International Symposium on Theoretical Aspects of Software Engineering TASE'2012 (Beijing, China), T. Margaria, Z. Qiu, H. Yang (editors), IEEE Press, July 2012, p. 119–126.
• 29H. R. Andersen.
  
  Partial Model Checking, in: Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science LICS (San Diego, California, USA), IEEE Computer Society Press, June 1995, p. 398–407.
• 30S. Basu, T. Bultan, M. Ouederni.
  
  Deciding Choreography Realizability, in: Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL'2012 (Philadelphia, Pennsylvania, USA), J. Field, M. Hicks (editors), ACM, January 2012, p. 191–202.
• 31S. Basu, T. Bultan, M. Ouederni.
  
  Synchronizability for Verification of Asynchronously Communicating Systems, in: Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation VMCAI'2012 (Philadelphia, PA, USA), V. Kuncak, A. Rybalchenko (editors), LNCS, Springer, January 2012, vol. 7148, p. 56–71.
• 32P. Beaucamps, I. Gnaedig, J.-Y. Marion.
  
  Abstraction-Based Malware Analysis Using Rewriting and Model Checking, in: Proceedings of the 17th European Symposium on Research in Computer Security ESORICS'2012 (Pisa, Italy), S. Foresti, M. Yung, F. Martinelli (editors), LNCS, Springer, September 2012, vol. 7459, p. 806–823.
• 33A. F. E. Belinfante.
  
  JTorX: A Tool for On-Line Model-Driven Test Derivation and Execution, in: Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2010 (Paphos, Cyprus), Lecture Notes in Computer Science, Springer Verlag, March 2010, vol. 6015, p. 266–270.
• 34F. Boyer, O. Gruber, G. Salaün.
  
  Specifying and Verifying the Synergy Reconfiguration Protocol with LOTOS NT/CADP, in: Proceedings of the 17th International Symposium on Formal Methods FM'2011 (Limerick, Ireland), M. Butler, W. Schulte (editors), LNCS, Springer, June 2011, vol. 6664, p. 103–117.
• 35F. Cappello, E. Caron, M. Daydé, F. Desprez, E. Jeannot, Y. Jegou, S. Lanteri, J. Leduc, N. Melab, G. Mornet, R. Namyst, P. Primet, O. Richard.
  
  Grid'5000: A Large Scale, Reconfigurable, Controlable and Monitorable Grid Platform, in: Proceedings of the 6th IEEE/ACM International Workshop on Grid Computing GRID'2005 (Seattle, USA), IEEE/ACM, November 2005, p. 99–106.
• 36D. Champelovier, X. Clerc, H. Garavel, Y. Guerte, C. McKinty, V. Powazny, F. Lang, W. Serwe, G. Smeding.
  
  Reference Manual of the LOTOS NT to LOTOS Translator (Version 5.7), November 2012, Inria/VASY, 153 pages.
• 37E. M. Clarke, E. A. Emerson, A. P. Sistla.
  
  Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications, in: ACM Transactions on Programming Languages and Systems, April 1986, vol. 8, n^o 2, p. 244–263.
• 38R. De Nicola, F. W. Vaandrager.
  
  Action versus State Based Logics for Transition Systems, LNCS, Springer Verlag, 1990, vol. 469, p. 407–419.
• 39M. Frappier, R. Saint-Denis.
  
  EB${}^3$: An Entity-Based Black-Box Specification Method for Information Systems, in: Software and System Modeling, 2003, vol. 2, n^o 2, p. 134-149.
• 40O. Ganea, F. Pop, C. Dobre, V. Cristea.
  
  Specification and Validation of a Real-Time Simple Parallel Kernel for Dependable Distributed Systems, in: Proceedings of the 3rd International Conference on Emerging Intelligent Data and Web Technologies EIDWT'2012 (Bucharest, Romania), IEEE Computer Society, September 2012, p. 320–325.
• 41H. Garavel.
  
  Compilation of LOTOS Abstract Data Types, in: Proceedings of the 2nd International Conference on Formal Description Techniques FORTE'89 (Vancouver B.C., Canada), S. T. Vuong (editor), North Holland, December 1989, p. 147–162.
• 42H. Garavel.
  
  OPEN/CÆSAR: An Open Software Architecture for Verification, Simulation, and Testing, in: Proceedings of the First International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'98 (Lisbon, Portugal), Berlin, B. Steffen (editor), LNCS, Springer, March 1998, vol. 1384, p. 68–84, Full version available as Inria Research Report RR-3352.
• 43H. Garavel, F. Lang.
  
  SVL: a Scripting Language for Compositional Verification, in: Proceedings of the 21st IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems FORTE'2001 (Cheju Island, Korea), M. Kim, B. Chin, S. Kang, D. Lee (editors), Kluwer Academic Publishers, August 2001, p. 377–392, Full version available as Inria Research Report RR-4223.
• 44H. Garavel, F. Lang, R. Mateescu.
  
  Compiler Construction using LOTOS NT, in: Proceedings of the 11th International Conference on Compiler Construction CC 2002 (Grenoble, France), N. Horspool (editor), LNCS, Springer, April 2002, vol. 2304, p. 9–13.
• 45H. Garavel, R. Mateescu, D. Bergamini, A. Curic, N. Descoubes, C. Joubert, I. Smarandache-Sturm, G. Stragier.
  
  DISTRIBUTOR and BCG_MERGE: Tools for Distributed Explicit State Space Generation, in: Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2006 (Vienna, Austria), H. Hermanns, J. Palberg (editors), LNCS, Springer, March–April 2006, vol. 3920, p. 445–449.
• 46H. Garavel, R. Mateescu, I. Smarandache-Sturm.
  
  Parallel State Space Construction for Model-Checking, in: Proceedings of the 8th International SPIN Workshop on Model Checking of Software SPIN'2001 (Toronto, Canada), Berlin, M. B. Dwyer (editor), LNCS, Springer, May 2001, vol. 2057, p. 217–234, Revised version available as Inria Research Report RR-4341 (December 2001).
• 47H. Garavel, W. Serwe.
  
  State Space Reduction for Process Algebra Specifications, in: Theoretical Computer Science, February 2006, vol. 351, n^o 2, p. 131–145.
• 48H. Garavel, J. Sifakis.
  
  Compilation and Verification of LOTOS Specifications, in: Proceedings of the 10th International Symposium on Protocol Specification, Testing and Verification (Ottawa, Canada), L. Logrippo, R. L. Probert, H. Ural (editors), North Holland, June 1990, p. 379–394.
• 49D. Guck, T. Han, J.-P. Katoen, M. R. Neuhäußer.
  
  Quantitative Timed Analysis of Interactive Markov Chains, in: Proceedings of the 4th NASA International Symposium on Formal Methods (Norfolk, VA, USA), A. Goodloe, S. Person (editors), LNCS, Springer, April 2012, vol. 7226, p. 8–23.
• 50M. Hennessy, R. Milner.
  
  Algebraic Laws for Nondeterminism and Concurrency, in: Journal of the ACM, 1985, vol. 32, p. 137–161.
• 51C. Jard, T. Jéron.
  
  TGV: Theory, Principles and Algorithms — A Tool for the Automatic Synthesis of Conformance Test Cases for Non-Deterministic Reactive Systems, in: Springer International Journal on Software Tools for Technology Transfer (STTT), August 2005, vol. 7, n^o 4, p. 297–315.
• 52N. Kokash, C. Krause, E. de Vink.
  
  Reo + mCRL2: A Framework for Model-Checking Dataflow in Service Compositions, in: Formal Aspects of Computing, March 2012, vol. 24, n^o 2, p. 187–216.
• 53E. Lantreibecq, W. Serwe.
  
  Model Checking and Co-simulation of a Dynamic Task Dispatcher Circuit Using CADP, in: Proceedings of the 16th International Workshop on Formal Methods for Industrial Critical Systems FMICS 2011 (Trento, Italy), G. Salaün, B. Schätz (editors), LNCS, Springer, August 2011, vol. 6959, p. 180–195.
• 54H.-V. Luong, A.-L. Courbis, T. Lambolais, T. L. Phan.
  
  IDCM : un outil d'analyse de composants et d'architectures dédié à la construction incrémentale, in: Actes des 11èmes Journées Francophones sur les Approches Formelles dans l'Assistance au Développement de Logiciels AFADL'2012 (Grenoble : France), January 2012.
• 55J. Magee, J. Kramer.
  
  Concurrency: State Models and Java Programs, 2006, Wiley, April 2006.
• 56R. Mateescu, D. Thivolle.
  
  A Model Checking Language for Concurrent Value-Passing Systems, in: Proceedings of the 15th International Symposium on Formal Methods FM'08 (Turku, Finland), J. Cuellar, T. Maibaum, K. Sere (editors), LNCS, Springer, May 2008, vol. 5014, p. 148–164.
• 57J. Parrow, P. Sjödin.
  
  Designing a Multiway Synchronization Protocol, in: Computer Communications, 1996, vol. 19, n^o 14, p. 1151–1160.
• 58B. Theelen, J.-P. Katoen, W. Hao.
  
  Model Checking of Scenario-Aware Dataflow with CADP, in: Proceedings of Design, Automation & Test in Europe Conference & Exhibition DATE'2012 (Dresden, Germany), W. Rosenstiel, L. Thiele (editors), IEEE Press, March 2012, p. 653–658.
• 59J. Tretmans.
  
  Model Based Testing with Labelled Transition Systems, in: Formal Methods and Testing, LNCS, Springer, 2008, vol. 4949, p. 1–38.
• 60K. J. Turner, K. L. L. Tan.
  
  Rigorous Development of Composite Grid Services, in: Journal of Network and Computer Applications, 2012, vol. 35, p. 1304–1316.
• 61F. Van der Berg.
  
  DFTCalc - Calculating DFTs using Lotos NT, University of Twente, 2012.
• 62H. Zhao, W. Wang, J. Sun, Y. Wei.
  
  Research on Formal Modeling and Verification of BPEL-based Web Service Composition, in: Proceedings of the 11th International Conference on Computer and Information Science ICIS'2012 (Shanghai, China), IEEE, June 2012.
• 63N. Zhar, M. Ait Ali, M. Eleuldj, A. Raji.
  
  A Specific-domain Design Tool for FPGA-based Image and Video Processing System, in: International Journal of Computer Applications, October 2012, vol. 56, n^o 11, p. 6–21.