% This file was created with JabRef 2.5.
% Encoding: Cp1252

@INPROCEEDINGS{Bicarregui2008,
  author = {Juan Bicarregui and Alvaro Arenas and Benjamin Aziz and Philippe
	Massonet and Christophe Ponsard},
  title = {Towards Modelling Obligations in Event-B},
  booktitle = {ABZ},
  year = {2008},
  pages = {181-194},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/asm/2008},
  ee = {http://dx.doi.org/10.1007/978-3-540-87603-8_15}
}

@INPROCEEDINGS{Cansell2007,
  author = {Dominique Cansell and Dominique Méry and Joris Rehm},
  title = {Time Constraint Patterns for Event B Development},
  booktitle = {B},
  year = {2007},
  pages = {140-154},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/b/2007},
  ee = {http://dx.doi.org/10.1007/11955757_13},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\Cansell_2007_Time_Constraint_Patterns_for_Event_B_Development.pdf:PDF}
}

@INPROCEEDINGS{Groslambert2007,
  author = {Julien Groslambert},
  title = {Verification of LTL on B Event Systems},
  booktitle = {B},
  year = {2007},
  pages = {109-124},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/b/2007},
  ee = {http://dx.doi.org/10.1007/11955757_11},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\Groslambert_2007_Verification_of_LTL_on_B_Event_Systems.pdf:PDF}
}

@INPROCEEDINGS{Jani2005,
  author = {Divya Jani and Damien Vanderveken and Dewayne E. Perry},
  title = {Deriving Architecture Specifications from KAOS Specifications: A
	Research Case Study},
  booktitle = {EWSA},
  year = {2005},
  pages = {185-202},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/ewsa/2005},
  ee = {http://dx.doi.org/10.1007/11494713_13},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\Divya-2005_Deriving_Architecture_Specifications_from_KAOS_Specifications_A_Research_Case_Study.pdf:PDF}
}

@INPROCEEDINGS{Lamsweerde2001,
  author = {Axel van Lamsweerde},
  title = {Goal-Oriented Requirements Engineering: A Guided Tour},
  booktitle = {RE},
  year = {2001},
  pages = {249},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/re/2001},
  ee = {http://computer.org/proceedings/re/1125/11250249abs.htm},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\01_AVL-RE01-GORE-guided-tour.pdf:PDF}
}

@INPROCEEDINGS{Ponsard2006,
  author = {Christophe Ponsard and Emmanuel Dieul},
  title = {From Requirements Models to Formal Specifications in B},
  booktitle = {ReMo2V},
  year = {2006},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/caise/2006remo2v},
  ee = {http://ceur-ws.org/Vol-241/paper10.pdf},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\Ponsard_remo2v.pdf:PDF}
}

@INPROCEEDINGS{Snook2007,
  author = {Colin Snook and Marina Waldén},
  title = {Refinement of Statemachines Using Event B Semantics},
  booktitle = {B},
  year = {2007},
  pages = {171-185},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/b/2007},
  ee = {http://dx.doi.org/10.1007/11955757_15},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\Snook_2007_Refinement_of_Statemachines_Using_Event_B_Semantics.pdf:PDF}
}

@BOOK{Abrial2009,
  title = {Modeling in Event-B: System and Software Engineering},
  publisher = {Cambridge University Press},
  year = {2009},
  author = {Jean-Raymond Abrial},
  file = {Ch 5 The Event-B Modeling Notation and Proof Obligations Rules:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\B-Book\\05-evtb.pdf:PDF;Ch1 Introdution:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\B-Book\\01-intro.pdf:PDF},
  timestamp = {2009.10.19}
}

