[vc_empty_space][vc_empty_space]
Formal verification of integrated modular avionics (IMA) health monitoring using timed automata
Budiyanto I.B.a, Kistijantoro A.I.b, Trilaksono B.R.b
a Informatics Department, Politeknik TEDC Bandung, Cimahi, Indonesia
b School of Electronics Engineering and Informatics, Institut Teknologi Bandung, Bandung, Indonesia
[vc_row][vc_column][vc_row_inner][vc_column_inner][vc_separator css=”.vc_custom_1624529070653{padding-top: 30px !important;padding-bottom: 30px !important;}”][/vc_column_inner][/vc_row_inner][vc_row_inner layout=”boxed”][vc_column_inner width=”3/4″ css=”.vc_custom_1624695412187{border-right-width: 1px !important;border-right-color: #dddddd !important;border-right-style: solid !important;border-radius: 1px !important;}”][vc_empty_space][megatron_heading title=”Abstract” size=”size-sm” text_align=”text-left”][vc_column_text]© 2015 IEEE.Specifications of safety-critical real-time systems which are made with natural language has many disadvantages, such as contradictory, vague, ambiguous, and incomplete. The weakness in this specification will continue to the next stages, and will result the system failure. Formal methods allow the designer to determine the specifications of the system at different abstraction levels and verify the consistency of this formal specification before it is implemented. This study aimed to build and verify the formal specification of integrated modular avionics (IMA) health monitoring which use the ARINC-653 standard using a model checking timed automata. The verified results will help developers to define logic effective of fault-tolerance, so as to guarantee the IMA system can always available.[/vc_column_text][vc_empty_space][vc_separator css=”.vc_custom_1624528584150{padding-top: 25px !important;padding-bottom: 25px !important;}”][vc_empty_space][megatron_heading title=”Author keywords” size=”size-sm” text_align=”text-left”][vc_column_text]Abstraction level,ARINC-653,Health monitoring,IMA,Integrated modular avionics,Natural languages,System failures,Timed Automata[/vc_column_text][vc_empty_space][vc_separator css=”.vc_custom_1624528584150{padding-top: 25px !important;padding-bottom: 25px !important;}”][vc_empty_space][megatron_heading title=”Indexed keywords” size=”size-sm” text_align=”text-left”][vc_column_text]ARINC-653,health monitor,IMA,timed automata[/vc_column_text][vc_empty_space][vc_separator css=”.vc_custom_1624528584150{padding-top: 25px !important;padding-bottom: 25px !important;}”][vc_empty_space][megatron_heading title=”Funding details” size=”size-sm” text_align=”text-left”][vc_column_text][/vc_column_text][vc_empty_space][vc_separator css=”.vc_custom_1624528584150{padding-top: 25px !important;padding-bottom: 25px !important;}”][vc_empty_space][megatron_heading title=”DOI” size=”size-sm” text_align=”text-left”][vc_column_text]https://doi.org/10.1109/ISITIA.2015.7219994[/vc_column_text][/vc_column_inner][vc_column_inner width=”1/4″][vc_column_text]Widget Plumx[/vc_column_text][/vc_column_inner][/vc_row_inner][/vc_column][/vc_row][vc_row][vc_column][vc_separator css=”.vc_custom_1624528584150{padding-top: 25px !important;padding-bottom: 25px !important;}”][/vc_column][/vc_row]