Formal verification of a time-triggered hardware interface

Details Formal verification of a time-triggered hardware interface Formal verification of a time-triggered hardware interface

2011-03-11

arxiv.org/abs/1103.2246v1

Computer Science

Logic in Computer Science

30 pages, 16 figures

Scientific paper

We present a formal proof of a time-triggered hardware interface. The design implements the bit-clock synchronization mechanism specified by the FlexRay standard for automotive embedded systems. The design is described at the gate-level. It can be translated to Verilog and synthesized on FPGA. The proof is based on a general model of asynchronous communications and combines interactive theorem proving in Isabelle/HOL and automatic model-checking using NuSMV together with a model-reduction procedure, IHaVeIt. Our general model of asynchronous communications defines a clear separation between analog and digital concerns. This separation enables the combination of theorem proving and model-checking for an efficient methodology. The analog phenomena are formalized in the logic of Isabelle/HOL. The gate-level hardware is automatically analyzed using IHaVeIt. Our proof reveals the correct values of a crucial parameter of the bit-clock synchronization mechanism. Our main theorem proves the functional correctness as well as the maximum number of cycles of the transmission.

Affiliated with

Also associated with

No associations

Rating

Formal verification of a time-triggered hardware interface does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Formal verification of a time-triggered hardware interface, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Formal verification of a time-triggered hardware interface will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-430268