ASMETA: A comprehensive tool set for formal system engineering based on abstract state machines

ASMETA is a tool set for the formal specification, validation, and verification of discrete event systems. It is based on the Abstract State Machine (ASM) formal method, and provides an interactive environment for editing and analyzing ASM models, as well as for transforming high-level models into code. ASMETA also integrates runtime validation and verification techniques to ensure runtime assurance and enforcement of systems. This paper provides a comprehensive overview of ASMETA, detailing its software architecture, capabilities, and illustrative applications. It concludes with a discussion on its impact and emerging research directions in cutting-edge domains, including runtime safety assurance, safeguarding of autonomous systems, and the use of formal models in next-generation Digital Twins.