Readle: A Formal Framework for Designing AI-based Edge Systems

TL;DR

Readle is a formal framework that systematically captures and unifies constraints in both edge system design and deep learning, aiding the development of reliable AI-based edge systems.

Contribution

The paper introduces READLE, a novel extendable approach using real-time logic and binary decision diagrams to formalize specifications for edge AI systems.

Findings

Unified specification generation for edge and deep learning constraints

Enhanced formal representation of timing and accuracy constraints

Insights to guide future formal methods in edge AI system design

Abstract

With the wide spread use of AI-driven systems in the edge (a.k.a edge intelligence systems), such as autonomous driving vehicles, wearable biotech devices, intelligent manufacturing, etc., such systems are becoming very critical for our day-to-day lives. A challenge in designing edge intelligence systems is that we have to deal with a large number of constraints in two design spaces that form the basis of such systems: the edge design space and the deep learning design space. Thus in this work, a new systematic, extendable, manual approach, READLE, is proposed for creating representations of specifications in edge intelligent systems, capturing constraints in the edge system design space (e.g. timing constraints and other performance constraints) and constraints in the deep learning space (e.g. model training duration, required level of accuracy) in a coherent fashion. In particular, READLE leverages benefits of real-time logic and binary decision diagrams to generate unified specifications. Several insights learned in building READLE are also discussed, which should help in future research in the domain of formal specifications for edge intelligent systems.