http://deploy.rkbexplorer.com/id/person-48157555e1676ac84f2922b9550bb50e-1877e60711d1072ffc125775995a8f18
family-name: Hallerstede
given-name: Stefan
full-name: Stefan Hallerstede
type: Person
type: Thing

eprints-156
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/156
has-title: Different Perspectives for Reasoning about Problems and Faults
has-url: http://deploy-eprints.ecs.soton.ac.uk/156/3/indexcodes.txt
has-url: http://deploy-eprints.ecs.soton.ac.uk/156/1/1151.pdf
type: Thing
type: Book-Reference

http://deploy.rkbexplorer.com/id/person-39e3145e96242ffbddcf0963bfce011d-d20afebb7c6b736f4c767bbc606997e6
family-name: Roth
given-name: A
full-name: A Roth
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-5ddfc06fd249424777b16a0fe71d1b48-976b96d2e90341673023c1022b6da59b
family-name: Ilic
given-name: Dubravka
full-name: Dubravka Ilic
type: Person
type: Thing

eprints-162
has-title: Patterns for Modelling Time and Consistency in Business Information Systems
type: Thing
has-url: http://deploy-eprints.ecs.soton.ac.uk/162/3/indexcodes.txt
has-abstract: Maintaining semantic consistency of data is a significant problem in distributed information systems, particularly those on which a business may depend. Our current work aims to use Event-B and the Rodin tools to support the specification and design of such systems in a way that integrates well into existing development processes. This paper presents Event-B patterns that may be used to represent recovery from timebounded inconsistency and illustrates their use in a model derived from industrial applications.
type: Publication-Reference
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/162
has-url: http://deploy-eprints.ecs.soton.ac.uk/162/1/iceccs%2Dfinal.pdf

eprints-134
has-url: http://deploy-eprints.ecs.soton.ac.uk/134/1/modesFM.pdf
type: Publication-Reference
has-url: http://deploy-eprints.ecs.soton.ac.uk/134/3/indexcodes.txt
has-abstract: Several safety-critical systems, such as avionic, transportation and space systems, use the notion of operation modes. Operation modes are useful structuring units that facilitate design, specially if used with state-based formal methods. However, modelling abstractions to support the specification, analysis and correct construction of modal systems are still lacking. The contribution of this paper is twofold: (i) modal systems and modal systems refinement are discussed and formalized; (ii) the relation of a modal system specification with an Event-B model is discussed, showing how to demonstrate that the behaviour of an Event-B model can satisfy a modal system.
type: Thing
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/134
has-title: Specifying Modal Systems using Event-B

http://deploy.rkbexplorer.com/id/person-0c236de338b4a8c19eb9b62f759fc75d-406ae0ea539f521602364e13345eb695
family-name: Daniel
given-name: Plagge
full-name: Plagge Daniel
type: Person
type: Thing

Publication export from Deploy
creator: ReSIST Project
description: This ontology contains information detailing publications held by Deploy
type: Thing
type: Ontology
imports: extension
imports: portal

http://deploy.rkbexplorer.com/id/person-cd2e9de277cbfd09b0bcf117f27d25ec-ba3c5866e89f0a392ce916877c8211be
family-name: Falampin
given-name: Jerome
full-name: Jerome Falampin
type: Person
type: Thing

http://lodlaundromat.org/.well-known/genid/27f1b9e18615e2d4306c1fdaa8ba64f8#2
has-title: DEPLOY Planery Meeting
type: Conference-Proceedings-Reference
type: Thing

http://deploy.rkbexplorer.com/id/person-998a5bbede82dfe9b971b24b65eecedf-976b96d2e90341673023c1022b6da59b
family-name: Varpaaniemi
given-name: Kimmo
full-name: Kimmo Varpaaniemi
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-ff82fc0b986befe1341ed098470d9883-1877e60711d1072ffc125775995a8f18
family-name: Butler
given-name: Michael
full-name: Michael Butler
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-30a798339149776498830688a6cb68b1-1877e60711d1072ffc125775995a8f18
family-name: Abrial
given-name: Jean-Raymond
full-name: Jean-Raymond Abrial
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-fbca151a6d9032482e2c898d6e62f573-72390008397cd47c8de541a3ccfb9beb
family-name: Damchoom
given-name: Kriangsak
full-name: Kriangsak Damchoom
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-4b91512d970d86a1f3707335a04be0a9-42c34226e0b90947e96c48ab8fb7c5c3
family-name: Iliasov
given-name: Alexei
full-name: Alexei Iliasov
type: Person
type: Thing

eprints-159
has-title: Supporting Reuse in Event B Development: Modularisation Approach
has-url: http://deploy-eprints.ecs.soton.ac.uk/159/1/Modules_paper%2Dfm.pdf
has-abstract: Recently, Space Systems Finland has undertaken formal Event B development of a part of on-board software for the BepiColombo space mission. As a result, lack of modularization mechanisms in Event B has been identified as a serious obstacle to scalability. One of the main benefit of modularization is that it allows us to decompose system models into components that can be independently developed. It also helps to manage complexity of models that in the industrial setting are usually very large and difficult to comprehend. On the other hand, modularization enables reuse of formally developed components in the formal product line development. In this paper we propose a conservative extension of Event B formalism to support modularization. We demonstrate how our approach can support reuse in the formal development in the space domain.
has-url: http://deploy-eprints.ecs.soton.ac.uk/159/3/indexcodes.txt
type: Publication-Reference
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/159
type: Thing

