Poster Abstract: Methods and Tools for Verification of Cyber-Physical Systems

Summary form only given. As chip technology scales, it is becoming possible to integrate multiple cores on a single chip which communicate using a network-on-chip (NoC) paradigm. An NoC must be carefully designed to avoid deadlock and be fault-tolerant while meeting latency and throughput goals. The key component of an NoC is the protocol that it employs to route packets between the processing elements. CPS systems like NoC router design are complex, and the concurrent, timing, and stochastic behavior must be thoroughly verified. To address this challenge,a comprehensive methodology around a unified modeling formalism that supports all these aspects is being developed. The concurrent and timing behavior of this model are verified using improved versions of traditional model checking methods. The stochastic behavior is being verified using both statistical and stochastic model checking.