Mojgan Kamali
- mojgan.kamali@cs.rwth-aachen.de
- Address
- Room 4207
Ahornstraße 55
D-52074 Aachen - Phone
- +49 241 80 21202
Research
I am a Post-Doc at the Software Modelling and Verification Group (MOVES), headed by Prof. Joost-Pieter Katoen. I am working on the DFG project PASYWI: PArameter SYnthesis for reliable, performant and efficient WIreless network protocols.
I received my PhD degree in computer science from Åbo Akademi University in 2019. You can access my PhD dissertation titled “Formal Analysis of Network Routing Protocols” here. During my PhD studies, I was awarded the Nokia Foundation Research Excellence as well as Finnish Foundation for Technology Promotion awards, for excellent postgraduate students in technology.
My research interests include applications of formal methods to networked systems. For instance, formal specification and verification of communication protocols applied in mobile ad-hoc networks, wireless mesh networks, etc.
Bachelor/Master Theses
If you are interested in applying formal methods in (real-life) networked systems, please do not hesitate to contact me either via email or in person. In the following you can find a couple of relevant topics. However, topics are not limited to those listed.
Wireless networks are on the rise, from laptops and smart phones in use everywhere, to sensor networks generating large amount of data. One of the contemporary wireless networks that our focus is on is Mobile Ad-hoc NETworks (MANETs). These networks have gained popularity and are increasingly applied in a wide range of application areas, such as public safety, emergency response networks, or disaster recovery. Due to the safety critical applications of such networks, their reliability, performance and efficiency are of high importance. Therefore, we apply formal methods to analyse these systems and provide assurance regarding their safety. We propose the following topics:
- One of the limitations of mobile devices (nodes) is their battery lifetime in ad-hoc networks. For instance, nodes that have more connectivity in the network may deplete their battery quicker than other network nodes and consequently yield to decrease the network performance and efficiency. The task in this study is to model battery depletion using the Kinetic Battery Model (KiBaM). This battery model is already available, however it needs to be adapted/translated to the Modest modelling language (probably make some abstractions, and extend it with recharging and stochastic loads) to be used for efficiency analysis of different networks.
- Formal analysis of a well-known routing protocol applied in mobile ad-hoc networks, namely Ad-hoc On-demand Distance Vector (AODV). This protocol has been already formally modelled and analysed w.r.t. performance and reliability. The task in this study is the analysis of the protocol regarding efficiency (energy consumption) by enriching the existing Probabilistic Timed Automata (PTA) models (reflecting the AODV behaviour) with prices to obtain priced PTA of this protocol. Prices at edges model instantaneous energy consumption and can be used to distinguish energy-expensive protocol operations from energy-neutral ones. Price rates at locations model the linear increase of energy over time. These rates can be achieved by combining battery models with the PTA models.
- Formal analysis of a well-known routing protocol applied in mobile ad-hoc networks, namely Optimised Link State Routing (OLSR). This protocol has been partially formally modelled. The task in this study is modelling this protocol formally using PTA (in Modest language) and analysing it regarding reliability, performance and efficiency (energy consumption) by enriching the developed PTA models (reflecting the OLSR behaviour) with prices to obtain priced PTA of this protocol. Prices at edges model instantaneous energy consumption and can be used to distinguish energy-expensive protocol operations from energy-neutral ones. Price rates at locations model the linear increase of energy over time. This can be achieved by combining battery models with the PTA models.