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

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.