Formal Analysis and Verification of Timing and Resource Adaptability for Internetware

doi:10.23940/ijpe.18.08.p16.17961803

Abstract

Abstract:

To address the trustworthiness of Internetware under open and dynamic environments, this paper proposes an approach to verify whether Internetware is satisfied with timing and resource constraints. Firstly, interface automata are extended with time and resource semantics. Then, timing and resource interface automata is used to model the behaviors of a software component. An algorithm is also provided to check whether all behaviors of an Internetware system are satisfied with resource constraints within a specified time. Finally, an online bookstore system is employed to illustrate our work, and the model checker Spin is used to verify the correctness of our approach.

Submitted on May 11, 2018; Revised on June 16, 2018; Accepted on July 17, 2018
References: 16

Zhongqun Wang, Jun Li, and Qi Xia. Formal Analysis and Verification of Timing and Resource Adaptability for Internetware [J]. Int J Performability Eng, 2018, 14(8): 1796-1803.

Add to citation manager EndNote|Reference Manager|ProCite|BibTeX|RefWorks

References 0

	H. Mei and J. Lü, “On Environment-Driven Software Model for Internetware,” Internetware, pp. 33-69, Springer, Singapore, 2016
	H. Mei and J. Lü, “Internetware: A Shift of Software Paradigm,” Internetware, pp. 3-17, Springer, Singapore, 2016
	T. Xie, A. V. Hoorn, H. Wang, and I. Weber, “Introduction to the Special Issue on Emerging Software Technologies for Internet-based Systems: Internetware and DevOps,” ACM Transactions on Internet Technology (TOIT), Vol. 18, No. 2, pp. 13, 2018
	L. de Alfaro, T. A. Henzinger, and M. Stoelinga, “Timed Interfaces,” pp. 208-122, Vinena: Springer-Verlag, 2002
	A. Chakrabarti, L. de Alfaro, and T. A. Henzinger, “Resource Interfaces,” pp. 117-133, Berlin: Springer-Verlag, 2003
	J. Hu, Z. Q. Huang, D. Cao, and B. F. Xu, “Formal Analysis and Verification of Resource Adaptability for Internetware,” Journal of Software, Vol. 19, No. 5, pp. 1186-1200, 2008
	J. Zhang and H. Lei, “Algorithm for Computing Reliability Evolution of Internetware,” Journal of Southwest Jiaotong University, Vol. 49, No. 2, pp. 311-318, 2014
	X. Q. Xie, J. A. Zhou, D. A. Zhang, and Q. J. Xie, “Research on Trust Model of Internetware based on Complex Network,” Journal of Frontiers of Computer Science and Technology, Vol. 10, No. 1, pp. 56-64, 2016
	Z. Wei, M. Fan, M. Song, H. Wang, and Z. Zhang, “Analysis on the Technology of the Internetware Comprehensive Testing,” Advances in Computer Science and Ubiquitous Computing, pp. 573-578, Springer, Singapore, 2017
	E. D. L. Vitrand, X. Zuo, H. Yu, and S. Zheng, “An Approach to Evolving Internetware Application,” in Proceedings of International Symposium on Advances in Electrical, Electronics and Computer Engineering, 2017
	S. Y. Bao and Z. Q. Wang, “Business Consistency Verification Approach of Internetware Evolution,” Computer Engineering, Vol. 37, No. 17, pp. 29-31, September 2011
	Q. Xia and Z. Q. Wang, “Formal Analysis and Verification of Randomness Resources for Internetware,” Journal of Computer Applications, Vol. 32, No. 11, pp. 3067-3070, November 2012
	H. A. Sang, M. Q. Zhang, and J. Tang, “A Validation Method of Simulation Component Interface Design based on Reachability Chart,” Computer Simulation, Vol. 27, No. 4, pp. 75-79, April 2010
	M. Ben-ari, “Principles of the Spin Model Checking,” Springer-Verlag, London, 2008
	G. Honlzmann, “Spin Model Checker: Primer and Reference Manual,” Addison-Wesley Publishing Company, Boston, USA, January 2004
	L. Tan and H. W. Zeng, “Interface Automata-based Verification for Web Applications,” Computer Engineering and Applications, Vol. 45, No. 3, pp. 70-73, March 2009