http://deploy.rkbexplorer.com/id/journal-736f63e305e5d7f4e6c533e04e7a7973
has-title: EWDC 2009
type: Publication-Reference
type: Journal
type: Thing

http://lodlaundromat.org/.well-known/genid/27f1b9e18615e2d4306c1fdaa8ba64f8#1
has-title: SBMF 2009
type: Conference-Proceedings-Reference
type: Thing

http://deploy.rkbexplorer.com/id/person-d0b267429a3f5057f3e5be3e68476f8f-d20afebb7c6b736f4c767bbc606997e6
family-name: Romanovsky
given-name: Alexander
full-name: Alexander Romanovsky
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-ff82fc0b986befe1341ed098470d9883-72390008397cd47c8de541a3ccfb9beb
family-name: Butler
given-name: Michael
full-name: Michael Butler
type: Person
type: Thing

eprints-125
has-url: http://deploy-eprints.ecs.soton.ac.uk/125/1/FlashFileSysPrj.zip
type: Thing
has-url: http://deploy-eprints.ecs.soton.ac.uk/125/3/FileSysSBMF2009.pdf
has-title: Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/27f1b9e18615e2d4306c1fdaa8ba64f8#1
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/125
type: Proceedings-Paper-Reference
has-url: http://deploy-eprints.ecs.soton.ac.uk/125/5/indexcodes.txt
has-abstract: Event-B is a formal method used for specifying and reasoning about systems. Rodin is a toolset for developing system models in Event-B. Our experiment which is outlined in this paper is aimed at applying Event-B and Rodin to a flash-based filestore. Refinement is a useful mechanism that allows developers to sharpen models step by step. Two uses of refinement, feature augmentation and structural refinement, were employed in our development. Event decomposition and machine decomposition are techniques on which we focus in this work. We present an outline of a verified refinement chain for the flash filestore. We also outline evidence of the applicability of the method and tool together with some guidelines.

http://deploy.rkbexplorer.com/id/person-d86ab6efc60ec381a24e6096e0c83284-406ae0ea539f521602364e13345eb695
family-name: Falampin
given-name: Jérôme
full-name: Jérôme Falampin
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/journal-fde68c7acd66a05ec80a53c900b8a41f
has-title: WSFM 2009
type: Publication-Reference
type: Journal
type: Thing

http://deploy.rkbexplorer.com/id/publishing-house-83bc84336b38939e1ecc84e982e2f582
has-title: University of Newcastle upon Tyne
type: Publishing-House
type: Thing

www.aktors.org
title: Turning Shoe Information to Knowledge of Technology and Deals
site name: Aktors
locale: en_US
description: Take a look at Nike and Adidas Shoe technology, and use Finish Line coupons to save money on athletic shoes and performance apparel
type: website
type: Thing

eprints-158
type: Article-Reference
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/158
has-url: http://deploy-eprints.ecs.soton.ac.uk/158/3/indexcodes.txt
has-abstract: While current studies on Web services composition are mostly focused - from the technical viewpoint - on standards and protocols, this work investigates the adoption of formal methods for dependable composition. The Web Services Business Process Execution Language (WS-BPEL) - an OASIS standard widely adopted both in academic and industrial environments - is considered as a touchstone for concrete composition languages and an analysis of its ambiguous Recovery Framework specification is offered. In order to show the use of formal methods, a precise and unambiguous description of its (simplified) mechanisms is provided by means of a conservative extension of the pi-calculus. This has to be intended as a well known case study providing methodological arguments for the adoption of formal methods in software specification. The aspect of verification is not the main topic of the paper but some hints are given.
has-url: http://deploy-eprints.ecs.soton.ac.uk/158/1/dtw09_submission_15.pdf
has-title: A Formal Semantics for the WS-BPEL Recovery Framework: The pi-Calculus Way
type: Thing

http://deploy.rkbexplorer.com/id/person-fbefdbd72426f7bc1eaabe61eadb588f-976b96d2e90341673023c1022b6da59b
family-name: Latvala
given-name: Timo
full-name: Timo Latvala
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-b0969d103babf36381149383f997b5f0-60c8afcae8579e7bf174edd989727cb0
family-name: Dotti
given-name: Fernando
full-name: Fernando Dotti
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-04b592f0afef77cd3140cf2dbcca5361-de95e90acaeb2337b75784632d7df588
family-name: Dragoni
given-name: Nicola
full-name: Nicola Dragoni
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/publishing-house-b2a3080ac80f2d9a662b86472e2c2513
has-title: Springer-Verlag
type: Publishing-House
type: Thing

eprints-81
has-title: SYRAMS Requirement Table (STS)
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/81
has-url: http://deploy-eprints.ecs.soton.ac.uk/81/1/sv6a5.xls
type: Publication-Reference
type: Thing

