Currently available topics for PhD projects:
Feel free to propose other topics within my research interests or look at the Master / Honours topics here, as they also can be expanded to a PhD topic.
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] Spichkova, M. (2016). ”Boring formal methods” or ”Sherlock Holmes deduction methods”? In Proceedings of Software Technologies: Applications and Foundations. Springer, pages 242-252.
[2] 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)
[3] Klein, G., et al. Comprehensive formal verification of an os microkernel. ACM Trans. Computing, 32 (2014
[4] 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.
[5] H. Schmidt, M. Spichkova. Towards Readability Aspects of Probabilistic Mode Automata. Proceedings of the 14th International Conference on Evaluation of Novel Approaches to Software Engineering, SciTePress, 555-562
[6] M. Spichkova, A. Zamansky. Teaching Formal Methods for Software Engineering. 11th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE), ISBN 978-989-758-189-2, pages 370-376
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.
References:
[1] D. Dicheva, C. Dichev, G. Agre, G. Angelova, Gamification in education: a systematic mapping study, Educ. Technol. Soc., 18 (3), pp. 75-88 2015.
[2] Richter, G.; Raban, D.R.; Rafaeli, S. Studying gamification: The effect of rewards and incentives on motivation.In Gamification in Education and Business; Springer: Berlin, Germany, 2015; pp. 21–46.
[3] Pedreira, O., García, F., Brisaboa, N. and Piattini, M. (2015). Gamification in software engineering – A systematic mapping. Information and Software Technology, 57, pp.157-168.
[4] Pereira, P., Duarte, E., Rebelo, F. and Noriega, P. (2014). A Review of Gamification for Health-Related Contexts. Design, User Experience, and Usability. User Experience Design for Diverse Interaction Platforms and Environments, pp.742-753.
[5] Baker, R., Martin, T., M. Rossi, L. Educational Data Mining and Learning Analytics. Cambridge University Press. 2016.
[6] A. Alharthi, T. Alsanoosy, M. Spichkova, M. Hamilton. Social Position and Gender Perspectives of eLearning Systems: A Study of Social Sustainability. Advances in Information Systems Development Proceedings of the International Conference on Information Systems Development, 34, Springer, 2019
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.