Development of a flash-based filestore - Revision history

imported>WikiSysop: /* Applying Event and Machine Decomposition to a Flash-Based Filestore */

2010-11-18T13:06:27Z

Applying Event and Machine Decomposition to a Flash-Based Filestore

← Older revision		Revision as of 13:06, 18 November 2010
Line 14:		Line 14:
	We present a verified model of a tree-structured ﬁle system which was carried out using Event-B and the Rodin platform. The model is focused on basic functionalities aﬀecting the tree structure including create, copy, delete and move. This work is aimed at constructing a clear and accurate model with all proof obligations discharged. While constructing the model of a ﬁle system, we begin with an abstract model of a ﬁle system and subsequently reﬁne it by adding more details through reﬁnement steps. We have found that careful formulation of invariants and useful theorems that can be reused for discharging similar proof obligations make models simpler and easier to prove.		We present a verified model of a tree-structured ﬁle system which was carried out using Event-B and the Rodin platform. The model is focused on basic functionalities aﬀecting the tree structure including create, copy, delete and move. This work is aimed at constructing a clear and accurate model with all proof obligations discharged. While constructing the model of a ﬁle system, we begin with an abstract model of a ﬁle system and subsequently reﬁne it by adding more details through reﬁnement steps. We have found that careful formulation of invariants and useful theorems that can be reused for discharging similar proof obligations make models simpler and easier to prove.

	=== [http://deploy-eprints.ecs.soton.ac.uk/125/ Applying Event and Machine Decomposition to a Flash-Based Filestore~~] ===~~		=== Applying Event and Machine Decomposition to a Flash-Based Filestore] ===
	~~By ''Damchoom~~, ~~Kriangsak and Butler~~, ~~Michael~~.		By ''Damchoom, Kriangsak and Butler, Michael.<ref>[http://deploy-eprints.ecs.soton.ac.uk/125/ Damchoom, Kriangsak and Butler, Michael Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B. In: SBMF 2009, 19-21 August 2009, Gramado, Brazil.]</ref>
	~~in SBMF 2009~~

	=== An Incremental Refinement Approach to a Development of a Flash File System [http://deploy-eprints.ecs.soton.ac.uk/243/ archive] ===		=== An Incremental Refinement Approach to a Development of a Flash File System [http://deploy-eprints.ecs.soton.ac.uk/243/ archive] ===

imported>WikiSysop at 13:05, 18 November 2010

2010-11-18T13:05:03Z

← Older revision		Revision as of 13:05, 18 November 2010
Line 10:		Line 10:

	=== Modelling and proof of a Tree-structured File System===		=== Modelling and proof of a Tree-structured File System===
	By ''Damchoom, Kriangsak and Butler, Michael and Abrial, Jean-Raymond''.<ref>[http://deploy-eprints.ecs.soton.ac.uk/22/ Damchoom, Kriangsak and Butler, Michael and Abrial, Jean-Raymond (2008) Modelling and proof of a Tree-structured File System. In: ICFEM 2008.]<\ref>		By ''Damchoom, Kriangsak and Butler, Michael and Abrial, Jean-Raymond''.<ref>[http://deploy-eprints.ecs.soton.ac.uk/22/ Damchoom, Kriangsak and Butler, Michael and Abrial, Jean-Raymond (2008) Modelling and proof of a Tree-structured File System. In: ICFEM 2008.]</ref>

	We present a verified model of a tree-structured ﬁle system which was carried out using Event-B and the Rodin platform. The model is focused on basic functionalities aﬀecting the tree structure including create, copy, delete and move. This work is aimed at constructing a clear and accurate model with all proof obligations discharged. While constructing the model of a ﬁle system, we begin with an abstract model of a ﬁle system and subsequently reﬁne it by adding more details through reﬁnement steps. We have found that careful formulation of invariants and useful theorems that can be reused for discharging similar proof obligations make models simpler and easier to prove.		We present a verified model of a tree-structured ﬁle system which was carried out using Event-B and the Rodin platform. The model is focused on basic functionalities aﬀecting the tree structure including create, copy, delete and move. This work is aimed at constructing a clear and accurate model with all proof obligations discharged. While constructing the model of a ﬁle system, we begin with an abstract model of a ﬁle system and subsequently reﬁne it by adding more details through reﬁnement steps. We have found that careful formulation of invariants and useful theorems that can be reused for discharging similar proof obligations make models simpler and easier to prove.

imported>WikiSysop at 13:04, 18 November 2010

2010-11-18T13:04:28Z

← Older revision		Revision as of 13:04, 18 November 2010
Line 10:		Line 10:

	=== Modelling and proof of a Tree-structured File System===		=== Modelling and proof of a Tree-structured File System===
	By ''Damchoom, Kriangsak and Butler, Michael and Abrial, Jean-Raymond''.<ref> [http://deploy-eprints.ecs.soton.ac.uk/22/ Damchoom, Kriangsak and Butler, Michael and Abrial, Jean-Raymond (2008) Modelling and proof of a Tree-structured File System. In: ICFEM 2008.]<\ref>		By ''Damchoom, Kriangsak and Butler, Michael and Abrial, Jean-Raymond''.<ref>[http://deploy-eprints.ecs.soton.ac.uk/22/ Damchoom, Kriangsak and Butler, Michael and Abrial, Jean-Raymond (2008) Modelling and proof of a Tree-structured File System. In: ICFEM 2008.]<\ref>

	We present a verified model of a tree-structured ﬁle system which was carried out using Event-B and the Rodin platform. The model is focused on basic functionalities aﬀecting the tree structure including create, copy, delete and move. This work is aimed at constructing a clear and accurate model with all proof obligations discharged. While constructing the model of a ﬁle system, we begin with an abstract model of a ﬁle system and subsequently reﬁne it by adding more details through reﬁnement steps. We have found that careful formulation of invariants and useful theorems that can be reused for discharging similar proof obligations make models simpler and easier to prove.		We present a verified model of a tree-structured ﬁle system which was carried out using Event-B and the Rodin platform. The model is focused on basic functionalities aﬀecting the tree structure including create, copy, delete and move. This work is aimed at constructing a clear and accurate model with all proof obligations discharged. While constructing the model of a ﬁle system, we begin with an abstract model of a ﬁle system and subsequently reﬁne it by adding more details through reﬁnement steps. We have found that careful formulation of invariants and useful theorems that can be reused for discharging similar proof obligations make models simpler and easier to prove.

imported>WikiSysop: /* Modelling and proof of a Tree-structured File System */

2010-11-18T13:02:57Z

Modelling and proof of a Tree-structured File System

← Older revision		Revision as of 13:02, 18 November 2010
Line 9:		Line 9:
	Other papers and Rodin achives are available below.		Other papers and Rodin achives are available below.

	=== [http://deploy-eprints.ecs.soton.ac.uk/22/ ~~Modelling and proof of a Tree-structured File System] ===~~		=== Modelling and proof of a Tree-structured File System===
	~~By ''~~Damchoom, Kriangsak and Butler, Michael and Abrial, Jean-Raymond''.		By ''Damchoom, Kriangsak and Butler, Michael and Abrial, Jean-Raymond''.<ref> [http://deploy-eprints.ecs.soton.ac.uk/22/ Damchoom, Kriangsak and Butler, Michael and Abrial, Jean-Raymond (2008) Modelling and proof of a Tree-structured File System. In: ICFEM 2008.]<\ref>
	in ICFEM 2008

	We present a verified model of a tree-structured ﬁle system which was carried out using Event-B and the Rodin platform. The model is focused on basic functionalities aﬀecting the tree structure including create, copy, delete and move. This work is aimed at constructing a clear and accurate model with all proof obligations discharged. While constructing the model of a ﬁle system, we begin with an abstract model of a ﬁle system and subsequently reﬁne it by adding more details through reﬁnement steps. We have found that careful formulation of invariants and useful theorems that can be reused for discharging similar proof obligations make models simpler and easier to prove.		We present a verified model of a tree-structured ﬁle system which was carried out using Event-B and the Rodin platform. The model is focused on basic functionalities aﬀecting the tree structure including create, copy, delete and move. This work is aimed at constructing a clear and accurate model with all proof obligations discharged. While constructing the model of a ﬁle system, we begin with an abstract model of a ﬁle system and subsequently reﬁne it by adding more details through reﬁnement steps. We have found that careful formulation of invariants and useful theorems that can be reused for discharging similar proof obligations make models simpler and easier to prove.

	=== [http://deploy-eprints.ecs.soton.ac.uk/125/ Applying Event and Machine Decomposition to a Flash-Based Filestore] ===		=== [http://deploy-eprints.ecs.soton.ac.uk/125/ Applying Event and Machine Decomposition to a Flash-Based Filestore] ===

imported>WikiSysop at 13:01, 18 November 2010

2010-11-18T13:01:29Z

← Older revision		Revision as of 13:01, 18 November 2010
Line 2:		Line 2:


	===~~[http://eprints.ecs.soton.ac.uk/21655/~~ An Incremental Refinement Approach to a Development of a Flash-Based File System in Event-B] ===		===An Incremental Refinement Approach to a Development of a Flash-Based File System in Event-B===

	The work on the development of a flash-based file system in Event-B is reported in a PhD thesis by Kriangsak Damchoom<ref>[http://eprints.ecs.soton.ac.uk/21655/ Damchoom, K. (2010) An Incremental Refinement Approach to a Development of a Flash-Based File System in Event-B. PhD thesis, University of Southampton.]		The work on the development of a flash-based file system in Event-B is reported in a PhD thesis by Kriangsak Damchoom<ref>[http://eprints.ecs.soton.ac.uk/21655/ Damchoom, K. (2010) An Incremental Refinement Approach to a Development of a Flash-Based File System in Event-B. PhD thesis, University of Southampton.]
	</ref>.		</ref>.

	~~Papers~~ and Rodin achives are available below.		Other papers and Rodin achives are available below.

	=== [http://deploy-eprints.ecs.soton.ac.uk/22/ Modelling and proof of a Tree-structured File System] ===		=== [http://deploy-eprints.ecs.soton.ac.uk/22/ Modelling and proof of a Tree-structured File System] ===

imported>WikiSysop: /* Multi-Levelled Refinement and Evolution of a Flash File System Model in Event-B and Rodin archive */

2010-11-18T13:00:16Z

Multi-Levelled Refinement and Evolution of a Flash File System Model in Event-B and Rodin archive

← Older revision		Revision as of 13:00, 18 November 2010
Line 38:		Line 38:
	can be achieved? and how flexibility of the language and tool are?		can be achieved? and how flexibility of the language and tool are?

	</~~references~~>		==References==
			<references/>

imported>WikiSysop at 12:58, 18 November 2010

2010-11-18T12:58:43Z

← Older revision		Revision as of 12:58, 18 November 2010
Line 37:		Line 37:
	the requirements change. The point is how to deal with this. How much changes that impact the models? How reusability		the requirements change. The point is how to deal with this. How much changes that impact the models? How reusability
	can be achieved? and how flexibility of the language and tool are?		can be achieved? and how flexibility of the language and tool are?

			</references>

imported>WikiSysop: /* An Incremental Refinement Approach to a Development of a Flash-Based File System in Event-B */

2010-11-18T12:58:03Z

An Incremental Refinement Approach to a Development of a Flash-Based File System in Event-B

← Older revision		Revision as of 12:58, 18 November 2010
Line 4:		Line 4:
	===[http://eprints.ecs.soton.ac.uk/21655/ An Incremental Refinement Approach to a Development of a Flash-Based File System in Event-B] ===		===[http://eprints.ecs.soton.ac.uk/21655/ An Incremental Refinement Approach to a Development of a Flash-Based File System in Event-B] ===

	The work on the development of a flash-based file system in Event-B is reported in a PhD thesis by Kriangsak Damchoom.		The work on the development of a flash-based file system in Event-B is reported in a PhD thesis by Kriangsak Damchoom<ref>[http://eprints.ecs.soton.ac.uk/21655/ Damchoom, K. (2010) An Incremental Refinement Approach to a Development of a Flash-Based File System in Event-B. PhD thesis, University of Southampton.]
			</ref>.

	Papers and Rodin achives are available below.		Papers and Rodin achives are available below.

imported>WikiSysop at 20:48, 26 October 2010

2010-10-26T20:48:45Z

← Older revision		Revision as of 20:48, 26 October 2010
Line 1:		Line 1:
	Nowadays, many formal methods are used in the area of software development accompanied by a number of advanced theories and tools. However, more experiments are still required in order to provide significant evidence that will convince and encourage users to use, and gain more benefits from, those theories and tools. Event-B is a formalism used for specifying and reasoning about systems. Rodin is an open and extensible toolset for Event-B specification, refinement and proof. The flash file system is a complex system that is challenging to specify and verify at this moment in time. This system was chosen as a case study for our experiments, carried out using Event-B and the Rodin tool. The experiments were aimed at developing a rigorous model of flash-based file system, and providing useful evidence and guidelines to developers and the software industry. We believe that these would convince users and make formal methods more accessible.		Nowadays, many formal methods are used in the area of software development accompanied by a number of advanced theories and tools. However, more experiments are still required in order to provide significant evidence that will convince and encourage users to use, and gain more benefits from, those theories and tools. Event-B is a formalism used for specifying and reasoning about systems. Rodin is an open and extensible toolset for Event-B specification, refinement and proof. The flash file system is a complex system that is challenging to specify and verify at this moment in time. This system was chosen as a case study for our experiments, carried out using Event-B and the Rodin tool. The experiments were aimed at developing a rigorous model of flash-based file system, and providing useful evidence and guidelines to developers and the software industry. We believe that these would convince users and make formal methods more accessible.

	~~Our~~ work on the development of a flash-based file system are ~~listed~~ below
			===[http://eprints.ecs.soton.ac.uk/21655/ An Incremental Refinement Approach to a Development of a Flash-Based File System in Event-B] ===

			The work on the development of a flash-based file system in Event-B is reported in a PhD thesis by Kriangsak Damchoom.

			Papers and Rodin achives are available below.

	=== [http://deploy-eprints.ecs.soton.ac.uk/22/ Modelling and proof of a Tree-structured File System] ===		=== [http://deploy-eprints.ecs.soton.ac.uk/22/ Modelling and proof of a Tree-structured File System] ===

imported>Kriangsak: /* Multi-Levelled Refinement and Evolution of a Flash File System Model in Event-B and Rodin archive */

2010-08-25T14:24:20Z

Multi-Levelled Refinement and Evolution of a Flash File System Model in Event-B and Rodin archive

← Older revision		Revision as of 14:24, 25 August 2010
Line 28:		Line 28:
	By ''Damchoom, Kriangsak and Butler, Michael''.		By ''Damchoom, Kriangsak and Butler, Michael''.

	This work is an extension of the work presented above. The focus of this work is to outline an evolution of the model when the requirements change. Evolution of the models ~~are also~~ necessary when		This work is an extension of the work presented above. The focus of this work is to outline an evolution of the model when the requirements change. Evolution of the models is necessary when
	the requirements change. The point is how to deal with this. How much changes that impact the models? How reusability		the requirements change. The point is how to deal with this. How much changes that impact the models? How reusability
	can be achieved? and how flexibility of the language and tool are?		can be achieved? and how flexibility of the language and tool are?