[Import DiVinE website as a basic help for GUI.
xmoracek@fi.muni.cz**20100117200453
Ignore-this: 7b03de488ca27964540fc41b6824dce
] adddir ./gui/help
addfile ./gui/help/CMakeLists.txt
hunk ./gui/help/CMakeLists.txt 1
+find_package(Qt4 REQUIRED)
+include(${QT_USE_FILE})
hunk ./gui/help/CMakeLists.txt 4
+file(GLOB HELP_SOURCE about.txt gui/* divine/* divine/pics/*)
+
+# QT_QCOLLECTIONGENERATOR_EXECUTABLE is defined in CMake 2.8
+if(${QT_QCOLLECTIONGENERATOR_EXECUTABLE})
+
+ add_custom_command(OUTPUT help_collection
+ COMMAND ${QT_QCOLLECTIONGENERATOR_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/divine-ide.qhcp
+ DEPENDS ${HELP_SOURCE}
+ )
+
+ add_custom_target(base_help ALL
+ DEPENDS help_collection
+ )
+
+ install(FILES divine-ide.qhc divine.qch DESTINATION ${GUI_HELP_DEST} COMPONENT help)
+
+ if(WIN32)
+ find_path(GUI_ASSISTANT_EXECUTABLE assistant.exe)
+ find_path(GUI_QTHELP_DLL QtHelp4.dll)
+ find_path(GUI_QTCLUCENE_DLL QtCLucene4.dll)
+ find_path(GUI_QTNETWORK_DLL QtNetwork4.dll)
+ find_path(GUI_QTSQL_DLL QtSql4.dll)
+ find_path(GUI_QTXML_DLL QtXml4.dll)
+ find_path(GUI_QTXMLPAT_DLL QtXmlPatterns4.dll)
+ find_path(GUI_QTWEBKIT_DLL QtWebKit4.dll)
+ find_path(GUI_QTPHONON_DLL phonon4.dll)
+ find_path(GUI_QTSQLITE_DLL qsqlite4.dll HINTS ${GUI_QTHELP_DLL}/../plugins/sqldrivers)
+ install(FILES ${GUI_ASSISTANT_EXECUTABLE}/assistant.exe DESTINATION ${GUI_BIN_DEST} COMPONENT help)
+ install(FILES ${GUI_QTHELP_DLL}/QtHelp4.dll DESTINATION ${GUI_BIN_DEST} COMPONENT help)
+ install(FILES ${GUI_QTCLUCENE_DLL}/QtCLucene4.dll DESTINATION ${GUI_BIN_DEST} COMPONENT help)
+ install(FILES ${GUI_QTNETWORK_DLL}/QtNetwork4.dll DESTINATION ${GUI_BIN_DEST} COMPONENT help)
+ install(FILES ${GUI_QTSQL_DLL}/QtSql4.dll DESTINATION ${GUI_BIN_DEST} COMPONENT help)
+ install(FILES ${GUI_QTXML_DLL}/QtXml4.dll DESTINATION ${GUI_BIN_DEST} COMPONENT help)
+ install(FILES ${GUI_QTXMLPAT_DLL}/QtXmlPatterns4.dll DESTINATION ${GUI_BIN_DEST} COMPONENT help)
+ install(FILES ${GUI_QTWEBKIT_DLL}/QtWebKit4.dll DESTINATION ${GUI_BIN_DEST} COMPONENT help)
+ install(FILES ${GUI_QTPHONON_DLL}/phonon4.dll DESTINATION ${GUI_BIN_DEST} COMPONENT help)
+ install(FILES ${GUI_QTSQLITE_DLL}/qsqlite4.dll DESTINATION ${GUI_BIN_DEST}/plugins/sqldrivers COMPONENT help)
+
+ # FIXME: additional hardcoded dependencies
+ find_file(GCC_DW_LIB libgcc_s_dw2-1.dll)
+ install(FILES ${GCC_DW_LIB} DESTINATION ${GUI_BIN_DEST} COMPONENT help)
+ endif(WIN32)
+
+endif(${QT_QCOLLECTIONGENERATOR_EXECUTABLE})
addfile ./gui/help/about.txt
hunk ./gui/help/about.txt 1
-
+DiVinE IDE is a development environment for DiViNE LTL model
+checking system.http://divine.fi.muni.cz
adddir ./gui/help/divine
addfile ./gui/help/divine-ide.qhcp
hunk ./gui/help/divine-ide.qhcp 1
+
+
+
+ DiVinE IDE Help
+ qthelp://divine.ide.base/doc/index.html
+ qthelp://divine.ide.base/doc/index.html
+
+ divine/pics/divine-ico.png
+ false
+ false
+
+ ParaDiSe/DiVinE IDE
+
+ About
+
+
+ about.txt
+ divine/pics/divine-logo.png
+
+
+
+
+
+
+ divine.qch
+
+
+
+ divine.qch
+
+
+
addfile ./gui/help/divine/casestudies.html
hunk ./gui/help/divine/casestudies.html 1
+
+
+
+
+ DiVinE Case Studies
+
+
+
+
+
+
+
+
+
+
+
+ Experimental evaluation of DiVinE Tools
+
+
The overall goal of DiVinE is to efficiently utilize available
+ computational resoururces to complete its verification task or complete it
+ sooner. The efficiency of selected DiVinE Tools is reported in the following
+ several case studies.
+
+
+
DiVinE Cluster on DAS-3
+
+
In this experiment we evaluated performance of algorithms MAP and OWCTY
+ as implemented in DiVinE Cluster . Our primary aim was to show that the
+ tool can scale up to 256 CPU cores. Our performance evaluation was done on
+ the Distributed ASCI Supercomputer (DAS-3), a wide-area distributed system
+ for Computer Science research in the Netherlands. The casestudy was done
+ by Kees Verstoep from VU University, Amsterdam.
+
+
Distributed ASCI Supercomputer (DAS-3)
+
+
DAS-3 consists of five clusters distributed over four sites. It uses
+ Myri-10G networking technology from Myricom both as an internal high-speed
+ interconnect as well as an interface to remote DAS-3 clusters. DAS-3 is
+ largely homogeneous: every cluster uses dual-CPU AMD Opteron nodes, but
+ with different clock speeds and/or number of CPU cores. For the purpose
+ of this experiment we employ DAS-3 cluster at VU University, which has the
+ largest number of compute nodes and cores (85 nodes with a dual-cpu,
+ dual-core 2.4 GHz AMD Opterons).
+
+
+
Intitial experiments on DAS-3 were performed with DiVinE Cluster
+ version 0.7.2 that contained several performance flaws due to which an
+ efficient usage of the tool was limited to clusters with small number of
+ nodes (less than 20). However, we succeed to optimize the tool to
+ efficently employ much larger number of cores that were available on DAS-3
+ system. The optimized implementation reffered below corresponds to the
+ DiVinE Cluster version 0.8 (will be released shortly).
+
+
Experiments on Scalability and Efficiency
+
+
First, we show graphs depicting the scalability of unoptimized and
+ optimized implementations. For the purpose of this experiment, we run
+ DiVinE Cluster on anderson.8.prop.dve model from BEEM database. Each line in the
+ graphs below shows scalability for the given number of nodes when using 1
+ core per node, 2 cores per node, and 4 cores per node.
+
+
+
+
+ MAP Scalability
+ OWCTY Scalability
+
+
+
+
+
+
+
+
To get an estimate on the efficiency of MAP and OWCTY, we ran
+ single-core versions on a special DAS-3/VU node equipped with 16GB memory
+ (the regular compute nodes have 4GB, which is insufficient to store the
+ state space there). The efficiencies of optimized implementations are
+ quite good even for 256 cores. In particular, MAP on a single core took
+ 1052.5 sec; the runtimes on 64, 128, and 256 cores are 23.0, 13.1, and 8.9
+ sec, giving efficiencies of 72%, 63% and 46%, respectively. OWCTY on a
+ single core took 631.7 sec; the runtime on 64, 128, and 256 cores are
+ 13.3, 7.4 and 5.0 sec, giving efficiencies of 74%, 67% and 49%,
+ respectively. The results are shown in the two following tables.
+
+
+
+
+ MAP Efficiency
+ OWCTY Efficiency
+
+
+
+ Cores Runtime (sec) Efficiency 1 1052.5 100% 64 23.0 72% 128 13.1 63% 256 8.9 46%
+
+
+ Cores Runtime (sec) Efficiency 1 631.7 100% 64 13.3 74% 128 7.4 67% 256 5.0 49%
+
+
+
+
+
+
+
Measuring Network Throughput
+
+
The following graphs illustrate the effect of the improvements on the
+ applications' throughput as a function of their runtime. In this case a
+ larger instance of the Anderson problem was used to obtain a higher
+ resolution graph.
+
+
+
+
+ MAP Throughput
+ OWCTY Throughput
+
+
+
+
+
+
+
+
+
+
+
DiVinE Multi-Core Performance Evaluation
+
+
The following tables reports on selected runtimes for Reachability and
+ LTL model checking verification tasks performed using DiVinE Multi-Core
+ version 1.1 . You may also be interested in the table with all
+ experiments .
+
+
Reported runtimes are in seconds (rounded). All models come from the
+ BEEM database . The
+ meassurements were performed for two different architectures:
+
+
+ manwe : 8x Dual Core AMD Opteron(tm) Processor 885
+ pheme : 2x Intel Xeon CPU 5130 @ 2.00GHz
+
+
+
+
The value X -- denotes that the corresponding
+ experiment was not performed.!
+
+
Reachability (generation of all reachable states)
+
+
Model divine @
+ manwe_64bit 1 core 2 cores 4 cores 8 cores 16
+ cores
divine @
+ pheme_64bit 1 core 2 cores 3 cores 4 cores
2:49:29 X 25:28 X 16:28 X 11:44 X 13:18 X
34:52 X 5:14 X 3:17 X 2:48 X
30:39 24:29 18:22 19:17 18:46
24:17 X 18:40 X 14:20 X 14:08 X
2:15:04 X 1:52:44 X 30:47 X 12:53 X 5:19 X
34:43 X 20:05 X 7:21 X 6:51 X
2:12:03 X 32:43 X 15:50 X 0 X 5:11 X
24:23 X 8:05 X 4:59 X 4:06 X
1:04:03 30:03 13:49 7:20 3:33
15:06:33 X 3:30:19 X 1:12:51 X 31:56 X 13:04 X
2:22:41 X 34:44 X 19:48 X 14:44 X
13:55 12:22 12:24 12:24 13:42
10:09 X 10:16 X 10:09 X 10:15 X
1:53:48 43:39 X 32:26 17:33 9:20
40:07 X 6:18 X 3:41 X 3:34 X
+
+
+
LTL Model checking
+
+
+
+ Model divine @ manwe_64bit 1 core 2 cores 4
+ cores 8 cores 16 cores
divine @ pheme_64bit 1 core 2 cores 3
+ cores 4 cores
49:21 38:16 29:56 30:45 32:04
16:35 X 10:44 X 7:05 X 7:15 X
elevator2.3.prop4 (valid )
elevator2.3a.prop4 (valid )
lamport.7.prop4
+ (valid )
1:26:43 X 20:32 X 10:03 X 6:04 X 0 X
21:17 X 5:13 X 3:16 X 2:40 X
1:32:48 X 20:01 X 9:46 X 6:00 X 3:09 X
22:49 X 5:10 X 3:07 X 2:36 X
leader_election.5.prop2 (valid )
leader_election.6.prop2 (valid )
leader_filters.6.prop2 (valid )
1:06:16 37:05 21:42 15:54 11:06
12:35 X 5:03 X 3:16 X 2:33 X
leader_filters.7.prop2 (valid )
31:06 10:53
+ X 8:56
+ X 7:26
+ X
1:38:18 52:58 32:12 20:20 13:35
26:06 X 4:27 X 3:09 X 2:45 X
1:51:46 58:48 36:18 22:40 15:41
26:22 X 7:49 X 5:55 X 4:19 X
public_subscribe.5.prop1 (n/a)
1:20:41 X 22:36 X 10:17 X 5:13 X 2:41 X
20:30 X 5:41 X 3:29 X 2:37 X
szymanski.4.prop4 (valid )
anderson.3.prop2 (invalid )
bakery.5.prop2
+ (invalid )
bakery.6.prop2
+ (invalid )
elevator.5.prop2 (invalid )
1:28:30 1:12:42 2:48
+ ! 1:08
+ ! 4
+ !
17:07 X 7:29 X 6:22 X 2:23 !
iprotocol.4.prop4 (invalid )
lamport.6.prop2
+ (invalid )
1:57:49 24:56 ! 39:44 26:21 19:18
25:22 X 7:05 X 5:33 X 4:20 X
peterson.5.prop2 (invalid )
1:43:02 14:20 ! 36:16 23:49 17:14
27:27 X 4:23 X 2:21 ! 1:40 !
phils.6.prop2
+ (invalid )
szymanski.5.prop2 (invalid )
1:00:52 7:34 ! 1:20 ! 8 ! 3 !
rether.5.prop6
+ (invalid )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
addfile ./gui/help/divine/contact.html
hunk ./gui/help/divine/contact.html 1
+
+
+
+
+ DiVinE Contact Information
+
+
+
+
+
+
+
+
+
+
+
+
+
+
Contact Information
+
+
If you have comments or questions about DiVinE
+ please email
+This e-mail address is being protected from spam bots, you need JavaScript enabled to view it
+
+
+
+
To file a bug report or an enhancement request, please use trac .
+
+
Address
+
+ Faculty of Informatics / ParaDiSe
+ Botanicka 68a
+
+ Brno, Czech Republic
+ Phone: +420 549 491 869
+
www.fi.muni.cz/paradise
+
+
+
Team
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Former members of the development team include (not complete):
+Pavel Moravec, Jiri Simsa, Radek Pelanek, Jitka Kudrnacova
+
+
Divine Cluster
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
DiVinE Cluster
+
+
Description
+
+
DiVinE Cluster is a parallel, distributed-memory enumerative
+ LTL model-checking tool for verification of concurrent systems. The tool can
+ employ aggregate power of network-interconnected workstations or clusters
+ to verify systems whose verification is beyond capabilities of sequential
+ tools. As a standard model-checker, DiVinE Cluster can be used to prove
+ correctness of verification models as well as to detect early design
+ errors.
+
+
+
DiVinE Cluster accepts models written in DiVinE native modeling language - DVE ,
+ and verifies them against specification formalized in Linear Temporal
+ Logic. Moreover, DiVinE Cluster provides means for the detection of
+ unreachable code, assertion violation, or deadlock.
+
+
DiVinE Cluster has also limited support for ProMeLa, that is the
+ modeling language of the verification tool SPIN. This capability makes
+ DiVinE Tool an ideal alternative to SPIN's users whose models cannot be
+ directly verified with SPIN because of insufficient memory resources of a
+ single computer. The restrictions for using DiVinE Cluster with ProMeLa
+ models are incapability of generating counterexamples, performing Partial
+ Order Reduction, verifying unreachable code and assertion violation.
+
+
Algorithms
+
+
DiVinE comes up with new algorithms for parallel accepting cycle
+detection problem which work on the graph that is partitioned into disjoint
+parts. Currently, DiVinE implements the following LTL parallel algorithms (for
+detailed references see Publications ):
+
+
+
+
+ Algorithm based on dependency structure .
+
+[Barnat and L. Brim and J.
+ Stribrna:
+Distributed LTL Model-Checking
+ in SPIN.
+Proc. SPIN Workshop on Model Checking of Software, Springer, 2001, volume
+2057 of LNCS, 200 - 216.]
+
+The algorithm performs partitioned
+depth-first search of the state space and is augmented with an additional data
+structure that keeps the global DFS postorder.
+
+
+
+ Algorithm based on negative cycles
+
+The LTL model checking problem is reduced to the negative cycle problem. The
+idea is to introduce an additional edge labeling function that assigns value -1
+to edges outgoing from accepting states and value 0 to all other edges. In this
+way, accepting cycles coincide with negative cycles. A single source shortest
+path algorithm is than engaged to identify negative cycles.
+
+
+
+ Property Driven Nested DFS
+
+The algorithm effectively uses the decomposition of the formula automaton
+into strongly connected components to achieve more efficient parallelization of
+nested depth-first search procedure.
+
+
+ SCC-based algorithm (OWCTY)
+
+The algorithm manipulates strongly connected components. A SCC decomposition
+is replaced by an iterative process in which non-perspective components (i.e.,
+those which do not contain any accepting cycle) are removed from the state
+space.
+ Algorithm based on back-level edges
+
+A completely different algorithmic solution based on breadth-first search
+(BFS) is presented in [ barnat03parallel , bc04fmics ]. It is based on a back-level edge
+concept. Back-level edge is any edge which does not increase the breadth-first
+search distance from the initial state. BFS is used to identify all back-level
+edges. As every cycle contains at least oneback-level edge, these can be used as
+triggers for detecting cycles.
+
+ Algorithm based on maximal accepting predecessors (MAP)
+
+
+The algorithm introduces an ordering on accepting states and relies on fact
+that there is a maximal accepting state on each accepting cycle. The algorithm
+computes and propagates the value of maximal accepting predecessor. Once an
+accepting state is propagated to itself, an accepting cycle is
+revealed. Otherwise the set of accepting states is modified and a new iteration
+is started.
+
+
Download
+
+
The latest release of DiVinE Cluster and install instructions can be found
+ here .
+
+
DiVinE CUDA
+
+
+
+
+
+
+
+
+
+
+
+
+
+
DiVinE CUDA
+
CUDA Accelerated LTL Model Checker
+
+
D iVinE CUDA is an extensible
+ open source tool for formal verification of concurrent
+ systems. DiVinE CUDA is a standalone verification tool that
+ supplements DiVinE verification tool chain with CUDA accelerated
+ LTL model checking ability.
+
+
+
D iVinE CUDA builds upon MAP
+ algorithm reformulated in terms of repeated matrix-vector
+ product. The tool first generate state space of the model under
+ inspection, stores it in a form of a matrix, and then employs
+ CUDA architecture to solve the accepting cycle detection problem
+ on the graph represented with the matrix.
+
+
Download and install instruction
+
+
+ P rerequisites:
+
+
+
+
+
+ I nstall instructions:
+
+
+
+
Using the tool
+
+
+
+ Before using the tool, make sure your PATH environment
+ variable contains path DiVinE binaries.
+
+ export PATH=:path_to_divine
+
+
+ Write your model in a DVE language and store it in a
+ file with extension .dve . F or details on DVE language see
+ our DVE
+ language guide .
+
+
+
+
+ Express the properties you want to verify and store
+ them in a file with extension .ltl .
+ .ltl files are as
+ follows.
+
+
+
+
+
+
+
+
+
+ Important! Combine your model file with the ltl
+ file using divine.combine script to
+ produce models with LTL specification. DiVinE
+ CUDA tool will not work on models that contain
+ no LTL specification or property process.
+
+ divine.combine model.dve specification.ltlspecification.ltl . Newly created files
+ will be named model.prop1.dve
+model.prop2.dve
+model.prop3.dve
+...
+
+
+
+ Important! Precompile your model with LTL specification using
+ divine.precompile to produce compiled representation of the model (file with .dveC extension). DiVinE
+ CUDA tool will not work on non-compiled DVE models.
+
+ $ divine.precompile model.prop1.dve
+ Run the algorithm to verify the model.
+
+ $ divine-cuda model.prop1.dveC$ divine-cuda elevator2.prop2.dveC
+Computing with MaxToMin numbering
+Start generating
+Size: 3314381, blockdim.x: 6474, threaddim.x: 512. Inner iterations: 42 (last took 913.658020 ms).
+Outer iterations 1 (last took 21.247986 ms). CUDA time: 0 minutes 0 seconds (982.206970 ms)
+Generating not finnished: Ap Size: 3521190, Aj Size: 33751128, m Size: 3569181,
+All States: 6814344, Used States: 3521187, All Edges: 77262797 Used Edges: 33751128
+Reachability time: 0 minutes 35 seconds (35847.054688 ms)
+============================
+
+Accepting cycle found
+
+============================$ divine-cuda elevator2.prop1.dveC
+Computing with MaxToMin numbering
+Start generating
+Generating finnished: Ap Size: 1722347, Aj Size: 20483544, m Size: 1722346,
+All States: 5015528, Used States: 1722344, All Edges: 63110616 Used Edges: 20483544
+Reachability time: 0 minutes 26 seconds (26855.355469 ms)
+Size: 1722347, blockdim.x: 3364, threaddim.x: 512. Inner iterations: 539 (last took 17.462891 ms).
+Outer iterations 14 (last took 17.244141 ms). CUDA time: 0 minutes 9 seconds (9093.107422 ms).
+==============================
+
+Accepting cycle NOT found
+
+==============================
+
+
+
+
+
DiVinE Multi-Core
+
+
+
+
+
+
+
+
+
+
+
+
+
+
Welcome to DIVINE Multi-Core!
+
+
The tool is based on automata-theoretic approach to LTL model checking. The
+input language allows for specification of processes in terms of extended
+finite automata and the verified system is then obtained as an asynchronous
+parallel composition of these processes. This system is in turn synchronously
+composed with a property process (negative claim automaton) obtained from the
+verified LTL formula through a Büchi automaton construction.
+
+
The resulting finite product automaton is then checked for presence of accepting
+cycles (fair cycles), indicating nonemptiness of its accepted language -- which
+in turn indicates invalidity of the verified LTL property.
+
+
Based on proven DiVinE LTL model checking system, DiVinE
+ Multi-Core brings parallel verification to contemporary
+ high-powered multi-core architectures. DiVinE Multi-Core
+ exploits full power of modern x86 hardware and reduces
+ unnecessary delays in workflow. Employing
+ state-of-the-art parallel liveness checking algorithm,
+ DiVinE Multi-Core offers unmatched scalability on shared
+ memory platforms in the range of 2- to 16-core
+ machines. Moreover, the tool supports 64-bit platforms out
+ of the box, allowing it to leverage all the memory
+ available in contemporary systems (and systems of the
+ upcoming years).
+
+
In the current DiVinE Multi-Core release, input is
+ provided in DVE format -- an industry-strength
+ specification language , as used in original DiVinE , with plenty of diverse
+ example models, ranging from simple toys to complex
+ real-world models. An extensive model database is
+ available at BEEM database .
+
+
+
+
Moreover, DiVinE can read models specified in ProMeLa (as
+ used in the SPIN tool), in addition to its native DVE
+ format. However, the capabilities of the tool on ProMeLa
+ models is currently limited by inability to produce
+ counterexamples: you can only obtain a yes/no answer.
+
+
+
DiVinE-MC Algortihm
+
+
The algorithm employed for accepting cycle detection is OWCTY augmented with a
+heuristic for on-the-fly cycle detection inspired by the MAP algorithm. It is
+not the purpose of this tool paper to go into details of the algorithm, so for
+in-depth description, we refer the reader to the two cited papers.
+
+
The main idea behind the OWCTY algorithm is to use topological sort for cycle
+detection -- an algorithm that does not depend on DFS postorder and can be thus
+parallelized reasonably well. Detection of cycles in this way is linear, but
+since we do accepting cycle detection, provisions for removing non-accepting
+cycles need to be added. This makes the algorithm quadratic in the worst case
+for general LTL properties, although for a significant subset of formulae
+(those that translate to weak Büchi automata) the algorithm runs in linear time
+in the size of the product automaton.
+
+
The MAP algorithm uses maximal accepting predecessors to identify accepting
+cycles in the product automaton. The main idea is based on the fact that each
+accepting vertex lying on an accepting cycle is its own predecessor. Instead
+of expensively computing and storing all accepting predecessors for each
+accepting vertex (which would be sufficient to conclude the presence of an
+accepting cycle), the algorithm computes only a single representative accepting
+predecessor for each vertex -- the maximal one in a suitable ordering. Clearly,
+if an accepting vertex is its own maximal accepting predecessor then it lies on
+an accepting cycle. This condition is used as the heuristic mentioned
+above. Note that the opposite direction does not hold in general. It can happen
+that the maximal accepting predecessor for an accepting vertex on a cycle does
+not lie on the cycle and the original MAP algorithm employs additional
+techniques to handle such a case.
+
+
If the heuristic fails, the OWCTY run will still detect accepting cycles if
+present. The heuristic does not interfere in any way when there are no
+accepting cycles -- OWCTY will detect that condition by itself. The cost of the
+heuristic is a very slight increase in per-state memory usage, and a small
+runtime penalty in the first phase of the first iteration of OWCTY. Overall, it
+does not increase the time complexity compared to OWCTY and in a number of
+cases it detects property violation without generating the entire state space,
+which makes the combined algorithm on-the-fly.
+
+
However, even though the algorithm is not asymptotically optimal, in practice
+it is hardly a problem when it comes to performance -- the bottlenecks can be
+found elsewhere.
+
+
Usage
+
+
Please refer to the Tool
+ Guide for an overview of tool usage.
+
+
Download
+
+
The latest release of DiVinE Multi-Core and install
+ instructions can be found on the download page .
+
+
+
+
element to add padding to the end of a text box */
+ border: 1px solid white;
+}
+
+.noBorderOnLeft {
+ border-left: none;
+}
+
+.dividingBorderAbove {
+ border-top: 1px solid rgb(204,204,204);
+}
+
+/* More elegant alternatives to .noBorderOnLeft & .dividingBorderAbove
+ * that don't require the creation of new classes - but which are not
+ * supported by MSIE - are the following:
+ *
+ * .rowOfBoxes > div:first-child {
+ * border-left: none;
+ * }
+ *
+ * .rowOfBoxes + .rowOfBoxes {
+ * border-top: 1px solid rgb(204,204,204);
+ * }
+ */
+
+
+/* ##### Footer ##### */
+
+#footer {
+ color: rgb(40,87,19);
+ background-color: rgb(239,239,239);
+ font-size: 87%;
+ text-align: center;
+ line-height: 1.25em;
+ margin: 2em 0 0 0;
+ padding: 1ex 10px;
+ clear: left;
+}
+
+#footer a {
+ color: rgb(40,87,19);
+ background-color: transparent;
+ text-decoration: underline;
+}
+
+#footer a:hover {
+ text-decoration: none;
+}
+
+#registration {
+ color: white;
+ background-color: rgb(40,87,19);
+ padding: 1ex;
+}
+
addfile ./gui/help/divine/divine-screen.css
hunk ./gui/help/divine/divine-screen.css 1
+/***************************************
+ * TITLE: Divine Screen Stylesheet *
+ * URI : divine-screen.css *
+ * MODIF: 2008-Jul-10 21:43 +0800 *
+ * this is a modification of *
+ * G. Behrmann's style *
+ ***************************************/
+
+
+/* ##### Common Styles ##### */
+
+body {
+ font-family: verdana, helvetica, arial, sans-serif;
+ font-size: 73%; /* Enables font size scaling in MSIE */
+ margin: 0;
+ padding: 0;
+}
+
+html > body {
+ font-size: 9pt;
+}
+
+acronym, .titleTip {
+ border-bottom: 1px dotted rgb(61,92,122);
+ cursor: help;
+ margin: 0;
+ padding: 0 0 0.4px 0;
+}
+
+a {
+ color: rgb(40,87,19);//#22464f; //rgb(61,92,122);
+ background-color: transparent;
+ text-decoration: underline;
+ margin: 0;
+ padding: 0 1px 2px 1px;
+}
+
+a:hover {
+ color: rgb(193,102,90);//rgb(117,144,174);
+ text-decoration: none;
+}
+
+ol {
+ margin: 1em 0 1.5em 0;
+ padding: 0;
+}
+
+ul {
+ list-style-type: square;
+ margin: 1em 0 1.5em 0;
+ padding: 0;
+}
+
+dl {
+ margin: 1em 0 0.5em 0;
+ padding: 0;
+}
+
+ul li {
+ line-height: 1.5em;
+ margin: 1.25ex 0 0 1.5em;
+ padding: 0;
+}
+
+ol li {
+ line-height: 1.5em;
+ margin: 1.25ex 0 0 2em;
+ padding: 0;
+}
+
+dt {
+ font-weight: bold;
+ margin: 0;
+ padding: 0 0 1ex 0;
+}
+
+dd {
+ line-height: 1.75em;
+ margin: 0 0 1.5em 1.5em;
+ padding: 0;
+}
+
+.doNotDisplay {
+ display: none !important;
+}
+
+
+.smallCaps {
+ font-size: 117%;
+ font-variant: small-caps;
+}
+
+
+/* ##### Header ##### */
+
+.superHeader {
+ color: rgb(130,128,154);
+ background-color: rgb(40,87,19);
+ text-align: right;
+ margin: 0;
+ padding: 0.5ex 10px;
+}
+
+.superHeader span {
+ color: rgb(195,196,210);
+ background-color: transparent;
+ font-weight: bold;
+ text-transform: uppercase;
+}
+
+.superHeader a {
+ color: rgb(195,196,210);
+ background-color: transparent;
+ text-decoration: none;
+ margin: 0;
+ padding: 0 0.25ex 0 0;
+}
+
+.superHeader a:hover {
+ color: rgb(193,102,90);
+ background-color: transparent;
+ text-decoration: none;
+}
+
+.midHeader {
+ color: white;
+ background-color: rgb(57,145,17);
+/* background-color: #22464f;*/
+ margin: 0;
+ padding: 0.26ex 10px;
+}
+
+.headerTitle {
+ font-size: 300%;
+ margin: 0;
+ padding: 0;
+}
+
+.headerSubTitle {
+ font-size: 151%;
+ font-weight: normal;
+ font-style: italic;
+ margin: 0 0 1ex 0;
+ padding: 0;
+}
+
+.headerLinks {
+ text-align: right;
+ margin: 0;
+ padding: 0 0 2ex 0;
+ position: absolute;
+ right: 1.5em;
+ top: 3.5em;
+}
+
+.headerLinks a {
+ color: white;
+ background-color: transparent;
+ text-decoration: none;
+ margin: 0;
+ padding: 0 0 0.5ex 0;
+ display: block;
+}
+
+.headerLinks a:hover {
+ color: rgb(195,196,210);
+ background-color: transparent;
+ text-decoration: underline;
+}
+
+.subHeader {
+ color: rgb(130,128,154);
+ background-color: rgb(40,87,19);
+ text-align: left;\\right;
+ font-weight: bold;
+ margin: 0;
+ padding: 0.5ex 10px;
+}
+
+.subHeader a {
+ color: rgb(195,196,210);
+ background-color: transparent;
+ text-decoration: none;
+ margin: 0;
+ padding: 0 0.25ex 0 0;
+}
+
+.subHeader a:hover {
+ color: rgb(193,102,90);
+ background-color: transparent;
+ text-decoration: none;
+}
+
+/* ##### Side Menu ##### */
+
+#side-bar {
+ color: rgb(204,204,204);
+ background-color: transparent;
+ list-style-type: square;
+ list-style-position: inside;
+ width: 10em;
+ margin: 0;
+ padding: 1ex 0;
+/* border: 1px solid rgb(204,204,204);*/
+ position: absolute;
+ left: 1.5ex;
+ top: 12em;
+}
+
+[id="side-bar"] {
+ position: fixed !important; /* Makes the side menu scroll with the page. Doesn't work in MSIE */
+}
+
+#side-bar a {
+ text-decoration: none;
+}
+
+#side-bar:hover {
+ color: rgb(117,144,174);
+ background-color: transparent;
+ border-color: rgb(117,144,174);
+}
+
+#side-bar li {
+ margin: 0;
+ padding: 0.75ex 0 1ex 1.75ex;
+}
+
+#side-bar li:hover {
+ color: rgb(61,92,122);
+ background-color: transparent;
+}
+
+
+#side-bar li a:hover {
+ text-decoration: underline;
+}
+
+/* ##### Main Copy ##### */
+
+#main-copy {
+ margin: 0;
+ padding: 0.5em 10px;
+ clear: left;
+}
+
+#main-copy h1 {
+ color: rgb(40,87,19); //#22464f; //rgb(117,144,174);
+ background-color: transparent;
+ font-family: "trebuchet ms", verdana, helvetica, arial, sans-serif;
+ font-size: 200%;
+ margin: 0;
+ padding: 0;
+}
+
+#main-copy h2 {
+ color: rgb(40,87,19);//#22464f; //rgb(61,92,122);
+ background-color: transparent;
+ font-family: "trebuchet ms", verdana, helvetica, arial, sans-serif;
+ font-weight: normal;
+ font-size: 151%;
+ margin: 0;
+ padding: 1ex 0 0 0;
+}
+
+#main-copy p {
+ line-height: 1.75em;
+ margin: 1em 0 1.5em 0;
+ padding: 0;
+}
+
+.newsHeading {
+ color: rgb(40,87,19);//#22464f; //rgb(61,92,122);
+ background-color: transparent;
+ font-family: "trebuchet ms", verdana, helvetica, arial, sans-serif;
+ font-size: 145%;
+ text-decoration: none;
+ margin: 0;
+ padding: 1ex 0 0 0;
+ display: block;
+}
+
+/*
+.newsHeading:hover {
+ color: rgb(117,144,174);
+ background-color: transparent;
+ text-decoration: underline;
+}
+*/
+.newsDate {
+ font-style: italic;
+ margin: 0 !important;
+ padding: 0;
+}
+
+.newsSummary {
+ margin: 1.5ex 0 2.5ex 0.75ex !important;
+ padding: 0;
+}
+
+.more {
+ text-align: right;
+ margin: 0;
+ padding: 0.5em 0;
+}
+
+.more a {
+ color: rgb(40,87,19); //rgb(61,92,122);
+ background-color: transparent;
+ font-size: 92%;
+ text-decoration: underline;
+ margin: 0;
+ padding: 0.25ex 0.75ex;
+}
+
+.more a:hover {
+ color: rgb(40,87,19);//rgb(117,144,174);
+ text-decoration: none;
+}
+
+.rowOfBoxes {
+ clear: both;
+}
+
+.oneThird, .twoThirds {
+ margin: 1em 0;
+ float: left;
+ border-left: 1px solid rgb(204,204,204);
+}
+
+.oneThird {
+ width: 28%;
+ padding: 0 1.9%;
+}
+
+.twoThirds {
+ text-align: justify;
+ width: 63%;
+ padding: 0 1.9%;
+}
+
+
+.filler { /* use with an empty
element to add padding to the end of a text box */
+ border: 1px solid white;
+}
+
+.noBorderOnLeft {
+ border-left: none;
+}
+
+
+/* ##### Footer ##### */
+
+#footer {
+ color: rgb(40,87,19); //rgb(51,51,102);
+ background-color: rgb(239,239,239);
+ font-size: 87%;
+ text-align: center;
+ line-height: 1.25em;
+ margin: 2em 0 0 0;
+ padding: 1ex 10px;
+ clear: left;
+}
+
+#footer a {
+ color: rgb(40,87,19); //rgb(0,68,204);
+ background-color: transparent;
+ text-decoration: underline;
+}
+
+#footer a:hover {
+ text-decoration: none;
+}
+
+#registration {
+ background-color: rgb(195,196,210);
+}
addfile ./gui/help/divine/divine.qhp
hunk ./gui/help/divine/divine.qhp 1
-
+
+
+ divine.web.base
+ doc
+
+ divine
+
+
+ divine
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ pics/divine-logo.png
+
+ pics/anderson-throughput-MAP.png
+ pics/anderson-throughput-OWCTY.png
+ pics/anderson-time-scale-MAP.png
+ pics/anderson-time-scale-OWCTY.png
+ pics/barnat.jpeg
+ pics/brim.jpeg
+ pics/cerna.jpeg
+ pics/ceska.jpeg
+ pics/chaloupka.jpeg
+ pics/janousek.jpeg
+ pics/moravec.jpeg
+ pics/rockai.jpeg
+ pics/simecek.jpeg
+ pics/tumova.jpeg
+ pics/vanessa.jpg
+ pics/Verstoep_Kees.jpg
+ pics/weber.jpeg
+
+ divine-screen.css
+ divine-screen-alt.css
+ divine-screen-alt-maruku.css
+
+ index.html
+
+ casestudies.html
+ contact.html
+ divine-cluster.html
+ divine-cuda.html
+ divine-mc.html
+ language.html
+ overview.html
+ probdivine.html
+ publications.html
+ tool.html
+
+
+
addfile ./gui/help/divine/index.html
hunk ./gui/help/divine/index.html 1
+
+
+
+
+ Welcome to DiVinE!
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
The goal of Distributed Verification Environment project DIVINE is to provide
+an extensible framework to support verification and analysis of large-scale
+computer systems on parallel architectures. DIVINE is a
+collection of state-of-the-art verification algorithms incorporated
+into a several tools which are as easy to install as most
+sequential tools.
+
+
+
DIVINE accomodates also two domain specific tools. BIO-DIVINE is
+intended for analysis of complex biological systems, PROB-DIVINE is a tool for
+verification of finite-state probabilistic systems. DIVINE offers specifically
+tailored versions for distributed-memory architectures (like clusters of
+workstations) - DIVINE CLUSTER ,
+for shared-memory architectures (like multi-core
+machines) - DIVINE MULTI-CORE ,
+for General Purpose GPUs - DIVINE
+CUDA , and for I/O efficient usage of external
+memory
+devices (like parallel hard-disks) - DIVINE I-O.
+
+
+
+
DIVINE is free for non-profit
+use, e.g. for evaluation, research, and teaching purposes.
+
+
+
+
Specification Language
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
Table Of Contents
+
+
+
+
+
+
Quick Guide Through the DVE Specification Language
+
+
DVE specification language has been created as a language that is both easy to interpret and sufficiently powerful to express interesting problems for the purpose of model checking.
+
+
A set of “case studies” is available, in the form of DVE source code, in the examples subdirectory of the DiVinE distribution.
+
+
Philosophy of DVE language
+
+
The basic modelling unit in DVE is a system, which is composed of processes. Processes can go from one process state to another through transitions, which can be guarded by a condition – this condition, also called a “guard” determines whether the transition can be activated.
+
+
Transitions can be synchronised through (named) channels. Only exactly 2 processes can be synchronised in one “moment” (in a single step). When more than 2 processes would be able to synchronise at the same time on a single channel, any combination of pairs can be picked at that time nondeterministically, however always just 2 of them in one moment. Through the synchronisation on a channel, a value can be optionally transmitted from one process to the other.
+
+
The transitions have so-called “effects”. Effects are generally assignments to local or global variables. Two processes undergoing a synchronisation should not be able to assign to the same variable – that would be a modelling error.
+
+
A system may be synchronous or asynchronous.
+
+
Uniqueness of identifiers
+
+
There is a single common namespace for channels, variables, processes and states. Identifiers have to be unique in any given scope of visibility. It means that e.g. when variable A is declared in the process P1 , then there cannot be a variable A , a state A in that process or a global variable A , nor a channel or a process A . The only other A variable may occur in a different process, eg. P2 .
+
+
Syntax elements
+
+
Processes
+
+
Declaration - short example:
+
+
process My_really_nice_process
+{ <code of a process> }
+
+
Variables
+
+
Variables can be global (declared at the beginning of DVE source) or local (declared at the beginning of a process). They can be of byte or int type. E.g.:
+
+
byte A[9];
+int i,j;
+
+
Constants
+
+
Constants can be declared identically as variables using the keyword const:
+
+
const byte k = 3;
+
+
This time constants cannot be used as parameters in declarations of arrays. For example this construct is erroneous:
+
+
byte field[k];
+
+
Process states
+
+
Declared after declaration of variables. You also have to write which of declared process states is the initial one. You can also optionally write which of them are accepting (but you probably will not need this feature at this moment). E.g.:
+
+
state start, run, reading_input, writing_output;
+init start;
+accept reading_input, writing_output;
+
+
For purposes of modelling atomic actions, there are so called committed states .
+
+
Committed state of a process = state declared as committed – e.g. in the following code states reading_input and writing_output are committed:
+
+
state start, run, reading_input, writing_output;
+init start;
+commit reading_input, writing_output;
+
+
Committed state of a system = state of a system, where at least one process is in a committed state. If the system is in a committed state, then only processes in committed states can transit to another state. It means that the sequence of transitions beginning with a transition leading to a committed state and ending with a transition leading to a non-committed state cannot be interlaced with other transitions leading from non-committed states.
+
+
Synchronization between processes in committed states and non-committed states is ignored. Synchronization between processes (both) in committed states is permitted (but it is probably very rare).
+
+
Transitions
+
+
Transitions are written as a transitions from one process state to another (e.g. run -> writing_output). The transition can be executed only if the process in the initial process state of a transition (in the above mentioned example in a state run). You should also define an additional condition when the transition can be executed (keyword guard ) and sometimes also a channel to synchronize through (keyword sync with followed by the channel name and ! or ?). There can synchronize only transitions with the same channel name and opposite operators ! and ?. When you want to transmit a value through the channel, you can write a value after ! and a variable (where the value will be transmitted) after ?. The last but not least element of transitions are effects – they are simple assignments to the variables.
+
+
Example:
+
+
process Sender {
+ byte value, sab, retry;
+ state ready, sending, wait_ack, failed;
+ init ready;
+ trans
+ ready -> sending {sync send?value; effect sab = 1 -sab; },
+ sending -> wait_ack {sync toK!(value*2+sab); effect retry = 1;},
+ wait_ack -> wait_ack {guard retry <2; sync toK!(value*2+sab); effect retry = retry+1;},
+ wait_ack -> ready {sync fromL?;},
+ wait_ack -> failed { guard retry == 2;};
+}
+
+
Expressions
+
+
In assignments, guards and synchronization values you can write arithmetic expressions. They can contain:
+
+
+constants: numbers, true, false
+
+parentheses: (, )
+
+variable identifiers
+
+unary operators -, ~ (= negation of bits) and not (= boolean negation)
+
+binary operators (ordered by precedence - higher line means a lower precedence):imply,or,and,|,^,&,==, !=,<, <=, >, >=,<<, >>,-, +,/, *, %and, or and imply (but their meaning is obvious).
+
+question on a state of some process (e.g. Sender.ready is equal to 1, iff process Sender is in a state ready. Otherwise it is equal to 0).
+
+
+
Channels
+
+
Declarations of channels follow declarations of global variables. For example:
+
+
byte i_am_a_variable;
+channel send, receive, toK, fromK, toL, fromL; // untyped unbuffered channels
+channel {byte} b_send[0], b_receive[0]; // typed unbuffered channels
+channel {byte,int} bi_send[0], bi_receive[0]; // typed unbuffered channels (transmitting 2 values simultaneously)
+channel {byte,int} buf_bi_send[4], buf_bi_receive[1]; // typed buffered channels
+
+
There is a big difference between buffered and unbuffered channels: * unbuffered channels can be untyped and they do not need to transmit values (they can play a role of handshake communication)
+
+
+buffered channels have to be always typed
+
+value transmission or handshake using unbuffered channel is synchronous – i.e. both sending and receiving processes execute their transitions in the same transition of a system
+
+value transmission using buffered channel is asynchronous – i.e. If the buffer is not full, value can be sent. If the buffer is not empty, value can be received. But this happens always in different transitions of a system.
+
+
+
Be aware: channel xxx and channel {byte} xxx[0] are both unbuffered channels and they behave almost the same way, but the second declaration is typed and the transmitted value is type casted (in this case to byte) before its transmission.
+
+
Type of a system
+
+
Synchronous:
+
+
system sync;
+
+
or asynchronous
+
+
system async;
+
+
This declaration should be written at the end of a DVE source.
+
+
Assertions
+
+
Assertions can be written in every process just before transitions definitions. Assertion can be understood as an expression, which should be valid (evaluated to non-zero value) in a given process state. Example:
+
+
process My_really_nice_process
+{
+ byte hello = 1;
+ state one, two, three;
+ init one;
+ assert one: hello >= 1,
+ two: hello < 1,
+ one: hello < 6;
+ trans
+ ...
+ ;
+}
+
+
DVE Modelling Tutorial
+
+
This tutorial will guide you through the creation of a model of the Peterson’s mutual exclusion algorithm for n processes. This will help you understand the following concepts:
+
+
+processes, transitions,
+
+global and local variables,
+
+guards, effects.
+
+
+
The Peterson’s algorithm
+
+
First, let us show you the algorithm itself as a C code snippet:
+
+
volatile int q[n] = { 0 };
+volatile int turn[n] = { 0 };
+
+void enter_critical_section(int i) {
+ int j, k;
+
+ for (j = 1; j < n; j++) {
+ q[i] = j;
+ turn[j] = i;
+
+ for (k = 0; k < n; k++)
+ while (k != i && (q[k] >= j && turn[j] == i));
+ }
+
+ q[i] = n;
+}
+
+void leave_critical_section(int i) {
+ q[i] = 0;
+}
+
+void process(int process_id) {
+ for (;;) {
+ enter_critical_section(process_id);
+ /* do work */
+ leave_critical_section(process_id);
+ }
+}
+
+
We will create a model of the process procedure and, using m4 macro language, make the model parametric.
+
+
Model, Processes, Transitions
+
+
A model in DVE consists of several processes, each of which is an extended finite state automaton. These are (usually) asynchronously composed to become an automaton of the model. The last line of an asynchronous model in DVE reads:
+
+
system async;
+
+
Let’s just put this line at the end of each model, for now. Synchronous models aren’t well supported yet.
+
+
A process declaration looks like this (the order of things is important):
+
+
process P1 {
+ variables
+ states
+ assertions
+ transitions
+}
+
+
As an example, we declare a process which alternates between two states: inside a critical section, and outside it.
+
+
process P1 {
+ state outCS, inCS;
+ init outCS;
+ trans
+ outCS -> inCS {},
+ inCS -> outCS {};
+}
+
+
The process starts in state outCS and there’s one transition from outCS to inCS and one from inCS to outCS, neither of them having any guards or effects. Indeed, performing a reachability analysis using DiVinE tells us that two states are reachable.
+
+
If we omit one of the transitions, we create a deadlock state – the automaton is stuck in it, not able to proceed. DiVinE is able to detect and describe such states.
+
+
Next, we’d like to have multiple similar processes, all described by one automaton but each having a different name and, possibly, some process number constant. In order to do this, we use the m4 macro language like this:
+
+
define(P, `process P_$1 {
+ state outCS, inCS;
+ init outCS;
+ trans
+ outCS -> inCS {},
+ inCS -> outCS {};
+} ')
+
+P(0)
+P(1)
+P(2)
+
+
If we process this definition with the m4 command, we get a model with three processes. Reachability analysis would tell us that we have 8 states, by the way.
+
+
To make the model parametric, we shall use some predefined m4 macros. Filename of the source of such model should end with the .mdve extension; usage of such files is described in the Tool guide . Finally, we get this parametric source:
+
+
default(N,3)
+
+define(P, `process P_$1 {
+ state outCS, inCS;
+ init outCS;
+ trans
+ outCS -> inCS {},
+ inCS -> outCS {};
+} ')
+
+forloop(i,0,N - 1, `P(i)')
+
+system async;
+
+
Variables, Guards, Effects
+
+
In DVE, you may define global and process-local variables . There are two types: byte and int, and you may define one-dimensional arrays using the C syntax. These variables can be modified using transition effects and transitions are enabled/disabled based on variable values using guards .
+
+
The variable declarations are similar to the C syntax, you’ll easily understand that from the following examples. We’ve already shown where process-local variable declarations go. Global variables are declared at the beginning of a DVE source.
+
+
Guards and effects go into the curly braces after a transition, like this:
+
+
trans
+ q0 -> q1 { guard (x == 1) && (y == 2);
+ effect x = x + 1, y = y - 1; };
+
+
For a quick overview, let’s say the two functions are a bit simpler (and wrong indeed):
+
+
volatile int mutex = 0;
+
+void enter_critical_section(int i) {
+ while (lock == 1) /* wait */;
+ lock = 1;
+}
+
+void leave_critical_section(int i) {
+ lock = 0;
+}
+
+
We shall declare a global variable mutex in the model as well (a byte type is enough, though).
+
+
byte lock = 0;
+
+
The leave_critical_section function is simple, it just resets the lock variable when leaving the critical section. We’ll model this as an effect on the inCS -> outCS edge:
+
+
trans
+ ...
+ inCS -> outCS { effect lock = 0; };
+
+
To model the enter_critical_section function, we’ll have to add a couple of states: a “waiting for lock becoming 0” state and a ”lock has just become 0” state. We’ll model the while loop as a cycle around the waiting state, and the assignment as a transition from the other state to inCS. It is very important to distinguish these two states since two processes may both reach the ”lock = 1” line at the same time; if we modelled the assignment as a transition from the waiting state, the model would not allow such behaviour.
+
+
The whole model of this faulty lock looks like this:
+
+
default(N,3)
+
+byte lock = 0;
+
+define(P, `process P_$1 {
+ state outCS, inCS, waiting, lockit;
+ init outCS;
+ trans
+ outCS -> waiting {},
+ waiting -> waiting { guard lock == 1; },
+ waiting -> lockit { guard lock == 0; },
+ lockit -> inCS { effect lock = 1; },
+ inCS -> outCS { effect lock = 0; };
+} ')
+
+forloop(i,0,N - 1, `P(i)')
+
+system async;
+
+
Now, you may want DiVinE to tell you if it is possible to get to a state where two processes are both in a critical section. An LTL property claiming that it is not is this:
+
+
#define c0 (P_0.inCS)
+#define c1 (P_1.inCS)
+#property !F (c0 && c1)
+
+
If we find a counterexample to this property then it is possible to reach such state and the lock is faulty. DiVinE finds such counterexample indeed. For information about using divine-mc.combine and divine-mc owcty to perform the check, please see the Tool guide .
+
+
Arrays, back to Peterson
+
+
We’ve shown how to create a DVE model of a simple lock in C. Let’s go back to our example model of Peterson’s algorithm now. You already know the needed syntax; let me repeat the way we transform a C source into a DVE model:
+
+
+while loops in C are modelled as cycles around a state; for loops may be transformed to while loops easily,
+
+each memory read and write should have its own transition – this way we model the possibility of being interrupted by some other process,
+
+global and local variables are often used without change (we usually use the smallest type that’s enough, though, to save memory).
+
+
+
Now we will carefully rewrite the C source to DVE. Let’s start by defining the global variables:
+
+
byte q[N];
+byte turn[N];
+
+
These arrays contain zeros in the initial state, you may count on that. To start with simple things, we shall model the leave_critical_section function:
+
+
define(P, `process P_$1 {
+ state outCS, inCS;
+ init outCS;
+ trans
+ inCS -> outCS { effect q[$1] = 0; };
+} ')
+
+
Next, we’ll create an outline of the enter_critical_section. We will need to add some local variables as well.
+
+
byte j, k;
+...
+trans
+ outCS -> for_j { effect j = 1; },
+ for_j -> inCS { guard j == N; effect q[$1] = N; },
+ ...
+
+
We have just modelled the initialization of the outer for loop, the end of it and the locking itself (q[i] = n means that process i is in the critical section). Let’s go to the inside of the loop:
+
+
trans
+ ...
+ for_j -> j1 { guard j < N; effect q[$1] = j; },
+ j1 -> for_k { effect turn[j] = $1, k = 0; },
+ /* for_k ... */
+ for_k -> for_j { guard k == N; effect j = j + 1; };
+
+
We combined two memory writes into one transition: turn[j] = $1 and k = 0 even though we said we should not. It’s ok here because the k variable is not shared. Okay, let’s finish it by defining the for_k transitions as well:
+
+
trans
+ ...
+ for_k -> while { guard k < N; },
+ while -> while { guard k != $1 && q[k] >= j && turn[j] == $1; },
+ while -> for_k { guard k == $1 || q[k] < j || turn[j] != $1;
+ effect k = k + 1; };
+
+
Note that there are two transitions going from a loop state, the guards of which are negations of each other (in a for loop with +1 increments, we usually have j < N and j == N, since that works too).
+
+
Okay, we have completed the model. Let me repeat the whole thing for you:
+
+
default(N,3)
+
+byte q[N];
+byte turn[N];
+
+define(P, `process P_$1 {
+ byte j, k;
+ state outCS, inCS, for_j, j1, for_k, while;
+ init outCS;
+
+ trans
+ /* enter_critical_section */
+ outCS -> for_j { effect j = 1; },
+ for_j -> j1 { guard j < N; effect q[$1] = j; },
+ j1 -> for_k { effect turn[j] = $1, k = 0; },
+ for_k -> while { guard k < N; },
+ while -> while { guard k != $1 && q[k] >= j && turn[j] == $1; },
+ while -> for_k { guard k == $1 || q[k] < j || turn[j] != $1;
+ effect k = k + 1; },
+ for_k -> for_j { guard k == N; effect j = j + 1; },
+ for_j -> inCS { guard j == N; effect q[$1] = N; },
+ /* leave_critical_section: */
+ inCS -> outCS { effect q[$1] = 0; };
+} ')
+
+forloop(i,0,N - 1, `P(i)')
+
+system async;
+
+
This model satisfies the before mentioned property indeed. That means a state where two processes are both in a critical section is not reachable. Now, proceed to the Tool guide to see how to combine the model with the property and how to run the model checker on the result.
+
+
PROBDVE extension
+
+
PROBDVE extends the DVE language with probabilistic transitions, making it possible to model Markov Decision Processes. Let us describe the syntax of such transitions on an example process:
+
+
process P {
+ byte x;
+ state q0, p1, p2, q3, q4;
+ init q0;
+
+ trans
+ q0 => { p1:1, p2:2 }, /* (0) */
+ q0 -> q3 { guard x == 0; }, /* (1) */
+ q0 -> q4 { effect x = x + 1; }; /* (2) */
+}
+
+
Suppose this process is in state q0. First, we nondeterministically choose which of the three – (0), (1) or (2) – transitions we use. If it is (1) or (2), the behaviour is the same as in DVE. If it is (0), the process gets to state p1 with probability 1/3 and to state p2 with probability 2/3.
+
+
DVE Language Reference and Semantics
+
+
The complete DVE language reference and semantics is given in Chapter 2 of the Master Thesis of Pavel Simecek, which is available in PDF format here .
+
+
Overview
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
Why DiVinE ?
+
+
+
+The computing power of computers has increased by a factor of a million over the
+past couple of decades. As a matter of fact, the development effort, both in
+industry and in academia, has gone into developing bigger, more powerful and
+more complex applications. In the next few decades we may still expect a
+similar rate of growth, due to various factors such as continuing
+miniaturization, parallel and distributed computing.
+
+
+
+With the increase in complexity of computer systems, it becomes even more
+important to develop formal methods for ensuring their quality and reliability.
+Various techniques for automated and semi-automated analysis and verification
+have been successfully applied to real-life computer systems. However, these
+techniques are computationally demanding and memory-intensive in general and their
+applicability to extremely large and complex systems routinely seen in practice
+these days is limited. The major hampering factor is the state space explosion
+problem due to which large industrial models cannot be efficiently handled
+unless we use more sophisticated and scalable methods and a balance of
+the usual trade-off between run-time, memory requirements, and precision of a
+method.
+
+
+
+A lot of attention has been paid to the development of approaches to battle the
+state space explosion problem. Many techniques, such as abstraction, state
+compression, state space reduction, symbolic state representation, etc., are
+used to reduce the size of the problem to be handled allowing thus a single
+old-fashioned single-processor computer to process larger systems. All these
+methods can be therefore characterized as reduction techniques.
+
+
+
Verification and analysis methods that are tailored to exploit the
+capabilities of the new hardware architectures are slowly appearing as well.
+These platform-dependent techniques focus on increasing the amount of
+available computational power. These are, for example, techniques to fight
+memory limits with efficient utilisation of external I/O devices, techniques
+that introduce cluster-based algorithms to employ aggregate power of
+network-interconnected computers, or techniques to speed-up the verification on
+multi-core processors.
+
+
+
+The idea of exploiting hard disks or parallel computers in verification already appeared
+ in the very early years of the formal verification era. However,
+inaccessibility of cheap parallel computers with sufficiently fast external
+memory together with negative theoretical complexity results excluded these
+approaches from the main stream in formal verification. The situation changed
+dramatically during the past several years. The computer progress over the past
+two decades has measured several orders of magnitude with respect to various
+physical parameters such as computing power, memory size at all hierarchy levels
+from caches to disk, power consumption, physical size and cost. In particular,
+the focus of novel computer architectures in parallel and distributed computing
+has shifted away from unique massively parallel systems competing for world
+records towards smaller and more cost effective systems built from personal
+computer parts. In addition, recent shift in the emphasis of research on
+parallel algorithms to pragmatic issues has provided practically efficient
+algorithms for solving computationally hard problems. As a matter of fact,
+interest in platform-depended verification has been revived and DiVinE was born.
+
+
+
+
About DiVinE
+
+
DiVinE is an open source and extensible system for platform-dependent
+formal verification of computer systems. DiVinE is in fact a set of tools
+each of them tailored to a particular platform, like distributed-memory (DiVinE Cluster ), shared-memory (DiVinE Multi-Core ), external hard disks
+(DiVinE I-O) etc. DiVinE in its current development phase offers mainly tools
+for platform-depended model checking of finite state systems against
+specification formulated in linear temporal logics
+(LTL) . Special DiVinE branches focus on model-checking of
+probabilistic systems (Markov decision
+processes ) - ProbDiVinE and on
+analyzis of complex biological systems BioDiVinE (under development).
+
+
+
+
LTL model checking algorithms in DiVinE follow the automata-based
+approach . Algorithms find accepting cycles in the product of the system model
+and a Buchi automaton for the negation of the formula.
+
+
In most sequential LTL model checkers Nested Depth-First Search and Tarjan's
+decomposition into strongly connected components are used for accepting cycle
+detection. Unfortunately, both algorithms strongly rely on depth-first search
+postorder which computation is known to be inherently sequential. Therefore,
+these algorithms are unsuitable for being used in parallel setting.
+DiVinE implements new algorithms for parallel accepting cycle detection problem.
+These are briefly described on the respective tool pages.
+
+
+
DiVinE tools differ in the platforms they are supposed to be run on,
+while DiVinE branches are domain specific tools.
+
+
+
+
+
+ DiVinE
+BRANCHES
+ DiVinE TOOLS Concurrent Systems Probabilistic Systems Biological Systems
+
+
+Clusters (distributed-memory) DiVinE CLUSTER parallel
+distributed-memory enumerative model-checking tool for verification of
+concurrent systems. The tool can employ aggregate power of
+network-interconnected workstations to verify systems whose verification is
+beyond capabilities of sequential tools. As a standard model-checker, DiVinE
+Cluster can be used to prove correctness of verification models as well as to
+detect early design errors.ProbDiVinE BioDiVinE (under development)
+
+
+
+Multi-cores (shared-memory) DiVinE
+MULTI-CORE parallel shared-memory enumerative model-checking tool for verification
+of concurrent systems. The tool can employ full power of modern 64-bit multi-core
+architectures. Similarly to DiVinE Cluster, it can be used to prove correctness
+of verification models as well as to detect early design errors. ProbDiVinE
+MC
+
+GPUs DiVinE
+CUDA
+
+
+
+Hard Disks DiVinE I-O (under development)
+
+
ProbDiVinE
+
+
+
+
+
+
+
+
+
+
+
+
+
+
ProbDiVinE
+
A Parallel Qualitative and Quantitative LTL Model Checker
+
+
P robDiVinE-MC is an
+ extensible open source system for parallel and/or distributed
+ formal verification of concurrent probabilistic
+ systems. ProbDiVinE-MC is an integral part of the distributed
+ verification tool DiVinE and as such can be viewed both as an
+ analyser and prototyping environment.
+
+
+
P robDiVinE-MC supports both
+ qualitative and quantitative LTL model checking of Markov
+ Decision Processes (MDPs) -- models supporting both
+ probability and non-determinism expressed in PROBDVE language
+ (see section "Usage"). Current version works in shared memory
+ environment.
+
+
+
T he main difference in
+ comparison to previous version (see section download) is that
+ ProbDiVinE-MC supports also quantitative verification and does
+ not require distributed memory environment.
+
+
+
P robDiVinE-MC uses the
+ automata-theoretic approach where qualitative LTL model
+ checking of MDPs is reduced to the question whether the
+ product automaton for a given MDP with a Buchi acceptance
+ condition contains an accepting end component (AEC). The
+ problem of quantitative LTL model checking is to determine
+ minimal or maximal probability the formula is satisfied,
+ i.e. we try to find minimal or maximal probability an AEC is
+ reachable from initial state, which is done via building and
+ solving linear programming problem.
+
+
+
+
T he tool implements a
+ parallel adaptations of the algorithm of de Alfaro [dA95] . It
+ computes the set of states, from which probability of reaching
+ accepting end component is 1. In particular, the algorithm
+ maintains approximation set of states that may belong to an
+ AEC or probability of reaching AEC from them is 1. The
+ algorithm repeatedly refines the approximation set by locating
+ and removing states from which AEC cannot be reached with
+ probability 1, we call this a pruning step. The core of the
+ algorithm are conditions determining the states to prune.
+
+
+
+
A fter determinig states with
+ probability 1, linear programming problem is built and
+ solved. Size of LP problem is crucial, thus several parallel
+ optimization techniques to reduce number of inequations were
+ developed and implemented. The techniques:
+
+
+ prune the graph, from which inequations are
+ generated
+
+ allow to divide LP problem to a sequence of LP
+ subproblems via parallel decomposition into strongly
+ connected component (SCC) graph
+
+ allow to solve some LP subproblems corresponding to SCCs,
+ independently or at least iteratively (in parallel)
+
+
+
+
P robDiVinE-MC is built on the
+ top of the DiVinE library that offers common functions needed
+ to develop a parallel or distributed enumerative model
+ checker. The only extension to the library that was necessary,
+ was the extension of the state generator to a probabilistic
+ state generator, hence, it can handle probabilistic
+ transitions of PROBDVE as introduced in section "Usage".
+
+
+
P robDiVinE-MC is currently
+ operated in command-line mode. The input is the model given as
+ a .probdve file and the LTL formula given as an .ltl
+ file. Further parameters include type of verification, number
+ of threads involved in the computation etc. See section
+ "Usage" .
+
+
Using the tool
+
+
+
+
+
+ Before using the tool, make sure your PATH environment
+ variable contains paths to both DiVinE and ProbDiVinE
+ binaries.
+
+ export PATH=:path_to_probdivine:path_to_divine
+
+
+
+
+
+ Write your model in a PROBDVE language and store it in a file with extension .probdve .
+
+
+ DVE specification language as used in DiVinE. A system is modeled
+ as a composition of processes, which can change their states via probabilistic
+ (=> ) or non-probabilistic (-> ) transitions and can synchronize
+ using channels. A non-probabilistic transition may have a guard (a
+ condition which has to be satisfied for the transition to be enabled), an
+ effect (assignment to a variable), and a sync expression (for
+ synchronization with another transition via channel). A probabilistic
+ transition just determines probability of resulting state, which is given by
+ weights assigned to states. For example, s=>{s:3, t:2, u:2} means that
+ from the state s the system evolves in the state s
+
+ with probability 3/7, in the state t with probability 2/7, as well as in
+ the state u .
+
+
+
+
+
+
+
+ Express the properties you want to verify and store them in a file with extension .ltl .
+ .ltl files are as follows.
+
+
+
+
+
+
+
+
+
+ Important! Combine your model file with the ltl file using
+ divine.combine script to produce models with LTL specification and use -d to obtain a product with semi-deterministic Buchi automaton. Only these can be used as input files to the probabilistic model
+ checker. Tools(algorithms) will not work on models that contain no LTL
+ specification or property process.
+
+
+ divine.combine -d model.probdve specification.ltl
+ This will produce as many files as there are properties in specification.ltl . Newly created files will be named model.prop1.probdve
+
+
+
+
+
+
+ ProbDiVinE-MC:
+
+ Run the algorithm to verify the model. NNN
+ stands for the number of threads required to perform the
+ computation. In case of quantitative verification, we
+ obtain minimal probability the formula holds:
+
+ divine-mc.probabilistic -n
+ NNN -t model.prop1.probdve
+
+ If you run qualitative verification only, the algorithm
+ outputs whether the LTL formula is satisfied with
+ probability one or not.
+
+ divine-mc.probabilistic -n NNN -l model.prop1.probdve
+
+
+
+
ProbDiVinE-1.0:
+
+
+ Run any of the algortihms to detect the presence of AEC. If
+ an AEC is present in the state space graph, the verifed
+ property does not hold true with probability one. The presence
+ of AEC is reported by the algorithms to the standard output.
+ probdivine.AECdetection is an MPI application and
+ must be executed with appropriate way. The particular ways differ according to
+ individual implementations of MPI standard. The following sequences of commands
+ relate to the two most used MPI implementations: mpich and
+ LAM/MPI. Note that NNN stands for the number of network
+ nodes required to perform the computation.
+
+
+ m pich:mpirun -np NNN probdivine.AECdetection model.prop1.probdve
+
+
+
+ L AM/MPI: lamboot
+
+ Algorithms probdivine.CY and
+ probdivine.CY_eliminate are standard serial algorithms that
+ are executed outside MPI environment.
+
+ probdivine.CY model.prop1.probdve
+
+
+
+
+
+
Download
+
+
The latest release of ProbDiVinE and install instructions can be found at
+ DiVinE download page .
+
+
+
Publications
+
+
+
+
+
+
+
+
+
+
+
Publications 2009 J. Barnat and L. Brim and S. Edelkamp and D. Sulewski and P. Simecek:
+
Can Flash Memory Help in Model Checking [
bibtex ,
pdf ]
+
Formal Methods for Industrial Critical Systems (FMICS 2008) , Springer-Verlag, 2009, volume 5596 of LNCS, 150--165.
+
J. Barnat and J. Chaloupka and J. Van De Pol:
+
Distributed Algorithms for SCC Decomposition [
bibtex ,
pdf ]
+
To appear in Journal of Logic and Computation , volume , 2009, .
K. Verstoep and H. Bal and J. Barnat and L. Brim:
+
Efficient Large-Scale Model Checking [
bibtex ,
pdf ]
+
23rd IEEE International Parallel & Distributed Processing Symposium (IPDPS 2009) , IEEE, 2009.
+
J. Barnat and L. Brim and I. Cerna and M. Ceska and J. Tumova:
+
Local Quantitative LTL Model Checking [
bibtex ,
pdf ]
+
Formal Methods for Industrial Critical Systems (FMICS 2008) , Springer-Verlag, 2009, volume 5596 of LNCS, 53--68.
+
2008 J. Barnat and L. Brim and P. Rockai:
+
DiVinE Multi-Core -- A Parallel LTL Model-Checker [
bibtex ,
pdf ]
+
Automated Technology for Verification and Analysis , Springer, 2008, volume 5311 of LNCS, 234-239.
+
J. Barnat and L. Brim and I. Cerna and S. Drazan and D. Safranek:
+
Parallel Model Checking Large-Scale Genetic Regulatory Networks with DiVinE [
bibtex ,
pdf ]
+
ENTCS , volume 194(3), 2008, 35--50.
J. Barnat and L. Brim and I. Cerna and M. Ceska and J. Tumova:
+
ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems [
bibtex ,
pdf ]
+
QEST '08: Proceedings of the 2008 Fifth International Conference on Quantitative Evaluation of Systems , IEEE Computer Society, 2008, 77--78.
+
J. Barnat and L. Brim and P. Simecek and M. Weber:
+
Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking [
bibtex ,
pdf ]
+
Tools and Algorithms for the Construction and Analysis of Systems (TACAS). , Springer, 2008, volume 4963 of LNCS, 48-62.
+
J. Barnat and P. Rockai:
+
Shared Hash Tables in Parallel Model Checking [
bibtex ,
pdf ]
+
ENTCS , volume 198(1), 2008, 79--91.
L. Brim and J.Barnat:
+
Squeeze All the Power Out of Your Hardware to Verify Your Software! [
bibtex ,
pdf ]
+
ISOLA 2008 , Springer Verlag, 2008, volume 17 of CCIS, 604-618.
+
2007 J. Barnat and L. Brim and P. Simecek:
+
I/O Efficient Accepting Cycle Detection [
bibtex ,
pdf ]
+
Computer Aided Verification , Springer, 2007, volume 4590 of LNCS, 281--293.
+
Jiri Barnat and Lubos Brim and Martin Leucker:
+
Parallel Model Checking and the FMICS-jETI Platform [
bibtex ,
pdf ]
+
The Twelfth IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2007) , IEEE Computer Society Press, 2007.
+
J. Barnat and L. Brim and I. Cerna and S. Drazan and D.Safranek:
+
Parallel Model-Checking Genetic Regulatory Networks [
bibtex ,
pdf ]
+
Towards Systems Biology , Verimag, 2007.
+
J. Barnat and L. Brim and I. Cerna and M. Ceska and J. Tumova:
+
ProbDiVinE: A Parallel Qualitative LTL Model Checker [
bibtex ,
pdf ]
+
Fourth International Conference on the Quantitative Evaluation of Systems (QEST'07) , IEEE Computer Society, 2007, 215-216.
+
J. Barnat and L. Brim and P. Rockai:
+
Scalable Multi-core LTL Model-Checking [
bibtex ,
pdf ]
+
Model Checking Software , Springer, 2007, volume 4595 of LNCS, 187--203.
+
L. Brim and J. Barnat:
+
Tutorial: Parallel Model Checking [
bibtex ,
pdf ]
+
Model Checking Software , Springer, 2007, volume 4595 of LNCS, 2--3.
+
2006 Jiri Barnat and Ivana Cerna:
+
Distributed Breadth-First Search LTL Model Checking [
bibtex ,
pdf ]
+
Special Issue on Parallel and Distributed Databases of Formal Methods in System Design , volume 29(2), September 2006, 117-134(18).
J. Barnat and L. Brim and I. Cerna and P. Moravec and P. Rockai and P. Simecek:
+
DiVinE -- A Tool for Distributed Verification (Tool Paper) [
bibtex ,
pdf ]
+
Computer Aided Verification , Springer Berlin / Heidelberg, 2006, volume 4144/2006 of LNCS, 278-281.
+
Jiri Barnat and Pavel Moravec:
+
Parallel Algorithms for Finding SCCs in Implicitly Given Graphs [
bibtex ,
pdf ]
+
Formal Methods: Applications and Technology , Springer, 2006, volume 4346 of LNCS, 316--330.
+
2005 J. Barnat and L. Brim and I. Cerna:
+
Cluster-Based LTL Model Checking of Large Systems [
bibtex ,
pdf ]
+
Formal Methods for Components and Objects , 2005, LNCS, 259-279.
+
J. Barnat and L. Brim and I. Cerna and P. Simecek:
+
DiVinE -- The Distributed Verification Environment [
bibtex ,
pdf ]
+
Proceedings of 4th International Workshop on Parallel and Distributed
+Methods in verifiCation , 2005, 89--94.
+
J. Barnat and V. Forejt and M. Leucker and M. Weber:
+
DivSPIN -- A SPIN compatible distributed model checker [
bibtex ,
pdf ]
+
Proceedings of 4th International Workshop on Parallel and Distributed
+Methods in verifiCation , 2005, 95--100.
+
J. Barnat and L. Brim and J. Chaloupka:
+
From Distributed Memory Cycle Detection to Parallel LTL Model
+ Checking [
bibtex ,
pdf ]
+
Electronic Notes in Theoretical Computer Science , volume 133(1,
+ month), 2005, 21--39.
L. Brim and I. Cerna and P. Moravec and J. Simsa:
+
How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors [
bibtex ,
pdf ]
+
4rd International Workshop on Parallel and Distributed Methods in verifiCation , 2005.
+
2004 L. Brim and I. Cerna and P. Moravec
+ and J. Simsa:
+
Accepting Predecessors are Better than Back
+ Edges in Distributed LTL Model-Checking [
bibtex ,
pdf ]
+
5th International Conference on Formal Methods in Computer-Aided Design (FMCAD'04) , Springer-Verlag, 2004, volume 3312 of LNCS, 352-366.
+
Jiri Barnat:
+
Distributed Memory LTL Model Checking [
bibtex ,
pdf ]
+Ph.D. Thesis,
Masaryk University Brno, Faculty of Informatics , 2004.
+
Lubos Brim and
+ Ivana Cerna and
+ Lukas Hejtmanek:
+
Distributed Negative Cycle Detection Algorithms [
bibtex ,
pdf ]
+
Parallel Computing: Software Technology, Algorithms, and Applications (PARCO'03) , Elsevier, 2004, volume 13 of Advances in Parallel Computing, 297--304.
+
L. Brim and I. Cerna and P. Moravec and J. Simsa:
+
Distributed Partial Order Reduction of State Spaces [
bibtex ,
pdf ]
+
3rd International Workshop on Parallel and Distributed Methods in verifiCation , 2004.
+
2003 I. Cerna and R. Pelanek:
+
Distributed Explicit Fair Cycle Detection [
bibtex ,
pdf ]
+
Proc. SPIN workshop , Springer, 2003, volume 2648 of LNCS, 49-74.
+
L. Brim and J. Barnat:
+
Distribution of Explicit-State LTL
+Model-Checking [
bibtex ,
pdf ]
+
8th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 03) , Elsevier, 2003, volume 80 of Electronic Notes in Theoretical Computer Science.
+
J. Barnat and L. Brim and J. Chaloupka:
+
Parallel Breadth-First Search LTL
+Model-Checking [
bibtex ,
pdf ]
+
18th IEEE International Conference on Automated Software
+Engineering (ASE'03) , IEEE Computer Society, 2003, 106--115.
+
2002 J. Barnat and L. Brim and I. Cerna:
+
Property driven distribution of Nested DFS [
bibtex ,
pdf ]
+
Proc. Workshop on Verification and Computational Logic , 2002, DSSE Technical Report, 1 - 10.
+
2001 L. Brim and I. Cerna and P. Krcal
+ and R. Pelanek:
+
Distributed LTL Model Checking Based on Negative
+ Cycle Detection [
bibtex ,
pdf ]
+
Proc. Foundations of Software Technology and Theoretical
+ Computer Science , Springer, 2001,
+ opteditor, volume 2245,
+ series of , 96--107.
+
J. Barnat and L. Brim and J.
+ Stribrna:
+
Distributed LTL Model-Checking
+ in SPIN [
bibtex ,
pdf ]
+
Proc. SPIN Workshop on Model Checking of Software , Springer, 2001, volume 2057 of LNCS, 200 - 216.
+
Tool Guide
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
This section will give you a quick overview on using DiVinE MC for verification purposes. Please note that we use DiVinE Multi-Core for practical examples of command invocations. Commands for DiVinE Cluster are slightly different, although the differences are quite superficial. Overview of differences is summarised below.
+
+
+
+
First and foremost, the model needs to be specified in DVE modelling language and the property needs to be specified either as an LTL formula or as a Büchi automaton. We will present usage of the tool on a simple example of a mutual exclusion protocol. Source code of a single process of such a model looks like this:
+
+
process P_$1 {
+byte j=0, k=0;
+state NCS, CS, wait, q2, q3;
+init NCS;
+trans
+ NCS -> wait { effect j = 1, active = $1, waiting[$1] = 1; },
+ wait -> q2 { guard j < N;
+ effect pos[$1] = j, active = $1; },
+ q2 -> q3 { effect step[j-1] = $1, k = 0, active = $1; },
+ q3 -> q3 { guard (k == $1 || pos[k]< j) && k < N;
+ effect k = k+1, active = $1; },
+ q3 -> wait { guard step[j-1] != $1 || k == N;
+ effect j = j+1, active = $1; },
+ wait -> CS { guard j == N;
+ effect in_critical = in_critical+1,
+ active = $1, waiting[$1] = 0; },
+ CS -> NCS { effect pos[$1] = 0, in_critical = in_critical-1,
+ active = $1; };
+}
+
+
For a more elaborate discussion on how to prepare models for DiVinE, please see the Language Guide . The first LTL property we will use is
+
+
GF c0 and GF c1
+
+
which is a naive formulation of the idea that the two processes are infinitely often in the critical section. An improved version of the formula that enforces fairness will be
+
+
GF(a0 and w0) -> GF c0 and (GF a1 and w1) -> GF c1
+
+
The propositions a and w mean that the given process is active (when a holds) and that it is waiting (when w holds). First of these formulae is invalid (and the tool produces a counterexample), whereas the second one will be shown to hold for the model presented.
+
+
An example invocation of the tool for the model with 3 processes (and the formulae extended to 3 processes straightforwardly) looks like this:
+
+
$ divine-mc owcty mutex_peterson.naive.dve
+ initialize... |S| = 81219
+------------- iteration 0 -------------
+ reachability... |S| = 81219
+ elimination & reset... |S| = 59736
+------------- iteration 1 -------------
+ reachability... |S| = 59736
+ elimination & reset... |S| = 59736
+ =====================================
+ Accepting cycle FOUND
+ =====================================
+ generating counterexample... done
+
+
The counterexample could be browsed by running divine-mc.simulator on the produced mutex_peterson.naive.trail. The simulator is currently fairly rudimentary, but it still serves the purpose. When the same verifier command is used on the second formula, no counterexample is generated and the tool declares that an accepting cycle has not been found, which means that the LTL property holds.
+
+
It can be seen that the input file to the verifier is a single DVE file that already contains a property process. Such a file could be written by hand (when the property has been specified as a Büchi automaton) or produced by divine-mc.combine, which takes a set of LTL formulae as input (in an .ltl file containing definitions of atomic propositions and the formulae. For example, such file containing the 2 discussed properties looks like this:
+
+
#define a_0 (active == 0)
+#define a_1 (active == 1)
+
+#define w_0 (waiting[0] == 1)
+#define w_1 (waiting[1] == 1)
+
+#define c_0 (P_0.CS)
+#define c_1 (P_1.CS)
+
+#property G(F(c_0)) && G(F(c_1))
+#property ((GF(a_0 && w_0)) -> GF(c_0)) && ((GF(a_1 && w_1)) -> GF(c_1))
+
+
The divine-mc.combine program will produce a single DVE file for each property, which can then be used as an input for the verifier.
+
+
Using DiVinE Cluster
+
+
The divine-mc.combine command is called divine.combine. When running divine-mc owcty, in cluster, you would instead use divine.owcty, and you cannot run it directly – please consult your MPI implementation manual how to run MPI programs in your cluster: This usually involves using mpiexec.
+
+
+ 
+
+ 
+
+
+
+
+
+
+
+
Welcome to DiVinE!