Research Supervision
PhD students (ongoing):
Chowdhury Shahriar Muzammel. Cultural Aspects Of Requirements Engineering (RMIT)
Hanin Aloufi. Improving Feedback for Computing Students by Analysing Perceptions (RMIT)
Shruthi Ravikumar. Abstract Reasoning Assessment Framework (ARAF) for Novice Programmers (RMIT)
Nasser Alzahrani. Secure Authenticated Data Structures in Haskell (RMIT)
PhD students - Thesis completed:
Tawfeeq Alsanoosy: Cultural Diversity Aspects of Software Requirements Engineering (RMIT, first supervisor). Successfully completed in 2021. The RMIT Deputy Vice-Chancellor’s Higher Degree by Research Prize. Now - Lecturer at Taibah University, Saudi Arabia
Ahmed Alharti: Requirements Engineering Aspects of ELearning Systems (RMIT, first supervisor). Successfully completed in 2019. Now - Assistant Professor, Dean for ELeaning in Umm Al-Qura University, Saudi Arabia
Master Thesis and Honours (RMIT, Thesis completed):
Christopher John Bond: Property Inspection Route Planning: What Properties do I have time to visit? (RMIT, first supervisor). Successfully completed in 2022. RMIT STEM award - Kmart Group Prize for the best Postgraduate Student in IT, Data Science or AI who completed study in 2022.
Mona Saleh Alzahrani. Autism and the Usability of User Interfaces Containing Animations. Successfully completed in 2021.
Sam Nolan. A living review of Interactive Theorem Provers. (RMIT, first supervisor). Successfully completed in 2021.
Nasser Alzahrani: Spatio-temporal models for property based testing. (RMIT, first supervisor). Successfully completed in 2016. After completion - PhD student at RMIT.
Phan Vo Thu Nhat: Model-based generation of natural language specifications (RMIT, first supervisor). Successfully completed in 2016. Now - Senior Full Stack Developer at EdgeWorks German R&D Software Ltd, Vietnam.
Master Thesis and Honours (TU Munich, Germany):
Christian Grewing: Development of a integrated SysML-model for architecture and behavior of an embedded system. Master Thesis successfully completed.
Cem Sekmen: Development of a Model-driven Software System to Recognize Significant Events From Multiple Sensor Information. In collaboration with Siemens AG, Corporate Technology. Master Thesis successfully completed.
Markus Müller: Erstellung eines Lastenheftes für die Innenlichtfunktionen in mehreren BMW-Fahrzeugbaureihen. In collaboration with BMW Group. Master research successfully completed.
Sebaistain Vöst: Verification of the M2L text editor using the example of a FOCUS formula editor. In collaboration with BMW Group. Honours Thesis uccessfully completed.
I am actively looking for students interested in my research areas. Get me in touch, if you would like to write your PhD, Masters or Bachelors Thesis under my supervision. Currently available topics for PhD are listed below as well as here.
A list of currently available topics for Master and Honours research projects (which can be also expanded to a PhD topic, if needed) you can find here. Also, feel free to propose other topics within my research interests.
Currently available topics for PhD projects:
Feel free to propose other topics within my research interests.
1. Game-based learning of formal reasoning
Software has an increasing impact on everyday life. Tasks such as navigation and banking heavily rely on software. A software error can lead to financial loss or even loss of human life, making correctness crucial for many safety-critical systems. This means it is increasingly important to be able to verify the correctness of software as it is developed [1]. This is usually done by the use of formal methods, in which the behavior of the software is modelled mathematically, allowing logical analysis of its properties. There have been some spectacular recent successes in this regard, such as the formal verification of a Linux kernel [2], which made heavy use of FMs.
This makes it vital for humans to understand formal models. Specifically we need to better understand how informal descriptions can be transformed into formal models, and how a software engineer can be sure that this transformation has been performed correctly. Put another way, how can we minimize and eliminate any mismatch between the intuitive (human) description and the formal (mathematical) specification of it? And can a game-based approach assist?
The aim of this project is to analyze possible solutions for this problem and to elaborate a game-based framework to assist in the understanding of difficulties in formalization. A potential solution is to combine real-world problems with puzzles based on famous stories and movies, or even magic tricks [3,4], thus making FMs and other aspects of STEM more appealing. This will enable uses to understand formal systems and their properties, and how solutions to formal problems can be solved automatically.
References
[1] Knight, J. C. Safety critical systems: challenges and directions. In Proceedings of the 24th International Conference on Software Engineering (ICSE), 2002,pages 547–550. (Review)
[2] Klein, G., et al. Comprehensive formal verification of an os microkernel. ACM Trans. Computing, 32 (2014
[3] Curzon, P. and McOwan, P. W. Teaching formal methods using magic tricks. In Fun with Formal Methods: Workshop at the 25th International Conference on Computer Aided Verification, 2013.
[4] Spichkova, M. (2016). ”Boring formal methods” or ”Sherlock Holmes deduction methods”? In Proceedings of Software Technologies: Applications and Foundations. Springer, pages 242-252.
Supervisors: Dr Maria Spichkova, Prof. James Harland
2. Gamification and learning analytics for health education
This project focuses on gamification of learning/ training activities and the corresponding tool support. Traditional educational board games have been used in some areas of medical and allied health professionals’ training and have been shown to enhance learners’ knowledge, enjoyment and interest in the subject. However conventional cardboard type board games need to be played synchronously and in one location, and playing these games in a class room setting may be perceived by students as a distraction to their primary goal of gaining content knowledge. Moreover, the traditional board games do not allow to collect data for further learning analytics. The proposed project will aim to solve the above problems, and cover the questions of usability and effectiveness of software solutions for the educational games.
As the core case study, this project will involve redesigning a conventional cardboard type board game and presenting it in an online format, enabling students to play asynchronously from off campus locations. The game focuses on aging and aims to increase the awareness of health care students in their dealings with patients promoting empathy and compassion for the elderly. Players encounter conditions associated with aging that may hinder the accomplishment of their goals and/or break down their self-images. These difficulties come in different forms, including physical disabilities, social judgements, financial setbacks and the loss of loved ones.
Supervisors: Dr Maria Spichkova, Prof. Ieva Stupans
3. Modelling and Verification of Automotive Software
Automotive software is one of the most challenging fields of software engineering. Automotive systems are highly complex and safety-critical, where a mistake can cost human lives. These systems have hard real-time requirements to guarantee the corresponding safety properties.
With the growing size and complexity of automotive software, it becomes more and more and more complicated to guarantee its correctness.
There are a number of works on modelling and verification of automotive and embedded software, cf. e.g., [1, 2, 4].
The aim of this project is to develop a formal framework for modelling and formal analysis of automotive software, focusing on the time-critical properties and automatisation of the verification process using Isabelle/HOL. Isabelle/HOL is an interactive theorem prover for a Higher Order Logic (HOL), which was successfully applied to verify models of an automotive eCall system [2], seL4 Microkernel [3], etc.
One of the possible case studies within the project might be modelling and verification of embedded system for RMIT Racing vehicles (http://rmitracing.com.au).
References:
[1] Aravantinos, V., Voss, S., Teufl, S., Hölzl, F., & Schätz, B. (2015). AutoFOCUS 3: Tooling Concepts for Seamless, Model-based Development of Embedded Systems. In MoDELS (pp. 19-26).
[2] Botaschanjan, J., Kof, L., Kühnel, C., & Spichkova, M. (2005). Towards verified automotive software. In ACM SIGSOFT Software Engineering Notes 30(4), ACM.
[3] Klein, G., Andronick, J., Elphinstone, K., Murray, T., Sewell, T., Kolanski, R., & Heiser, G. (2014). Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems (TOCS), 32(1), ACM
[4] Spichkova, M., Simic, M. and Schmidt, H. (2016). From automotive to autonomous: Time-triggered operating systems. In Intelligent Interactive Multimedia Systems and Services, Springer.
Supervisor: Dr Maria Spichkova
4. Usability Aspects of eResearch Software
Scientific experiments can be very challenging from a domain point of view; even in the case the computation can be done on a local desktop machine. Instruments such as synchrotrons and atomic force microscopy produce massive amounts of data.
To support these experiments, software should be reliable, allow long running computations and demand for high-performance computing. Cloud computing provides a great opportunity for scientists, but to unlock all its benefits, we require a platform with a user-friendly interface and an easy-to-use methodology for conducting the experiments. Researchers at RMIT University have addressed some of the issues within Chiminey, an open-source platform, especially focusing on scalable and fault-tolerant cloud computations [1,2,3]. Chiminey enables researchers to focus on domain-specific problems, and to delegate to the tool to deal with the detail that comes with accessing high-performance and cloud computing infrastructure, and the data management challenges it poses. However, there are still many open questions and challenges.
This project focuses on usability aspects of the software to conducting scientific experiments (eReasearch software), which are a specific software domain with specific user requirements and needs.
References
[1] Spichkova, M., Thomas, I.E., Schmidt, H.W., Yusuf, I.I., Drumm, D.W., Androulakis, S., Opletal, G. and Russo, S.P., 2015, December. Scalable and fault-tolerant cloud computations: modelling and implementation. In Parallel and Distributed Systems (ICPADS), 2015 IEEE 21st International Conference on (pp. 396-404). IEEE.
[2] Yusuf, Iman I., Ian E. Thomas, Maria Spichkova, Steve Androulakis, Grischa R. Meyer, Daniel W. Drumm, George Opletal, Salvy P. Russo, Ashley M. Buckle, and Heinz W. Schmidt. "Chiminey: Reliable computing and data management platform in the cloud." In Proceedings of the 37th International Conference on Software Engineering-Volume 2, pp. 677-680. IEEE Press, 2015.
[3] Yusuf, I. I., Thomas, I. E., Spichkova, M., & Schmidt, H. W. (2017). Chiminey: Connecting scientists to hpc, cloud and big data. Big Data Research, 8, 39-49.
Supervisor: Dr Maria Spichkova
If you are interested in my supervision:
Make sure you meet the Entry Requirements for DR221 PhD (Computer Science) program at RMIT.
Especially note that to be eligible for PhD study at RMIT you should:
Have the required research component in your study (Master or Honours Bachelor),
Your GPA should be above 70%,
You should meet the English requirements.
However:
If you have publications at top-ranked conferences or in top-ranked journals, this can be considered as alternative for research component.
If your GPA is below 70% but above 60%, you might be eligible to enrol in the for Master by Research study with a possibility to transfer later to PhD in the case you have very good results within the first year of Master by Research study.
Check my areas of research through my publications and find a common interest. If you cannot find a common interest, you need to look for some other supervisors who work on the topics you are interested in. If you have issues to access full text of any of my papers, simply request a private copy via ResearchGate.
Contact me by sending me the following information via email:
The research area that you would like to pursue a PhD under my supervision (e.g., requirements engineering, testing, formal methods, etc.).
GPA of your highest degree (please also send me a copy of your academic transcripts).
If you have publications already, send me the one you consider to be your best, including the venue it was published in.
A title and a brief description of a problem/project you would like to work on. I also provide a number of "ready" topics (see them below). If you are interested in any of these, check the topic in depth, explain what exactly and how you would like to do within this project.
Your funding situation:
Are you self-funded? Do you already have a scholarship? Are you going to apply for a scholarship?
In the case you are going to apply for a scholarship: What kind of scholarship you are going to apply?
Please note that for the international students the current annual tuition fee at RMIT is AU$33,600.
If you are an international student looking for an RMIT scholarship (either full scholarship or to cover only tuition fees): RMIT scholarships for international applicants are unfortunately extremely limited and difficult to obtain. To have some chances, you need to have both (1) top grades, i.e., GPA 85-100%, and (2) publications in A/A*-ranked conferences or Q1/Q2 ranked journals. If your grades are not so high, I suggest you to look for a scholarship from your home country or consider a self-funded option (and work part-time while studying full-time), as application for an RMIT scholarship would make no sense in this case. If your grades are really very high, but you don't have any publications in top-venues yet, we can discuss your case.
When we have project funding for scholarships, we advertise them explicitly. Note, that if we propose project scholarships, this is also a competitive process, where top grades and publications in top-ranked conferences and journals are the core criteria (local students have preference in this process).