← All projects
Research Formal Verification Unity CEA LIST

ARTiMon

A research demo for CEA LIST (French Atomic Energy Commission) integrating the ARTiMon runtime monitoring engine into a Unity serious game.

Context

ARTiMon is a formal verification engine developed by CEA LIST that evaluates temporal logic specifications against real-time data streams. The challenge for this demo was to connect ARTiMon to a live Unity serious via a Raspberry Pi and demonstrate runtime biosensor monitoring in an interactive setting.

What I built

I was one of two contributors, owning the formal specification, the hardware bridge, the Unity socket client, and the entire biosensor simulation system.

C socket bridge on Raspberry Pi — A TCP server that receives sensor data from Unity, tokenises the payload, and feeds it into ARTiMon's embedded C API — creating a frame-by-frame Unity → TCP → C → ARTiMon pipeline.

Unity TCP socket client — A C# MonoBehaviour that opens a persistent connection to the Raspberry Pi and streams data once per second.

Biosensor simulation system — Simulates realistic physiology from in-game state.

Outcome

A product booth featured in CEA LIST's showroom demonstrating their research.