Behavioral Compatibility Analysis of Component-based Real-time System

Full Text (PDF, 222KB), PP.70-76

Views: 0 Downloads: 0


Lin Xi 1 Qinglei Zhou 1

1. Zhengzhou University, Zhengzhou, China

* Corresponding author.


Received: 13 Oct. 2010 / Revised: 25 Nov. 2010 / Accepted: 3 Jan. 2011 / Published: 8 Feb. 2011

Index Terms

Behavioral compatibility, component-based real-time system, timed automata, UPPAAL


For verification of component behavior compatibility in component-based real-time system, we make use of the timed automata to formally describe the component. In this way, the problem of component behavior compatibility is equivalent to whether the complementary actions can really synchronize over common channels on the system’s TA models. We then use the verification function of UPPAAL to automatically generate result, and finally conduct a case study to demonstrate how our technique works.

Cite This Paper

Lin Xi, Qinglei Zhou,"Behavioral Compatibility Analysis of Component-based Real-time System", IJEM, vol.1, no.1, pp.70-76, 2011. DOI: 10.5815/ijem.2011.01.11


[1] W. Aalst,K. Hee,R. Toom. Component-Based software architectures: A framework based on inheritance of behavior. Science of Computer Programming, 42:129一171,2002.

[2] M. Bemardo,P.Ciancarini ,L. Donatiello. Architecting families of software systems with process algebras. ACM Transactions on Software Engineering and Methodology,11(4):386-426,2002.

[3] P. Inverardi, A.Wolf. Formal specification and analysis of software architectures using the chemical abstract machine model. IEEE Transactions on Software Engineering,21(4):373-386,1995.

[4] R. Allen, D. Garlan. A formal basis for architectural connection. ACM Transactions on Software Engineering and Methodology,6(3):213-249,July 1997.

[5] A. Aldini,M. Bernardo. On the usability of Process algebra: An architectural view. Theoretical Computer Science,335:281-329,2005.

[6] N. Medvidovic, D. Rosenblum, and R. Taylor. A language and environment for architecture-based software development and evolution. In Proceedings of the 21st ACM International Conference on Software Engineering, 1999.

[7] H. Mei, L. Zhang, F. Yang. A component-based software configuration management model and its supporting system. Journal of Computer Science and Technology. 17(4), July, 2002.

[8] Y. Lin and S. Reiss. Configuration management with logical structures. In Proceedings 18th ACM International Conference on Software Engineering, 1996.

[9] C. Szyersky, D. Gruntz, S .Murer. Component software: Beyond object-oriented Programming. 2nd. Massachusetts: Addison-Wesley Professional,2002.

[10] A. Vallecillo,J. Hemandez,and J. Troya. New issues in object interoperability. In Proc. Of the ECOOP 2000 Workshop on Object Interoperability. LNCS 1964: 256-269,France,2000.

[11] Jin Xian-li. Research on the Formalization of Semantic Features and Behavior Composition for Real-Time Service Component (in Chinese). Ph.D. Thesis,Beijing University of Posts and Telecommunications,2007.

[12] A. David, W. Yi. Hierarchical timed automata for UPPAAL.10th Nordic Workshop on Programming Theory (NWPT’98). Turku Center for Computer Science (TUCS), Finland, 1998.

[13] R.Alur, D.L.Dill. A theory of timed automata. Theoretical Computer Science, 1994. 126:183-235.

[14] R.Alur. Timed Automata. 11th International conference on Computer-Aided Verification, CAV’99. Trento, Italy, Lecture Notes in Computer Science, Springer-Verlag Berlin Heidelberg, LNCS 1633, pp.8-22.

[15] Johan Bengtsson, Fredrik Larsson, Fredrik Larson, paul Pettersson, and Wang Yi.UPPAAL-a Tool for Automatic Verification of Real-time Systems[C]. Proceedings of the DIMACS/SYCON workshop on Verification and control of Hybrid systems Ⅲ.Springer-Verlag New York,October 1995. pages 232-243.