PV2 ⊧ Mapping Synthesis Toolgiven a high level spec and a low level spec, produces a set of property-preserving mappings

Tool to synthesize a set of implementation decisions ensuring that a desired property is preserved from a high-level design into a low-level platform implementation

Application domain/field

• Event-based behavioural models
• Synthesis

Type of tool

Synthesis tool

Expected input

• Processes P and Q
• Specification $\Phi$
• Mapping constraint C

Format:

Alloy model (.als file)

Expected output

If it exists, a maximal set of mappings that ensures that the resulting platform implementation preserves the given property.

Internals

Uses Alloy and Alloy Analyzer

Comments

Note the authors themselves call this a "prototype implementation" and it doesn't seem to have been updated since the paper was published.