Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Mobile Networks and Applications
Erschienen in: Mobile Networks and Applications 1/2019

29.09.2018

Formal Verification of mCWQ Using Extended Hoare Logic

verfasst von: Wanling Xie, Huibiao Zhu, Xi Wu, Phan Cong Vinh

Erschienen in: Mobile Networks and Applications | Ausgabe 1/2019

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Node mobility, as one of the most important features of Wireless Sensor Networks (WSNs), may affect the reliability of communication links in the networks, leading to abnormalities and decreasing the quality of service provided by WSNs. The mCWQ calculus (i.e., CWQ calculus with mobility) is recently proposed to capture the feature of node mobility and increase the communication quality of WSNs. In this paper, we present a proof system for the mCWQ calculus to prove its correctness. Our specifications and verifications are based on Hoare Logic. In order to describe the timing of observable actions, we extend the assertion language with primitives. And terminating and non-terminating computations both can be described in our proof system. We also give some examples to illustrate the application of our proof system.
Vorheriger Artikel An Approach to Modeling and Estimating Power Consumption of Mobile Applications
Nächster Artikel A Comparative Study of Consumers’ Purchase Intention on Different Internet Platforms

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Weitere Produktempfehlungen anzeigen
Literatur
1.
Akyildiz IF, Su W, Sankarasubramaniam Y, Cayirci E (2002) Wireless sensor networks: a survey. Comput Netw 38(4):393–422CrossRef
2.
Apt KR, de Boer FS, Olderog E (2009) Verification of sequential and concurrent programs. Texts in computer science. Springer
3.
4.
Barthe G, Gaboardi M, Arias EJG, Hsu J, Kunz C, Strub P (2014) Proving differential privacy in hoare logic. In: IEEE 27th Computer security foundations symposium, CSF 2014, Vienna, Austria, 19-22 July 2014, pp 411–424
5.
6.
de Boer FS (2002) A hoare logic for dynamic networks of asynchronously communicating deterministic processes. Theor Comput Sci 274(1-2):3–41MathSciNetCrossRef
7.
Camp T, Boleng J, Davies V (2002) A survey of mobility models for ad hoc network research. Wirel Commun Mob Comput 2(5):483–502CrossRef
8.
Duran A, Cavalcanti A, Sampaio A (2010) An algebraic approach to the design of compilers for object-oriented languages. Formal Asp Comput 22(5):489–535CrossRef
9.
Ene C, Muntean T (2001) A broadcast-based calculus for communicating systems. In: Proceedings of the 15th international parallel & distributed processing symposium (IPDPS-01). San Francisco, CA, April 23–27, 2001, p 149
10.
Fehnker A, van Glabbeek RJ, Höfner P, McIver A, Portmann M, Tan WL (2012) A process algebra for wireless mesh networks. In: Programming languages and systems - 21st European symposium on programming, ESOP 2012. Held as Part of the European joint conferences on theory and practice of software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, pp 295–315
11.
Ghassemi F, Fokkink W, Movaghar A (2008) Restricted broadcast process theory. In: Sixth IEEE International conference on software engineering and formal methods, SEFM 2008. Cape Town, South Africa, 10-14 November 2008, pp 345–354
12.
Godskesen JC (2007) A calculus for mobile ad hoc networks. In: Coordination models and languages, 9th international conference, coordination 2007. Paphos, Cyprus, June 6-8, 2007, Proceedings, pp 132–150
13.
Godskesen JC, Nanz S (2009) Mobility models and behavioural equivalence for wireless networks. In: Coordination models and languages, 11th international conference, coordination 2009. Lisboa, Portugal, June 9-12, 2009. Proceedings, pp 106–122
14.
He J (1994) Provably correct systems: modelling of communication languages and design of optimized compilers. The McGraw-Hill International Series in Software Engineering
15.
16.
He J, Zhao X (2016) Reasoning about actions with loops via hoare logic. Front Comput Sci 10(5):870–888CrossRef
17.
Hennessy M (1988) Algebraic theory of processes. MIT Press series in the foundations of computing, MIT Press
18.
Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576–580CrossRef
19.
Hoare CAR (1985) Communicating sequential processes. Prentice-Hall
20.
Hoare CAR, He J (1998) Unifying theories of programming. Prentice Hall International Series in Computer Science
21.
Hoare CAR, Hayes IJ, He J, Morgan C, Roscoe AW, Sanders JW, Sørensen IH, Spivey JM, Sufrin B (1987) Laws of programming. Commun ACM 30(8):672–686MathSciNetCrossRef
22.
23.
Hoare T (2013) Unifying semantics for concurrent programming. In: Computation, logic, games, and quantum foundations. The many facets of Samson Abramsky - essays dedicated to Samson Abramsky on the occasion of his 60th birthday, pp 139–149
24.
25.
Hooman J (1991) Compositional verification of real-time systems using extended hoare triples. In: Real-time: theory in practice, REX workshop. Mook, The Netherlands, June 3–7, 1991, Proceedings, pp 252–290
26.
Hooman J (1994) Extending hoare logic to real-time. Formal Asp Comput 6(6A):801–826CrossRef
27.
Lanese I, Sangiorgi D (2010) An operational semantics for a calculus for wireless systems. Theor Comput Sci 411(19):1928–1948MathSciNetCrossRef
28.
Lee EA (2015) Architectural support for cyber-physical systems. In: Proceedings of the twentieth international conference on architectural support for programming languages and operating systems, ASPLOS ’15. Istanbul, Turkey, March 14-18, 2015, p 1
29.
Luo C, Qin S, Qiu Z (2008) Verifying bpel-like programs with hoare logic. Front Comput Sci Chin 2 (4):344–356CrossRef
30.
Merro M (2009) An observational theory for mobile ad hoc networks (full version). Inf Comput 207(2):194–208MathSciNetCrossRef
31.
Merro M, Ballardin F, Sibilio E (2011) A timed calculus for wireless systems. Theor Comput Sci 412 (47):6585–6611MathSciNetCrossRef
32.
Milner R (1980) A calculus of communicating systems, lecture notes in computer science, vol 92. Springer
33.
Milner R (1999) Communicating and mobile systems - the Pi-calculus. Cambridge University Press
34.
Nanz S, Hankin C (2006) Formal security analysis for ad-hoc networks. Electr Notes Theor Comput Sci 142:195–213CrossRef
35.
Nielson HR, Nielson F, Vigo R (2012) A calculus for quality. In: Formal aspects of component software, 9th international symposium, FACS 2012. Mountain View, CA, USA, September 12-14, 2012. Revised Selected Papers, pp 188–204
36.
37.
Perkins CE (1999) Belding-Royer EM Ad-hoc on-demand distance vector routing. In: 2nd Workshop on mobile computing systems and applications (WMCSA ’99), February 25-26, 1999. New Orleans, LA, USA, pp 90-100
38.
39.
40.
Rappaport TS (1996) Wireless communications - principles and practice. Prentice Hall
41.
Santi P (2005) Topology control in wireless ad hoc and sensor networks. ACM Comput Surv 37(2):164–194CrossRef
42.
Song L, Godskesen JC (2010) Probabilistic mobility models for mobile and wireless networks. In: Theoretical computer science - 6th IFIP TC 1/WG 2.2 international conference, TCS 2010, Held as Part of WCC 2010, Brisbane, Australia, September 20-23, 2010. Proceedings, pp 86–100
43.
Stoy JE (1979) Foundations of denotational semantics. In: Abstract software specifications, 1979 Copenhagen Winter School, January 22 - February 2, 1979, Proceedings, pp 43–99
44.
Wu X, Zhu H (2015) A calculus for wireless sensor networks from quality perspective. In: 16th IEEE International symposium on high assurance systems engineering, HASE 2015, Daytona Beach, FL, USA, January 8-10, 2015, pp 223–231
45.
Wu X, Zhao Y, Zhu H (2016) Integrating a calculus with mobility and quality for wireless sensor networks. In: 17th IEEE International symposium on high assurance systems engineering, HASE 2016, Orlando, FL, USA, January 7-9, 2016, pp 220–227
46.
Xie W, Wu X, Zhu H, Lu G, Liu A (2017) A proof system for mCWQ. In: Proc. COMPSAC 2017: 41st IEEE computer society signature conference on computers, software and applications, pp 45–50
Metadaten
Titel
Formal Verification of mCWQ Using Extended Hoare Logic
verfasst von
Wanling Xie
Huibiao Zhu
Xi Wu
Phan Cong Vinh
Publikationsdatum
29.09.2018
Verlag
Springer US
Erschienen in
Mobile Networks and Applications / Ausgabe 1/2019
Print ISSN: 1383-469X
Elektronische ISSN: 1572-8153
DOI
https://doi.org/10.1007/s11036-018-1142-8

Weitere Artikel der Ausgabe 1/2019

Mobile Networks and Applications 1/2019 Zur Ausgabe

OriginalPaper

Key Technologies and Solutions of Remote Distributed Virtual Laboratory for E-Learning and E-Education

OriginalPaper

Data Transmission Using IoT in Vehicular Ad-Hoc Networks in Smart City Congestion

OriginalPaper

A Robust Parallel Object Tracking Method for Illumination Variations

EditorialNotes

Introduction of Key Problems in Long-Distance Learning and Training

OriginalPaper

An IoT Service Aggregation Method Based on Dynamic Planning for QoE Restraints

OriginalPaper

Effective Big Data Retrieval Using Deep Learning Modified Neural Networks

Neuer Inhalt

    Bildnachweise