Built with the tools and technologies:
- DeMoL - A DSL for modeling IoT Devices
- 📜 Table of Contents
- 📖 Overview
- 👾 Features
- 🚀 Getting Started
- 📚 Language Reference
- 🔌 Supported Sensors & Actuators
- 📐 Formal Semantics
- 🔍 Semantic Validations
- 🔧 Usage
- 📜 License
- 🎩 Acknowledgments
- 🌟 Star History
Device Modeling Language (DeMoL) is a domain-specific language (DSL) designed for the automated synthesis of Internet of Things (IoT) device open-source software, in a hardware-aware manner. It provides a high-level, declarative abstraction for defining hardware configurations, peripheral interconnections, and communication protocols, decoupling the device logic from the underlying platform implementation.
DeMoL employs a model-driven engineering (MDE) approach to facilitate the generation of platform-specific code (e.g., Python for Raspberry Pi, C for RiotOS) from platform-independent models. By enforcing rigorous semantic validation rules—including electrical compatibility checks, pin conflict detection, and protocol constraints—DeMoL ensures the correctness and safety of the synthesized artifacts, thereby reducing development complexity and mitigating hardware-level errors in IoT system design.
| Feature | Summary | |
|---|---|---|
| 🔌 | Hardware-Aware |
|
| 🛡️ | Semantic Safety |
|
| � | Automated Synthesis |
|
| 🌐 | Protocol-Agnostic |
|
| 🧩 | Declarative Design |
|
This project requires the following dependencies:
- Programming Language: Python 3.7+
- Packages: textX, jinja2
- Package Manager: Pip
Download this repository and either use the CLI and the API of the DSL directly from source, or in docker container.
- Pull this repository locally
git clone https://github.com/robotics-4-all/demol.git- Create a Virtual environment (Optional Step)
python -m venv venv && source ./venv/bin/activate- Install the DSL package in
developmode
pip install -e .The DeMoL DSL is built using the textX framework and provides a declarative approach to modeling IoT devices.
The grammar is modular and split into 4 interconnected files located in demol/grammar/:
| File | Purpose | Key Concepts |
|---|---|---|
device.tx |
Main device model definition | DeviceModel, Connect |
component.tx |
Board & peripheral hardware specs | Board, Sensor, Actuator, Pins |
communication.tx |
Message broker configurations | AMQPBroker, MQTTBroker, RedisBroker |
common.tx |
Common utilities & types | AttributeSet, VALUE, Imports |
The language is built around these fundamental concepts:
- Device - Complete IoT device definition with metadata and configuration
- Board - Microcontroller/SBC hardware (ESP32, Raspberry Pi, etc.)
- Peripheral - External sensors and actuators (BME680, SRF04, etc.)
- Connect - Defines how peripherals connect to boards (power + data + remote)
- MessageBroker - Communication infrastructure (MQTT, AMQP, Redis)
- Network - WiFi configuration
File Extensions:
.dev- Device models (complete IoT device definitions).hwd- Hardware component models (boards and peripherals)
Every .dev file follows this structure:
DEVICE DeviceName WITH description="Device description", author="author_name", os=raspbian;
NETWORK[WiFi] WITH ssid="WiFi_SSID", password="password";
BROKER[MQTT] BrokerName WITH host="mqtt.example.com", port=1883, auth.username="user", auth.password="pass";
USE BoardModelName;
USE PeripheralModel1(InstanceName1), PeripheralModel2(InstanceName2);
CONNECT InstanceName1 WITH
POWER
board_pin -- peripheral_pin,
board_pin2 -- peripheral_pin2
DATA
gpio[mode="output"] board_pin -- peripheral_pin
@ "device/sensor/topic";
Describes the device and target platform using the DEVICE statement:
DEVICE SmartSensor WITH description="Environmental monitoring sensor", author="developer_name", os=raspbian;
Target Operating Systems:
raspbian- For Raspberry Pi devicesriotos- For embedded systems (ESP32, ESP8266, etc.)freertos,arduino,esp-idf,esp-idf-rtos- Other embedded platforms
WiFi network settings using the NETWORK statement:
NETWORK[WiFi] WITH ssid="IoT_Network", password="secure_password";
Specifies the hardware composition using USE statements:
USE RaspberryPi_4B_4GB;
USE BME680(EnvSensor) [poll_period = 5], SonarSRF04(DistanceSensor);
USE WS2812(StatusLED);
Features:
USE <BoardName>;defines the main board.USE <Peripheral>(<Name>);defines peripherals.- Board references are resolved from the global repository in
demol/builtin_models/boards/ - Peripheral models are loaded from
demol/builtin_models/peripherals/ - Supports multi-file imports using FQN (Fully Qualified Names)
- Named peripheral instances for easy reference in connections
- Attributes can be overridden using square bracket syntax
Peripheral attributes can be customized when declaring instances:
USE BME680(EnvSensor) [
poll_period = 5,
filter_size = 7
];
USE SonarSRF04(DistanceSensor) [
max_distance = 300
];
Key Points:
- Attributes override peripheral default values
- Use square brackets
[ ]after the instance name - Comma-separated attribute assignments within square brackets
- Comma-separated peripheral instances in the peripherals list
- Only override attributes you need to change
- Supports lists and dictionaries:
colors = ['0xFF0000', '0x00FF00']orconfig = {timeout = 5000}
Boards are defined in .hwd files and describe microcontroller/SBC specifications using the Board[Type] name syntax:
BOARD[RPI] RaspberryPi_4B_4GB WITH
OP
vcc=5V,
ioVcc=3V3,
energy=1.4 W, 7.6 W, 3.5 W, // min, max, avg power consumption
memory.flash=16 gb,
memory.ram=4 gb,
cpu.family=PiArmCortex,
cpu.freq=1500 mhz,
cpu.fpu=true,
wifi.name=RPi4_WiFi,
wifi.version=5,
wifi.bands=[2.4GHz, 5GHz],
bluetooth=BT5
PORTS
spi=2,
i2c=2,
uart=2,
gpio=28
PINS
power_5v[5V] @ 2,
gnd_1[GND] @ 6,
p_21[gpio,sda-1] @ 40,
p_22[gpio,scl-1] @ 38
;
Board Types: RPI (Raspberry Pi), ESP (ESP32/ESP8266), ARDUINO
Pin Syntax:
name [type] @ number- Power pins (VCC, GND)name [funcs] @ number- Digital/IO pins with functions
Pin Functions: gpio, adc, dac, pwm-<channel>, sda-<bus>, scl-<bus>, mosi-<bus>, miso-<bus>, sck-<bus>, cs-<bus>, tx-<bus>, rx-<bus>
Power Types: GND, 3V3, 5V, 12V
Sensors use the Sensor[Type] name syntax where Type indicates the sensor category and its message schema:
SENSOR[Env] BME680 WITH
OP
vcc=5V,
ioVcc=3V3,
energy=0.01 mW, 39.6 mW, 3 mW // min, max, avg power consumption
PINS
vcc[5V] @ 1,
gnd[GND] @ 5,
sda[sda-0] @ 2,
scl[scl-0] @ 3
TEMPLATES
raspbian="bme680.py.tmpl",
riotos="bme680.c.tmpl"
ATTRIBUTES
poll_period[int] = 10,
humidity_oversample[int] = 2,
temperature_oversample[int] = 8,
filter_size[int] = 3
;
Available Sensor Types: Distance, Temperature, Humidity, Gas, Env, AirQuality, Light, UV, Sound, Acceleration, Gyroscope, Magnetometer, IMU, Tracker, Proximity, Motion, Presence, ADC, Current, Voltage, Power, Flow, Level, Weight, Force, Vibration, Camera, RFID, Fingerprint, GPS, Color
For complete sensor type documentation and message schemas, see SENSORS_ACTUATORS.md.
Actuators use the Actuator[Type] name syntax:
ACTUATOR[ServoController] PCA9685 WITH
OP
vcc=5V,
ioVcc=5V
PINS
GND_1[GND] @ 1,
SCL_1[scl-0] @ 2,
SDA_1[sda-0] @ 3,
VCC_1[5V] @ 4
ATTRIBUTES
num_servos[int] = 16,
frequency[int] = 50
;
Available Actuator Types: MotorController, ServoController, Relay, Switch, Led, LedArray, NeoPixel, Display, LCD, OLED, Buzzer, Speaker, Stepper, DCMotor, Pump, Valve, Heater, Cooler, Fan
For complete actuator type documentation and command schemas, see SENSORS_ACTUATORS.md.
Units:
- Memory:
b,kb,mb,gb - Frequency:
hz,khz,mhz,ghz - Distance:
mm,cm,m - Power:
uW,mW,W
Connections define how peripherals connect to the board through power and IO pins:
CONNECT DistanceSensor WITH
POWER
gnd_1 -- gnd,
power_5v -- vcc
DATA
gpio[mode="output"] p_13 -- trigger,
gpio[mode="input"] p_14 -- echo
@ "sensors/distance";
CONNECT EnvSensor WITH
POWER
gnd_1 -- GND,
power_5v -- VCC
DATA
i2c[slave_address=0x76] sda p_21 -- sda, scl p_22 -- scl
@ "sensors/environment";
CONNECT DisplayModule WITH
POWER
gnd_1 -- GND,
power_3v3 -- VCC
DATA
spi[bus_speed=1000000, mode=0] mosi p_23 -- mosi, miso p_19 -- miso, sck p_18 -- sck, cs p_5 -- cs;
CONNECT GPSModule WITH
POWER
gnd_1 -- GND,
power_5v -- VCC
DATA
uart[baudrate=115200] tx p_1 -- RXD, rx p_3 -- TXD
@ "sensors/gps";
Note: UART connections require TX→RX and RX→TX crossover (board TX connects to peripheral RX, and vice versa).
The @ symbol in connections specifies the MQTT/AMQP/Redis topic for this peripheral:
CONNECT MySensor WITH
POWER ...
DATA ...
@ "device/sensor/data"; // optional
Auto-generated Topics: If @ is omitted, topics may be auto-generated based on device and peripheral names.
DeMoL supports three message broker types:
BROKER[MQTT] MyMqttBroker WITH
host="mqtt.example.com",
port=1883,
ssl=False,
basePath="/mqtt", // optional
webPath="/ws", // optional
webPort=8080, // optional
auth.username="sensor_client",
auth.password="secure_pass";
BROKER[AMQP] MyAmqpBroker WITH
host="rabbitmq.example.com",
port=5672,
vhost="/", // optional
topicExchange="amq.topic", // optional
rpcExchange="amq.rpc", // optional
ssl=False,
auth.username="guest",
auth.password="guest";
BROKER[Redis] MyRedisBroker WITH
host="redis.example.com",
port=6379,
db=0, // optional
ssl=False,
auth.username="default",
auth.password="redis_pass";
Authentication Methods:
- Username/Password:
auth.username="user", auth.password="pass" - API Key:
auth.key="api_key_value"
Here's a complete device model demonstrating all features:
DEVICE SmartEnvironmentMonitor WITH description="Multi-sensor environmental monitoring device", author="john_doe", os=raspbian;
NETWORK[WiFi] WITH ssid="IoT_Network", password="secure_password";
BROKER[MQTT] SmartHomeBroker WITH
host="mqtt.smarthome.local",
port=1883,
ssl=True,
auth.username="sensor_node",
auth.password="node_pass";
USE RaspberryPi_4B_4GB;
USE BME680(EnvSensor) [poll_period = 5], SonarSRF04(DistanceSensor);
USE WS2812(StatusLED) [colors = ['0xFF0000', '0x00FF00', '0x0000FF']];
CONNECT EnvSensor WITH
POWER
gnd_1 -- GND,
power_5v -- VCC
DATA
i2c[slave_address=0x76] sda p_21 -- sda, scl p_22 -- scl
@ "home/environment/living_room";
CONNECT DistanceSensor WITH
POWER
gnd_2 -- gnd,
power_5v -- vcc
DATA
gpio[mode="output"] p_23 -- trigger,
gpio[mode="input"] p_24 -- echo
@ "home/distance/entrance";
CONNECT StatusLED WITH
POWER
gnd_3 -- GND,
power_5v -- VCC
DATA
gpio[mode="output"] GPIO10 -- DIN
@ "home/status/led";
DeMoL supports 35 sensor types and 23 actuator types covering a wide range of IoT applications:
- Environmental: Temperature, Humidity, Pressure, Gas, Env, AirQuality, Light, UV, Sound
- Motion & Position: Distance, Proximity, Motion, Presence, Acceleration, Gyroscope, Magnetometer, IMU, Tracker
- Specialized: ADC, Current, Voltage, Power, Flow, Level, Weight, Force, Vibration
- Smart: Camera, RFID, Fingerprint, GPS, Color
- Basic: MotorController, ServoController, Relay, Switch
- Display & Light: Led, LedArray, NeoPixel, Display, LCD, OLED
- Sound: Buzzer, Speaker
- Advanced: Stepper, DCMotor, Pump, Valve, Heater, Cooler, Fan
Each sensor and actuator type has a defined message schema for standardized communication:
Example Sensor Message (Environmental):
{
"temperature": 23.5,
"humidity": 65.2,
"pressure": 1013.25,
"gas": 450.0,
"timestamp": 1638360000000
}Example Actuator Command (NeoPixel):
{
"leds": [
{"index": 0, "r": 255, "g": 0, "b": 0},
{"index": 1, "r": 0, "g": 255, "b": 0}
],
"brightness": 128,
"mode": "static",
"timestamp": 1638360000000
}For complete documentation of all sensor and actuator types with their message schemas, see SENSORS_ACTUATORS.md.
For a complete formal specification of the DeMoL language, see SEMANTICS.md, which provides:
- Abstract Syntax: Mathematical representation of DeMoL constructs using syntactic domains and abstract syntax trees
- Formal Grammar: Complete EBNF specification of the concrete syntax
- Static Semantics: Well-formedness rules, type checking, and validation using inference rules
- Operational Semantics: Runtime behavior defined via small-step transition systems covering device initialization, broker connections, GPIO/I2C/SPI/UART operations, and message passing
- Axiomatic Semantics: Hoare logic specifications with pre/post conditions and invariants for device operations
- Type System: Complete type judgments, typing rules, and subtyping relations
- Verification Conditions: Safety properties (no short-circuits, voltage limits), liveness properties (message delivery, sensor readings), and correctness conditions
This formal foundation enables rigorous reasoning about device models, verified code generation, and static analysis tools.
DeMoL implements comprehensive semantic validations based on the formal semantics defined in SEMANTICS.md. These validations ensure device models are well-formed, safe, and correct before code generation.
Ensures electrical compatibility between board and peripheral power connections:
- Voltage Compatibility: Power pins must have compatible voltages (within 0.5V tolerance)
- GND Connections: Both pins must be GND when connecting ground
- VCC Connections: Non-GND voltages must match peripheral requirements
- Voltage Limits: Power supplied must not exceed peripheral's maximum rated voltage
Example Error:
[Conn-Power] Incompatible power connection: board pin power_5v (5.0V) cannot
connect to peripheral pin vcc (3.3V). Voltage difference exceeds 0.5V tolerance.
Validates pin functionality and protocol-specific requirements:
GPIO Connections:
- Both pins must have GPIO functionality
- Valid properties:
mode(input/output),pullup,pulldown - Mode must be either 'input' or 'output'
I2C Connections:
- Board and peripheral pins must have SDA/SCL functionality
- Slave address must be in range 0x00-0x7F
- Valid properties:
slave_address,bus_speed - All I2C addresses on the same bus must be unique
SPI Connections:
- All required pins (MOSI, MISO, SCK, CS) must have SPI functionality
- Valid properties:
bus_speed,mode(0-3)
UART Connections:
- TX/RX pins must have proper UART functionality
- Board TX connects to Peripheral RX (and vice versa)
- Baudrate must be a common value (9600, 115200, etc.)
- Valid properties:
baudrate,parity,stop_bits,data_bits
Example Errors:
[Conn-GPIO] Board pin GPIO5 does not have GPIO functionality.
[Conn-I2C] I2C slave address 0x80 out of valid range [0x00-0x7F]
[Conn-UART] Board pin TX connects to Peripheral TX. UART requires
connecting Board TX to Peripheral RX.
Critical safety validations to prevent hardware damage:
Pin Conflict Detection:
- Each board pin can only be used once (except I2C and power pins)
- I2C pins (SDA/SCL) can be shared (bus architecture)
- Power pins (GND/VCC) can be shared (common nets)
IO Voltage Compatibility:
- Board IO voltage must match peripheral IO voltage
- Prevents communication errors and potential damage
- Emits warnings for voltage mismatches
Common Ground Validation:
- Each peripheral should have at least one GND connection
- Ensures proper electrical reference and signal integrity
- Emits warnings when ground connection is missing
Example Errors:
[Safety-Pin-Conflicts] Pin conflict detected: Board pin 'GPIO4' is already
used by peripheral 'Sensor1' as 'GPIO'. Cannot reuse for peripheral 'Sensor2'.
[Safety-I2C-Address] I2C address conflict: Address 0x76 is already used by
peripheral(s): BME680. Cannot reuse for peripheral 'TempSensor'.
[Safety-IO-Voltage] IO Voltage Incompatibility: Board 'RaspberryPi_5_8GB'
operates at 5.0V (IO), but peripheral 'BME680' operates at 3.3V (IO).
Structural validations ensuring model completeness:
- All Peripherals Connected: Every peripheral must have at least one connection
- Unique Peripheral Names: All peripheral instances must have unique names
- Unique Pin Numbers: Pin numbers must be unique within each component
- Broker Requirements: Broker must be configured if remote endpoints are used
- Pin Existence: All referenced pins must exist in component definitions
Example Errors:
[WF-All-Peripherals-Connected] Unconnected peripherals detected: DistanceSensor.
All peripherals must have at least one connection defined.
[WF-Unique-Peripheral-Names] Duplicate peripheral name 'MySensor'. Peripheral
names must be unique within the device.
[WF-Unique-Pin-Numbers] Duplicate pin number 4 used by pins: GPIO4, SDA1. Pin
numbers must be unique within a component.
- Syntax Validation: textX parser validates grammar compliance
- Semantic Validation: Custom validators check:
- Power connection compatibility
- IO connection functionality
- Safety properties (pin conflicts, voltage limits)
- Well-formedness rules
- Warning Generation: Non-critical issues emit warnings:
- IO voltage incompatibility
- Missing ground connections
- Unusual baudrates
Validate a single model:
demol validate examples/rpi_iot_device.devValidate all examples:
python scripts/validate_examples.pyValidate builtin hardware models:
python scripts/validate_builtin_models.pySuccessful validation:
[*] Processing model: examples/rpi_iot_device.dev
[✓] All validation checks passed!
Validation with warnings:
[*] Processing model: examples/esp_iot_device.dev
⚠ [Safety-IO-Voltage] IO Voltage Incompatibility at examples/esp_iot_device.dev:26
[✓] Validation passed with warnings
Validation failure:
[*] Processing model: examples/invalid_device.dev
✗ [Conn-Power] Incompatible power connection: board pin power_5v (5.0V)
cannot connect to peripheral pin vcc (3.3V)
All semantic validations are implemented in demol/lang/semantics.py based on the formal semantics specification. The validation system uses:
- Type checking for pin functionality verification
- Constraint validation for safety properties
- Well-formedness rules for structural correctness
- Location tracking for precise error reporting
For the complete formal specification of validation rules, see SEMANTICS.md sections 4 (Well-Formedness), 7 (Type System), and 8 (Verification Conditions).
The DSL provides a command-line interface (CLI) for operating on models.
venv [I] ➜ demol --help
Usage: demol [OPTIONS] COMMAND [ARGS]...
An example CLI for interfacing with a document
Options:
--help Show this message and exit.
Commands:
gen
validate
The gen command allows you to execute Model-to-Text (M2T) transformations to generate code, documentation, or diagrams.
Usage:
demol gen [GENERATOR] [MODEL_FILE]Available Generators:
svg: Generates a professional schematic SVG diagram of the device connections.pi: Generates Python code for Raspberry Pi (using RPi.GPIO).riot: Generates C code for RiotOS (using RIOT-OS).
Example - Generate SVG Diagram:
demol gen svg examples/rpi_iot_device.devThis command will generate an SVG file (e.g., SmartEnvironmentMonitor.svg) in the current directory, visualizing the pin-level connections between the board and peripherals.
The validate command is used to validate input models.
To validate a device model, for example the ./examples/raspi_iot_device.dev, head to the examples directory and execute:
demol validate raspi_iot_device.devYou should see an output similar to the below, in case of successful validation of the model.
[*] Running validation for model rpi_iot_device.dev
PowerPinConnection:
gnd_1 -> gnd
PowerPinConnection:
power_5v -> vcc
I2C-Connection:
SDA: p_21 -> sda
SCL: p_22 -> scl
[*] Validation passed!Otherwise, the parser will raise an error:
textx.exceptions.TextXSemanticError: rpi_iot_device.dev:29:17: Unknown object "MyBME2" of class "PeripheralDef"DeMoL supports automated code generation for multiple platforms using a model-driven architecture.
The code generation system uses an abstract BaseCodeGenerator class that provides common model querying capabilities. Platform-specific generators inherit from this base class to implement target-specific logic.
Device Model → BaseCodeGenerator (abstract)
↓
┌───────┴────────┐
↓ ↓
RPiCodeGenerator ESPCodeGenerator (future)
↓ ↓
Templates Templates
- Raspberry Pi (Python): Generates Python code using
RPi.GPIO,smbus2, andspidev. - RiotOS (C): (In development) Generates C code for RiotOS-supported boards.
To generate code for a device model:
# Generate Raspberry Pi code
demol gen pi examples/rpi_iot_device.devThis will:
- Parse the device model
- Validate semantics
- Resolve platform-specific templates
- Generate the runtime software for the device
The DeMoL API provides REST endpoints for validating models and generating code. The API is secured with API keys.
Authentication
All API requests must include a valid API key in the X-API-Key header.
Endpoints
Validates a DeMoL model file (.dev or .hwd).
- Request:
multipart/form-datafile: The model file to validate.
- Example Request:
curl -X POST "http://localhost:8000/validate" \ -H "X-API-Key: YOUR_API_KEY" \ -F "file=@/path/to/your/model.dev"
- Success Response (
200 OK):{ "status": "success", "message": "Model validation successful" } - Error Response (
400 Bad Request):{ "detail": "Validation error: ..." }
Generates code or documentation from a DeMoL model file.
- Request:
multipart/form-datafile: The model file to generate code from.target: The generation target.
- Supported Targets:
plantuml: Generates a PlantUML diagram of the device.json: Generates a JSON representation of the model.
- Example Request:
curl -X POST "http://localhost:8000/generate" \ -H "X-API-Key: YOUR_API_KEY" \ -F "file=@/path/to/your/model.dev" \ -F "target=plantuml" \ --output generated_code.zip
- Success Response (
200 OK): A zip file containing the generated artifact(s) is returned. - Error Response:
400 Bad Request: If the target is invalid.501 Not Implemented: If the target is valid but not yet implemented (e.g.,rpi,docs).500 Internal Server Error: If code generation fails.
This directory contains tests for the DeMoL DSL, covering parsing, semantic validation, and model transformations.
To run the tests, ensure you have the virtual environment activated and pytest installed.
# Install test dependencies (if not already installed)
pip install pytest
# Run all tests
pytest tests/
# Run specific test file
pytest tests/test_board_semantics.py-
test_board_semantics.py: Validates Board model semantics.
- Port count consistency.
- Nested operational properties.
- Unique pin numbers.
-
test_component_semantics.py: Validates Component (Sensor/Actuator) semantics.
- Valid Sensor/Actuator definitions.
- Attribute parsing.
- Template parsing.
-
test_device_semantics.py: Validates Device model semantics.
- IO Voltage compatibility (Warning).
- Common ground connection (Warning).
- MQTT topic format validation.
- Pin function compatibility.
-
test_power_gpio_semantics.py: Validates Power and GPIO connection semantics.
- Power voltage compatibility.
- Ground connection rules.
- GPIO mode validation (input/output).
- GPIO property validation.
-
test_i2c_spi_semantics.py: Validates I2C and SPI connection semantics.
- I2C address range and uniqueness.
- I2C bus speed validation.
- Pin function checks (SDA/SCL).
-
test_uart_safety_semantics.py: Validates UART and Safety semantics.
- UART baudrate validation.
- Pin conflict detection (Safety-Unique-Pins).
- Unique peripheral names.
- Unconnected peripheral detection.
- Broker requirement validation.
DeMoL is protected under the MIT License. For more details, refer to the MIT LICENSE uri.
TODO ...
