Herramientas Personales
Usted está aquí: Inicio › Investigación › Grupos de Investigación › rfm › DynAlloy: An Efficient Extension of Alloy with Procedural Actions
 

DynAlloy: An Efficient Extension of Alloy with Procedural Actions

Welcome to DynAlloy Home Page

DynAlloy is an extension to the Alloy specification language to describe dynamic properties of systems using actions. Actions allow us to appropriately specify dynamic properties, particularly, properties regarding execution traces, in the style of dynamic logic specification.

DynAlloy extends Alloy’s syntax with a notation for partial correctness assertions, whose semantics relies on an adaptation of Dijkstra’s weakest liberal precondition. These assertions, defined in terms of actions, allow us to easily express properties regarding executions, favoring the separation of concerns between the static and dynamic aspects of a system specification.

Installing DynAlloy

  1. Download dynalloy4.zip (requires Java 1.6)
  2. unzip dynalloy4.zip
  3. cd dynalloy4
  4. Run the DynAlloy Analyzer

java -Djava.library.path=[your_arch] -jar dynalloy4.jar viz

The available architectures are: amd64-linux , x86-freebsd , x86-linux , x86-mac , x86-windows

Running a simple example

 

0. Download the list_example.dals model.

I. Load the list_example.dals file

dynalloy_viz_1.jpg

II. Execute command Check always_gt_zero. This command should return a counterexample.

III. Navigate through the counterexample trace. You may use the watches expressions to inspect any expression or formula value

 dynalloy_viz_2.png

The Language

DynAlloy language is composed of:

  • Atomic Actions: atomic transitions from a precondition P to a postcondition P'.
  • Programs: composed of atomic actions, test actions (assume P) sequential composition (S;S), a finite non-deterministic iteration (repeat {S}), while statements (while P do Q), conditionals (if P then Q else R}, variable assignment (L:=R), non-deterministic choice (S+S), and, program invocation (call S')
  • Dijkstra's Partial Correctness Assertions

    A more challenging DynAlloy model showing more of DynAlloy's grammar can be downloaded here. This DynAlloy model shows a partial correctness assertion for checking the correctness of a program inserting an element to a singly-linked list.

A grammar description of the DynAlloy extension to Alloy can be downloaded from dynalloyGrammar.txt

.

Publications

Please visit this link for a detailed list of publications on DynAlloy

About Us

DynAlloy was developed by the Relational Formal Methods Group at the Universidad de Buenos Aires.

Contact Us

Please email us any further question, comment or bug report at jgaleotti (AT) dc (DOT) uba (DOT) ar