Introduction to special section on formal methods in pervasive computing

Mohamed Bakhouya, R H Campbell, Antonio Coronato, Giuseppe De Pietro, Anand Ranganathan

Research output: Contribution to journalReview article

Abstract

Ubiquitous and pervasive applications may present critical requirements from the point of view of functional correctness, reliability, availability, security, and safety. Unlike traditional safety-critical applications, the behavior of ubiquitous and pervasive applications is affected by the movements and location of users and resources. In this article, we first present emerging formal methods for the description of both entities and their behavior in pervasive computing environments; then, we introduce this special issue. Despite many previous works that have focused on modeling the entities, relatively few have concentrated on modeling or verifying behaviors; and almost none has dealt with combining techniques proposed in these two aspects. The articles accepted in this special issue cover some of the topics aforementioned and constitute a representative sample of the latest development of formal methods in pervasive computing environments.

Original languageEnglish (US)
Article number6
JournalACM Transactions on Autonomous and Adaptive Systems
Volume7
Issue number1
DOIs
StatePublished - Apr 2012

Fingerprint

Formal methods
Ubiquitous computing
Availability

Keywords

  • Formal specification and verification
  • Methodologies and tools
  • Ubiquitous and pervasive safetycritical applications

ASJC Scopus subject areas

  • Control and Systems Engineering
  • Software
  • Computer Science (miscellaneous)

Cite this

Introduction to special section on formal methods in pervasive computing. / Bakhouya, Mohamed; Campbell, R H; Coronato, Antonio; De Pietro, Giuseppe; Ranganathan, Anand.

In: ACM Transactions on Autonomous and Adaptive Systems, Vol. 7, No. 1, 6, 04.2012.

Research output: Contribution to journalReview article

Bakhouya, Mohamed ; Campbell, R H ; Coronato, Antonio ; De Pietro, Giuseppe ; Ranganathan, Anand. / Introduction to special section on formal methods in pervasive computing. In: ACM Transactions on Autonomous and Adaptive Systems. 2012 ; Vol. 7, No. 1.
@article{eaf7350258a0443ba4a6e2c354b3ea76,
title = "Introduction to special section on formal methods in pervasive computing",
abstract = "Ubiquitous and pervasive applications may present critical requirements from the point of view of functional correctness, reliability, availability, security, and safety. Unlike traditional safety-critical applications, the behavior of ubiquitous and pervasive applications is affected by the movements and location of users and resources. In this article, we first present emerging formal methods for the description of both entities and their behavior in pervasive computing environments; then, we introduce this special issue. Despite many previous works that have focused on modeling the entities, relatively few have concentrated on modeling or verifying behaviors; and almost none has dealt with combining techniques proposed in these two aspects. The articles accepted in this special issue cover some of the topics aforementioned and constitute a representative sample of the latest development of formal methods in pervasive computing environments.",
keywords = "Formal specification and verification, Methodologies and tools, Ubiquitous and pervasive safetycritical applications",
author = "Mohamed Bakhouya and Campbell, {R H} and Antonio Coronato and {De Pietro}, Giuseppe and Anand Ranganathan",
year = "2012",
month = "4",
doi = "10.1145/2168260.2168266",
language = "English (US)",
volume = "7",
journal = "ACM Transactions on Autonomous and Adaptive Systems",
issn = "1556-4665",
publisher = "Association for Computing Machinery (ACM)",
number = "1",

}

TY - JOUR

T1 - Introduction to special section on formal methods in pervasive computing

AU - Bakhouya, Mohamed

AU - Campbell, R H

AU - Coronato, Antonio

AU - De Pietro, Giuseppe

AU - Ranganathan, Anand

PY - 2012/4

Y1 - 2012/4

N2 - Ubiquitous and pervasive applications may present critical requirements from the point of view of functional correctness, reliability, availability, security, and safety. Unlike traditional safety-critical applications, the behavior of ubiquitous and pervasive applications is affected by the movements and location of users and resources. In this article, we first present emerging formal methods for the description of both entities and their behavior in pervasive computing environments; then, we introduce this special issue. Despite many previous works that have focused on modeling the entities, relatively few have concentrated on modeling or verifying behaviors; and almost none has dealt with combining techniques proposed in these two aspects. The articles accepted in this special issue cover some of the topics aforementioned and constitute a representative sample of the latest development of formal methods in pervasive computing environments.

AB - Ubiquitous and pervasive applications may present critical requirements from the point of view of functional correctness, reliability, availability, security, and safety. Unlike traditional safety-critical applications, the behavior of ubiquitous and pervasive applications is affected by the movements and location of users and resources. In this article, we first present emerging formal methods for the description of both entities and their behavior in pervasive computing environments; then, we introduce this special issue. Despite many previous works that have focused on modeling the entities, relatively few have concentrated on modeling or verifying behaviors; and almost none has dealt with combining techniques proposed in these two aspects. The articles accepted in this special issue cover some of the topics aforementioned and constitute a representative sample of the latest development of formal methods in pervasive computing environments.

KW - Formal specification and verification

KW - Methodologies and tools

KW - Ubiquitous and pervasive safetycritical applications

UR - http://www.scopus.com/inward/record.url?scp=84862104324&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84862104324&partnerID=8YFLogxK

U2 - 10.1145/2168260.2168266

DO - 10.1145/2168260.2168266

M3 - Review article

AN - SCOPUS:84862104324

VL - 7

JO - ACM Transactions on Autonomous and Adaptive Systems

JF - ACM Transactions on Autonomous and Adaptive Systems

SN - 1556-4665

IS - 1

M1 - 6

ER -