Tutorial-2: Formal Verification of Internet of Things (IoT)

Duration: 3 Hours

These days IoTs are increasingly being advocated to be used in safety-critical domains, such as electronic military and medicine equipment and automated transportation systems. This fact makes the accuracy of their analysis very important as an uncaught system bug may endanger human life or lead to a significant financial loss. Traditionally, the verification of these systems has predominantly been accomplished by paper-and-pencil proof methods or computer simulations. However, these techniques do not ascertain 100% correctness and thus may lead to unfortunate incidents due to an erroneous IoT based system deployed in a safety-critical domain. The focus of this tutorial is on formal verification, which is a computer based mathematical technique for system analysis. Due to its mathematical nature it provides accurate system analysis and thus overcomes the above-mentioned limitations of traditional techniques. Formal verification is an emerging research trend that can be applied to analyze a variety of IoT aspects, ranging from computation algorithms, telecommunication protocols to hardware analog and mixed signal designs, so the tutorial could be very beneficial to researchers of almost all disciplines of IoT. The half-day tutorial is designed in such a way that it caters to an audience with no prior knowledge of formal methods and provides a brief introduction to formal verification along with highlighting some of its potential application domains and some hands on experience with a few state-of-the-art formal verification tools.

Key objectives

To describe the main motivation for using formal verification methods for analyzing IoTs. To provide an overview of some of the main formal verification methods and their main strengths and weaknesses To allow the attendees to have some hand-on experience with some formal verification tools

Tutorial Outline

• Introduction to Formal Verification and its applications in IoT
• Formal Verification Techniques
• Model Checking
• Theorem Proving
• Applications of Formal Verification
• Hands on Experience
• A few basic examples with a Model Checking Tool
• A few basic examples with a Theorem Proving Tool
• Conclusions and Q/A Session

Targeted Audience

Our target ordinance includes academics and companies, postgrad students, and other researchers and engineers. The tutorial will be a great venture especially for students at both the graduate and under-graduate levels to pursue research/development in this area.

Tutorial Fees

For Students:
IEEE Student Members: Rs. 500
Non-IEEE Student Members: Rs. 800
For Professionals:
IEEE Members: Rs. 3000
Non-IEEE Members: Rs. 4000

Instructor Biography

Osman Hasan received in 1997 the BEng (Hons) degree from the N-W.F.P University of Engineering and Technology, Pakistan, and in 2001 and 2008 the MEng and PhD degrees from Concordia University, Montreal, Quebec, Canada, respectively. He worked as a postdoctoral fellow at the Hardware Verification Group (HVG) of Concordia University for one year until August 2009. Currently, he is an Assistant Professor in the School of Electrical Engineering and Computer Science, National University of Science and Technology (NUST), Islamabad, Pakistan. He is the founder and director of System Analysis and Verification (SAVe) Lab at NUST, which mainly focuses on the design and formal verification of embedded systems. He has received several awards and distinctions, including the Pakistan’s Higher Education Commission’s Best University Teacher (2010) and Best Young Researcher Award (2011). Dr. Hasan is a senior member of IEEE, member of Association for Automated Reasoning (AAR) and member of the Pakistan Engineering Council. He has over 100 articles at reputable conferences and high impact journals.