Cyber-physical systems (CPSs) are ubiquitous and are becoming increasingly important in the functioning of our society. CPSs have complex discrete and continuous behaviors. In recent years, learning enabled components (LECs) built using machine learning approaches are increasingly used in CPSs to perform autonomous tasks to deal with uncertain and unfamiliar environments. CPSs with LECs are even more difficult to develop. We have developed a methodology for formally modeling and analyzing CPSs with LECs. Hybrid predicate transition nets (HPrTNs) are used as the underlying formal method to model CPSs with LECs and their training through their simulation capability. In this paper, we present our new analysis methodology for CPSs with LECs consisting of three complementary techniques, including a testing technique based on HPrTN simulation capability, a simulation guided barrier certificate technique, and a SMT based bounded model checking technique. The above analysis methodology is partially supported by a tool chain and is demonstrated through an example.
