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.