中央研究院 資訊科學研究所

Cyber-Physical Systems (CPS) are deployed in a wide variety of safety 

critical applications from avionics, medical, and automotive domains.  

For these applications, it is essential to create a precise specification and formally verify that the implementation behaves as specified.  The formal verification of these systems presents a wide variety of challenges.  Models of these systems must represent the physical world, analog sensors and actuators, computer hardware and software, networks, and feedback control.  These models must deal with the fact that correctness may depend on timing, concurrency, system dynamics, and stochastic behavior.  To address this, our research has developed a general unified hybrid system modeling formalism that is capable of representing continuous and discrete dynamics, timing, and stochastic behavior.  To address the complexity of formally verifying CPS models, our group has developed automated model abstraction methods to reduce model complexity, partial order reduction methods to address model concurrency, symbolic methods to utilize efficient data representations, and compositional reasoning methods to exploit model structure.  This talk will describe this work, and its application to the development of a new fault-tolerant routing algorithm for a network-on-chip (NoC) for electronic control units (ECUs) used in automative applications.

Chris J. Myers received the B.S. degree in Electrical Engineering and Chinese history in 1991 from the California Institute of Technology, Pasadena, CA, and the M.S.E.E. and Ph.D. degrees from Stanford University, Stanford, CA, in 1993 and 1995, respectively.  He is a Professor in the Department of Electrical and Computer Engineering, University of Utah, Salt Lake City, UT.  Dr. Myers is the author of over 100 technical papers and the textbooks Asynchronous Circuit Design and Engineering Genetic Circuits.  He is also a co-inventor on 4 patents.  His research interests include asynchronous circuit design, formal verification of analog/mixed signal circuits and cyber-physical systems, and modeling, analysis, and design of genetic circuits.  Dr. Myers received an NSF Fellowship in 1991, an NSF CAREER award in 1996, and best paper awards at the 1999 and 2007  Symposiums on Asynchronous Circuits and Systems. 

  Dr. Myers is a Fellow of the  IEEE, and he is a Member of the Editorial Boards for the IEEE Transactions on VL SI Systems, IEEE Design & Test Magazine, and Springer journal on Formal Methods  in System Design.  Dr. Myers also serves as an editor for the Systems Biology Markup Language (SBML) standard and on the advisory board for the SyntheticBiology Open Language (SBOL) standard.