FlexRay: Verifikation of the FOCUS Specification in Isabelle/HOL. A Case Study

Title:: FlexRay: Verifikation of the FOCUS Specification in Isabelle/HOL. A Case Study
Document type:: Technical Report
Author(s):: Maria Spichkova
Abstract:: This paper represents a translation of the FOCUS specifications of the FlexRay communication protocol the Higher Order Logic specification in Isabelle/HOL and the corresponding formal Isabelle/HOL proofs for the translated specifications, which shows that the specified FlexRay architecture fulfills the specified FlexRay requirements.
Keywords:: FlexRay; FOCUS; formalization; specification; verification; refinement
Year:: 2006
Year / month:: 2006-02-01 00:00:00
Pages:: 26
BibTeX

Occurrences: