Behavioral Verification of Small Networks of State-Machines Built with Arduino-like Processors

  • Author / Creator
    Delfani, Parisa
  • Inexpensive yet versatile limited-capability processors enable computing to be embedded in many kinds of devices and situations. Most applications are simple purpose-programmed reactive systems that interact with the environment through sensors and actuators. Because the processors are limited state-machines, and in principle can be fully specified, they are amenable to rigorous formal verification. Low cost wired and wireless connection schemes permit the easy aggregation of these processors into networks with both static and dynamic topologies. The resulting networks will often have unexpected behavior or emergent properties. This thesis is a step towards formally reasoning about such networks. Our contribution is a simple domain-specific programming environment that generates both the model for performing verification via model checking, and extracts executable code that runs on the Arduino computing platform.

  • Subjects / Keywords
  • Graduation date
    Fall 2012
  • Type of Item
  • Degree
    Master of Science
  • DOI
  • License
    This thesis is made available by the University of Alberta Libraries with permission of the copyright owner solely for non-commercial purposes. This thesis, or any portion thereof, may not otherwise be copied or reproduced without the written consent of the copyright owner, except to the extent permitted by Canadian copyright law.
  • Language
  • Institution
    University of Alberta
  • Degree level
  • Department
  • Supervisor / co-supervisor and their department(s)
  • Examining committee members and their departments
    • Nikolaidis, Ioanis (Computing Science)
    • Hoover, H. James (Computing Science)
    • Reformat, Marek (Electrical and Computer Engineering)