Abstract
Wireless technology has been widely used in various wireless network scenarios and applications. To model and analyze wireless systems, a calculus of wireless system called CWS has been introduced. In this paper, we put forward an assertion-based reasoning method for this calculus in order to support the verification of the correctness and some interesting properties of wireless system. To simplify the complexity of verification, we first present the assertion-based verification rules for processes separately. Due to the features of wireless system (e.g., broadcast, synchrony, interference), cooperation rules are introduced to combine the processes into a complete system. Finally, there is a case study about using our method to analyze and prove the correctness of Stop-and-Wait ARQ Protocol as well as some properties.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Willig, A., Matheus, K., Wolisz, A.: Wireless technology in industrial networks. Proc. IEEE 93(6), 1130–1151 (2005)
Fratu, O., Pejanovic-Djurisic, M., Poulkov, V., Gavrilovska, L.: Introduction to special issue “current trends in information and communications technology”. Wireless Pers. Commun. 87(3), 615–617 (2016)
Prasad, K.V.S.: A calculus of broadcasting systems. Sci. Comput. Program. 25(2–3), 285–327 (1995)
Lanese, I., Sangiorgi, D.: An operational semantics for a calculus for wireless systems. Theor. Comput. Sci. 411(19), 1928–1948 (2010)
Godskesen, J.C.: A calculus for mobile ad hoc networks. In: Murphy, A.L., Vitek, J. (eds.) COORDINATION 2007. LNCS, vol. 4467, pp. 132–150. Springer, Heidelberg (2007). doi:10.1007/978-3-540-72794-1_8
Merro, M.: An observational theory for mobile ad hoc networks (full version). Inf. Comput. 207(2), 194–208 (2009)
Nanz, S., Hankin, C.: Formal security analysis for ad-hoc networks. Electr. Notes Theor. Comput. Sci. 142, 195–213 (2006)
Apt, K.R., de Boer, F.S., Olderog, E.: Verification of sequential and concurrent programs. In: Apt, K.R., de Boer, F.S., Olderog, E. (eds.) Texts in Computer Science. Springer, Heidelberg (2009)
Xu, Q., de Roever, W.P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Formal Asp. Comput. 9(2), 149–174 (1997)
Goguen, H.: Soundness of the logical framework for its typed operational semantic. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol. 1581, pp. 177–197. Springer, Heidelberg (1999). doi:10.1007/3-540-48959-2_14
Mezzetti, N., Sangiorgi, D.: Towards a calculus for wireless systems. Electr. Notes Theor. Comput. Sci. 158, 331–353 (2006)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)
Gallier, J.: Mathematical reasoning, proof principles, and logic. In: Gallier, J. (ed.) Discrete Mathematics. Springer, New York (2011)
De Vuyst, S., Tworus, K., Wittevrongel, S., Bruneel, H.: Analysis of stop-and-wait ARQ for a wireless channel. 4OR 7(1), 61–78 (2008)
Wu, J., Fan, P.: A survey on high mobility wireless communications: challenges, opportunities and solutions. IEEE Access 4, 450–476 (2016)
Wu, X., Zhu, H., Wu, X.: Observation-oriented semantics for calculus of wireless systems. In: Naumann, D. (ed.) UTP 2014. LNCS, vol. 8963, pp. 105–124. Springer, Cham (2015). doi:10.1007/978-3-319-14806-9_6
Hoare, C.A.R.: Algebra of concurrent programming. In: Meeting 52 of WG 2.3. (2011)
Acknowledgment
This work was partly supported by the Danish National Research Foundation and the National Natural Science Foundation of China (Grant No. 61361136002) for the Danish-Chinese Center for Cyber Physical Systems. It was also supported by Shanghai Collaborative Innovation Center of Trustworthy Software for Internet of Things (No. ZF1213).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this chapter
Cite this chapter
Wang, L., Xie, W., Zhu, H. (2017). Assertion-Based Reasoning Method for Calculus of Wireless System. In: Aceto, L., Bacci, G., Bacci, G., Ingólfsdóttir, A., Legay, A., Mardare, R. (eds) Models, Algorithms, Logics and Tools. Lecture Notes in Computer Science(), vol 10460. Springer, Cham. https://doi.org/10.1007/978-3-319-63121-9_24
Download citation
DOI: https://doi.org/10.1007/978-3-319-63121-9_24
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-63120-2
Online ISBN: 978-3-319-63121-9
eBook Packages: Computer ScienceComputer Science (R0)