RADLER
Overview
RADLER is a comprehensive framework designed for developing distributed real-time systems with verifiable behaviors. It implements a publish/subscribe architecture where computational nodes execute quasi-periodically within defined time bounds, communicating through typed message channels with guaranteed delivery constraints. The framework provides a specialized architecture definition language (RADL) that enables developers to specify both logical and physical aspects of their distributed system, including node periodicities, communication patterns, and resource mappings. RADLER's distinctive features include its certified build system, formal verification capabilities, and contract-based development approach, allowing developers to establish and verify critical system properties such as timing constraints, type safety, and behavioral correctness. The framework supports traceable requirement implementation and includes tools for analyzing worst-case execution times, making it particularly suitable for safety-critical applications in domains where predictable behavior and formal verification are essential. By combining these features with a robust runtime environment that handles inter-node communication and execution scheduling, RADLER provides a complete solution for building reliable distributed systems that can be formally verified to meet their specifications.
Radler Tool Demo Video
Radler Architecture Definition Language
Radler Example for Advanced Fail Safe of Arducopter using MAVROS to handle battery low level conditions (https://github.com/SRI-CSL/radler/tree/ros2/examples/ardupilot)
Radler architecture as performed in an assurance-driven design process for the DesCert Project
Playlist
-
DesCert ConOps
-
Radler Architecture Definition Language
-
Arducopter Advanced Fail Safe System in Radler
-
Radler Architecture in the DesCert Project
Links
Contacts
-
Natarajan Shankar
Contributors
-
Léonard Gérard
-
Minyoung Kim
-
Aravind Sundaresan
-
Natarajan Shankar