Verification of real-time designs: Combining scheduling theory with automatic formal verification

We present an automatic approach to verify designs of real- Time distributed systems for complex timing requirements. We focus our analysis on designs which adhere to the hypothesis of analytical theory for Fixed-Priority scheduling. Unlike previous formal approaches, we draw from that theory and bu...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Braberman, V.A., Felder, M.
Formato: SER
Materias:
Analytical theory
Automatic approaches
Distributed systems
Fixed-priority scheduling
Formal verifications
Model checking tools
Scheduling analysis
Timing requirements
Automata theory
Design
Model checking
Scheduling
Software engineering
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_03029743_v1687LNCS_n_p494_Braberman
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id todo:paper_03029743_v1687LNCS_n_p494_Braberman
record_format dspace
spelling todo:paper_03029743_v1687LNCS_n_p494_Braberman2023-10-03T15:18:52Z Verification of real-time designs: Combining scheduling theory with automatic formal verification Braberman, V.A. Felder, M. Analytical theory Automatic approaches Distributed systems Fixed-priority scheduling Formal verifications Model checking tools Scheduling analysis Timing requirements Automata theory Design Model checking Scheduling Software engineering We present an automatic approach to verify designs of real- Time distributed systems for complex timing requirements. We focus our analysis on designs which adhere to the hypothesis of analytical theory for Fixed-Priority scheduling. Unlike previous formal approaches, we draw from that theory and build small formal models (based on Timed Automata) to be analyzed by means of model checking tools. We are thus integrating scheduling analysis into the framework of automatic formal verification. © Springer-Verlag Berlin Heidelberg 1999. Fil:Braberman, V.A. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. SER info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_03029743_v1687LNCS_n_p494_Braberman
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic Analytical theory
Automatic approaches
Distributed systems
Fixed-priority scheduling
Formal verifications
Model checking tools
Scheduling analysis
Timing requirements
Automata theory
Design
Model checking
Scheduling
Software engineering
spellingShingle Analytical theory
Automatic approaches
Distributed systems
Fixed-priority scheduling
Formal verifications
Model checking tools
Scheduling analysis
Timing requirements
Automata theory
Design
Model checking
Scheduling
Software engineering
Braberman, V.A.
Felder, M.
Verification of real-time designs: Combining scheduling theory with automatic formal verification
topic_facet Analytical theory
Automatic approaches
Distributed systems
Fixed-priority scheduling
Formal verifications
Model checking tools
Scheduling analysis
Timing requirements
Automata theory
Design
Model checking
Scheduling
Software engineering
description We present an automatic approach to verify designs of real- Time distributed systems for complex timing requirements. We focus our analysis on designs which adhere to the hypothesis of analytical theory for Fixed-Priority scheduling. Unlike previous formal approaches, we draw from that theory and build small formal models (based on Timed Automata) to be analyzed by means of model checking tools. We are thus integrating scheduling analysis into the framework of automatic formal verification. © Springer-Verlag Berlin Heidelberg 1999.
format SER
author Braberman, V.A.
Felder, M.
author_facet Braberman, V.A.
Felder, M.
author_sort Braberman, V.A.
title Verification of real-time designs: Combining scheduling theory with automatic formal verification
title_short Verification of real-time designs: Combining scheduling theory with automatic formal verification
title_full Verification of real-time designs: Combining scheduling theory with automatic formal verification
title_fullStr Verification of real-time designs: Combining scheduling theory with automatic formal verification
title_full_unstemmed Verification of real-time designs: Combining scheduling theory with automatic formal verification
title_sort verification of real-time designs: combining scheduling theory with automatic formal verification
url http://hdl.handle.net/20.500.12110/paper_03029743_v1687LNCS_n_p494_Braberman
work_keys_str_mv AT brabermanva verificationofrealtimedesignscombiningschedulingtheorywithautomaticformalverification
AT felderm verificationofrealtimedesignscombiningschedulingtheorywithautomaticformalverification
_version_ 1782028094338498560

Ejemplares similares