Tutorial Enabling Analysis - Revision history

David Geleßus: Use wikilinks instead of URLs

2022-11-18T13:19:17Z

Use wikilinks instead of URLs

← Older revision		Revision as of 13:19, 18 November 2022
Line 1:		Line 1:
	The B-method and in particular its successor Event-B are methodologies for formal development and verification of systems. In Event-B, a machine is usually viewed as a reactive system executing continuously enabled (atomic) events in an interleaved fashion. Thus, parallel events of the system are easily modeled as an interleaving of operation executions. On the other hand, the introduction of abstract counters is required when events are supposed to be executed in some (sequential) order. This, however, can in some cases slow the work of understanding and verifying a model since identifying the sequential ordering of events in an Event-B model is not that obvious. Thus, using methods for determining the control flow can be sometimes very beneficial for understanding the model, as well as for techniques for automatic verification such as model checking.		The B-method and in particular its successor Event-B are methodologies for formal development and verification of systems. In Event-B, a machine is usually viewed as a reactive system executing continuously enabled (atomic) events in an interleaved fashion. Thus, parallel events of the system are easily modeled as an interleaving of operation executions. On the other hand, the introduction of abstract counters is required when events are supposed to be executed in some (sequential) order. This, however, can in some cases slow the work of understanding and verifying a model since identifying the sequential ordering of events in an Event-B model is not that obvious. Thus, using methods for determining the control flow can be sometimes very beneficial for understanding the model, as well as for techniques for automatic verification such as model checking.

	In this tutorial we present a static analysis for B and Event-B that can be used to reveal the control flow of a machine and to optimize model checking of models written in B and Event-B (see also [~~https://www3.hhu.de/stups/prob/index.php/Tutorial_Various_Optimizations~~#~~Partial_Guard_Evaluation~~ Tutorial on Partial Guard Evaluation ]). The results of the analysis, designated also as ‘’enabling analysis’’, can be presented as relations by means of a table or by means of a graph. For simplicity, we will concentrate mainly on B and use the terminology of the formalism.		In this tutorial we present a static analysis for B and Event-B that can be used to reveal the control flow of a machine and to optimize model checking of models written in B and Event-B (see also [[Tutorial Various Optimizations#Partial Guard Evaluation\|Tutorial on Partial Guard Evaluation]]). The results of the analysis, designated also as ‘’enabling analysis’’, can be presented as relations by means of a table or by means of a graph. For simplicity, we will concentrate mainly on B and use the terminology of the formalism.

	== Enabling Relations ==		== Enabling Relations ==
Line 55:		Line 55:
	[[File:KeepRelation.png]]		[[File:KeepRelation.png]]

	We can take (Op1,Op2) and (Op1,Op3) as examples of pairs in <tt>Example.mch</tt> that are elements of the keep relation. ‘’keep’’ relations can sometimes be easily determined by analyzing just the syntactic structure of both operations, or more precisely the “read” and “write” sets of both operations.<ref>For an operation op the set read(op) denotes the set of variables that are read by op. Accordingly, by write(op) we denote the set of variables that are written by op.</ref> If, for example, an operation op1 does not write any variable of the machine that is read in the guard condition of op2, then we can infer that op1 ‘’keeps’’ op2. In that case we also say that op1 does not change op2 syntactically. In the class of the ‘’keep’’ relations are included also relations such as independence. Two operations op1 and op2 are called independent if each of them cannot disable the other operation and the both orders of execution <op1,op2> and <op2,op1> have the same effect.<ref>See the [~~https://www3.hhu.de/stups/prob/index.php/Tutorial_Various_Optimizations~~#~~Partial_Order_Reduction~~ Tutorial on Partial Order Reduction] for more information on independence between operations.</ref>		We can take (Op1,Op2) and (Op1,Op3) as examples of pairs in <tt>Example.mch</tt> that are elements of the keep relation. ‘’keep’’ relations can sometimes be easily determined by analyzing just the syntactic structure of both operations, or more precisely the “read” and “write” sets of both operations.<ref>For an operation op the set read(op) denotes the set of variables that are read by op. Accordingly, by write(op) we denote the set of variables that are written by op.</ref> If, for example, an operation op1 does not write any variable of the machine that is read in the guard condition of op2, then we can infer that op1 ‘’keeps’’ op2. In that case we also say that op1 does not change op2 syntactically. In the class of the ‘’keep’’ relations are included also relations such as independence. Two operations op1 and op2 are called independent if each of them cannot disable the other operation and the both orders of execution <op1,op2> and <op2,op1> have the same effect.<ref>See the [[Tutorial Various Optimizations#Partial Order Reduction\|Tutorial on Partial Order Reduction]] for more information on independence between operations.</ref>

	All three classes (‘’guaranteed’’, ‘’impossible’’ and ‘’keep’’) of enabling relations presented so far represent definite relations. That is, if a pair of operations (op1,op2) is confirmed to be a relation of one of this three classes, then we can certainly say what effect on the enabling condition of op2 would the execution of op1 have. However, for some pairs of operations we cannot certainly say what effect an operation would have on the enabling condition of another operation. This is due to the fact that the enabling status of an operation does not only depend on the effect of the executed operations, but also on the current variables’ evaluation. Take, for instance, the tuple (Op3,Op1) from the B machine above. Considering the action part of Op3 and the guard condition of Op1 we can assume that Op3 can enable Op1. Since the guard of Op1 depends not only on the current value of x, but also on y, there could be transitions s -> s' of Op3 in the state space of the machine where Op1 is disabled in both states s and s’. Though, what we could definitely say is that Op3 cannot disable Op1. This relationship we can illustrate as follows:		All three classes (‘’guaranteed’’, ‘’impossible’’ and ‘’keep’’) of enabling relations presented so far represent definite relations. That is, if a pair of operations (op1,op2) is confirmed to be a relation of one of this three classes, then we can certainly say what effect on the enabling condition of op2 would the execution of op1 have. However, for some pairs of operations we cannot certainly say what effect an operation would have on the enabling condition of another operation. This is due to the fact that the enabling status of an operation does not only depend on the effect of the executed operations, but also on the current variables’ evaluation. Take, for instance, the tuple (Op3,Op1) from the B machine above. Considering the action part of Op3 and the guard condition of Op1 we can assume that Op3 can enable Op1. Since the guard of Op1 depends not only on the current value of x, but also on y, there could be transitions s -> s' of Op3 in the state space of the machine where Op1 is disabled in both states s and s’. Though, what we could definitely say is that Op3 cannot disable Op1. This relationship we can illustrate as follows:

Michael Leuschel: /* Performing Enabling Analysis within ProB */

2016-09-09T12:41:32Z

Performing Enabling Analysis within ProB

← Older revision		Revision as of 12:41, 9 September 2016
Line 155:		Line 155:
	<pre>$ probcli file.mch -enabling_analysis_csv FILE </pre>		<pre>$ probcli file.mch -enabling_analysis_csv FILE </pre>
	where FILE is the name of the CSV-file in which the results of the analysis are stored.		where FILE is the name of the CSV-file in which the results of the analysis are stored.

			Related to this command is the feasibility analysis, which just checks whether a single event is in principle possible (given the invariant):
			<pre>$ probcli file.mch -feasibility_analysis_csv FILE </pre>

	== References and Footnotes ==		== References and Footnotes ==

Ivaylo Dobrikov: /* Performing Enabling Analysis within ProB */

2016-06-06T10:44:01Z

Performing Enabling Analysis within ProB

← Older revision		Revision as of 10:44, 6 June 2016
Line 110:		Line 110:
	== Performing Enabling Analysis within ProB ==		== Performing Enabling Analysis within ProB ==

	The enabling analysis has been implemented in the ProB toolset. The computation of the enabling relations is based on syntactic and constraint-based techniques. The identification of relations such as ‘’syntactic_independent’’ and ‘’syntactic_unchanged’’ requires just a thorough study of the syntactic structure of the operations, i.e. no calls to the constraint solver have to be made. However, to confirm, for example, that an operation is guaranteed or impossible to be executed after another operation the use of the ProB’s constraint solver is unavoidable. For instance, consider the pair (Op2,Op1) from <tt>Example.mch</tt>. As we have seen, in <tt>Example.mch</tt> the operation Op1 is guaranteed to be enabled after each execution of Op2. In ProB this could be computed by feeding the (before-after) predicate “ (x mod 2 = 1) ~~=> [~~x:=x+1 \|\| y:=2] (x+y<4)” into the constraint solver. As a result, the constraint solver will not find a solution for the predicate, i.e. the constraint solver will not find a state ‘’s’’ satisfying “x mod 2 = 1” from which after executing Op2 at ‘’s’’ a solution state s’ will be found that fulfills “x+y<4”; note that “x+y<4” is the negation of the guard of Op1. Since there is no after-state of Op2 at which Op1 is disabled we can conclude that Op1 is guaranteed to be executed after Op2. When constraints are getting more complex the constraint solver may need more time for solving ~~and determining~~ the enabling relations may become a very time-expensive task. Therefore, a time-out for each constraint solver call is set. In other words, if the constraint solver does not find a solution in the given time by the user, then the respective relation will be denoted as time-outed. By default, in ProB the time-out for each constraint solver call is set to 300 ms.		The enabling analysis has been implemented in the ProB toolset. The computation of the enabling relations is based on syntactic and constraint-based techniques. The identification of relations such as ‘’syntactic_independent’’ and ‘’syntactic_unchanged’’ requires just a thorough study of the syntactic structure of the operations, i.e. no calls to the constraint solver have to be made. However, to confirm, for example, that an operation is guaranteed or impossible to be executed after another operation the use of the ProB’s constraint solver is unavoidable. For instance, consider the pair (Op2,Op1) from <tt>Example.mch</tt>. As we have seen, in <tt>Example.mch</tt> the operation Op1 is guaranteed to be enabled after each execution of Op2. In ProB this could be computed by feeding the (before-after) predicate “ (x mod 2 = 1) & (x'=x+1 & y=2) & (x'+y'<4)” into the constraint solver. As a result, the constraint solver will not find a solution for the predicate, i.e. the constraint solver will not find a state ‘’s’’ satisfying “x mod 2 = 1” from which after executing Op2 at ‘’s’’ a solution state s’ will be found that fulfills “x+y<4”; note that “x+y<4” is the negation of the guard of Op1. Since there is no after-state of Op2 at which Op1 is disabled we can conclude that Op1 is guaranteed to be executed after Op2. When constraints are getting more complex the constraint solver may need more time for solving. Thus, the computation of the enabling relations may become a very time-expensive task. Therefore, a time-out for each constraint solver call is set. In other words, if the constraint solver does not find a solution in the given time by the user, then the respective relation will be denoted as time-outed. By default, in ProB the time-out for each constraint solver call is set to 300 ms.

	Within <tt>ProB Tcl/Tk</tt> you can find the menu "Enabling Analysis" in the "Analysis" menu of the menu bar.		Within <tt>ProB Tcl/Tk</tt> you can find the menu "Enabling Analysis" in the "Analysis" menu of the menu bar.

Ivaylo Dobrikov: /* Performing Enabling Analysis within ProB */

2016-02-23T09:36:07Z

Performing Enabling Analysis within ProB

← Older revision		Revision as of 09:36, 23 February 2016
Line 152:		Line 152:
	</pre>		</pre>

	To perform enabling analysis from the command line and save the results to a CSV-file use the following commando:		To perform enabling analysis from the command line and save the results into a CSV-file use the following commando:
	<pre>$ probcli file.mch -enabling_analysis_csv FILE </pre>		<pre>$ probcli file.mch -enabling_analysis_csv FILE </pre>
	where FILE is the name of the CSV-file in which the results of the analysis are stored.		where FILE is the name of the CSV-file in which the results of the analysis are stored.

	== References and Footnotes ==		== References and Footnotes ==

Ivaylo Dobrikov: /* Summary of the Enabling Relations */

2016-02-23T09:35:54Z

Summary of the Enabling Relations

← Older revision		Revision as of 09:35, 23 February 2016
Line 103:		Line 103:
	* ''possible_enable'': op2 possible after op1, but op2 cannot be disabled by op1.		* ''possible_enable'': op2 possible after op1, but op2 cannot be disabled by op1.
	[[File: PossibleEnableExample.png]]		[[File: PossibleEnableExample.png]]
	* ''possible_disable'': op2 possible after ~~iop1~~, but op2 cannot be enabled by op1.		* ''possible_disable'': op2 possible after op1, but op2 cannot be enabled by op1.
	[[File: PossibleDisableExample.png]]		[[File: PossibleDisableExample.png]]
	* ''infeasible'': op1 is not feasible and thus cannot influence op2.		* ''infeasible'': op1 is not feasible and thus cannot influence op2.

Ivaylo Dobrikov: /* Enabling Relations */

2016-02-22T12:56:08Z

Enabling Relations

← Older revision		Revision as of 12:56, 22 February 2016
Line 70:		Line 70:

	[[File: EnablingResults.png]]		[[File: EnablingResults.png]]

			Rather than showing the enabling information for each pair of operations of the machine, one can display the enabling relations by means of a graph. The graph contains the operations as nodes and the above enabling relations as edges between the nodes, with the exception that relations marked as impossible, independent or infeasible are not shown in the graph. We denote such graphs as enable graphs. The enable graph of <tt>Example.mch</tt> looks as follows.

			[[File: EnableGraph_Example.png]]

			From the enable graph one can recognize the control flow of the model and deduce some properties. For example, we can clearly see that <tt>Op4</tt> cannot occur after the execution of another operation.

	== Summary of the Enabling Relations ==		== Summary of the Enabling Relations ==

Ivaylo Dobrikov: /* Performing Enabling Analysis within ProB */

2016-02-16T14:51:34Z

Performing Enabling Analysis within ProB

← Older revision		Revision as of 14:51, 16 February 2016
Line 108:		Line 108:
	Within <tt>ProB Tcl/Tk</tt> you can find the menu "Enabling Analysis" in the "Analysis" menu of the menu bar.		Within <tt>ProB Tcl/Tk</tt> you can find the menu "Enabling Analysis" in the "Analysis" menu of the menu bar.
	[[File: EnablingAnalysisMenu.png]]		[[File: EnablingAnalysisMenu.png]]

	The "Enabling Analysis" menu provides multiple commands:		The "Enabling Analysis" menu provides multiple commands:
	* "Enabling Analysis (Table)": this command performs a (fast) enabling analysis on the respective B model using a time-out of 300 ms for the constraint-solver calls. The result of the enabling analysis is shown in a table. The table lists all enabling relations between the operations of the loaded B model. These can be exported to a CSV file. The table for <tt>Example.mch</tt> at the end of the ''' Enabling Relations''' section was constructed this way.		* "Enabling Analysis (Table)": this command performs a (fast) enabling analysis on the respective B model using a time-out of 300 ms for the constraint-solver calls. The result of the enabling analysis is shown in a table. The table lists all enabling relations between the operations of the loaded B model. These can be exported to a CSV file. The table for <tt>Example.mch</tt> at the end of the ''' Enabling Relations''' section was constructed this way.

Ivaylo Dobrikov: /* Performing Enabling Analysis within ProB */

2016-02-16T14:51:21Z

Performing Enabling Analysis within ProB

← Older revision		Revision as of 14:51, 16 February 2016
Line 108:		Line 108:
	Within <tt>ProB Tcl/Tk</tt> you can find the menu "Enabling Analysis" in the "Analysis" menu of the menu bar.		Within <tt>ProB Tcl/Tk</tt> you can find the menu "Enabling Analysis" in the "Analysis" menu of the menu bar.
	[[File: EnablingAnalysisMenu.png]]		[[File: EnablingAnalysisMenu.png]]
	The "Enabling Analysis" menu provides multiple commands:		The "Enabling Analysis" menu provides multiple commands:
	* "Enabling Analysis (Table)": this command performs a (fast) enabling analysis on the respective B model using a time-out of 300 ms for the constraint-solver calls. The result of the enabling analysis is shown in a table. The table lists all enabling relations between the operations of the loaded B model. These can be exported to a CSV file. The table for <tt>Example.mch</tt> at the end of the ''' Enabling Relations''' section was constructed this way.		* "Enabling Analysis (Table)": this command performs a (fast) enabling analysis on the respective B model using a time-out of 300 ms for the constraint-solver calls. The result of the enabling analysis is shown in a table. The table lists all enabling relations between the operations of the loaded B model. These can be exported to a CSV file. The table for <tt>Example.mch</tt> at the end of the ''' Enabling Relations''' section was constructed this way.
	* "Enabling Analysis (Precise, Table)": this command performs an enabling analysis using a time-out of 2800 ms for each of the constraint-solver calls. As for the command above, the result of the analysis is shown in a table that can be exported to a CSV file.		* "Enabling Analysis (Precise, Table)": this command performs an enabling analysis using a time-out of 2800 ms for each of the constraint-solver calls. As for the command above, the result of the analysis is shown in a table that can be exported to a CSV file.

Ivaylo Dobrikov: /* Performing Enabling Analysis within ProB */

2016-02-16T14:50:58Z

Performing Enabling Analysis within ProB

← Older revision		Revision as of 14:50, 16 February 2016
Line 107:		Line 107:

	Within <tt>ProB Tcl/Tk</tt> you can find the menu "Enabling Analysis" in the "Analysis" menu of the menu bar.		Within <tt>ProB Tcl/Tk</tt> you can find the menu "Enabling Analysis" in the "Analysis" menu of the menu bar.

	[[File: EnablingAnalysisMenu.png]]		[[File: EnablingAnalysisMenu.png]]

	The "Enabling Analysis" menu provides multiple commands:		The "Enabling Analysis" menu provides multiple commands:
	* "Enabling Analysis (Table)": this command performs a (fast) enabling analysis on the respective B model using a time-out of 300 ms for the constraint-solver calls. The result of the enabling analysis is shown in a table. The table lists all enabling relations between the operations of the loaded B model. These can be exported to a CSV file. The table for <tt>Example.mch</tt> at the end of the ''' Enabling Relations''' section was constructed this way.		* "Enabling Analysis (Table)": this command performs a (fast) enabling analysis on the respective B model using a time-out of 300 ms for the constraint-solver calls. The result of the enabling analysis is shown in a table. The table lists all enabling relations between the operations of the loaded B model. These can be exported to a CSV file. The table for <tt>Example.mch</tt> at the end of the ''' Enabling Relations''' section was constructed this way.

Ivaylo Dobrikov: /* Performing Enabling Analysis within ProB */

2016-02-16T14:44:27Z

Performing Enabling Analysis within ProB

← Older revision		Revision as of 14:44, 16 February 2016
Line 106:		Line 106:
	The enabling analysis has been implemented in the ProB toolset. The computation of the enabling relations is based on syntactic and constraint-based techniques. The identification of relations such as ‘’syntactic_independent’’ and ‘’syntactic_unchanged’’ requires just a thorough study of the syntactic structure of the operations, i.e. no calls to the constraint solver have to be made. However, to confirm, for example, that an operation is guaranteed or impossible to be executed after another operation the use of the ProB’s constraint solver is unavoidable. For instance, consider the pair (Op2,Op1) from <tt>Example.mch</tt>. As we have seen, in <tt>Example.mch</tt> the operation Op1 is guaranteed to be enabled after each execution of Op2. In ProB this could be computed by feeding the (before-after) predicate “ (x mod 2 = 1) => [x:=x+1 \|\| y:=2] (x+y<4)” into the constraint solver. As a result, the constraint solver will not find a solution for the predicate, i.e. the constraint solver will not find a state ‘’s’’ satisfying “x mod 2 = 1” from which after executing Op2 at ‘’s’’ a solution state s’ will be found that fulfills “x+y<4”; note that “x+y<4” is the negation of the guard of Op1. Since there is no after-state of Op2 at which Op1 is disabled we can conclude that Op1 is guaranteed to be executed after Op2. When constraints are getting more complex the constraint solver may need more time for solving and determining the enabling relations may become a very time-expensive task. Therefore, a time-out for each constraint solver call is set. In other words, if the constraint solver does not find a solution in the given time by the user, then the respective relation will be denoted as time-outed. By default, in ProB the time-out for each constraint solver call is set to 300 ms.		The enabling analysis has been implemented in the ProB toolset. The computation of the enabling relations is based on syntactic and constraint-based techniques. The identification of relations such as ‘’syntactic_independent’’ and ‘’syntactic_unchanged’’ requires just a thorough study of the syntactic structure of the operations, i.e. no calls to the constraint solver have to be made. However, to confirm, for example, that an operation is guaranteed or impossible to be executed after another operation the use of the ProB’s constraint solver is unavoidable. For instance, consider the pair (Op2,Op1) from <tt>Example.mch</tt>. As we have seen, in <tt>Example.mch</tt> the operation Op1 is guaranteed to be enabled after each execution of Op2. In ProB this could be computed by feeding the (before-after) predicate “ (x mod 2 = 1) => [x:=x+1 \|\| y:=2] (x+y<4)” into the constraint solver. As a result, the constraint solver will not find a solution for the predicate, i.e. the constraint solver will not find a state ‘’s’’ satisfying “x mod 2 = 1” from which after executing Op2 at ‘’s’’ a solution state s’ will be found that fulfills “x+y<4”; note that “x+y<4” is the negation of the guard of Op1. Since there is no after-state of Op2 at which Op1 is disabled we can conclude that Op1 is guaranteed to be executed after Op2. When constraints are getting more complex the constraint solver may need more time for solving and determining the enabling relations may become a very time-expensive task. Therefore, a time-out for each constraint solver call is set. In other words, if the constraint solver does not find a solution in the given time by the user, then the respective relation will be denoted as time-outed. By default, in ProB the time-out for each constraint solver call is set to 300 ms.

	Within <tt>ProB Tcl/Tk</tt> you can find the menu "Enabling Analysis" in the "Analysis" menu of the menu bar. The "Enabling Analysis" menu provides multiple commands:		Within <tt>ProB Tcl/Tk</tt> you can find the menu "Enabling Analysis" in the "Analysis" menu of the menu bar.

			[[File: EnablingAnalysisMenu.png]]

			The "Enabling Analysis" menu provides multiple commands:
	* "Enabling Analysis (Table)": this command performs a (fast) enabling analysis on the respective B model using a time-out of 300 ms for the constraint-solver calls. The result of the enabling analysis is shown in a table. The table lists all enabling relations between the operations of the loaded B model. These can be exported to a CSV file. The table for <tt>Example.mch</tt> at the end of the ''' Enabling Relations''' section was constructed this way.		* "Enabling Analysis (Table)": this command performs a (fast) enabling analysis on the respective B model using a time-out of 300 ms for the constraint-solver calls. The result of the enabling analysis is shown in a table. The table lists all enabling relations between the operations of the loaded B model. These can be exported to a CSV file. The table for <tt>Example.mch</tt> at the end of the ''' Enabling Relations''' section was constructed this way.
	* "Enabling Analysis (Precise, Table)": this command performs an enabling analysis using a time-out of 2800 ms for each of the constraint-solver calls. As for the command above, the result of the analysis is shown in a table that can be exported to a CSV file.		* "Enabling Analysis (Precise, Table)": this command performs an enabling analysis using a time-out of 2800 ms for each of the constraint-solver calls. As for the command above, the result of the analysis is shown in a table that can be exported to a CSV file.