Model-based simulation at runtime with abstract state machines

Software systems are rapidly growing in complexity and scale, and are subject to different kinds of uncertainties related to the dynamics of resource availability or changes in system objectives. So, many real usage scenarios might be impossible to reproduce and validate at design-time. As envisioned by the Models@run.time research community, the use of models at runtime is fundamental to address this challenge. Our focus is on providing guarantees for changing safety goals at runtime (a form of uncertainty) with the employment of mathematically-based runtime analysis techniques from the area of formal methods (FM@run.time). In this paper, we propose a novel framework for the runtime simulation of Abstract State Machine models and the on-the-fly changes of safety assertions at the model level to provide software assurance guarantees at runtime. The framework is called AsmetaS@run.time and is being developed as part of the ASM specification and analysis toolset ASMETA.