Sie befinden Sich nicht im Netzwerk der Universität Paderborn. Der Zugriff auf elektronische Ressourcen ist gegebenenfalls nur via VPN oder Shibboleth (DFN-AAI) möglich. mehr Informationen...
Rigorous development process of a safety-critical system: from ASM models to Java code
Ist Teil von
International journal on software tools for technology transfer, 2017-04, Vol.19 (2), p.247-269
Ort / Verlag
Berlin/Heidelberg: Springer Berlin Heidelberg
Erscheinungsjahr
2017
Link zum Volltext
Quelle
Alma/SFX Local Collection
Beschreibungen/Notizen
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.