Abstract
This paper reports on an effort to integrate two verification tools, the Concurrency Workbench of the New Century (CWB-NC) and PIOATool. Our aim is to build a single tool that combines the “functional” analysis capabilities of the CWB-NC with the compositional performance-analysis features of PIOATool. We discuss some of the issues involved in the integration, highlighting a particular integration paradigm in which one tool becomes a subshell of the other.
Research supported by NSF grants CCR-9988155, CCR-9988489, and CCR-0098037 and Army Research Office grants DAAD190110003 and DAAD190110019.
Chapter PDF
References
M. Bernardo. An algebra-based method to associate rewards with EMPAterms. In ICALP’97, vol. 1256 of LNCS, pages 358–368, Jul. 1997.
M. Bernardo, R. Cleaveland, S. Sims, and W. Stewart. TwoTowers: A tool integrating functional and performance analysis of concurrent systems. In FORTE XI/PSTV XVIII’ 98, pages 457–467, Nov. 1998.
R. Cleaveland, E. Madelaine, and S. Sims. A front-end generator for verification tools. In TACAS’95, vol. 1019 of LNCS, pages 153–173, May 1995.
R. Cleaveland, J. Parrow, and B. Steffen. The Concurrency Workbench: A semantics-based tool for the verification of finite-state systems. ACM TOPLAS, 15(1):36–72, Jan. 1993.
R. Cleaveland and S. Sims. The NCSU ConcurrencyWorkbench. In Computer Aided Verification (CAV’ 96), vol. 1102 of LNCS, pages 394–397, Jul. 1996.
R. Cleaveland and S. Sims. Generic tools for verifying concurrent systems. Science of Computer Programming, 42(1):39–47, Jan. 2002.
H. Garavel and H. Hermanns. On combining functional verification and performance evaluation using CADP. In FME, vol. 2391 of LNCS, pages 410–429, 2002.
N. Lynch and M. Tuttle. Hierarchical correctness proofs for distributed algorithms. In 6th ACM PODC, pages 137–151, 1987.
E. Stark and G. Pemmasani. Implementation of a compositional performance analysis algorithm for probabilistic I/O automata. In 7th PAPM, pages 3–24, 1999.
E. Stark and S. Smolka. Compositional analysis of expected delays in networks of probabilistic I/O automata. In Proc. 13th LICS, pages 466–477, Jun. 1998.
E. Stark, S. Smolka, and R. Cleaveland. Aprocess-algebraic language for PIOA. Unpublished draft, 2003.
E. Stark. Compositional performance analysis using probabilistic I/O automata. In CONCUR 2000, vol. 1877 of LNCS, pages 25–28, Aug. 2000.
W. Stewart. Introduction to the Numerical Solution of Markov Chains. Princeton University Presss, 1994.
S. Wu, S. Smolka, and E. Stark. Composition and behaviors of probabilistic I/O automata. Theoretical Computer Science, 176(1-2):1–38, Apr. 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhang, D., Cleaveland, R., Stark, E.W. (2003). The Integrated CWB-NC/PIOATool for Functional Verification and Performance Analysis of Concurrent Systems. In: Garavel, H., Hatcliff, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2003. Lecture Notes in Computer Science, vol 2619. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36577-X_31
Download citation
DOI: https://doi.org/10.1007/3-540-36577-X_31
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00898-9
Online ISBN: 978-3-540-36577-8
eBook Packages: Springer Book Archive