[. Marsan, G. Balbo, and G. Conte, A Class of Generalized Stochastic Petri Nets for the Performance Evaluation of Multiprocessor Systems, ACM Transactions on Computer Systems, vol.2, issue.2, 1984.

[. Ansi, Small Computer System Interface-2. Standard X3.131-1994, 1994.

[. Bolognesi and E. Brinksma, Introduction to the ISO specification language LOTOS, Computer Networks and ISDN Systems, vol.14, issue.1, pp.25-59, 1988.
DOI : 10.1016/0169-7552(87)90085-7

L. Blair, G. Blair, and A. Andersen, Separating Functional Behaviour and Performance Constraints: Aspect-Oriented Specification, Distributed Multimedia Research Group Report MPG-98-07, 1998.

G. [. Buchholz, S. Ciardo, P. Donatelli, and . Kemper, Complexity of Memory-Efficient Kronecker Operations with Applications to the Solution of Markov Models, INFORMS Journal on Computing, vol.12, issue.3, pp.203-222, 2000.
DOI : 10.1287/ijoc.12.3.203.12634

W. [. Bernardo, S. T. Cleaveland, W. J. Sims, and . Stewart, Twotowers: A Tool Integrating Functional and Performance Analysis of Concurrent Systems, Proceedings of the 18th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems, 1998.
DOI : 10.1007/978-0-387-35394-4_28

D. Bert, Preuve de propriétés d'´ equité en B : Preuve de l'algorithme d'arbitrage du bus SCSI-3

R. [. Bernardo and . Gorrieri, A tutorial on EMPA: A theory of concurrent processes with nondeterminism, priorities, probabilities and time, Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS'98), pp.1-54, 1998.
DOI : 10.1016/S0304-3975(97)00127-8

J. De-meer, R. Roth, and S. Vuong, Introduction to algebraic specifications based on the language ACT ONE, Computer Networks and ISDN Systems, vol.23, issue.5, pp.363-392, 1992.
DOI : 10.1016/0169-7552(92)90013-G

B. [. Ehrig and . Mahr, Fundamentals of Algebraic Specification 1 ? Equations and Initial Semantics, EATCS Monographs on Theoretical Computer Science, vol.6, 1985.

]. D. Fer86 and . Ferrari, Considerations on the Insularity of Performance Evaluation, IEEE Transactions on Software Engineering SE?, vol.12, issue.6, pp.678-683, 1986.

H. Garavel, Compilation of LOTOS Abstract Data Types

J. [. Gilmore and . Hillston, The PEPA workbench: A tool to support a process algebra-based approach to performance modelling, 7th Int. Conf. on Modelling Techniques and Tools for Computer Performance Evaluation, 1994.
DOI : 10.1007/3-540-58021-2_20

U. [. Götz, M. Herzog, and . Rettelbach, Multiprocessor and distributed system design: The integration of functional specification and performance analysis using Stochastic Process Algebras, Tutorial Proc. of the 16th Int. Symposium on Computer Performance Modelling, Measurement and Evaluation , PERFORMANCE '93, 1993.
DOI : 10.1007/BFb0013851

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'2001, pp.377-392, 2001.
DOI : 10.1007/0-306-47003-9_24
URL : https://hal.archives-ouvertes.fr/inria-00072396

[. Garavel, F. Lang, and R. Mateescu, An Overview of CADP 2001, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00069920

H. Garavel and J. Sifakis, Compilation and Verification of LOTOS Specifications, Proceedings of the 10th International Symposium on Protocol Specification, Testing and Verification, pp.379-394, 1990.

B. [. Graf, G. Steffen, and . Lüttgen, Compositional minimisation of finite state systems using interface specifications, Formal Aspects of Computing, vol.17, issue.5, pp.607-616, 1996.
DOI : 10.1007/BF01211911

I. F. Groote and J. Van, State Space Reduction Using Partial ??-Confluence, Proceedings of the 25th International Symposium on Mathematical Foundations of Computer Science MFCS'2000, pp.383-393, 2000.
DOI : 10.1007/3-540-44612-5_34
URL : http://library.tue.nl/csp/dare/LinkToRepository.csp?recordnumber=660478

A. [. Hjiej, A. Benzekri, and . Valderruten, From Annotated LOTOS Specifications to Queueing Networks: Automating Performance Models Derivation. Decentralized and Distributed Systems, 1993.

]. H. Her98 and . Hermanns, Interactive Markov Chains, 1998.

U. Hermanns, U. Herzog, V. Klehmet, M. Mertsiotakis, and . Siegle, Compositional performance modelling with the TIPPtool, Performance Evaluation, vol.39, pp.1-45, 2000.
DOI : 10.1007/3-540-68061-6_5
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.6603

U. [. Hermanns, J. Herzog, and . Katoen, Process algebra for performance evaluation, Theoretical Computer Science, vol.274, issue.1-2, 2002.
DOI : 10.1016/S0304-3975(00)00305-4
URL : http://doi.org/10.1016/s0304-3975(00)00305-4

]. J. Hil94 and . Hillston, The Nature of Synchronisation, Proc. of the 2nd Workshop on Process Algebras and Performance Modelling, pp.51-70, 1994.

]. J. Hil96 and . Hillston, A Compositional Approach to Performance Modelling, 1996.

J. [. Hermanns and . Katoen, Automated compositional Markov chain generation for a plain-old telephone system, Science of Computer Programming, vol.36, issue.1, pp.97-127, 2000.
DOI : 10.1016/S0167-6423(99)00019-2

J. [. Hermanns, J. Katoen, M. Meyer-kayser, and . Siegle, A Markov Chain Model Checker, LNCS, vol.1785, pp.347-362, 2000.
DOI : 10.1007/3-540-46419-0_24
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.43.1396

]. C. Hoa85 and . Hoare, Communicating Sequential Processes, 1985.

[. Iec, LOTOS ? A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour, International Organization for Standardization ? Information Processing Systems ? Open Systems Interconnection, 1988.

[. Iec, Enhancements to LOTOS (E-LOTOS) International Standard 15437, International Organization for Standardization ? Information Technology, 2001.

G. [. Kwiatkowska, R. Norman, and . Segala, Automated Verification of a Randomised Distributed Consensus Protocol Using Cadence SMV and PRISM

[. Lang, Compositional Verification Using SVL Scripts, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2002, pp.465-469, 2002.
DOI : 10.1007/3-540-46002-0_33

]. A. Mbc-+-94, A. Marsan, L. Bianco, R. Ciminiera, A. Sisto et al., A LOTOS Extension for the Performance Analysis of Distributed Systems, IEEE/ACM Transactions on Networking, vol.2, issue.2, pp.151-164, 1994.

[. Milner, A Calculus of Communicating Systems, Lecture Notes in Computer Science, vol.92, 1980.
DOI : 10.1007/3-540-10235-3

[. Milner, Communication and Concurrency, 1989.

]. M. Neu81 and . Neuts, Matrix-geometric Solutions in Stochastic Models?An Algorithmic Approach, 1981.

[. Park, Concurrency and automata on infinite sequences, Theoretical Computer Science, pp.167-183, 1981.
DOI : 10.1007/BFb0017309

]. W. Ste94 and . Stewart, Introduction to the Numerical Solution of Markov Chains, 1994.

G. [. Vissers, M. Scollo, E. Van-sinderen, and . Brinksma, Specification styles in distributed systems design and verification, Theoretical Computer Science, vol.89, issue.1, pp.179-206, 1991.
DOI : 10.1016/0304-3975(90)90111-T

M. Zendri, Studio ed implementazione di un modello del bus SCSI, 1992.

I. Unité-de-recherche and . Lorraine, Technopôle de Nancy-Brabois -Campus scientifique 615, rue du Jardin Botanique -BP 101 -54602 Villers-l` es-Nancy Cedex (France) Unité de recherche INRIA Rennes : IRISA, Campus universitaire de Beaulieu -35042 Rennes Cedex (France) Unité de recherche INRIA Rocquencourt : Domaine de Voluceau -Rocquencourt -BP 105 -78153 Le Chesnay Cedex (France) Unité de recherche, 2004.

I. Editeur and . De-voluceau-rocquencourt, BP 105 -78153 Le Chesnay Cedex (France) http://www.inria.fr ISSN, pp.249-6399