, ? Om/rr protocol for traffic control 22, vol.86

, Bull's Cfs distributed file system for Aix 24, vol.64

?. Philips,

, Single pulser and bus arbitration hardware designs 26

, ? Sync-stop & Chandi-Lamport checkpoint algorithms 27, vol.35

, Sophia Antipolis (fr)

, Faust asynchronous network-on-chip 30, Cea/Leti

, ? Diagrams for choreographies 31 [70], Málaga (es) and Santa Barbara (us)

, ? Trivial File Transfer Protocol

, ? Cress diagrams for Web and grid services 33, vol.77

, ? Fault-tolerant routing algorithm for a network-on-chip 35, vol.89

, Compositional minimisation has also been used for performance evaluation: ? Performance analysis of a Plain Old Telephone System 37, vol.43

, European Train Control System, vol.39, issue.8

A. Arnold, Synchronized Behaviours of Processes and Rational Relations, Acta Informatica, vol.17, pp.21-29, 1982.

I. Attali, T. Barros, and E. Madelaine, Parameterized Specification and Verification of the Chilean Electronic Invoices System, Proceedings of the 24th International Conference of the Chilean Computer Science Society (SCCC'04), pp.14-25, 2004.

S. Bainbridge and L. Mounier, Specification and Verification of a Reliable Multicast Protocol, 1991.

T. Barros, L. Henrio, and E. Madelaine, Behavioural Models for Hierarchical Components, Proceedings of the 12th International Workshop on Model Checking of Software (SPIN'05), vol.3639, pp.154-168, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00070416

T. Barros, L. Henrio, and E. Madelaine, Verification of Distributed Hierarchical Components, Proceedings of the International Workshop on Formal Aspects of Component Software (FACS'05), 2005.
URL : https://hal.archives-ouvertes.fr/inria-00122926

T. Barros and E. Madelaine, Formalization and Proofs of the Chilean Electronic Invoices System, INRIA Research Report, vol.5527, 2004.

J. A. Bergstra, A. Ponse, and S. A. Smolka, Handbook of Process Algebra, 2001.

E. Böde, M. Herbstritt, H. Hermanns, S. Johr, T. Peikenkamp et al., Compositional Performability Evaluation for Statemate, Proceedings of the 3rd International Conference on the Quantitative Evaluation of Systems (QUEST'06), pp.167-178, 2006.

A. Boulgakov, T. Gibson-robinson, and A. W. Roscoe, Computing Maximal Weak and Other Bisimulations, Formal Aspects of Computing, vol.28, issue.3, pp.381-407, 2016.

A. Bouzafour, M. Renaudin, H. Garavel, R. Mateescu, and W. Serwe, Model-checking Synthesizable SystemVerilog Descriptions of Asynchronous Circuits, Proceedings of the 24th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC'18), 2018.
URL : https://hal.archives-ouvertes.fr/hal-01777093

G. Chehaibar, H. Garavel, L. Mounier, N. Tawbi, and F. Zulian, Specification and Verification of the PowerScale Bus Arbitration Protocol: An Industrial Experiment with LOTOS, Proceedings of the IFIP Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification (FORTE/PSTV'96), pp.435-450, 1996.
URL : https://hal.archives-ouvertes.fr/inria-00073740

S. C. Cheung and J. Kramer, Enhancing Compositional Reachability Analysis with Context Constraints, Proceedings of the 1st ACM SIGSOFT International Symposium on the Foundations of Software Engineering, pp.115-125, 1993.

S. C. Cheung and J. Kramer, Compositional Reachability Analysis of FiniteState Distributed Systems with User-Specified Constraints, Proceedings of the 3rd ACM SIGSOFT International Symposium on the Foundations of Software Engineering, pp.140-150, 1995.

S. C. Cheung and J. Kramer, Context Constraints for Compositional Reachability, ACM Transactions on Software Engineering Methodology (TOSEM), vol.5, issue.4, pp.334-377, 1996.

E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, Counterexample-Guided Abstraction Refinement, Proceedings of the 12th International Conference on Computer Aided Verification (CAV'00), pp.154-169, 2000.

P. Crouzen and F. Lang, Smart Reduction, Proceedings of Fundamental Approaches to Software Engineering (FASE'11), pp.111-126, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00572535

T. Anthony-de-jacquier, C. Massart, and . Hernalsteen, Vérification et correction d'un protocole de contrôle aérien, 1997.

J. Fernandez, ALDEBARAN : un système de vérification par réduction de processus communicants, 1988.

J. Fernandez, H. Garavel, L. Mounier, A. Rasse, C. Rodríguez et al., A Toolbox for the Verification of LOTOS Programs, Proceedings of the 14th International Conference on Software Engineering (ICSE'14), pp.246-259, 1992.

J. Fogel, A Survey of Verification Techniques for Solving the State Explosion Problem, Proceedings of the IFAC Conference on Control Systems Design (CSD'00), vol.33, pp.361-366, 2000.

C. A. Furia, A Compositional World: A Survey of Recent Works on Compositionality in Formal Methods, Dipartimento di Elettronica e Informazione, vol.22, 2005.

H. Garavel, . Open, and . Caesar, An Open Software Architecture for Verification, Simulation, and Testing, Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'98), vol.1384, pp.68-84, 1998.
URL : https://hal.archives-ouvertes.fr/inria-00073337

H. Garavel and S. Graf, Formal Methods for Safe and Secure Computers Systems, Bundesamt für Sicherheit in der Informationstechnik, vol.875, 2013.

H. Garavel and H. Hermanns, On Combining Functional Verification and Performance Evaluation using CADP, Proceedings of the 11th International Symposium of Formal Methods Europe (FME'02), vol.2391, pp.410-429, 2002.
URL : https://hal.archives-ouvertes.fr/inria-00072096

H. Garavel and F. Lang, SVL: a Scripting Language for Compositional Verification, Proceedings of the 21st IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'01), pp.377-392, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00072396

H. Garavel, F. Lang, and R. Mateescu, Compositional Verification of Asynchronous Concurrent Systems Using CADP, Acta Informatica, vol.52, issue.4, pp.337-392, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01138749

H. Garavel, F. Lang, R. Mateescu, and W. Serwe, CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes, Springer International Journal on Software Tools for Technology Transfer (STTT), vol.15, issue.2, pp.89-107, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00715056

H. Garavel, F. Lang, and W. Serwe, From LOTOS to LNT, ModelEd, TestEd, TrustEd-Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday, vol.10500, pp.3-26, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01621670

H. Garavel and L. Mounier, Specification and Verification of Various Distributed Leader Election Algorithms for Unidirectional Ring Networks, Science of Computer Programming, vol.29, issue.1-2, pp.171-197, 1997.

H. Garavel and M. Sighireanu, A Graphical Parallel Composition Operator for Process Algebras, Proceedings of the IFIP Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification (FORTE/PSTV'99), pp.185-202, 1999.

H. Garavel and D. Thivolle, Verification of GALS Systems by Combining Synchronous Languages and Process Calculi, Proceedings of the 16th International SPIN Workshop on Model Checking of Software (SPIN'09), vol.5578, pp.241-260, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00388819

H. Garavel, C. Viho, and M. Zendri, System Design of a CC-NUMA Multiprocessor Architecture using Formal Specification, ModelChecking, Co-Simulation, and Test Generation, Springer International Journal on Software Tools for Technology Transfer (STTT), vol.3, issue.3, pp.314-331, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00072597

D. Giannakopoulou, Model Checking for Concurrent Software Architectures, 1999.

D. Giannakopoulou, K. S. Namjoshi, and C. S. Pasareanu, Compositional Reasoning, Handbook of Model Checking, pp.345-383, 2018.
DOI : 10.1007/978-3-319-10575-8_12

G. Godza, V. Cristea, and R. Mateescu, Formal Specification of Checkpointing Algorithms, Proceedings of 13th International Conference on Control Systems and Computer Science (CSCS'13), pp.311-317, 2001.

S. Graf and B. Steffen, Compositional Minimization of Finite State Systems, Proceedings of the 2nd Workshop on Computer-Aided Verification (CAV'90), vol.531, pp.186-196, 1990.

S. Graf and B. Steffen, Compositional Minimization of Finite State Systems. Aachener Informatik-Berichte AIB 1991-23, 1991.

S. Graf, B. Steffen, and G. Lüttgen, Compositional Minimization of Finite State Systems Using Interface Specifications, 1995.

S. Graf, B. Steffen, and G. Lüttgen, Compositional Minimization of Finite State Systems Using Interface Specifications. 10-page article published in the paper version of the journal, Formal Aspects of Computing, vol.8, issue.5, pp.607-616, 1996.

S. Graf, B. Steffen, and G. Lüttgen, Compositional Minimization of Finite State Systems using Interface Specifications. 28-page article published in the electronic repository of the journal "Formal Aspects of Computing, vol.8, pp.286-313, 1996.

, 2FBF01211911/MediaObjects/165_2005_BF01211911_MOESM1_ESM.pdf

J. He and K. J. Turner, Specification and Verification of Synchronous Hardware using LOTOS, Proceedings of the IFIP Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols and Protocol Specification, Testing, and Verification (FORTE/PSTV'99), pp.295-312, 1999.

H. Hermanns, Interactive Markov Chains and the Quest for Quantified Quality, Lecture Notes in Computer Science, vol.2428, 2002.

H. Hermanns and J. Katoen, Automated Compositional Markov Chain Generation for a Plain-Old Telephone System, Science of Computer Programming, vol.36, pp.97-127, 2000.

C. A. Hoare, Communicating Sequential Processes, Communications of the ACM, vol.21, issue.8, pp.666-677, 1978.

C. A. Hoare, Communicating Sequential Processes, 1985.

. Iso/iec, LOTOS-A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. International Standard 8807, International Organization for Standardization-Information Processing Systems-Open Systems Interconnection, 1989.

A. Kerbrat and S. B. Atallah, Formal Specification of a Framework for Groupware Development, Proceedings of the 8th International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE'95), pp.303-310, 1995.

F. Kordon, H. Garavel, E. Lom-messan-hillah, L. Paviotadet, F. Jezequel et al., Jaco van de Pol, and Karsten Wolf. MCC'2017-The Seventh Model Checking Contest. Transactions on Petri Nets and Other Models of Concurrency, 2018.

J. Krimm, Une approche compositionnelle pour la vérification de programmes LOTOS, 1996.

J. , P. Krimm, and L. Mounier, Compositional State Space Generation from LOTOS Programs, Proceedings of the 3rd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'97), vol.1217, 1997.
DOI : 10.1007/bfb0035392
URL : https://link.springer.com/content/pdf/10.1007%2FBFb0035392.pdf

F. Lang, Compositional Verification using SVL Scripts, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'02), vol.2280, pp.465-469, 2002.
DOI : 10.1007/3-540-46002-0_33
URL : https://link.springer.com/content/pdf/10.1007%2F3-540-46002-0_33.pdf

F. Lang, Refined Interfaces for Compositional Verification, Proceedings of the 26th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'06), vol.4229, pp.159-174, 2006.
DOI : 10.1007/11888116_13
URL : https://hal.archives-ouvertes.fr/inria-00106312

M. Luukkainen and A. Ahtiainen, Compositional Verification of Large SDL Systems, Proceedings of the 1st Workshop of the SDL Forum Society on SDL and MSC (SAM'98), 1998.

J. Malhotra, S. A. Smolka, A. Giacalone, and R. Shapiro, A Tool for Hierarchical Design and Simulation of Concurrent Systems, Proceedings of the BCS-FACS Workshop on Specification and Verification of Concurrent Systems, pp.140-152, 1988.

R. Mateescu and W. Serwe, A Study of Shared-Memory Mutual Exclusion Protocols using CADP, Proceedings of the 15th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'10), pp.180-197, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00532897

R. Mateescu and W. Serwe, Model Checking and Performance Evaluation with CADP Illustrated on Shared-Memory Mutual Exclusion Protocols, Science of Computer Programming, vol.78, issue.7, pp.843-861, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00671321

F. Mazzanti and A. Ferrari, Ten Diverse Formal Models for a CBTC Automatic Train Supervision System, Proceedings of the 3rd Workshop on Models for Formal Analysis of Real Systems and the 6th International Workshop on Verification and Program Transformation (MARS/VPT'18)

G. Thessaloniki, Electronic Proceedings in Theoretical Computer Science, vol.268, pp.104-149, 2018.

F. Mazzanti, A. Ferrari, and G. O. Spagnolo, Towards Formal Methods Diversity in Railways: An Experience Report with Seven Frameworks, Springer International Journal on Software Tools for Technology Transfer (STTT), vol.20, issue.3, pp.263-288, 2018.

N. Mendes, F. Lang, Y. Cornec, R. Mateescu, G. Batt et al., Composition and Abstraction of Logical Regulatory Modules: Application to Multicellular Systems, Bioinformatics, vol.29, issue.6, pp.749-757, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00785564

R. Milner, A Calculus of Communicating Systems, Lecture Notes in Computer Science, vol.92, 1980.

L. Mounier, A LOTOS Specification of a Transit-Node. Rapport SPECTRE 94-8, 1994.

R. Oliveira, S. Dupuy-chessa, G. Calvary, and D. Dadolle, Using Formal Models to Cross Check an Implementation, Proceedings of the 8th ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS'16), pp.126-137, 2016.
DOI : 10.1145/2933242.2933257
URL : https://hal.archives-ouvertes.fr/hal-01492641

D. Park, Concurrency and Automata on Infinite Sequences, Lecture Notes in Computer Science, vol.104, pp.167-183, 1981.
DOI : 10.1007/bfb0017309
URL : http://wrap.warwick.ac.uk/47224/1/WRAP_Park_cs-rr-035.pdf

C. Pecheur, Advanced Modelling and Verification Techniques Applied to a Cluster File System, Proceedings of the 14th IEEE International Conference on Automated Software Engineering (ASE'99) Cocoa, 1999.
URL : https://hal.archives-ouvertes.fr/inria-00073273

H. Peng-andsofì-ene-tahar, A Survey on Compositional Verification, 1998.

W. De-roever, U. Frank-de-boer, J. Hanneman, and . Hooman, Yassine Lakhnech, Mannes Poel, and Job Zwiers. Concurrency Verification-Introduction to Compositional and Noncompositional Methods, vol.54, 2001.

J. Romijn, Analysing Industrial Protocols with Formal Methods, 1999.

K. Krishan, A. M. Sabnani, M. Lapone, and . Uyar, An Algorithmic Procedure for Checking Safety Properties of Protocols, IEEE Transactions on Communications, vol.37, issue.9, pp.940-948, 1989.

M. Sage and C. Johnson, A Declarative Prototyping Environment for the Development of Multi-User Safety-Critical Systems, Proceedings of the 17th International System Safety Conference (ISSC'99), 1999.

G. Salaün and T. Bultan, Realizability of Choreographies using Process Algebra Encodings, Proceedings of the 7th International Conference on Integrated Formal Methods (IFM'09), vol.5423, pp.167-182, 2009.

G. Salaün and W. Serwe, Translating Hardware Process Algebras into Standard Process Algebras-Illustration with CHP and LOTOS, Proceedings of the 5th International Conference on Integrated Formal Methods (IFM'05), vol.3771, pp.287-306, 2005.

G. Salaün, W. Serwe, Y. Thonnart, and P. Vivet, Formal Verification of CHP Specifications with CADP-Illustration on an Asynchronous Network-on-Chip, Proceedings of the 13th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC'07), pp.73-82, 2007.

I. Schieferdecker, Abruptly-Terminated Connections in TCP-A Verification Example, Proceedings of the COST 247 International Workshop on Applied Formal Methods in System Design, pp.136-145, 1996.

W. Serwe, Formal Specification and Verification of Fully Asynchronous Implementations of the Data Encryption Standard, Proceedings of the International Workshop on Models for Formal Analysis of Real Systems (MARS'15), vol.196, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01227999

C. Kuo, P. V. Tai, and . Koppol, An Incremental Approach to Reachability Analysis of Distributed Programs, Proceedings of the 7th International Workshop on Software Specification and Design, pp.141-150, 1993.

C. Kuo, P. V. Tai, and . Koppol, Hierarchy-Based Incremental Reachability Analysis of Communication Protocols, Proceedings of the IEEE International Conference on Network Protocols, pp.318-325, 1993.

L. Tan, Case Studies Using CRESS to Develop Web and Grid Services, Department of Computing Science and Mathematics, 2009.

F. Tronel, F. Lang, and H. Garavel, Compositional Verification Using CADP of the ScalAgent Deployment Protocol for Software Components, Proceedings of the 6th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'03), pp.244-260, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00071572

A. Valmari, Compositional State Space Generation, Advances in Petri Nets 1993-Papers from the 12th International Conference on Applications and Theory of Petri Nets (ICATPN'91), vol.674, pp.427-457, 1993.
DOI : 10.1007/3-540-56689-9_54

A. Valmari, Compositionality in State Space Verification Methods, Proceedings of the 17th International Conference on Application and Theory of Petri Nets (ICATPN'96), vol.1091, pp.29-56, 1996.

A. Valmari, Composition and Abstraction, Proceedings of the 4th Summer School on Modeling and Verification of Parallel Processes (MOVEP'00), vol.2067, pp.58-98, 2000.

A. Valmari, J. Kemppainen, M. Clegg, and M. Levanto, Putting Advanced Reachability Analysis Techniques Together: the ARA Tool, Proceedings of the 1st International Symposium of Formal Methods Europe (FME'93), vol.670, pp.597-616, 1993.

A. Valmari and I. Kokkarinen, Unbounded Verification Results by Finite-State Compositional Techniques: 10 any States and Beyond, Proceedings of the 1st International Conference on Application of Concurrency to System Design (ACSD'98), pp.75-85, 1998.
DOI : 10.1109/csd.1998.657541

R. J. Van-glabbeek and W. Peter-weijland, Branching Time and Abstraction in Bisimulation Semantics, Journal of the ACM, vol.43, issue.3, pp.555-600, 1996.

T. Willemse, J. Tretmans, and A. Klomp, A Case Study in Formal Methods: Specification and Validation of the OM/RR Protocol, Proceedings of the 5th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'00), vol.91, pp.331-344, 2000.

A. C. Tim and . Willemse, The Specification and Validation of the OM/RRProtocol, 1998.

Y. Wei-jen, Controlling State Explosion in Reachability Analysis, 1993.

J. Wei, M. Yeh, and . Young, Compositional Reachability Analysis Using Process Algebra, Proceedings of the ACM SIGSOFT Symposium on Testing, Analysis, and Verification (SIGSOFT'91), pp.49-59, 1991.

Z. Zhang, W. Serwe, J. Wu, T. Zheng, and C. Myers, An Improved Fault-Tolerant Routing Algorithm for a Network-on-Chip Derived with Formal Analysis, Science of Computer Programming, vol.118, pp.24-39, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01261234