{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T03:26:19Z","timestamp":1777519579784,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540439288","type":"print"},{"value":"9783540456148","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45614-7_23","type":"book-chapter","created":{"date-parts":[[2007,5,17]],"date-time":"2007-05-17T04:45:28Z","timestamp":1179377128000},"page":"410-429","source":"Crossref","is-referenced-by-count":32,"title":["On Combining Functional Verification and Performance Evaluation Using CADP"],"prefix":"10.1007","author":[{"given":"Hubert","family":"Garavel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"A. Marsan, G. Balbo, and G. Conte. A Class of Generalized Stochastic Petri Nets for the Performance Evaluation of Multiprocessor Systems. ACM Trans. on Comp. Sys., 2(2), 1984.","DOI":"10.1145\/190.191"},{"key":"23_CR2","unstructured":"ANSI. Small Computer System Interface-2. Standard X3.131-1994, American National Standards Institute, 1994."},{"key":"23_CR3","volume-title":"Proc. FORTE\u201998","author":"M. Bernardo","year":"1998","unstructured":"M. Bernardo, W.R. Cleaveland, S.T. Sims, and W.J. Stewart. TwoTowers: A Tool Integrating Functional and Performance Analysis of Concurrent Systems. In Proc. FORTE\u201998, IFIP, North-Holland, 1998."},{"key":"23_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(97)00127-8","volume":"202","author":"M. Bernardo","year":"1998","unstructured":"M. Bernardo and R. Gorrieri. A Tutorial on EMPA: A Theory of Concurrent Processes with Nondeterminism, Priorities, Probabilities and Time. Th. Comp. Sci., 202:1\u201354, 1998.","journal-title":"Th. Comp. Sci."},{"key":"23_CR5","unstructured":"D. Bert. Preuve de propri\u00e9t\u00e9s d\u2019\u00e9quit\u00e9 en B: Preuve de l\u2019algorithme d\u2019arbitrage du bus SCSI-3. In Proc. AFADL\u20192001 (Nancy, France), pages 221\u2013241, June 2001."},{"key":"23_CR6","unstructured":"L. Blair, G. Blair, and A. Andersen. Separating Functional Behaviour and Performance Constraints: Aspect-Oriented Specification. Technical Report MPG-98-07, Computing Department, Lancaster University, 1998."},{"issue":"1","key":"23_CR7","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0169-7552(87)90085-7","volume":"14","author":"T. Bolognesi","year":"1988","unstructured":"T. Bolognesi and E. Brinksma. Introduction to the ISO Specification Language LOTOS. Comp. Netw. and ISDN Sys., 14(1):25\u201359, 1988.","journal-title":"Comp. Netw. and ISDN Sys."},{"issue":"3","key":"23_CR8","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1287\/ijoc.12.3.203.12634","volume":"13","author":"P. Buchholz","year":"2000","unstructured":"P. Buchholz, G. Ciardo, S. Donatelli, and P. Kemper. Complexity of memory-efficient Kronecker operations with applications to the solution of Markov models. INFORMS J. on Comp., 13(3):203\u2013222, 2000.","journal-title":"INFORMS J. on Comp."},{"key":"23_CR9","unstructured":"L. de Alfaro. How to specify and verify the long-run average behavior of probabilistic systems. In Proc. Symp. on Logic in Computer Science, 1998."},{"issue":"6","key":"23_CR10","doi-asserted-by":"crossref","first-page":"678","DOI":"10.1109\/TSE.1986.6312965","volume":"SE-12","author":"D. Ferrari","year":"1986","unstructured":"D. Ferrari. Considerations on the Insularity of Performance Evaluation. IEEE Trans. on Softw. Eng., SE-12(6):678\u2013683, June 1986.","journal-title":"IEEE Trans. on Softw. Eng."},{"key":"23_CR11","unstructured":"H. Garavel. Compilation of LOTOS abstract data types. In Proc. FORTE\u201989, pages 147\u2013162. IFIP, North-Holland, 1989."},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"H. Garavel and F. Lang. SVL: A Scripting Language for Compositional Verification. In Proc. FORTE\u20192001, pages 377\u2013392. IFIP, Kluwer Academic, 2001. Full version available as INRIA Research Report RR-4223.","DOI":"10.1007\/0-306-47003-9_24"},{"key":"23_CR13","unstructured":"H. Garavel and J. Sifakis. Compilation and verification of LOTOS specifications. In Proc. PSTV\u201990, pages 379\u2013394. IFIP, North-Holland, 1990."},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"S. Gilmore and J. Hillston. The PEPA Workbench: A Tool to Support a Process Algebra-Based Approach to Performance Modelling. In Proc. TOOLS\u201994, 1994.","DOI":"10.1007\/3-540-58021-2_20"},{"key":"23_CR15","series-title":"Lect Notes Comput Sci","volume-title":"Tutorial Proc. PERFORMANCE\u2019 93","author":"N. G\u00f6tz","year":"1993","unstructured":"N. G\u00f6tz, U. Herzog, and M. Rettelbach. Multiprocessor and distributed system design: The integration of functional specification and performance analysis using stochastic process algebras. In Tutorial Proc. PERFORMANCE\u2019 93. Springer, LNCS 729, 1993."},{"issue":"5","key":"23_CR16","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1007\/BF01211911","volume":"8","author":"S. Graf","year":"1996","unstructured":"S. Graf, B. Steffen, and G. Luettgen. Compositional Minimization of Finite State Systems. Formal Asp. of Comp., 8(5):607\u2013616, 1996.","journal-title":"Formal Asp. of Comp."},{"key":"23_CR17","unstructured":"H. Garavel, F. Lang, and R. Mateescu. An Overview of CADP 2001. INRIA Technical Report RT-254, December 2001."},{"key":"23_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1007\/3-540-44612-5_34","volume-title":"Proc. MFCS\u20192000","author":"J.F. Groote","year":"2000","unstructured":"J.F. Groote and J. van de Pol. State space reduction using partial \u03c4-confluence. In Proc. MFCS\u20192000, pages 383\u2013393. Springer, LNCS 1893, 2000."},{"key":"23_CR19","unstructured":"H. Hermanns. Interactive Markov Chains. PhD thesis, Universit\u00e4t Erlangen-N\u00fcrnberg, 1998. revised version to appear as Springer LNCS monograph."},{"issue":"1\u20132","key":"23_CR20","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/S0304-3975(00)00305-4","volume":"274","author":"H. Hermanns","year":"2002","unstructured":"H. Hermanns, U. Herzog, and J.-P. Katoen. Process algebra for performance evaluation. Th. Comp. Sci., 274(1\u20132):43\u201387, 2002.","journal-title":"Th. Comp. Sci."},{"issue":"1\u20134","key":"23_CR21","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1016\/S0166-5316(99)00056-5","volume":"39","author":"H. Hermanns","year":"2000","unstructured":"H. Hermanns, U. Herzog, U. Klehmet, V. Mertsiotakis, and M. Siegle. Compositional performance modelling with the TIPPtool. Perf. Eval., 39(1\u20134):5\u201335, January 2000.","journal-title":"Perf. Eval."},{"key":"23_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/3-540-46419-0_24","volume-title":"Proc. TACAS\u20192000","author":"H. Hermanns","year":"2000","unstructured":"H. Hermanns, J.-P. Katoen, J. Meyer-Kayser, and M. Siegle. A Markov Chain Model Checker. In Proc. TACAS\u20192000, pages 347\u2013362, Springer, LNCS 1785, 2000."},{"issue":"1","key":"23_CR23","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/S0167-6423(99)00019-2","volume":"36","author":"H. Hermanns","year":"2000","unstructured":"H. Hermanns and J.P. Katoen. Automated compositional Markov chain generation for a plain-old telephony system. Sci. of Comp. Prog., 36(1):97\u2013127, 2000.","journal-title":"Sci. of Comp. Prog."},{"key":"23_CR24","unstructured":"O. Hjiej, A. Benzekri, and A. Valderruten. From Annotated LOTOS specifications to Queueing Networks: Automating Performance Models Derivation. Decentralized and Distributed Systems (North Holland), 1993."},{"key":"23_CR25","unstructured":"J. Hillston. The Nature of Synchronisation. In Proc. PAPM\u201994, Arbeitsberichte des IMMD, Universit\u00e4t Erlangen-N\u00fcrnberg. pages 51\u201370, 1994."},{"key":"23_CR26","doi-asserted-by":"crossref","unstructured":"J. Hillston. A Compositional Approach to Performance Modelling. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511569951"},{"key":"23_CR27","unstructured":"ISO\/IEC. LOTOS \u2014 A Formal Description Technique based on the Temporal Ordering of Observational Behaviour. International Standard 8807, ISO-Information Processing Systems-Open Systems Interconnection, 1988."},{"key":"23_CR28","unstructured":"ISO\/IEC. Enhancements to LOTOS (E-LOTOS). International Standard 15437:2001, ISO-Information Technology, 2001."},{"issue":"2","key":"23_CR29","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1109\/90.298433","volume":"2","author":"A. Marsan","year":"1994","unstructured":"A. Marsan, A. Bianco, L. Ciminiera, R. Sisto, and A. Valenzano. A LOTOS Extension for the Performance Analysis of Distributed Systems. IEEE\/ACM Trans, on Networking, 2(2), 151\u2013164, 1994.","journal-title":"IEEE\/ACM Trans, on Networking"},{"key":"23_CR30","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/3-540-46002-0_5","volume-title":"Proc. TACAS\u20192002","author":"M. Kwiatkowska","year":"2002","unstructured":"M. Kwiatkowska, G. Norman, and D. Parker. Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach. In Proc. TACAS\u20192002, pages 52\u201366, 2002, Springer LNCS 2280."},{"key":"23_CR31","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1007\/3-540-46002-0_33","volume-title":"Proc. TACAS\u20192002","author":"F. Lang","year":"2002","unstructured":"F. Lang. Compositional Verification using SVL Scripts. In Proc. TACAS\u20192002, pages 465\u2013469, 2002, Springer LNCS 2280."},{"key":"23_CR32","unstructured":"M.F. Neuts. Matrix-geometric Solutions in Stochastic Models-An Algorithmic Approach. The Johns Hopkins University Press, 1981."},{"key":"23_CR33","doi-asserted-by":"crossref","unstructured":"M.L. Puterman. Markov Decision Processes. John Wiley, 1994.","DOI":"10.1002\/9780470316887"},{"key":"23_CR34","doi-asserted-by":"crossref","unstructured":"W.J. Stewart. Introduction to the numerical solution of Markov chains. Princeton University Press, 1994.","DOI":"10.1515\/9780691223384"},{"key":"23_CR35","unstructured":"K. J. Turner, editor. Using Formal Description Techniques-An Introduction to ESTELLE, LOTOS, and SDL. John Wiley, 1993."},{"issue":"1","key":"23_CR36","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/0304-3975(90)90111-T","volume":"89","author":"C. Vissers","year":"1991","unstructured":"C. Vissers, G. Scollo, M. van Sinderen, and E. Brinksma. Specification styles in distributed systems design and verification. Th. Comp. Sci., 89(1):179\u2013206, 1991.","journal-title":"Th. Comp. Sci."},{"key":"23_CR37","unstructured":"M. Zendri. Studio ed implementazione di un modello del bus SCSI. Laurea thesis, Politecnico di Milano, Facolt\u00e0 di Ingegneria, Dip. di Elettronica, 1992."}],"container-title":["Lecture Notes in Computer Science","FME 2002:Formal Methods\u2014Getting IT Right"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45614-7_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,11]],"date-time":"2023-05-11T22:04:58Z","timestamp":1683842698000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45614-7_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439288","9783540456148"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/3-540-45614-7_23","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}