2023 -- 2024: PI of ASSA (Automated safety and security assessments in Cyber-Physical Systems with IoT features) --  DigitalLead Innovation Project til midler fra UFS-samarbejdspuljen.  This project provides Danish companies with a formal approach combining safety and security assessments in a systematic and automatic manner to support the development of trustworthy Cyber-Physical Systems. Thus, stakeholders become rapidly aware of potential safety and security risks involved in the system development at an earlier stage and apply relevant safety and security protection technologies. The aim of this project is to encompass a range of automated safety and security risk assessments in CPS/IoT including (1) analysis of privacy and security attacks, (2) countermeasures to risks, and (3) formal proof of guaranteeing the functional safety in the systems based on the security solutions provided by (1) and (2).

2021 -- 2024: PI and Co-PI of EF-CPS (Error-Free Cyber-Physical Systems within an Industry 4.0 Platform) --  TEK  SDU Industry 4.0 Digital Autonomous Production project.  This project proposes tool-supported methodologies for combining various  verification and validation (V&V) techniques that are suitable for both modelling CPS applications and supporting automatic (semi)-formal analysis within an Industry 4.0 platform. V&V strategies classified into the two work packages are applied to automate safety and reliability assessment processes of CPS:

• • [P1] Formal V&V of Safety & Security-critical Cyber-Physical Robotic Manufacturing Systems (PI)

  • [P2] Property-Based Testing of an I4.0 Infrastructure (Co-PI)

2016 -- 2020: PI of EASY (Energy-aware CPS & Automotive System Specification Analysis Methodology)  --  National Natural Science Foundation of China (The Research Fund for International Young Talented Scientists). International (Regional) Cooperation and Exchange Program project. This project addresses the need for specification and analysis techniques to support development of safety-critical energy-aware real-time (ERT) Cyber Physical Systems (CPS), such as automotive systems. We develop a probabilistic timing and energy-aware modeling and analysis methodology to cover the entire development process. Specific algorithm and tool support will be considered to (1) manage and analyze specific probabilistic ERT constraints information; (2) exchange the ERT constraints information between different parties and types of tools; (3) reuse this information and different use case scenarios. The EASY methodology enables a system designer to specify complex problems in an efficient manner as well as to get feedback in the form of probability distribution and to compare probabilities in order to analyze performance aspects of systems. A formal interchange format which preserves semantics of probabilistic-timing and -energy specification for design models will be defined and facilitates the statistical probabilistic analysis of ERT behaviors of the system during the development process.

2015 -- 2016: PI of FV-PRoDES (Formal Verification and Proof-oriented Development of Embedded Systems)  -- The Central Universities' Fundamental Research Funds for Sun Yat-sen University young talented teachers project. This project addresses the need for design and analysis techniques to support correct development of software in embedded systems. An important concern is to ensure a system model in different design stages (design model) functions correctly and meets the specified requirement (specification model) during development of embedded systems. We develop a methodology that integrates different modeling and analysis techniques for correct development of embedded systems by using (semi)-automated mathematical techniques based on theoretic refinement approaches: refining high-level models (specification) into lower-level models (designs and implementations) in a manner that preserves the desired system properties (i.e. functionality, behaviors, dependency, relationships) across the specification models and improved (further refined) design models. This methodology allows us to capture different aspects of modeling languages into a uniform format that supports transformation of a specification model into a design model and ensures correct relations across a series of further refined design models. This notion combines a proof mechanism among different abstract models during refinement procedures and an evaluation mechanism over each abstract model at different design levels.

2011 --  2014: VEREV (Verication de logiciel recursif, evolutif, et temps-reel  -- Verication Recursive, Scalable, and Real-Time Softwares) funded by PReCISE Research Centre (finished 2012). Co-PI of TPA-FOCOME (Theory and Practice of Logic and Automata --  Analysis of Feature Oriented COMponent based Embedded systems) project granted by FNRS1 (2012  -- 2014).  Scientific collaboration between PReCISE Research Centre, University of Namur and Sun Yat-Sen University -- including the following research themes:

• [R1] Modeling and analysis of energy-aware real-timed (ERT) behaviors of safety-critical embedded systems which covers the declarations of system modes, computation/transfer functions, execution dynamics, and related error behaviors.

• [R2] Resource optimization of embedded systems including methods, techniques and tools for this area and focusing on their application on timing and energy optimization. The techniques include model checking and controller synthesis.

• [R3] Model-based integration, formal design and V&V for mixed-criticality of automotive embedded systems in either an event-triggered or a time-triggered architecture.

2013 -- 2015: FTOP (Formal specification and verification Technologies for Open Programmable networking) project funded by the ICT Standardization program of Korea Communications Commission, the National Research Foundation of Korea, the Ministry of Education, Science & Technology and in collaboration with Korea University and ETRI (Electronics and Telecommunications Research Institute). We provide formal analysis techniques to guarantee the reliability and correctness of open programmable networking topologies and define a set of control rules, which can be used as the system requirements and validated during formal analysis. We have developed a set of open flow network protocols (rules) to program flow-tables in switches and routers in the network. I have also investigated the detection of rules violations, a study of omission errors through an analysis of a set of packet forwarding rules. This assists in .finding feasible solutions to improve drawbacks of the current network system.

2010 -- 2011: During my research fellowship at PROGRESS in Sweden, I conducted research on assuring the required quality of embedded systems by applying and further developing model-based formal analysis and verification techniques and tools that can be put into industrial practice. My research centered on high quality safety related products in the transportation domain (e.g. safety-critical and real-time embedded systems in automotive and avionics) at reduced cost in terms of time, resource, and energy.

2008 -- 2009: rCOS (Refinement of Component and Object Systems) HighQSoftD, HTTS funded by Macau S&T and United Nations University - International Institute Software Technology, and NSFC Project. The aim of this work was to present the design and progress of a theory supported tool (an Eclipse-based UML modeling tool) for component-based model driven software development. I contributed to the extension of validation techniques to a tool for consistency checking of component-based object systems. As a result, tool-supported pre- and post-style specification and its refinement to object-oriented component code were successfully presented, and associated verification problems during refinement were solved by generating output from the tool, such as CSP scripts and proof obligations, to 3rd party verification tools. A concept of assume-guarantee to refinements of component models was extended as Black-Box design that a complex design becomes simpler. This approach decreases the degree of coupling between components during their composition, and reduces the possibility of failures caused by the composition of independent components.

2002 -- 2007: Ph.D. project - PARTES (Parametric Analysis of Real-Time Systems) funded by NWO (Dutch Government Scholarship Organization), Delft University of Technology in The Netherlands and INRIA-LORIA (French Institute for Research in Computer Science and Automation) in Nancy, France. I developed theoretical and practical verification techniques for concurrent and real-time systems based on the combination of real-time model checking, abstract interpretation, and deductive techniques. In particular, I addressed an efficient verification algorithm for the analysis of real-time systems by combining SAT-based model checking and abstract interpretation/refinement techniques. This algorithm scaled up formal methods and integrated them into engineering development processes for the correct construction and maintenance of real-time systems with several tools-support. 

2002 -- 2004: ELM (Experiments with Lego Mindstorms) funded by TU-Delft. This project aimed to integrate formal methods into the embedded software development process. I investigated how to apply model checking in combination with requirement engineering, architecture design, and implementation phases of the software development lifecycle. I revealed the difficulties that arise when integrating model checking with the typical software engineering practice, and proposed what I regard as the keystone principles in tackling those limitations.