Rigorous development process of a safety-critical system: from ASM models to Java code

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F17%3A10312267" target="_blank" >RIV/00216208:11320/17:10312267 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/s10009-015-0394-x" target="_blank" >http://dx.doi.org/10.1007/s10009-015-0394-x</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/s10009-015-0394-x" target="_blank" >10.1007/s10009-015-0394-x</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Rigorous development process of a safety-critical system: from ASM models to Java code

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Rigorous development process of a safety-critical system: from ASM models to Java code

Popis výsledku anglicky

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.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2017

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

International Journal on Software Tools for Technology Transfer

ISSN

1433-2779

e-ISSN

—

Svazek periodika

19

Číslo periodika v rámci svazku

2

Stát vydavatele periodika

DE - Spolková republika Německo

Počet stran výsledku

23

Strana od-do

247-269

Kód UT WoS článku

000398167200007

EID výsledku v databázi Scopus

2-s2.0-84938650937