Validation, Verification, and Formal Methods for Cyber-Physical Systems

Research output: Chapter in Book/Report/Conference proceedingChapter

1 Citation (Scopus)

Abstract

Cyber-physical systems (CPSs), such as smart grids, unmanned aerial vehicles, and medical devices, are complex systems consisting of networks of computing units that interact in a stochastic manner with their physical environment. This interaction between the networked computing system and the physical environment gives rise to unexpected configurations also known as aggregate effects, which is not observed when the CPS components are standalone. Hypoglycemia control using multidrug infusion is a beneficial effect. However, uncontrolled aggregate effects can have dire consequences for the physical system. For example, chemotherapeutic drug interaction can kill healthy cells and selforganization in smart grids can result in large scale spread of critical failure. Thus, characterization and analysis of aggregate effect is essential for designing safe CPSs. This chapter will discuss the formal methods available for characterizing aggregate effects in CPSs and the verification and validation of models of CPSs.

Original languageEnglish (US)
Title of host publicationCyber-Physical Systems
Subtitle of host publicationFoundations, Principles and Applications
PublisherElsevier Inc.
Pages175-191
Number of pages17
ISBN (Electronic)9780128038741
ISBN (Print)9780128038017
DOIs
StatePublished - Sep 11 2016

Fingerprint

Formal methods
Drug interactions
Unmanned aerial vehicles (UAV)
Large scale systems
Cells
Cyber Physical System

Keywords

  • Aggregate effects
  • Emergent behavior
  • Formal methods

ASJC Scopus subject areas

  • Computer Science(all)

Cite this

Bagade, P., Banerjee, A., & Gupta, S. (2016). Validation, Verification, and Formal Methods for Cyber-Physical Systems. In Cyber-Physical Systems: Foundations, Principles and Applications (pp. 175-191). Elsevier Inc.. https://doi.org/10.1016/B978-0-12-803801-7.00012-2

Validation, Verification, and Formal Methods for Cyber-Physical Systems. / Bagade, P.; Banerjee, Ayan; Gupta, Sandeep.

Cyber-Physical Systems: Foundations, Principles and Applications. Elsevier Inc., 2016. p. 175-191.

Research output: Chapter in Book/Report/Conference proceedingChapter

Bagade, P, Banerjee, A & Gupta, S 2016, Validation, Verification, and Formal Methods for Cyber-Physical Systems. in Cyber-Physical Systems: Foundations, Principles and Applications. Elsevier Inc., pp. 175-191. https://doi.org/10.1016/B978-0-12-803801-7.00012-2
Bagade P, Banerjee A, Gupta S. Validation, Verification, and Formal Methods for Cyber-Physical Systems. In Cyber-Physical Systems: Foundations, Principles and Applications. Elsevier Inc. 2016. p. 175-191 https://doi.org/10.1016/B978-0-12-803801-7.00012-2
Bagade, P. ; Banerjee, Ayan ; Gupta, Sandeep. / Validation, Verification, and Formal Methods for Cyber-Physical Systems. Cyber-Physical Systems: Foundations, Principles and Applications. Elsevier Inc., 2016. pp. 175-191
@inbook{8179cfc762774a92b66b7f2eb103c746,
title = "Validation, Verification, and Formal Methods for Cyber-Physical Systems",
abstract = "Cyber-physical systems (CPSs), such as smart grids, unmanned aerial vehicles, and medical devices, are complex systems consisting of networks of computing units that interact in a stochastic manner with their physical environment. This interaction between the networked computing system and the physical environment gives rise to unexpected configurations also known as aggregate effects, which is not observed when the CPS components are standalone. Hypoglycemia control using multidrug infusion is a beneficial effect. However, uncontrolled aggregate effects can have dire consequences for the physical system. For example, chemotherapeutic drug interaction can kill healthy cells and selforganization in smart grids can result in large scale spread of critical failure. Thus, characterization and analysis of aggregate effect is essential for designing safe CPSs. This chapter will discuss the formal methods available for characterizing aggregate effects in CPSs and the verification and validation of models of CPSs.",
keywords = "Aggregate effects, Emergent behavior, Formal methods",
author = "P. Bagade and Ayan Banerjee and Sandeep Gupta",
year = "2016",
month = "9",
day = "11",
doi = "10.1016/B978-0-12-803801-7.00012-2",
language = "English (US)",
isbn = "9780128038017",
pages = "175--191",
booktitle = "Cyber-Physical Systems",
publisher = "Elsevier Inc.",

}

TY - CHAP

T1 - Validation, Verification, and Formal Methods for Cyber-Physical Systems

AU - Bagade, P.

AU - Banerjee, Ayan

AU - Gupta, Sandeep

PY - 2016/9/11

Y1 - 2016/9/11

N2 - Cyber-physical systems (CPSs), such as smart grids, unmanned aerial vehicles, and medical devices, are complex systems consisting of networks of computing units that interact in a stochastic manner with their physical environment. This interaction between the networked computing system and the physical environment gives rise to unexpected configurations also known as aggregate effects, which is not observed when the CPS components are standalone. Hypoglycemia control using multidrug infusion is a beneficial effect. However, uncontrolled aggregate effects can have dire consequences for the physical system. For example, chemotherapeutic drug interaction can kill healthy cells and selforganization in smart grids can result in large scale spread of critical failure. Thus, characterization and analysis of aggregate effect is essential for designing safe CPSs. This chapter will discuss the formal methods available for characterizing aggregate effects in CPSs and the verification and validation of models of CPSs.

AB - Cyber-physical systems (CPSs), such as smart grids, unmanned aerial vehicles, and medical devices, are complex systems consisting of networks of computing units that interact in a stochastic manner with their physical environment. This interaction between the networked computing system and the physical environment gives rise to unexpected configurations also known as aggregate effects, which is not observed when the CPS components are standalone. Hypoglycemia control using multidrug infusion is a beneficial effect. However, uncontrolled aggregate effects can have dire consequences for the physical system. For example, chemotherapeutic drug interaction can kill healthy cells and selforganization in smart grids can result in large scale spread of critical failure. Thus, characterization and analysis of aggregate effect is essential for designing safe CPSs. This chapter will discuss the formal methods available for characterizing aggregate effects in CPSs and the verification and validation of models of CPSs.

KW - Aggregate effects

KW - Emergent behavior

KW - Formal methods

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

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

U2 - 10.1016/B978-0-12-803801-7.00012-2

DO - 10.1016/B978-0-12-803801-7.00012-2

M3 - Chapter

AN - SCOPUS:85024134827

SN - 9780128038017

SP - 175

EP - 191

BT - Cyber-Physical Systems

PB - Elsevier Inc.

ER -