If you are interested in my supervision:
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, 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).
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 (Senior Supervisor, maria.spichkova@rmit.edu.au)
Associate Professor James Harland (Associate Supervisor, james.harland@rmit.edu.au)
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 (Joint Senior Supervisor, maria.spichkova@rmit.edu.au)
Professor Ieva Stupans (Joint Senior Supervisor, ieva.stupans@rmit.edu.au)
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.
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.