My research interests centre on the theory of interactive and concurrent systems, including both theoretical aspects of their semantics and application of formal techniques to the modelling and verification of such systems. In particular, modelling and verification based on modularity and compositionality of Petri nets and interactivity of systems. My research also focuses on “automated synthesis”, which is an attractive approach for constructing computational systems. Synthesis procedures guarantee that the resulting systems are “correct by design”, which can make the system verification complementary or even redundant. Moreover, I am generally interested in the development and application of formal techniques and tools for modelling and understanding computer systems. This interest involves investigating the development of formal techniques to model and analyse safety-critical systems, such as aviation environments, medical devices and intelligent systems.

Further research interests include:

• Formal methods, model checking and temporal logic

• Analysis of communication protocols using Promela and Spin model checker

• Formal modelling and verification using VDM and MAL languages

• Design, usability analysis and prototyping of interactive interfaces

• Application of formal analysis to Smart systems, Internet of Things (IoT), Cryptography and Machine Learning

Project Title: “Modelling and Verification of Ambient Systems Using Petri Nets”

Brief synopsis:

There is a growing need to introduce and develop formal techniques for computational models capable of faithfully modelling systems whose behaviour is of high complexity and concurrent. Such systems are the Ambient Systems. Modelling and verification of this kind of systems were addressed by proposing a new modelling approach that is based on the modularity and the compositionality of a class of Coloured Petri Nets with inhibitor arcs, the Ambient Petri Nets. This approach uses modular inhibitor nets that represent individual interactions between the users and the system. Two case studies of Ambient Systems were examined in the context of interactivity by applying that approach, which produced their behavioural models through the composition of the modular inhibitor nets. The modularity of these models resulted in useful modelling observations about the key features and components of Ambient Systems that affect the interactivity. The correctness of the obtained models with respect to the specification of the examined systems was verified by analysing both qualitative and model checking properties, which were related to fundamental properties of Petri net and Ambient Systems respectively. The verification results of these properties confirmed the correctness of the models produced by the new modelling approach.