Formal specification of a reactive system: an exercise in VHDL, LOTOS and UNITY
Laurence Pierre · 1996
Introduction To guarantee the correctness of hardware/software systems, formal verification provides an alternative approach to methods such as test, or simulation. In that framework, one can either formally verify that an implementation of the expected device/program fulfills its specification, or transform the initial specification by stepwise correctnesspreserving refinements. In both cases, an informal specification does not suffice. This is the reason why formal languages or methods, such as Z, VDM, B, CSP, CCS are becoming so vital in today's world where the importance of specifying and validating distributed architectures/programs, concurrent and reactive systems, communication protocols,... is increasing every day. We are developing a specification and proof environment, called PREVAIL [1], which is to support several input languages (currently, only VHDL is supported) and which proposes a set of proof tools to verify appropriate descriptions/specifications. Nqthm [2]