Modularisation Plug-in Tutorial - Revision history

imported>Mathieu: Category:Plugin

2009-11-10T20:58:59Z

← Older revision		Revision as of 20:58, 10 November 2009
Line 208:		Line 208:
	There is, however, also a additional proof obligation that requires to demonstrate that a call to ''d1_open'' was done in a state satisfying the operation preconditions. This is the reason we are required to add ''d1_error = FALSE'' into the event guard.		There is, however, also a additional proof obligation that requires to demonstrate that a call to ''d1_open'' was done in a state satisfying the operation preconditions. This is the reason we are required to add ''d1_error = FALSE'' into the event guard.

	[Category:Plugin]]		[[Category:Plugin]]

imported>Mathieu: [Category:Plugin]]

2009-11-10T20:58:28Z

[Category:Plugin]]

← Older revision		Revision as of 20:58, 10 November 2009
Line 1:		Line 1:

	Go to the [[Modularisation Plug-in\|plug-in description page]].		Go to the [[Modularisation Plug-in\|plug-in description page]].

Line 208:		Line 207:

	There is, however, also a additional proof obligation that requires to demonstrate that a call to ''d1_open'' was done in a state satisfying the operation preconditions. This is the reason we are required to add ''d1_error = FALSE'' into the event guard.		There is, however, also a additional proof obligation that requires to demonstrate that a call to ''d1_open'' was done in a state satisfying the operation preconditions. This is the reason we are required to add ''d1_error = FALSE'' into the event guard.

			[Category:Plugin]]

imported>Alexili at 08:16, 23 October 2009

2009-10-23T08:16:32Z

← Older revision		Revision as of 08:16, 23 October 2009
Line 127:		Line 127:
	VARIABLES door error		VARIABLES door error
	INVARIANTS		INVARIANTS
	@inv1 door ∈ BOOL		@inv1 door ∈ BOOL
	@inv2 error ∈ BOOL		@inv2 error ∈ BOOL
	OPERATIONS		OPERATIONS

	operation for opening a door		operation for opening a door
	open ≙ PRE		open ≙ PRE
	@pre1: door = FALSE		@pre1: door = FALSE
	@pre2: error = FALSE		@pre2: error = FALSE
Line 143:		Line 143:

	operation for closing a door		operation for closing a door
	close ≙ PRE		close ≙ PRE
	@pre1: door = TRUE		@pre1: door = TRUE
	@pre1: error = FALSE		@pre1: error = FALSE

imported>Alexili at 08:15, 23 October 2009

2009-10-23T08:15:21Z

← Older revision		Revision as of 08:15, 23 October 2009
Line 133:		Line 133:
	operation for opening a door		operation for opening a door
	open ≙ PRE		open ≙ PRE
	@pre1: door = FALSE		@pre1: door = FALSE
	@pre2: error = FALSE		@pre2: error = FALSE
	RETURN error_status		RETURN error_status
	POST		POST
	@post1: door' = TRUE		@post1: door' = TRUE
	@post2: error' ∈ BOOL		@post2: error' ∈ BOOL
	@post3: error_status' = error'		@post3: error_status' = error'
	END		END

	operation for closing a door		operation for closing a door
	close ≙ PRE		close ≙ PRE
	@pre1: door = TRUE		@pre1: door = TRUE
	@pre1: error = FALSE		@pre1: error = FALSE
	RETURN error_status		RETURN error_status
	POST		POST
	@post1: door' = FALSE		@post1: door' = FALSE
	@post2: error' ∈ BOOL		@post2: error' ∈ BOOL
	@post3: error_status' = error'		@post3: error_status' = error'
	END		END
	END		END

imported>Alexili at 08:13, 23 October 2009

2009-10-23T08:13:47Z

← Older revision		Revision as of 08:13, 23 October 2009
Line 65:		Line 65:
	@act4 error ≔ FALSE		@act4 error ≔ FALSE
	end		end

	event open1		event open1
	where		where
Line 75:		Line 74:
	@act2 error :∈ BOOL		@act2 error :∈ BOOL
	end		end

	event close1		event close1
	where		where
Line 84:		Line 82:
	@act2 error :∈ BOOL		@act2 error :∈ BOOL
	end		end

	event open2		event open2
	where		where
Line 94:		Line 91:
	@act2 error :∈ BOOL		@act2 error :∈ BOOL
	end		end

	event close2		event close2
	where		where
Line 103:		Line 99:
	@act2 error :∈ BOOL		@act2 error :∈ BOOL
	end		end

	event pressure_low		event pressure_low
	where		where
Line 113:		Line 108:
	@act2 error :∈ BOOL		@act2 error :∈ BOOL
	end		end

	event pressure_high		event pressure_high
	where		where
Line 210:		Line 204:
	then		then
	@act1 error :∈ BOOL		@act1 error :∈ BOOL
	@act2 d1_door ≔ TRUE		@act2 d1_door ≔ TRUE
	end		end

	There is, however, also a additional proof obligation that requires to demonstrate that a call to ''d1_open'' was done in a state satisfying the operation preconditions. This is the reason we are required to add ''d1_error = FALSE'' into the event guard.		There is, however, also a additional proof obligation that requires to demonstrate that a call to ''d1_open'' was done in a state satisfying the operation preconditions. This is the reason we are required to add ''d1_error = FALSE'' into the event guard.

imported>Alexili at 08:12, 23 October 2009

2009-10-23T08:12:32Z

Show changes

imported>Alexili at 13:40, 22 October 2009

2009-10-22T13:40:10Z

@@ Line 1: / Line 1: @@
-==Modularisation Plug-in Tutorial==
 Go to the [[Modularisation Plug-in|plug-in description page]].
 The tutorial illustrates the use of the modularisation plug-in in an Event-B development. The example used is rather small scale but it still demonstrates some basic principles of introducing modules during the development process.
