Abstract
The paper presents an approach for rigorous development of safety-critical systems based on the Abstract State Machine formal
method. The development process starts from a high level formal view of the system and, through refinement, derives more detailed
models till the desired level of specification. Along the process, different validation and verification activities are available,
as simulation, model review, and model checking. Moreover, each refinement step can be proved correct using an SMT-based approach.
As last step of the refinement process, a Java implementation can be developed and linked to the formal specification. The
correctness of the implementation w.r.t. its formal specification can be proved by means of model-based testing and runtime
verification. The process is exemplified by using a Landing Gear System as case study.
[read the copyright and download the pdf file] [DOI]