Prof. Simon K.S. Cheung

Director of Information Technology

Hong Kong Metropolitan University

Biography: Dr. Cheung is currently the Director of IT at the Hong Kong Metropolitan University. He received his BSc and PhD in Computer Science and Master of Public Administration from the City University of Hong Kong and the University of Hong Kong respectively. He was admitted as IET fellow, IMA fellow, BCS fellow, CMA fellow, HKIE fellow, HKCS fellow. He is active in research, with over 200 publications in the form of books, book chapters, journal articles and conference papers in two distinct areas, namely, software and system engineering, and technology in education. He won the Outstanding Research Publication Award from the Open University of Hong Kong in 2016, 1st class Achievement in Computer and IT from Shenzhen Science and Technology Association in 2016, 1st class Outstanding CIO Award from the Hong Kong IT Joint Council in 2015, and Honoree for IT Excellence from the CIO Asia in 2015. He has been listed in Who’s Who in Science and Engineering since 2007.

Title:A Property-Preserving Synthesis Approach to Component-based Software Engineering

Abstract: Design correctness is always required in component-based software engineering to ensure that the system is free from erroneous situations such as deadlock and capacity overflow, especially for distributed systems with concurrent processes competing some shared resources. This presentation describes a formal and mathematically sound approach based on augmented marked graphs. With a special structure readily used for modelling systems with shared resources, augmented marked graphs possess desirable properties pertaining to liveness (implying freeness of deadlock) and boundedness (implying freeness of capacity overflow. These properties can be preserved under certain conditions after composition. When applying to component-based software design for distributed systems with shared resources, each system component can be modelled as an augmented marked graph. Liveness and boundedness of the individual system components can be analyzed, based on the properties of augmented marked graphs. By composing them via shared resources, the liveness and boundedness of the integrated system can be derived, based on the property-preserving composition.