On the verification of hybrid DEVS models

This paper introduces a new methodology to formally verify hybrid systems modeled with DEVS formalism. Hybrid systems where continuous and discrete phenomena interact are found in many natural and artificial systems. One exam-ple of such systems are real-time embedded systems where a discrete controller interacts with a continuous plant. Verify-ing real-time systems for correctness is of most importance as results of incorrect behavior could be catastrophic. Simula-tion is one of most used tools to study hybrid real-time systems due to lack of robust formal methods. In this paper, we in-troduce a verification method to verify real-time hybrid systems modeled by DEVS formalism.

@Conference_Paper\{SW12,
  author       = "Saadawi, Hesham and Wainer, Gabriel A.",
  title        = "On the verification of hybrid DEVS models",
  category     = "Multi Modeling and Modeling Formalisms",
  booktitle    = "Proceedings of 2012 Spring Simulation Conference (SpringSim12), DEVS/TMS Symposium",
  month        = "March",
  year         = "2012",
  publisher    = "ACM",
  organization = "Society for Modeling and Simulation International (SCS)",
  address      = "Orlando, FL",
  url          = "http://cell-devs-02.sce.carleton.ca/publications/2012/SW12"
}