S E M I N A R
Formal Verification of Cyber-Physical Systems
Prof. Sofiène Tahar
Concordia University, Canada
Due to major breakthroughs in software and engineering technologies, embedded systems are increasingly being utilized in areas ranging from aerospace and next-generation transportation systems, to smart grid and smart cities, to health care systems, and broadly speaking to what is known as Cyber-Physical Systems (CPS). A CPS is primarily composed of several computing, communications, control, and physical actuators and sensors. The modeling and verification of such complex infrastructure poses a number of technical challenges due to the mix of heterogeneous underlying (mathematical) models and their intricate interactions. Traditionally, computer simulation approaches are used to verify and validate such systems. However, due to long simulation runs and the use of numerical approximations, system bugs remain uncaught during the analysis and in turn cause unwanted scenarios that may have serious consequences in safety critical applications. In this seminar, we introduce a complementary approach to simulation based on computerized mathematical reasoning, called “formal verification”. Formal methods allow a generic and exhaustive validation while working with accurate models, similar to paper-and-pencil analytical approaches. Formal methods have been classically used for the verification of software, digital hardware or high level protocols. We will display recent activities carried out by our Hardware Verification Group (HVG) at Concordia University (http://hvg.ece.concordia.ca), on the formal verification and analysis of CPS. Namely, the formal performance analysis of probabilistic and statistical properties; the formal verification of reliability, security and privacy issues; and the formal analysis of physical devices, in particular, optical and photonics systems (actuators and sensors).
Bio: Sofiène Tahar is Professor and Senior Research Chair in the Department of Electrical and Computer Engineering at Concordia University, Montreal, Quebec, Canada. He received his PhD degree in Computer Science with “Distinction” in 1994 from the University of Karlsruhe and his Diploma degree in Computer Engineering in 1990 from the University of Darmstadt, Germany. Prof. Tahar is founder and director of the Hardware Verification Group (http://hvg.ece.concordia.ca) at Concordia University. He has made contributions and published over 350 papers in the areas of formal hardware verification, microprocessor and system-on-chip verification, analog and mixed signal circuits verification, VLSI design automation, and formal probabilistic, statistical and reliability analysis of systems. Prof. Tahar has received several awards and distinctions, including in 2007 Concordia University’s Senior Research Award earning him the title of University Fellow. In 2010, he was the recipient of a national Discovery Accelerator Award, given to the top 100 researchers in Canada in engineering and sciences. He is member of the Order of Engineers of Quebec, Senior member of IEEE and Senior member of ACM.
DATE: 23 November 2017, Thursday @ 13:40