Interface Specifications

Hi. Ny name is Brian Bailey and I will admit at the onset, that I have,
at present, a very small knowledge base in formal methods and their 
underlying mathematics. So, forgive me if I make some absurd comments. Please
correct me as you feal appropriate.

My interest in Larch, is perhaps, a little different from its current purpose.
I am looking for a way to express the interface between the hardware and
software components of an embedded system. In many companies, this interface
is incompletely described, is open to many interpretations and as a result, when
the hardware has been designed and built, and the software is loaded: it doesnt
work. I am looking at possible solutions to this problem and so Larch appears
to me to be a possible may to describe the interface. Tools would then need
to be constructed to ensure the implementations of both the hardware and the
software conform to this single specification.

I understand that this does not formally prove the quality or completeness of
the interface definition, but it seams to me to be a good starting point for
the deployment of some level of formality in the design process.

Any comments or suggestions would be greatly received.