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

Type of tool

Synthesis tool

Expected input

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.

Links

Repository: https://github.com/eskang/MappingSynthesisTool

Last commit date

3 February 2019

Related papers

https://doi.org/10.1007/978-3-030-25540-4_12 (CAV 2019)

Last publication date

12 July 2019

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.