Abstract
Safety-critical systems require development methods and processes that lead to provably correct systems in order to prevent
catastrophic consequences due to system failure or unsafe operation. The use of models and formal analysis techniques is highly
demanded both at design-time, to guarantee safety and other desired qualities already at the early stages of the system development,
and at runtime, to address requirements assurance during the system operational stage. In this paper, we present the modeling
features and analysis techniques supported by ASMETA (ASM mETAmodeling), a set of tools for the Abstract State Machines formal
method. We show how the modeling and analysis approaches in ASMETA can be used during the design, development, and operation
phases of the assurance process for safety-critical systems, and we illustrate the advantages of integrated use of tools as
that provided by ASMETA.
[download the pdf file] [DOI] [url]