model_checking_with_af3.html

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">

<!--
 Documentation of the Semantic Inspector View.
 
 @author becker
 @ConQAT.Rating GREEN Hash: 434648996FF02802133EB40B4275941A
-->

<html>
<head>
	<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
	<title>Model Checking with AF3</title>
</head>

<body>
<h2><u><font color="#336699">Model checking with Auto FOCUS 3</font></u></h2>
<font color="#000000" style="font-family:Verdana, Geneva, sans-serif" size="2px">


<h3><font color="#336699">Introduction</font></h3>
AF3 provides a deep integration of the <a href="http://nusmv.fbk.eu/">NuSMV</a> model checker, and of its successor <a href="https://nuxmv.fbk.eu/">nuXmv</a>, 
with the following features: 
<ul>
<li><b> user proximity: </b> AF3 brings model checker closer to its users. Model checking with 
AF3 is easy to understand, easy to learn, simple and efficient to use. 
<li> <b>easy to specify properties:</b> AF users can work at the abstraction level of AF3 models.
<li> <b>analyses results are easy to interpret</b>. Counter-examples can be simulated in AF3 such that 
the users gain an immediate feedback about the causes that brought the property violation.
</ul>
</li>
</ul>

<h3><font color="#336699">Prerequisite: NuSMV/nuXmv</font></h3>

First ensure that nuXmv or NuSMV is installed: see <a href="external_tools.html">External Tools</a> for instructions.

<h3><font color="#336699">Activation</font></h3>
You need to ensure that the reachability check is activated:
<ol>
<li>Double click on the root of your project:
<br>
<img src="./pictures/clickOnRoot.png" border="1" />
<br>
<br></li>
<li>And check "All states are reachable":
<br>
<img src="./pictures/activateReachability.png" border="1" />
<br>
<br>
</ol>
Be sure also that the configuration in which this check is activated is the one which is the "current objective".

<p>
This will trigger the check that all state automata of the project have 100% state coverage 
and activate the automatic trigger of this check for every state automaton that you might 
add later on to your project. It will also trigger a check for every state automaton as soon
as it is modified.


<h3><font color="#336699">Example</font></h3>

Open the simple traffic light example and double-click on the Controller component.
Open the V&V dashboard tab below the editor and add a specification as follows:

<br>
<br>
<img src="./pictures/TLSpec.png" border="1" />
<br>
<br>

You shall see that the check has automatically been run (and in this case provides a successful result).
In case of failure:
<br>
<br>
<img src="./pictures/TLSpecFail.png" border="1" />
<br>
<br>
Double-clicking the status message will start a simulation demonstrating the coutner-example.

</body>
</html>