Skip to content

RobertGawron/PlantWateringDevice

Repository files navigation

Plant Watering Device

Formal Verification Unit Tests Simulation Build

This is a device for watering indoor plants based on the 8-pin PIC10F202-IOT microcontroller.

The goal is to try to make a project on this small MCU and learn how to deal with the limitations of such a small chip, as well as to learn the PIC MCU family ecosystem.

Features:

  • Sensing soil humidity using a cheap capacitance sensor
  • Display of actual soil humidity and low-level soil humidity when the watering is started; what is presented on the display is selected by a button, and an additional two LEDs indicate the current reading shown on the display
  • Possibility to change the quantity of water that is dispersed when the soil is detected as dry; the level can be modified via a button and the current setting is shown on a 10-segment LED bargraph
  • Possibility to select the moisture level when the soil is considered dry and the watering should be started via a potentiometer

Device in use

Device top

Device bottom

Device mechanical

Device cables

Software

The software is written in C (C99 with _Static_assert from C11).

Software details.

Formal Verification

The watering logic is formally verified using frama-c to mathematically prove correctness properties such as:

  • Watering is never activated when soil moisture is above the threshold
  • Watering always stops after the configured duration
  • No integer overflows or out-of-bounds array accesses occur

This provides stronger guarantees than testing alone — instead of checking specific inputs, it exhaustively verifies all possible input combinations.

Simulation

The software can be run in a web browser to speed up development (no need to flash the device, soil humidity can be simulated as wanted, etc.).

Simulation window.

Simulation details.

Hardware

Hardware details.

Design tools: KiCad

Mechanical

In order to keep the pump, PCB, display, and potentiometer in one place, a simple 3D printed holder was made.

Mechanical specifications and assembly details.

Design tools: OpenSCAD and FreeCad

Mechanical render