http://deploy.rkbexplorer.com/id/person-d9148b3bf8c7c006f7fbea8b5183e8f6-de95e90acaeb2337b75784632d7df588
family-name: Mazzara
given-name: Manuel
full-name: Manuel Mazzara
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-f16d1b162d624fa00f2dd695673733c7-d20afebb7c6b736f4c767bbc606997e6
family-name: Fitzgerald
given-name: John S
full-name: John S Fitzgerald
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-1aa3f5c8208afb3fe7c9ae8a07807336-d20afebb7c6b736f4c767bbc606997e6
family-name: Bryans
given-name: Jeremy W
full-name: Jeremy W Bryans
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-35afd411ed3300230573bf5e14dbf722-406ae0ea539f521602364e13345eb695
family-name: Leuschel
given-name: Michael
full-name: Michael Leuschel
type: Person
type: Thing

eprints-60
type: Thing
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/27f1b9e18615e2d4306c1fdaa8ba64f8#2
has-url: http://deploy-eprints.ecs.soton.ac.uk/60/3/indexcodes.txt
has-title: Formal Development of the BepiColombo Pilot
has-url: http://deploy-eprints.ecs.soton.ac.uk/60/1/Plenary_presentation.pdf
type: Proceedings-Paper-Reference
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/60

http://deploy.rkbexplorer.com/id/person-d0b267429a3f5057f3e5be3e68476f8f-2db999ca37e94089f055e45631fd0f63
family-name: Romanovsky
family-name: Alexander
given-name: Romanovsky
given-name: Alexander
full-name: Romanovsky Alexander
full-name: Alexander Romanovsky
type: Person
type: Thing

eprints-157
has-url: http://deploy-eprints.ecs.soton.ac.uk/157/3/indexcodes.txt
type: Thing
type: Article-Reference
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/157
has-abstract: This paper proposes a method for deriving formal specifications of systems. To accomplish this task we pass through a non trivial number of steps, concepts and tools where the first one, the most important, is the concept of method itself, since we realized that computer science has a proliferation of languages but very few methods. We also propose the idea of Layered Fault Tolerant Specification (LFTS) to make the method extensible to Dependable Systems. The principle is layering the specification, for the sake of clarity, in (at least) two different levels, the first one for the normal behavior and the others (if more than one) for the abnormal. The abnormal behavior is described in terms of an Error Injector (EI) which represents a model of the erroneous interference coming from the environment. This structure has been inspired by the notion of idealized fault tolerant component but the combination of LFTS and EI using rely guarantee thinking to describe interference can be considered one of the main contributions of this work. The progress toward this method and the way to layer specifications. has been made experimenting on the Transportation and the Automotive Case Studies of the DEPLOY project.
has-url: http://deploy-eprints.ecs.soton.ac.uk/157/1/RigorousDevelopment_1.pdf
has-title: Deriving Specifications of Dependable Systems: toward a Method

http://deploy.rkbexplorer.com/id/person-0c4837098db3478289c268a564772ec1-1877e60711d1072ffc125775995a8f18
family-name: Voisin
given-name: Laurent
full-name: Laurent Voisin
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-d9148b3bf8c7c006f7fbea8b5183e8f6-a2aa6da3d2b976820fb8cfb38b4b44f5
family-name: Mazzara
given-name: Manuel
full-name: Manuel Mazzara
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-3cbf087c384a4d5e40c009e24538ed84-42c34226e0b90947e96c48ab8fb7c5c3
family-name: Troubitsyna
given-name: Elena
full-name: Elena Troubitsyna
type: Person
type: Thing

eprints-80
type: Book-Reference
type: Thing
has-url: http://deploy-eprints.ecs.soton.ac.uk/80/3/indexcodes.txt
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/80
has-url: http://deploy-eprints.ecs.soton.ac.uk/80/1/mathextn090109.pdf
has-title: Proposals for Mathematical Extensions for Event-B

http://deploy.rkbexplorer.com/id/person-a6f26d9b594b8229b90808ce917de6f9-1877e60711d1072ffc125775995a8f18
family-name: Schmalz
given-name: Matthias
full-name: Matthias Schmalz
type: Person
type: Thing

eprints-149
type: Book-Section-Reference
has-title: Automated Property Verification for Large Scale B Models
type: Thing
has-url: http://deploy-eprints.ecs.soton.ac.uk/149/3/indexcodes.txt
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/149
has-url: http://deploy-eprints.ecs.soton.ac.uk/149/1/siemens_fm09_final.pdf

http://deploy.rkbexplorer.com/id/person-0429503d75804875b71f6f9d9e6e41e2-54472938055d841bb87509ac2055a7e7
family-name: Laibinis
given-name: Linas
full-name: Linas Laibinis
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-611e3d7a0d072e550905c0f772131279-406ae0ea539f521602364e13345eb695
family-name: Fabian
given-name: Fritz
full-name: Fritz Fabian
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-d9148b3bf8c7c006f7fbea8b5183e8f6-c53324d49050109fe56a91525cab3c0b
family-name: Mazzara
given-name: Manuel
full-name: Manuel Mazzara
type: Person
type: Thing