Unified Verification and Monitoring of Executable UML Specifications

This repository contains the formalization in Lean (https://leanprover.github.io/) of:

• our Semantic Transition Relation (STR) interface,
• our EMI2STR adapter used to implement the STR interface with our model interpreter interface,
• our synchronous composition operator,
• our operator used to add implicit transitions.

The Lean code provided in the formalization.lean is machine-checkable. To check its validity, it can be loaded in the Web editor of Lean.