Executable Operational Semantics of Reflex Language

Abstract

This paper discusses the construction of a formal executable operational semantics for Reflex, a process-oriented programming language designed for embedded and distributed microcontroller systems. The work is motivated by the need to improve the reliability of software in such systems, and also by the fact that earlier formal descriptions of Reflex were based on an outdated version of the language and were not executable, which limited their use for automated verification and for building correct tooling. The paper provides basic information about the language and the ABML notation used to formalize the semantic model. The main focus is on building an ontological model of Reflex that describes constants, identifiers, data types, expressions, operators, and declarators as ABML types. This ontology defines the static structure of a valid program and serves as a foundation for further model execution, as well as for formal analysis of syntactic and semantic correctness of program constructs. A separate section discusses the limitations of the proposed semantics. We clarify the assumptions made, including the lack of modeling for interrupts, node concurrency, physical variables, and C embeddings. We describe the preprocessing steps for ontological models: name resolution, detection of implicit type conversions, and normalization of language constructs. These transformations help unify the internal representation of programs and prepare them for formal execution. The paper also formalizes the operational semantics of Reflex using an agent-based model and attribute closures. We define the structure of agents responsible for evaluating models, as well as the environment that stores global static information for the agents and determines the evaluation order. The results provide a formal foundation for further development of deductive verification tools, static analysis, and a verified compiler for the Reflex language.