📦 Latest pre-release: v0.1-beta

hyperAlloy Analyzer

This tool extends the Alloy Analyzer to support formal verification of hyperproperties specified in HyperLTL, leveraging HyperQB and AutoHyper backends.

• HyperQB: recommended for general hyperproperty verification scenarios.
• AutoHyper: still in its early development stage, supports only the analysis of very simple models.

Requirements

Alloy runs on all operating systems with a recent JVM (Java 6 or later). It is made available as a runnable jar file with both a cross-platform SAT solver (Sat4j and more efficient native SAT solvers (minisat, lingeling/plingeling, glucose).

To perform hyperproperty analysis, one needs to have installed Electrod program, as well as NuSMV, nuXmv and HyperQB.

Important:

1. Add HYPERQB_HOME environment variable.
2. Running docker without needing sudo.

Running

Download the executable jar (or build it) and launch it simply as

 $ java -jar hyperAlloy.jar

TL;DR

Checkout the project and type ./gradlew build. You find the executable JAR in org.alloytools.alloy.dist/target/org.alloytools.alloy.dist.jar after the build has finished.

 $ java -version           # requires 1.8 (and NOT 1.9, gradle does not run on 1.9)
 java version "1.8.0_144"
 Java(TM) SE Runtime Environment (build 1.8.0_144-b01)
 Java HotSpot(TM) 64-Bit Server VM (build 25.144-b01, mixed model
 $ git clone --recursive https://github.com/rfago/hyperAlloy.git
 $ cd hyperalloy
 $ ./gradlew build
 $ java -jar org.alloytools.alloy.dist/target/org.alloytools.alloy.dist.jar
 # opens GUI

Building Alloy

The Alloy build is using a bnd workspace setup using a maven layout. This means it can be build with Gradle and the Eclipse IDE for interactive development. Projects are setup to continuously deliver the executable.

Projects

The workspace is divided into a number of projects:

• cnf – Setup directory. Dependencies are specified in [cnf/central.xml] using the maven POM layout
• org.alloytools.alloy.application – Main application code includes the parser, ast, visualiser, and application code
• org.alloytools.alloy.dist – Project to create the distribution executable JAR
• org.alloytools.alloy.extra – Models and examples
• org.alloytools.pardinus – A Kodkod extension without native code
• org.alloytools.kodkod.nativesat – The native code libraries for Kodkod

Relevant Project files

This workspace uses bnd. This means that the following have special meaning:

• cnf/build.xml – Settings shared between projects
• ./bnd.bnd – Settings for a project. This file will drag in code in a JAR.
• cnf/central.xml – Dependencies from maven central

Eclipse

The workspace is setup for interactive development in Eclipse with the Bndtools plugin. Download Eclipse and install it. You can then Import existing projects from the Git workspace. You should be asked to install Bndtools from the market place. You can also install Bndtools directly from the Eclipse Market place (see Help/Marketplace and search for Bndtools).

Bndtools will continuously create the final executable. The projects are setup to automatically update when a downstream project changes.

Run hyperAlloy

After having built hyperAlloy and all its dependencies, you are ready to use hyperAlloy. You can run hyperAlloy by running

 $ java -jar hyperAlloy.jar

Test hyperproperties with HyperQB and AutoHyper

Once the Alloy model has been defined without errors, we can proceed with the verification of hyperproperties. The process begins by defining a sig that contains all the atoms necessary for the verification of the hyperproperty. We illustrate this process with a simple example:

sig A, B extends Main {}

hyperltl hyperprop {
     forall A. exists B. G (A.Prop1 = B.Prop2)             
}


verify hyperprop //@hyperqb: [10 -pes -find]

verify hyperprop //@autohyper: []