Formal methods at the systems level
Perry Alexander, Phillip Baraona · 2002
This paper presents an attempt at using formal methods as engineering mathematics. We present a Larch interface language for VHDL, called VSPEC, that provides a mechanism for specifying and analyzing systems level requirements. Further, this language supports abstractions and concepts familiar to traditional digital hardware designers. Using VSPEC, it is possible to specify and verify both functional requirements and constraints. Components are specifying using the traditional axiomatic style extended to include performance constraints and activation conditions. Additionally, using VHDL's structural specification features, it is possible to specify and verify abstract architectures formally. The paper opens by describing general characteristics of VSPEC including single component representation and architecture representation. Design rationale are presented to show how VSPEC provides familiar abstractions to the system designer. Finally, annotated examples are presented to demonstrate the language and its expected uses.