The difficulties in designing reliable embedded control systems stem from the complexity of both control and distributed (concurrent) computing systems. Design flaws in these systems may arise from the unforeseen interactions among the computing, communication and control components. Motivated by the challenges of finding this type of bugs, in this talk, I will present mathematical frameworks, based on formal methods, to facilitate the design and analysis of such systems. An expressive specification language of linear temporal logic is used to specify the desired system properties. Our approach incorporates methodology from computer science and control, including model checking, theorem proving, synthesis of digital designs, hybrid system theory, reachability analysis, Lyapunov-type methods and receding horizon control. The practicality of the proposed frameworks is demonstrated through several applications, including autonomous vehicles, sensor networks and traffic control.
Click here for more information.