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

  • Sensor Networks
  • Model Checking
  • Formal Methods
  • Software Engineering

• Graduation date

  Fall 2012

• Type of Item

  Thesis

• Degree

  Master of Science

• DOI

  https://doi.org/10.7939/R3PT4V

• 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.