Abstract
Considering functional correctness and performance evaluation in a common framework is desirable, both for scientific and economic reasons. In this paper, we describe how the Cadp toolbox, originally designed for verifying the functional correctness of Lotos specifications, can also be used for performance evaluation. We illustrate the proposed approach by the performance study of the Scsi-2 bus arbitration protocol.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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.
ANSI. Small Computer System Interface-2. Standard X3.131-1994, American National Standards Institute, 1994.
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’98, IFIP, North-Holland, 1998.
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–54, 1998.
D. Bert. Preuve de propriétés d’équité en B: Preuve de l’algorithme d’arbitrage du bus SCSI-3. In Proc. AFADL’2001 (Nancy, France), pages 221–241, June 2001.
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.
T. Bolognesi and E. Brinksma. Introduction to the ISO Specification Language LOTOS. Comp. Netw. and ISDN Sys., 14(1):25–59, 1988.
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–222, 2000.
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.
D. Ferrari. Considerations on the Insularity of Performance Evaluation. IEEE Trans. on Softw. Eng., SE-12(6):678–683, June 1986.
H. Garavel. Compilation of LOTOS abstract data types. In Proc. FORTE’89, pages 147–162. IFIP, North-Holland, 1989.
H. Garavel and F. Lang. SVL: A Scripting Language for Compositional Verification. In Proc. FORTE’2001, pages 377–392. IFIP, Kluwer Academic, 2001. Full version available as INRIA Research Report RR-4223.
H. Garavel and J. Sifakis. Compilation and verification of LOTOS specifications. In Proc. PSTV’90, pages 379–394. IFIP, North-Holland, 1990.
S. Gilmore and J. Hillston. The PEPA Workbench: A Tool to Support a Process Algebra-Based Approach to Performance Modelling. In Proc. TOOLS’94, 1994.
N. Götz, 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’ 93. Springer, LNCS 729, 1993.
S. Graf, B. Steffen, and G. Luettgen. Compositional Minimization of Finite State Systems. Formal Asp. of Comp., 8(5):607–616, 1996.
H. Garavel, F. Lang, and R. Mateescu. An Overview of CADP 2001. INRIA Technical Report RT-254, December 2001.
J.F. Groote and J. van de Pol. State space reduction using partial τ-confluence. In Proc. MFCS’2000, pages 383–393. Springer, LNCS 1893, 2000.
H. Hermanns. Interactive Markov Chains. PhD thesis, Universität Erlangen-Nürnberg, 1998. revised version to appear as Springer LNCS monograph.
H. Hermanns, U. Herzog, and J.-P. Katoen. Process algebra for performance evaluation. Th. Comp. Sci., 274(1–2):43–87, 2002.
H. Hermanns, U. Herzog, U. Klehmet, V. Mertsiotakis, and M. Siegle. Compositional performance modelling with the TIPPtool. Perf. Eval., 39(1–4):5–35, January 2000.
H. Hermanns, J.-P. Katoen, J. Meyer-Kayser, and M. Siegle. A Markov Chain Model Checker. In Proc. TACAS’2000, pages 347–362, Springer, LNCS 1785, 2000.
H. Hermanns and J.P. Katoen. Automated compositional Markov chain generation for a plain-old telephony system. Sci. of Comp. Prog., 36(1):97–127, 2000.
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.
J. Hillston. The Nature of Synchronisation. In Proc. PAPM’94, Arbeitsberichte des IMMD, Universität Erlangen-Nürnberg. pages 51–70, 1994.
J. Hillston. A Compositional Approach to Performance Modelling. Cambridge University Press, 1996.
ISO/IEC. LOTOS — A Formal Description Technique based on the Temporal Ordering of Observational Behaviour. International Standard 8807, ISO-Information Processing Systems-Open Systems Interconnection, 1988.
ISO/IEC. Enhancements to LOTOS (E-LOTOS). International Standard 15437:2001, ISO-Information Technology, 2001.
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–164, 1994.
M. Kwiatkowska, G. Norman, and D. Parker. Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach. In Proc. TACAS’2002, pages 52–66, 2002, Springer LNCS 2280.
F. Lang. Compositional Verification using SVL Scripts. In Proc. TACAS’2002, pages 465–469, 2002, Springer LNCS 2280.
M.F. Neuts. Matrix-geometric Solutions in Stochastic Models-An Algorithmic Approach. The Johns Hopkins University Press, 1981.
M.L. Puterman. Markov Decision Processes. John Wiley, 1994.
W.J. Stewart. Introduction to the numerical solution of Markov chains. Princeton University Press, 1994.
K. J. Turner, editor. Using Formal Description Techniques-An Introduction to ESTELLE, LOTOS, and SDL. John Wiley, 1993.
C. Vissers, G. Scollo, M. van Sinderen, and E. Brinksma. Specification styles in distributed systems design and verification. Th. Comp. Sci., 89(1):179–206, 1991.
M. Zendri. Studio ed implementazione di un modello del bus SCSI. Laurea thesis, Politecnico di Milano, Facoltà di Ingegneria, Dip. di Elettronica, 1992.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Garavel, H., Hermanns, H. (2002). On Combining Functional Verification and Performance Evaluation Using CADP. In: Eriksson, LH., Lindsay, P.A. (eds) FME 2002:Formal Methods—Getting IT Right. FME 2002. Lecture Notes in Computer Science, vol 2391. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45614-7_23
Download citation
DOI: https://doi.org/10.1007/3-540-45614-7_23
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43928-8
Online ISBN: 978-3-540-45614-8
eBook Packages: Springer Book Archive