TY - GEN
T1 - Linking operational semantics and algebraic semantics for wireless networks
AU - Wu, Xiaofeng
AU - Zhu, Huibiao
PY - 2013
Y1 - 2013
N2 - Wireless technology has achieved lots of applications in computer networks. To model and analyze wireless systems, a calculus called CWS and its operational semantics have been investigated. This paper considers the linking between the algebraic semantics and the operational semantics for this calculus. Our approach is to derive the operational semantics from the algebraic semantics. Firstly we present the algebraic semantics and introduce the concept of head normal form. Secondly we present the strategy of deriving the operational semantics from the algebraic semantics. Based on the strategy, an operational semantics is derived, which shows that the operational semantics is sound with respect to the algebraic semantics. Then the equivalence between the derivation strategy and the derived transition system is proved. This shows the completeness of the derived operational semantics. Finally, we investigate the mechanical approach to our linking method using the equational and rewriting logic system Maude. We mechanize the algebraic laws, the derivation strategy and the derived operational semantics.
AB - Wireless technology has achieved lots of applications in computer networks. To model and analyze wireless systems, a calculus called CWS and its operational semantics have been investigated. This paper considers the linking between the algebraic semantics and the operational semantics for this calculus. Our approach is to derive the operational semantics from the algebraic semantics. Firstly we present the algebraic semantics and introduce the concept of head normal form. Secondly we present the strategy of deriving the operational semantics from the algebraic semantics. Based on the strategy, an operational semantics is derived, which shows that the operational semantics is sound with respect to the algebraic semantics. Then the equivalence between the derivation strategy and the derived transition system is proved. This shows the completeness of the derived operational semantics. Finally, we investigate the mechanical approach to our linking method using the equational and rewriting logic system Maude. We mechanize the algebraic laws, the derivation strategy and the derived operational semantics.
UR - https://www.scopus.com/pages/publications/84889566960
U2 - 10.1007/978-3-642-41202-8_25
DO - 10.1007/978-3-642-41202-8_25
M3 - 会议稿件
AN - SCOPUS:84889566960
SN - 9783642412011
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 380
EP - 396
BT - Formal Methods and Software Engineering - 15th International Conference on Formal Engineering Methods, ICFEM 2013, Proceedings
T2 - 15th International Conference on Formal Engineering Methods, ICFEM 2013
Y2 - 29 October 2013 through 1 November 2013
ER -