Cooperating Formal Methods Prototype Code

摘要

The prototype formal methods interface (FMI) can easily be linked to a variety offormal tools. This is achieved by representing the underlying specification language (RSML) in an attribute grammar and predefining a rich set of attributes that capture RSML semantics. A developer wishing to model aspects of RSML within a formal tool can access these predefined attributes directly, and may also add an arbitrary collection of new attributes. Editable WEB-style templates simplify this task. This attachment demonstrates the usefulness of our techniques by showing how the EVES and PVS theorem provers and the SPIN model checker were rapidly linked to the FMI.