@UNPUBLISHED{Abrial2009a,
  author = {Jean-Raymond Abrial},
  title = {Event Model Decomposition},
  note = {\url{http://deploy-eprints.ecs.soton.ac.uk/109/}},
  month = {June},
  year = {2009},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\Abrial_2009_Event_Model_Decomposition.pdf:PDF},
  timestamp = {2009.12.07}
}

@ARTICLE{Abrial2007,
  author = {J.-R. Abrial},
  title = {Formal Methods: Theory Becoming Practice},
  journal = {Journal of Universal Computer Science},
  year = {2007},
  volume = {13},
  pages = {619--628},
  number = {5},
  note = {\url|http://www.jucs.org/jucs_13_5/formal_methods_theory_becoming|},
  abstract = {This paper gives a tutorial introduction to the ideas behind system
	development usingthe B-Method. Properly handled, the crucial relationship
	between requirements and formal model leads to systems that are correct
	by construction. Some industrial successes are outlined.},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\jucs_13_5_0619_0628_abrial.pdf:PDF}
}

@BOOK{Abrial1996,
  title = {The B-book: assigning programs to meanings},
  publisher = {Cambridge Univ Press},
  year = {1996},
  author = {Jean-Raymond Abrial}
}

@INPROCEEDINGS{Aziz2009,
  author = {Benjamin Aziz and Alvaro Arenas and Juan Bicarregui and Christophe
	Ponsard and Philippe Massonet},
  title = {From Goal-Oriented Requirements to Event-B Specifications},
  booktitle = {First Nasa Formal Method Symposium},
  year = {2009},
  pages = {96--105},
  month = {April},
  abstract = {In goal-oriented requirements engineering methodologies, goals are
	structured into refinement trees from high-level system-wide goals
	down to fine-grained requirements assigned to specific software/
	hardware/human agents that can realise them. Functional goals assigned
	to software agents need to be operationalised into specification
	of services that the agent should provide to realise those requirements.
	In this paper, we propose an approach for operationalising requirements
	into specifications expressed in the Event-B formalism. Our approach
	has the benefit of aiding software designers by bridging the gap
	between declarative requirements and operational system specifications
	in a rigorous manner, enabling powerful correctness proofs and allowing
	further refinements down to the implementation level. Our solution
	is based on verifying that a consistent Event-B machine exhibits
	properties corresponding to requirements.},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\Aziz-nfm-reqs-eventb.pdf:PDF},
  url = {http://deploy-eprints.ecs.soton.ac.uk/91/}
}

@PHDTHESIS{Ball2008,
  author = {Elisabeth Ball},
  title = {An Incremental Process for the Development of Multi-agent Systems
	in Event-B},
  school = {University of Southampton},
  year = {2008},
  month = {August},
  note = {\url{http://eprints.ecs.soton.ac.uk/16575/}},
  abstract = {A multi-agent system is a group of software or hardware agents that
	cooperate or compete to achieve individual or shared goals. A method
	for developing a multi-agent system must be capable of modelling
	the concepts that are central to multi-agent systems. These concepts
	are identified in a review of Agent Oriented Software Engineering
	methodologies. The rigorous development of complex systems using
	formal methods can reduce the number of design faults. Event-B is
	a formal method for modelling and reasoning about reactive and distributed
	systems. There is currently no method that guides the developer specifically
	in the modelling of agent-based concepts in Event-B. The use of formal
	methods is seen by some developers as inaccessible. This thesis presents
	an Incremental Development Process for the development of multi-agent
	systems in Event-B. Development following the Incremental Development
	Process begins with the construction of informal models, based on
	agent concepts. The informal models relate system goals using a set
	of relationships. The developer is provided with guidance to construct
	formal Event-B models based on the informal design. The concepts
	that are central to multi-agent systems are captured in the Event-B
	models through the translation from the goal models. The Event-B
	models are refined and decomposed into specifications of roles that
	will be performed by the agents of the system. Two case studies illustrate
	how the Incremental Development Process can be applied to multi-agent
	systems. An additional aid to the developer presented in this thesis
	is a set of modelling patterns that provide fault-tolerance for Event-B
	models of interacting agents.},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\Ball_2008_An_Incremental_Process_for_the_Development_of_Multi-agent_Systems_in_Event-B.pdf:PDF},
  url = {http://eprints.ecs.soton.ac.uk/16575/}
}

@BOOK{Budinsky2003,
  title = {Eclipse modeling framework},
  publisher = {Pearson Education},
  year = {2003},
  editor = {Addison Wesley},
  author = {Frank Budinsky and David Steinberg and Ed Merks and Raymond Ellersick
	and Timothy J. Grose}
}

@ARTICLE{Butler2009,
  author = {Butler, M.},
  title = {Decomposition structures for Event-B},
  journal = {Integrated Formal Methods iFM2009, Springer, LNCS},
  year = {2009},
  volume = {5423},
  pages = {20-38},
  abstract = {Event-B provides a flexible approach to modelling and refinement of
	systems. In this paper we outline two important ways in which Event-B
	refinement can be augmented with additional structuring to support
	further the management of complex refinements. Firstly we show how
	event refinement diagrams can be used to structure refinement steps
	involving decomposition of atomicity. Secondly we outline a technique
	for decomposing models into sub-models to allow for independent refinement.
	We show how these two structuring techniques can be used together.},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\Butler-2009_Decomposition_Structures_for_Event-B.pdf:PDF},
  publisher = {Springer}
}

@MANUAL{CEDITI2003,
  title = {A KAOS Tutorial},
  author = {CEDITI},
  month = {September},
  year = {2003},
  note = {\url{http://www.cediti.be/}},
  file = {:D\:\\Documents\\FUNDP 2008-2009\\INFO M431 Ingénierie des exigences\\Lecture_obligatoire_2008_2009\\07-KAOS-literature\\Kaos_tutorial.pdf:PDF},
  timestamp = {2009.10.19}
}

@BOOK{Chung2000,
  title = {Non-Functional Requirements in Software Engineering},
  publisher = {Kluwer Academic Publishers},
  year = {2000},
  author = {Lawrence Chung and Brian A. Nixon and Eric Yu and John Mylopoulos},
  timestamp = {2009.11.10}
}

@CONFERENCE{Fisher1992,
  author = {Fisher, M.},
  title = {A normal form for first-order temporal formulae},
  booktitle = {Proceedings of Eleventh International Conference on Automated Deduction
	(CADE)},
  year = {1992},
  pages = {370--384},
  organization = {Springer},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\A_NF_for_FOTF.pdf:PDF}
}

@MISC{Gervais2009,
  author = {Frédéric Gervais and Christophe Gnaho and Régine Laleau and Abderrahman
	Matoussi and Farida Semmak},
  title = {TACOS Livrable L1.2 : KAOS extension with non-functional properties},
  howpublished = {\url{http://tacos.loria.fr/drupal/?q=node/74}},
  month = {January},
  year = {2009},
  note = {Projet TACOS : Trustworthy Assembling of Components:
	
	frOm requirements to Specification
	
	ANR-06-SETI-017
	
	Janvier 2007 - D´ecembre 2009},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\L+n54XYN.pdf.part.pdf:PDF},
  timestamp = {2009.11.09}
}

@BOOK{Holt2001,
  title = {UML for systems engineering},
  publisher = {Institution of Electrical Engineers},
  year = {2001},
  editor = {IEE},
  author = {Jon Holt},
  timestamp = {2009.11.24}
}

@ARTICLE{Jouault2008,
  author = {Jouault, F. and Allilaire, F. and Bézivin, J. and Kurtev, I.},
  title = {ATL: A model transformation tool},
  journal = {Science of Computer Programming},
  year = {2008},
  volume = {72},
  pages = {31--39},
  number = {1-2},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\Bezivin____ATL-_A_model_transformation_tool.pdf:PDF},
  publisher = {Elsevier}
}

@BOOK{Lamsweerde2009,
  title = {Requirements Engineering: From System Goals to UML Models to Software
	Specifications},
  publisher = {Wiley},
  year = {2009},
  author = {van Lamsweerde, Axel},
  month = {March},
  abstract = {The book presents both the current state of the art in requirements
	engineering and a systematic method for engineering high-quality
	requirements, broken down into four parts. The \_first part\_ introduces
	fundamental concepts and principles including the aim and scope of
	requirements engineering, the products and processes involved, requirements
	qualities to aim at and flaws to avoid, and the critical role of
	requirements engineering in system and software engineering.
	
	The \_second part\_ of the book is devoted to system modeling in the
	specific context of engineering requirements. It presents a multi-view
	modeling framework that integrates complementary techniques for modeling
	the system-as- is and the system-to-be. The \_third part\_ of the
	book reviews goal-based reasoning techniques to support the various
	steps of the KAOS method. The \_fourth part\_ of the book goes beyond
	requirements engineering to discuss the mapping from goal-oriented
	requirements to software specifications and to software architecture.
	
	Online resources will accompany the book and will add value to both
	classroom and self-study by enabling students to build models and
	specifications involved in the book's exercises and case studies,
	helping them to discover the latest RE technology solutions. Instructor
	resources such as slides, solutions, models and animations will be
	available from an accompanying website.},
  citeulike-article-id = {3487562},
  citeulike-linkout-0 = {http://www.amazon.ca/exec/obidos/redirect?tag=citeulike09-20\&amp;path=ASIN/0470012706},
  citeulike-linkout-1 = {http://www.amazon.de/exec/obidos/redirect?tag=citeulike01-21\&amp;path=ASIN/0470012706},
  citeulike-linkout-2 = {http://www.amazon.fr/exec/obidos/redirect?tag=citeulike06-21\&amp;path=ASIN/0470012706},
  citeulike-linkout-3 = {http://www.amazon.jp/exec/obidos/ASIN/0470012706},
  citeulike-linkout-4 = {http://www.amazon.co.uk/exec/obidos/ASIN/0470012706/citeulike00-21},
  citeulike-linkout-5 = {http://www.amazon.com/exec/obidos/redirect?tag=citeulike07-20\&path=ASIN/0470012706},
  citeulike-linkout-6 = {http://www.worldcat.org/isbn/0470012706},
  citeulike-linkout-7 = {http://books.google.com/books?vid=ISBN0470012706},
  citeulike-linkout-8 = {http://www.amazon.com/gp/search?keywords=0470012706\&index=books\&linkCode=qs},
  citeulike-linkout-9 = {http://www.librarything.com/isbn/0470012706},
  file = {:D\:\\Livres\\RE_From_System_Goal_to_UML_Models_to_Software_Specification_Axel_van_LAMSWEERDE.pdf:PDF},
  howpublished = {Paperback},
  isbn = {0470012706},
  keywords = {rqe},
  posted-at = {2009-10-14 09:32:26},
  priority = {5},
  url = {http://www.amazon.com/exec/obidos/redirect?tag=citeulike07-20\&path=ASIN/0470012706}
}

@CONFERENCE{Lamsweerde2000,
  author = {van Lamsweerde, Axel},
  title = {Formal specification: a roadmap},
  booktitle = {Proceedings of the conference on The future of Software engineering},
  year = {2000},
  pages = {147--159},
  organization = {ACM New York, NY, USA},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\FormalSpec-avl.pdf:PDF}
}

@MISC{Landtsheer2007,
  author = {Renaud De Landtsheer},
  title = {Deriving Event-based Security Policy from Declarative Security Requirements},
  month = {October},
  year = {2007},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\LTL2PolPa.pdf:PDF},
  timestamp = {2009.11.16}
}

@PHDTHESIS{Landtsheer2007a,
  author = {Renaud De Landtsheer},
  title = {Elaborating Complete and Consistent Requirements for Security-Critical
	Systems},
  school = {Université Catholique de Louvain},
  year = {2007},
  note = {\url{http://www.info.ucl.ac.be/~rdl/thesis/}},
  abstract = {The elaboration of requirements is a crucial step in the development
	of software-intensive security-critical application. From this stage
	on, the security engineering process heads towards the implementation
	of the identified security requirements. A missing, inadequate, imprecise
	or inconsistent requirement might cause the resulting application
	to have vulnerabilities, despite the huge amount of work that might
	be invested in implementing the elaborated security requirements.
	
	Vulnerabilities in requirements models notably arise from incompleteness
	and inconsistency. Incompleteness refers to missing requirements;
	inconsistency refers to requirements prescribing incompatible behaviors.
	Inconsistent requirements might give rise to vulnerabilities because
	they cannot be enforced altogether: one of them will be violated
	at run time.
	
	This thesis proposes three techniques for assisting engineers in the
	elaboration of complete and consistent requirements through model-based
	analysis. The two first focus on completeness issues, the last one
	on consistency. The three techniques build on a specific model-based
	framework for goal-oriented requirements analysis. They are demonstrated
	through models of an e-purse system and an e-signature system.
	
	The first technique is a formal framework for specifying and analyzing
	confidentiality concerns. Our framework makes it possible to discover
	confidentiality violations at requirements engineering time through
	model checking.
	
	The second technique focuses on the responsibility assignment of security
	requirements. Some agents in the software or in its environment might
	be malicious or too vulnerable. One should not rely on them in the
	enforcement of security goals. This technique introduces a security-specific
	completeness criterion ensuring that the enforcement of security
	goals only depends on the behavior of agents that are known to be
	trustworthy or built to be trustworthy. A systematic process is proposed
	for elaborating requirements models complying with this criterion.
	
	The third technique makes it possible to automatically detect goal-level
	inconsistencies called divergences. Divergences between goals lead
	to inconsistencies between requirements, and to potential vulnerabilities
	in the running system.},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\DeLandtsheer_2007_Elaborating_Complete_and_Consistent_Requirements_for_Security-Critical_Systems.pdf:PDF},
  timestamp = {2009.12.09}
}

@ARTICLE{Landtsheer2004,
  author = {Renaud De Landtsheer and Emmanuel Letier and Axel van Lamsweerde},
  title = {Deriving tabular event-based specifications from goal-oriented requirements
	models},
  journal = {Requir. Eng.},
  year = {2004},
  volume = {9},
  pages = {104-120},
  number = {2},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://dx.doi.org/10.1007/s00766-004-0189-1},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\Landtsheer-2004_Deriving_tabular_event-based_specifications_from_goal-oriented_requirements models.pdf:PDF}
}

@UNPUBLISHED{Delandtsheer2009,
  author = {Renaud De Landtsheer and Christophe Ponsard},
  title = {Goal-Oriented Requirements Engineering in Action in the Transportation
	Sector},
  note = {\url{http://deploy-eprints.ecs.soton.ac.uk/151/}},
  month = {September},
  year = {2009},
  abstract = {This report presents the goal-oriented approach to engineer high-quality
	requirements. Starting from informally structured textual requirements,
	this report illustrates some of the benefits of using a goal-oriented
	approach in terms of guarantee of completeness, consistency, reasoning
	on the system boundaries, identifying the responsibilities and dealing
	with potential conflicts. This report is mainly on semi-formal notations
	but it also shortly considers the formalization process. It is consistently
	illustrated on the first simplified pilot problem developed by the
	transportation sector during the DEPLOY project and known as "mini-pilot".},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\DEPLOY-GORE-in-action.pdf:PDF},
  publisher = {DEPLOY},
  type = {Technical Report},
  url = {http://deploy-eprints.ecs.soton.ac.uk/151/}
}

@TECHREPORT{Lapouchnian2005,
  author = {Alexei Lapouchnian},
  title = {Goal-Oriented Requirements Engineering: An Overview of the Current
	Research},
  institution = {University of Toronto},
  year = {2005},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\Lapouchnian-Depth_lapouchnianGORE.pdf:PDF}
}

@PHDTHESIS{Letier2001,
  author = {Emmanuel Letier},
  title = {Reasoning about Agents in Goal-Oriented Requirements Engineering},
  school = {Université Catholique de Louvain},
  year = {2001},
  month = {May},
  abstract = {The thesis proposes a number of techniques for elaborating requirements
	constructively from high-level goals. The techniques are based on
	the KAOS goal-oriented method for requirements engineering. This
	method consists in identifying goals and refining them into subgoals
	until the latter can be assigned as responsibilities of single agents
	such as humans, devices and software. Domain properties and assumptions
	about the software environment are also used during the goal refinement
	process. The method supports the exploration of alternative goal
	refinements and alternative responsibility assignments of goals to
	agents. It also supports the identification and resolution of conflicts
	between goals, and the identification and resolution of exceptional
	agent behaviors, called obstacles, that violate goals and assumptions
	produced during the goal refinement process.
	
	
	The thesis enriches the KAOS framework through three kinds of techniques:
	
	
	(a) techniques for identifying agents, goal refinements, and alternative
	responsibility assignments, and for deriving agent interfaces from
	such responsibility assignments;
	
	
	(b) techniques for deriving operational requirements from goal specifications;
	
	
	(c) techniques for generating obstacles to the satisfaction of idealized
	goals and assumptions, and for generating alternative obstacle resolutions.
	
	
	The result is a coherent body of systematic techniques for requirements
	elaboration that are both theoretically well-founded (a formal model
	of agent is defined) and effective in practice (the techniques are
	validated on two real case studies of significant size: the London
	ambulance despatching system, and the Bay Area Rapid Transit train
	system).},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\letier_thesis.pdf:PDF;:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\letierSection3.pdf:PDF},
  url = {http://www.info.ucl.ac.be/~eletier/thesis.html}
}

@ARTICLE{Letier2008,
  author = {Emmanuel Letier and Jeff Kramer and Jeff Magee and Sebasti{\'a}n
	Uchitel},
  title = {Deriving event-based transition systems from goal-oriented requirements
	models},
  journal = {Autom. Softw. Eng.},
  year = {2008},
  volume = {15},
  pages = {175-206},
  number = {2},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://dx.doi.org/10.1007/s10515-008-0027-7},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\letierSection3.pdf:PDF}
}

@PHDTHESIS{Mansour2009,
  author = {Riham Hassan Abdel-Moneim Mansour},
  title = {Formal Analysis and Design for Engineering Security (FADES)},
  school = {Virginia Polytechnic Institute and State University},
  year = {2009},
  address = {Blacksburg, Virginia},
  month = {March},
  note = {\url{http://scholar.lib.vt.edu/theses/available/etd-03232009-182707/}},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\These FADES.pdf:PDF},
  keywords = {Security Engineering, Software Engineering, Goal-Oriented Requirements,
	Analysis, Formal Analysis and Design, Security, Formal methods},
  timestamp = {2009.11.06},
  url = {http://scholar.lib.vt.edu/theses/available/etd-03232009-182707/}
}

@CONFERENCE{Mashkoor2009,
  author = {Atif Mashkoor},
  title = {Formal Domain Modeling: From Specification to Validation},
  booktitle = {Proceedings of Formal Methods 2009 Doctoral Symposium},
  year = {2009},
  pages = {53},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\main_2.pdf:PDF},
  timestamp = {2009.11.16}
}

@UNPUBLISHED{Mashkoor2010,
  author = {Atif Mashkoor and Abderrahman Matoussi},
  title = {Towards validation of requirements models},
  note = {In 2nd International Conference on Abstract State Machines (ASM),
	Alloy, B and Z (ABZ'10), Orford, Québec, Canada},
  month = {February},
  year = {2010},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\main.pdf:PDF},
  timestamp = {2009.11.16}
}

@UNPUBLISHED{Matoussi2009a,
  author = {Abderrahman Matoussi},
  title = {Expressing KAOS Goal Models with Event-B},
  note = {LACL, Université Paris-Est},
  year = {2009},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\Fm09-Doctoral-Paper.pdf:PDF},
  timestamp = {2009.10.28}
}

@CONFERENCE{Matoussi2008,
  author = {Abderrahman Matoussi and Frédéric Gervais and Régine Laleau},
  title = {A First Attempt to Express KAOS Refinement Patterns with Event B},
  booktitle = {Proc. of the Int. Conf. on ASM, B and Z (ABZ). Lecture Notes in Computer
	Science, Springer-Verlag},
  year = {2008},
  pages = {12--14},
  organization = {Springer},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\Matoussi_2008_A_First_Attempt_to_Express_KAOS_Refinement_Patterns_with_Event B.pdf:PDF}
}

@TECHREPORT{Matoussi2009,
  author = {Abderrahman Matoussi and Regine Laleau and Dorian Petit},
  title = {Bridging the gap between KAOS requirements models and B specifications},
  institution = {LACL (Laboratory of Algorithms, Complexity and Logic), University
	of Paris-Est (Paris 12)},
  year = {2009},
  number = {TR-LACL-2009-5},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\Matoussi_TR-LACL-2009-5.pdf:PDF},
  pdf = {http://lacl.univ-paris12.fr/Rapports/TR/TR-LACL-2009-5.pdf}
}

@MISC{Metayer2005,
  author = {Christophe Métayer and Jean-Raymond Abrial and Laurent Voisin},
  title = {RODIN deliverable 3.2: Event-B language},
  howpublished = {\url{http://rodin.cs.ncl.ac.uk/deliverables/D7.pdf}},
  month = {may},
  year = {2005},
  note = {\url{http://rodin-b-sharp.sourceforge.net}},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\Metayer-2005_RODIN_Deliverable_3-2.pdf:PDF;:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\kernel_lang.pdf:PDF},
  timestamp = {2009.10.19}
}

@TECHREPORT{OMG2009,
  author = {OMG},
  title = {OMG Unified Modeling Language (OMG UML), Infrastructure, V2.2},
  institution = {Object Management Group},
  year = {2009},
  month = {February},
  note = {v 2.2},
  citeulike-article-id = {2638391},
  citeulike-linkout-0 = {http://www.omg.org/spec/UML/2.1.2/Infrastructure/PDF},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\09-02-04.pdf:PDF},
  keywords = {tech, uml},
  posted-at = {2008-04-07 19:04:51},
  priority = {2},
  timestamp = {2009.10.29},
  url = {http://www.omg.org/spec/UML/2.2/Infrastructure}
}

@TECHREPORT{OMG2009a,
  author = {OMG},
  title = {OMG Unified Modeling Language (OMG UML), Superstructure, V2.2},
  institution = {Object Management Group},
  year = {2009},
  month = {February},
  note = {v 2.2},
  citeulike-article-id = {2638391},
  citeulike-linkout-0 = {http://www.omg.org/spec/UML/2.1.2/Infrastructure/PDF},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\09-02-02.pdf:PDF},
  keywords = {tech, uml},
  posted-at = {2008-04-07 19:04:51},
  priority = {2},
  url = {http://www.omg.org/spec/UML/2.2/Infrastructure}
}

@TECHREPORT{OMG2007,
  author = {OMG},
  title = {Meta Object Facility (MOF) 2.0 Query/View/Transformation Specification},
  institution = {Object Management Group},
  year = {2007},
  month = {July},
  note = {v 1.0},
  citeulike-article-id = {2638415},
  citeulike-linkout-0 = {http://www.omg.org/spec/UML/2.1.2/Superstructure/PDF},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\QVT_Spec_OMG.pdf:PDF},
  keywords = {tech, qvt},
  posted-at = {2008-04-07 19:10:32},
  priority = {2},
  url = {http://www.omg.org/spec/UML/2.1.2/Superstructure/PDF}
}

@TECHREPORT{OMG2006,
  author = {OMG},
  title = {Diagram Interchange},
  institution = {Object Management Group},
  year = {2006},
  month = {April},
  note = {v 1.0},
  citeulike-article-id = {2638415},
  citeulike-linkout-0 = {http://www.omg.org/spec/UML/2.1.2/Superstructure/PDF},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\UMLDI_Spec_OMG.pdf:PDF},
  keywords = {tech, UMLDI},
  posted-at = {2008-04-07 19:10:32},
  priority = {2},
  timestamp = {2009.10.29},
  url = {http://www.omg.org/spec/UML/2.1.2/Superstructure/PDF}
}

@MANUAL{Paulin2001,
  title = {Génie logiciel: Introduction à la méthode B},
  author = {Christine Paulin},
  month = {may},
  year = {2001},
  note = {Maitrise 2001-2002},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\Paulin-2001_Maîtrise_Cours_de_Genie_Logiciel_2_ Atelier_B-LRI.ps:PostScript},
  timestamp = {2009.10.19},
  url = {http://www.lri.fr/~paulin/B/poly.ps.gz}
}

@MANUAL{Respect-IT,
  title = {Objectiver Metamodel},
  author = {Respect-IT},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\Meta-Model.pdf:PDF},
  timestamp = {2009.10.20}
}

@MANUAL{Respect-ITa,
  title = {Objectiver Query Langage},
  author = {Respect-IT},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\ObjectiverQueryLanguage.pdf:PDF},
  timestamp = {2009.10.20}
}

@MISC{Respect-ITv2.1,
  author = {Respect-IT},
  title = {Objectiver Metamodel},
  howpublished = {\url{http://www.objectiver.com/}},
  year = {v2.1},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\Metamodel Objectiver\\index.html:URL}
}

@MISC{Respect-ITv3.0.0,
  author = {Respect-IT},
  title = {Objectiver},
  howpublished = {\url{http://www.objectiver.com/}},
  year = {v 3.0.0},
  timestamp = {2009.11.30}
}

@MISC{REVERv9.0.1,
  author = {REVER},
  title = {DB-Main},
  howpublished = {\url{http://www.db-main.be}},
  year = {v 9.0.1},
  timestamp = {2009.12.04}
}

@MISC{RODINv1.1,
  author = {RODIN},
  title = {RODIN Platform},
  howpublished = {\url{http://www.event-b.org/}},
  year = {v 1.1},
  timestamp = {2009.12.07}
}

@MANUAL{RODIN2007,
  title = {User Manual of the RODIN Platform},
  author = {RODIN},
  month = {October},
  year = {2007},
  note = {Version 2.3},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\RODIN_User_manual-2.3.pdf:PDF},
  timestamp = {2009.10.19}
}

@INPROCEEDINGS{Said2009a,
  author = {Mar yah Said and Michael Butler and Colin Snook},
  title = {Language and Tool Support for Class and State Machine Refinement
	in UML-B},
  booktitle = {FM2009 - 16th International Symposium on Formal Methods},
  year = {2009},
  number = {LNCS 5},
  pages = {579--595},
  month = {November},
  publisher = {Springer},
  abstract = {UML-B is a ?UML-like? graphical front end for Event-B that provides
	support for object-oriented modelling concepts. In particular, UML-B
	supports class diagrams and state machines, concepts that are not
	explicitly supported in plain Event-B. In Event-B, refinement is
	used to relate system models at different abstraction levels. The
	same abstraction-refinement concepts can also be applied in UML-B.
	This paper introduces the notions of refined classes and refined
	state machines to enable refinement of classes and state machines
	in UML-B. Together with these notions, a technique for moving an
	event between classes to facilitate abstraction is also introduced.
	Our work makes explicit the structures of class and state machine
	refinement in UML-B. The UML-B drawing tool and Event-B translator
	are extended to support the new refinement concepts. A case study
	of an auto teller machine (ATM) is presented to demonstrate application
	and effectiveness of refined classes and refined state machines.},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\Sais_2009_Language_and_Tool_Support_for_Class_and_State_Machine_Refinement_in_UML-B.pdf:PDF},
  keywords = {UML-B, Event-B, Rodin, Refinement, },
  url = {http://eprints.ecs.soton.ac.uk/18268/}
}

@UNPUBLISHED{Said2009,
  author = {Mar Yah Said and Michael Butler and Colin Snook},
  title = {Class and State Machine Refnement in UML-B},
  note = {\url{http://eprints.ecs.soton.ac.uk/17133/}},
  month = {February},
  year = {2009},
  booktitle = {Integration of Model-based Formal Methods and Tools (workshop at
	iFM 2009)},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\IM_FMT2009_Paper23_MarYah.pdf:PDF},
  url = {http://eprints.ecs.soton.ac.uk/17133/}
}

@BOOK{Schneider2001,
  title = {The B-method: an introduction},
  publisher = {Palgrave Macmillan, Basingstoke},
  year = {2001},
  author = {Steve Schneider}
}

@INPROCEEDINGS{Snook2008,
  author = {Colin Snook and Michael Butler},
  title = {UML-B and Event-B: an integration of languages and tools},
  booktitle = {The IASTED International Conference on Software Engineering - SE2008},
  year = {2008},
  month = {February},
  abstract = {UML-B is a graphical front end for Event-B. It adds support for class-oriented
	modelling but retains the Event-B concept of a closed system characterized
	by families of spontaneous events. UML-B is similar to UML but is
	essentially a new notation based on a separate meta-model. We provide
	tool support for UML-B, including drawing tools and a translator
	to generate Event-B models. The tools are closely integrated with
	the Event-B verification tools so that when a drawing is saved the
	translator automatically generates the corresponding Event-B model.
	The Event-B verification tools (syntax checker and prover) then run
	automatically providing an immediate display of problems. We introduce
	the UML-B notation its tool support and its integration with Event-B.},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\SnBu08.pdf:PDF},
  keywords = {Visual modelling languages, Formal, UML, Event-B},
  url = {http://eprints.ecs.soton.ac.uk/14926/}
}

@ARTICLE{Snook2006,
  author = {Snook, Colin and Butler, Michael},
  title = {UML-B: Formal modeling and design aided by UML},
  journal = {ACM Trans. Softw. Eng. Methodol.},
  year = {2006},
  volume = {15},
  pages = {92--122},
  number = {1},
  month = {January},
  address = {New York, NY, USA},
  citeulike-article-id = {784999},
  citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1125811},
  citeulike-linkout-1 = {http://dx.doi.org/10.1145/1125808.1125811},
  citeulike-linkout-2 = {http://dx.doi.org/http://dx.doi.org/10.1145/1125808.1125811},
  citeulike-linkout-3 = {http://dx.doi.org/10.1145/1125808.1125811},
  doi = {10.1145/1125808.1125811},
  file = {:D\:\\Documents\\FUNDP 2009-2010\\Stage\\Documentation\\snook06_UMLBeprint.pdf:PDF},
  keywords = {2006, b, uml},
  posted-at = {2006-08-03 20:38:38},
  priority = {2},
  publisher = {ACM Press},
  url = {http://dx.doi.org/10.1145/1125808.1125811}
}

