Projects

FOAM tool

Project: FOAM tool - Verification of Use-Cases
Managed by: ViliamSimko
Homepage http://vlx.matfyz.cz/Projects/FoamTool
Abstract My PhD Thesis focuses on formal verification of textual use-cases.

The FOAM tool allows users to capture behaviour in use-cases using annotations and to verify various temporal constraints.


Edit gallery

DEMO of the FOAM tool

Direct Download

Prerequisities and Notes

  • This demo works on Linux and Windows
    • tested on Linux Mint 14 Nadia 64bit
    • tested on Windows 7 64bit
  • FOAM tool is a console-based application. Do not expect any GUI! However, the generated HTML report should be viewed in a web browser.
  • Java 1.7+ must be installed (check out java -version)
  • Graphviz DOT 2.30+ must be installed (check out dot -V)
  • The archive contains a bundled NuSMV model checker - a binary blob for Linux and Windows. Latest NuSMV version can be downloaded from http://nusmv.fbk.eu/
  • After running the demos, open the generated html-report in your web browser, e.g. foam-demo/examples/valid-specification/html-report/index.html

Instructions for running the DEMO on Linux

  1. Download the archive FOAM tool demo (ZIP 26M)
  2. Open a terminal where you downloaded the ZIP file
  3. Extract the ZIP, e.g. unzip foam-demo-2013-05-03.zip
  4. Go into the extracted directory: cd foam-demo
  5. Run the script: ./run-foam-demo.sh
  6. The script displays a message telling you that it requires a single parameter.
 ./run-foam-demo.sh valid   - demo of valid specification
 ./run-foam-demo.sh invalid - demo of invalid specif.

Instructions for running the DEMO on Windows

  1. Download the archive FOAM tool demo (ZIP 26M)
  2. Extract the archive, e.g. using Explorer
  3. Open the console - press Win+R and type cmd
  4. Navigate to the extracted directory by typing cd "C:\Path\To\The\Extracted\foam-demo"
  5. Run the script: run-foam-demo.bat
  6. The script displays a message telling you that it requires a single parameter.
 run-foam-demo.bat valid   - demo of valid specification
 run-foam-demo.bat invalid - demo of invalid specif.

Theoretical Background

First paper

The method has been outlined for the first time in the following paper: Simko V., Hnetynka P., Bures T., Plasil F.: FOAM : A Lightweight Method for Verification of Use-Cases, Proceedings of 38th EUROMICRO Conference on Software Engineering and Advanced Applications (SEAA'12), pp.228-232, September 5-8, 2012, Cesme, Izmir, Turkey, doi: 10.1109/SEAA.2012.15, PDF

Further development

It has been later extended in our Tech. Report and a submission to a journal is pending: Simko V., Hnetynka P., Bures T., Plasil F.: Formal Verification of Annotated Use-Cases (FOAM Method), Tech. Report No. 2012/2, D3S, Charles University in Prague, February 2012, PDF