-===Sluice Control Example===
+==Sluice Control Example==
 The example is a sluice with two doors connecting areas with dramatically different pressures. The pressure difference makes it unsafe to open a door unless the pressure is leveled between the areas connected by the door. The purpose of the system is to adjust the pressure in the sluice area and control the door locks to allow a user to get safely inside to outside. Such system can be deployed, for example, on a submarine to allow divers to get out while submerged.
@@ Line 27: / Line 27: @@
 [[Image:SluiceControllerSolution.png|500px]]
 The shaded rectagles denote a pressure level, high pressure area corresponds to a higher rectangle. The "u" label marks the current position of a system user. Initially, a user is inside and the sluice pressure is levelled with the outside pressure. Before the door connecting to the sluice is opened, the pressure is decreased to level it with the inside pressure. Once the door is open, the user moves in, the door is sealed again. Finally, the sluice pressure is set to match the outside pressure and the door leading may be safely opened.

imported>Alexili at 13:04, 22 October 2009

2009-10-22T13:04:45Z

← Older revision		Revision as of 13:04, 22 October 2009
Line 25:		Line 25:
	The following diagram shows the stages of the system operation that let a user to get outside starting in the inside area.		The following diagram shows the stages of the system operation that let a user to get outside starting in the inside area.

	[[Image:SluiceControllerSolution.png\|~~400px~~]]		[[Image:SluiceControllerSolution.png\|500px]]

	The shaded rectagles denote a pressure level, high pressure area corresponds to a higher rectangle. The "u" label marks the current position of a system user. Initially, a user is inside and the sluice pressure is levelled with the outside pressure. Before the door connecting to the sluice is opened, the pressure is decreased to level it with the inside pressure. Once the door is open, the user moves in, the door is sealed again. Finally, the sluice pressure is set to match the outside pressure and the door leading may be safely opened.		The shaded rectagles denote a pressure level, high pressure area corresponds to a higher rectangle. The "u" label marks the current position of a system user. Initially, a user is inside and the sluice pressure is levelled with the outside pressure. Before the door connecting to the sluice is opened, the pressure is decreased to level it with the inside pressure. Once the door is open, the user moves in, the door is sealed again. Finally, the sluice pressure is set to match the outside pressure and the door leading may be safely opened.

imported>Alexili at 13:04, 22 October 2009

2009-10-22T13:04:23Z

← Older revision		Revision as of 13:04, 22 October 2009
Line 25:		Line 25:
	The following diagram shows the stages of the system operation that let a user to get outside starting in the inside area.		The following diagram shows the stages of the system operation that let a user to get outside starting in the inside area.

	[[Image:SluiceControllerSolution.png]]		[[Image:SluiceControllerSolution.png\|400px]]

	The shaded rectagles denote a pressure level, high pressure area corresponds to a higher rectangle. The "u" label marks the current position of a system user. Initially, a user is inside and the sluice pressure is levelled with the outside pressure. Before the door connecting to the sluice is opened, the pressure is decreased to level it with the inside pressure. Once the door is open, the user moves in, the door is sealed again. Finally, the sluice pressure is set to match the outside pressure and the door leading may be safely opened.		The shaded rectagles denote a pressure level, high pressure area corresponds to a higher rectangle. The "u" label marks the current position of a system user. Initially, a user is inside and the sluice pressure is levelled with the outside pressure. Before the door connecting to the sluice is opened, the pressure is decreased to level it with the inside pressure. Once the door is open, the user moves in, the door is sealed again. Finally, the sluice pressure is set to match the outside pressure and the door leading may be safely opened.

imported>Alexili at 13:04, 22 October 2009

2009-10-22T13:04:00Z

← Older revision		Revision as of 13:04, 22 October 2009
Line 1:		Line 1:
	==Modularisation Plug-in Tutorial==		==Modularisation Plug-in Tutorial==
			Go to the [[Modularisation Plug-in\|plug-in description page]].

	The tutorial illustrates the use of the modularisation plug-in in an Event-B development. The example used is rather small scale but it still demonstrates some basic principles of introducing modules during the development process.		The tutorial illustrates the use of the modularisation plug-in in an Event-B development. The example used is rather small scale but it still demonstrates some basic principles of introducing modules during the development process.
Line 9:		Line 10:
	The system parts are two doors that can be operated independently of each other and a pressure controller that allows the change of pressure in the sluice area. The following is a schematic depiction of the system.		The system parts are two doors that can be operated independently of each other and a pressure controller that allows the change of pressure in the sluice area. The following is a schematic depiction of the system.

	[[Image:SluiceController.png]]		[[Image:SluiceController.png\|300px]]

	The system is summarised with the following set of requirements:		The system is summarised with the following set of requirements:
Line 19:		Line 20:
	# at most one door is open at any moment;		# at most one door is open at any moment;
	# the pressure can only be switched on when the doors are closed.		# the pressure can only be switched on when the doors are closed.

			Requirements 1-4 characterise the system by stating its goal and its major parts. The last three characterise the system behaviour. More precisely, they are the safety properties of the system.

			The following diagram shows the stages of the system operation that let a user to get outside starting in the inside area.

			[[Image:SluiceControllerSolution.png]]

			The shaded rectagles denote a pressure level, high pressure area corresponds to a higher rectangle. The "u" label marks the current position of a system user. Initially, a user is inside and the sluice pressure is levelled with the outside pressure. Before the door connecting to the sluice is opened, the pressure is decreased to level it with the inside pressure. Once the door is open, the user moves in, the door is sealed again. Finally, the sluice pressure is set to match the outside pressure and the door leading may be safely opened.