University Professor in the Digital Sciences Department at ENSEEIHT - Toulouse INP.
Head of the Numerics and Mathematics Department of the French National Research Agency (ANR). France
He holds an engineering degree from the Institut National d'Enseignement Supérieur en Informatique (Tizi-Ouzou - Algeria), a DEA and a PhD in Computer Science from ENSAE-SUPAERO in Toulouse, and a habilitation to direct research in Computer Science from the University of Poitiers.
He has held a number of research positions, including Deputy Director of the doctoral school of Science information engineering, mathematics at ENSMA Poitiers (2009-2011), Director of the scientific and industrial information technologie Laboratory LISI-ENSMA-UP Poitiers (2008-2011) and Head of the Software Reliability and Dependability (FSL) department at the Institut de information technology research Toulouse - (IRIT - UMR CNRS 5505) (2016-2020). He has also been a member of the Allistene alliance expert group since 2010, a scientific advisor to the HCERES research evaluation department (DER) since 2019 and a head of the Numerics and Mathematics Department of the French National Research Agency (ANR) since 2021.
Talk title: Descriptive and prescriptive system models formalised in Event-B
Abstract: The Event-B method has shown its effectiveness in the rigorous development of complex systems, whether these systems are software, hardware or hybrid. A system model is formalized as a machine that encodes a state-transition system. This machine relies on a set of definitions and theorems defined in a context. A set of proof obligations is automatically generated. When discharged, these proof obligations guarantee the consistency of a model as well as its correctness.
Recently, the Event-B method has been extended with the possibility to define new types, being either constructive or axiomatic, described using algebraic theories. These theories are particularly useful for defining generic data types and associated operators, as well as for proving theorems reflecting their properties.
This extension paves the way for the formalization of models of complex systems and makes it possible to reduce the proof effort thanks to the exploitation of the new proof obligations induced by the definition of these types. Indeed, axioms and theorems borrowed from these theories are useful to discharge designed models proof obligations and contribute to reduce the proof effort as the theorems of the theories are proved once and for all.
In this presentation, we show how Event-B machines and algebraic theories are set up to formalize prescriptive models for defining particular systems as well as descriptive models, to describe domain knowledge or system environments.
Professor (Research) , Department of Engineering Science, Faculty of Innovation Engineering
Macau University of Science and Technology, China
Zhiwu Li received the B.S., M.S., and Ph.D. degrees all from Xidian University, Xi’an, China, in 1989, 1992, and 1995, respectively. Dr. Li held visiting professor positions at different universities, such as the University of Toronto, Martin-Luther University at Halle (supported by Alexander von Humboldt Foundation), University of Cagliari, Politecnico di Bari, Conservatoire National des Arts et Métiers (CNAM, supported by the program of Research in Paris), King Saud University, and Meliksah University. He has published three monographs in Springer (2009; 2023) and CRC Press (2013). His research was cited by leading business giants including IBM, HP, ABB, Volvo, GE, GM, Mitsubishi, Ford Car, and Huawei. His current research interests include Petri net theory & applications, supervisory control of discrete event systems, and production automation. He is a Fellow of IEEE (2016) and was selected as Thomson Reuters Highly Cited Researchers in the category of Engineering from 2014-2018.
Talk title: Fault diagnosis of discrete-event systems using Petri nets
Abstract: Fault diagnosis and diagnosability analysis in cyber-physical systems have received much attention from researchers and practitioners. This talk touches upon this problem from the lens of discrete-event systems that are a technical abstract or model of cyber-physical systems, where a plant is modeled with a labeled Petri net. We present two lines of fault diagnosis in this particular formalism: structural analysis and reachability analysis. The former addresses the problem by integer linear programming, while the latter employs a compact reachable space presentation approach called a basis reachability graph. Diagnosability enforcement is recapitulated using the basis reachability graph. Finally, future exploration in the community is regularly platitudinized.