Thesis supervisor: Gergely Kovásznai
Location of studies (in Hungarian): University of Debrecen Faculty of Informatics Abbreviation of location of studies: DE IK
Description of the research topic:
Wireless Sensor Network (WSNs) are widely used in industry, agriculture, intelligent traffic systems, military applications and, in general, different areas of everyday life. The networks consist of sensor devices that have limited power supply, therefore it is high priority to operate those networks in an energy-efficient way. It is also very important to operate those networks in a secure way, with particular attention to networks in critical systems.
Formal methods make us able to verify systems for which exhaustive testing is infeasible and/or does not provide sufficient guarantees. It has great potential to apply SAT and SMT solvers, that are already widely used in industry to formally verify complex system (e.g., hardware, software, air traffic control systems, etc.). While verification guarantees a secure model to operate a given WSN, optimization provides an optimal model which makes the WSN operate for as long as possible. For this, we can use, for instance, MaxSAT and OMT solvers.
In this subject, one can join an existing research with existing results. We have created a formal model of WSNs, including security criteria that are important in practice. We have successfully verified and optimized WSNs by applying existing OMT solvers (Z3, OptiMathSAT, Symba). We have developed an OMT solver (Puli 2.0), which outperforms existing solvers on benchmarks representing WSN and other optimization problems. The research continues with the improvement of our OMT solver, with implementing new solving approaches, and with enhancing our formal model of WSNs in order to take into consideration more physical parameters of energy efficiency.
Bibliography
• G. Kovásznai, Cs. Biró, B. Erdélyi. Puli – A Problem-Specific OMT solver. 16th International Workshop on Satisfiability Modulo Theories (SMT 2018), aff. to IJCAR 2018, 2018.
• G. Kovásznai, Cs. Biró, B. Erdélyi. Generating Optimal Scheduling for Wireless Sensor Networks by Using Optimization Modulo Theories Solvers. 15th International Workshop on Satisfiability Modulo Theories (SMT 2017), aff. to CAV 2017, CEUR, Vol. 1889, pp. 15-27, 2017.
• Q. Duan, S. Al-Haj, E. Al-Shaer. Provable configuration planning for wireless sensor networks. 8th Int. Conf. on Network and Service Management (CNSM) and Workshop on Systems Virtualization Management (SVM), pp. 316–321, 2012.
• R. Sebastiani, P. Trentin. OptiMathSAT: A tool for optimization modulo theories. Int. Conf. on Computer-Aided Verification (CAV), LNCS, vol. 9206, pp 447-454.
Deadline for application: 2022-11-15
2024. IV. 17. ODT ülés Az ODT következő ülésére 2024. június 14-én, pénteken 10.00 órakor kerül sor a Semmelweis Egyetem Szenátusi termében (Bp. Üllői út 26. I. emelet).
Login
