/BWDM

Test Cases Auto-Generation from a VDM++ Specification

Primary LanguageKotlinGNU General Public License v3.0GPL-3.0

BWDM: Verification tool for Vienna Development Method

Test Cases Auto-Generation from a VDM Specification.

codecov

Execution Environment, using Libraries,

  • OS : macOS or Linux
  • VDMJ Ver.4 : Lexer and Parser
  • Z3 : Theorem Prover
  • PICT : Pairwise Independent Combinatorial Testing
  • pict4java : PICT wrappers for java-class

install

  1. Install Microsoft Z3 library.
  2. Download BWDM.jar.

example

$ DYLD_LIBRARY_PATH=./libs java -Djna.library.path=./libs -Djava.library.path=./libs -jar BWDM.jar ./vdm_files/probrem.vdmpp -n -a -i -s -b -p -d

or

$ gradle run -Pargs="./vdm_files/problem.vdmpp"

options

Option Content
-n Basically Info.
-a Info. of BVA.
-i Info. of Symbolic Exe.
-b Output ONLY testcases of BVA.
-p Output ONLY testcases of BVA with pairwise.
-s Output OHLY testcases of Symbolic Exe.
-f Output testcase into a file(default:display on console).
-v Version.
-h Help.

build

$ DYLD_LIBRARY_PATH=./libs;LD_LIBRARY_PATH=./libs; export LD_LIBRARY_PATH; gradle jar