Safety is an important challenge for the critical systems, specifically cyber physical systems (CPS), such as robots and drones. It becomes even more challenging when uncertainties are involved in CPS due to the disturbance in noise or sensor/actuator noise. Hence, our broad goal is to develop safety verification methods/tools for CPS using formal methods towards enabling the formal verification practical. Towards this, we have developed tool BEAVer: bounded error approximation based verifier for linear hybrid systems and networked linear hybrid systems, and tool ProCEGARVer: probabilistic counter-example guided abstraction refinement based verifier for probabilistic polyhedral hybrid systems.

Cyber physical systems are commonly developed according to model-based design. Engineers use Verification-Validation (V-V) approach to implement the model-based design. In V-V approach, The requirement specification of CPS is divided into sub-requirements in top-down fashion, and the system is implemented and validated its requirement in bottom-up fashion. At any stage, if validation is failed, then one possibility is that the requirement may not be formulated correctly. Hence, our broad goal is to develop methods for identifying inconsistencies in the requirement prior to the development. Towards this,we have developed an automatic trace generation method which generates a set of satisfying and violating behaviors of the system with respect to its requirement. In the method, the requirement is expressed in the form of signal temporal logic (STL), which is a popular formalism of expressing continuous behaviors. The development of tool STLTraceGen: Signal Temporal Logic Trace Generator is under the process.

Autonomous systems are popularly used in many applications, such as mail delivery, pesticide spraying, data collection from the crops, which are performed using autonomous vehicles, ground robots, and drones, respectively. Due to limited resources, these tasks are required to be performed in an optimal way. Hence, optimal path/motion for the autonomous systems save both energy and time. Towards this, we have developed an optimal multi-robot path planning and a time-optimal multi quad-rotor trajectory generation for pesticide spraying in an agricultural field. We have developed tools MRPPlaner: multi-robot path planer and MQTGen: multi quad-rotor trajectory generator for pesticide spraying in an agricultural field.