Abstract
This paper presents the VCS verification tool for the BIP modeling language. The tool admits sophisticated interactions specified in BIP models. Particularly, private variables in components can be updated by user-defined interactions. On the verification back-end, the BIP models are formulated as transition systems. Several efficient algorithms are proposed for verification of transition systems on safety properties. Experimental results show very promising performance of VCS. It runs several magnitudes faster than NuSMV for a variety of examples.
This work was supported by the National 973 Plan (No. 2010CB328003), the NSF of China (No. 61272001, 60903030, 91218302), the Chinese National Key Technology R&D Program (No. SQ2012BAJY4052), the NSC 101-2221-E-001-007, and the Tsinghua University Initiative Scientific Research Program.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Feiler, P.H.: The architecture analysis & design language (AADL): An introduction. Technical report, CMU/SEI-2006-TN-011 (2006)
Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in bip. In: SEFM 2006, pp. 3–12. IEEE (2006)
Bensalem, S., Bozga, M., Nguyen, T.-H., Sifakis, J.: D-finder: A tool for compositional deadlock detection and verification. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 614–619. Springer, Heidelberg (2009)
Bozga, M., Jaber, M., Sifakis, J.: Source-to-source architecture transformation for performance optimization in bip. IEEE Transactions on Industrial Informatics 5(4), 708–718 (2010)
Yin, L., He, F., Gu, M.: Optimizing the sat decision ordering of bounded model checking by structural information. In: Proceedings of the 7th International Symposium on Theoretical Aspects of Software Engineering, TASE (2013)
Eén, N., Sorensson, N.: Temporal induction by incremental sat solving. Electronic Notes in Theoretical Computer Science 89(4), 543–560 (2003)
Wan, H., Huang, C., Wang, Y., He, F., Gu, M., Chen, R., Marius, B.: Modeling and validation of a data process unit control for space applications. In: Embedded Real Time Software and Systems (2012)
Wang, R., Zhou, M., Yin, L., Zhang, L., Gu, M., Sun, J., Bozga, M.: Modeling and validation of plc-controlled system: A case study. Technical report, Tsinghua University (2011)
Cha, G., Gu, T.: Formal Analysis and Design of Network Protocols (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing Switzerland
About this paper
Cite this paper
He, F., Yin, L., Wang, BY., Zhang, L., Mu, G., Meng, W. (2013). VCS: A Verifier for Component-Based Systems. In: Van Hung, D., Ogawa, M. (eds) Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol 8172. Springer, Cham. https://doi.org/10.1007/978-3-319-02444-8_39
Download citation
DOI: https://doi.org/10.1007/978-3-319-02444-8_39
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-02443-1
Online ISBN: 978-3-319-02444-8
eBook Packages: Computer ScienceComputer Science (R0)