http://deploy.rkbexplorer.com/id/person-4ef974fb25cfb6b4eb44f161c699d79b-b99a02d2c9ff728fc223264257663aa8
family-name: Castor Filho
given-name: Fernando
full-name: Fernando Castor Filho
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-6d563199864eb366d0332ba2ce8f83dc-50e781599010d56fea9f185edc7635d6
family-name: Delandtsheer
given-name: Renaud
full-name: Renaud Delandtsheer
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-ff5cdf051fdf6a057cc6f5dc942a9bd4-61605da97a72f30dbe474eb6bb8128f0
family-name: Aziz
given-name: Benjamin
full-name: Benjamin Aziz
type: Person
type: Thing

http://lodlaundromat.org/.well-known/genid/d7411f87c87a06e2299f170288045342#2
has-title: 12th European Workshop on Dependable Computing (EWDC 2009)
has-date: http://www.aktors.org/ontology/date#2009
type: Conference-Proceedings-Reference
type: Thing

http://deploy.rkbexplorer.com/id/person-4426af11fb79eafb04bdaa47ad49b58b-ac38a9c88ff871dce313d7bc26c9d18b
family-name: Hoang
given-name: Thai Son
full-name: Thai Son Hoang
type: Person
type: Thing

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

http://deploy.rkbexplorer.com/id/person-07080cab5f0586a6ad91d3cf3aee631f-61605da97a72f30dbe474eb6bb8128f0
family-name: Massonet
given-name: Philippe
full-name: Philippe Massonet
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-da824ad74fa69b9674207b955a92d4fd-ab5f6058bd71f3e5f3146c68c25ecf5c
family-name: Arief
given-name: Budi
full-name: Budi Arief
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/journal-8179c03fa8954255cd7faa1662c25a89
has-title: 21st IFIP Int. Conference on Testing of Communicating Systems and the 9th Int. Workshop on Formal Approaches to Testing of Software TESTCOM/FATES 2009
type: Publication-Reference
type: Journal
type: Thing

eprints-146
has-date: http://www.aktors.org/ontology/date#2009
type: Thing
has-url: http://deploy-eprints.ecs.soton.ac.uk/146/3/indexcodes.txt
has-title: Applying Model Checking to Generate Model-based Integration Tests from Choreography Models
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/146
has-url: http://deploy-eprints.ecs.soton.ac.uk/146/1/testcom_camera_ready.pdf
type: Article-Reference
has-abstract: Choreography models describe the communication protocols between services. Testing of service choreographies is an important task for the quality assurance of service-based systems as used e.g. in the context of service-oriented architectures (SOA). The formal modeling of service choreographies enables a model-based integration testing (MBIT) approach. We present MBIT methods for our service choreography modeling approach called Message Choreography Models (MCM). For the model-based testing of service choreographies, MCMs are translated into Event-B models and used as input for our test generator which uses the model checker ProB.

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

eprints-91
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/91
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/d7411f87c87a06e2299f170288045342#3
has-url: http://deploy-eprints.ecs.soton.ac.uk/91/1/nfm%2Dreqs%2Deventb.pdf
type: Proceedings-Paper-Reference
has-date: http://www.aktors.org/ontology/date#2009
has-url: http://deploy-eprints.ecs.soton.ac.uk/91/3/indexcodes.txt
type: Thing
has-page-numbers: 96-105
has-title: From Goal-Oriented Requirements to Event-B Specifications
has-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.

http://deploy.rkbexplorer.com/id/person-5cc9c64726103b8a48f3f67342f4f17d-3ad7dd5a50ae24311ca45c5bda0ca90c
family-name: Bicarregui
given-name: Juan
full-name: Juan Bicarregui
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-c7b767b687a24231ceaafc7bebcaa9ca-a23031a7e27367e2eaa6abe09294e0e6
family-name: Bicarregui
given-name: J C
full-name: J C Bicarregui
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-fcf60f0e9cace527953dd94605cba917-a23031a7e27367e2eaa6abe09294e0e6
family-name: Woodcock
given-name: J C P
full-name: J C P Woodcock
type: Person
type: Thing

eprints-133
has-date: http://www.aktors.org/ontology/date#2009
has-url: http://deploy-eprints.ecs.soton.ac.uk/133/3/indexcodes.txt
type: Thing
has-page-numbers: 16-22
has-title: SAL, Kodkod, and BDDs for Validation of B Models. Lessons and Outlook.
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/133
has-url: http://deploy-eprints.ecs.soton.ac.uk/133/1/afm_sal_kodkod_prob.pdf
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/d7411f87c87a06e2299f170288045342#6
type: Proceedings-Paper-Reference
has-abstract: PROB is a model checker for high-level B and Event-B models based on constraint-solving. In this paper we investigate alternate approaches for validating high-level B models using alternative techniques and tools based on using BDDs, SAT-solving and SMT-solving. In particular, we examine whether PROB can be complemented or even supplanted by using one of the tools BDDBDDB, Kodkod or SAL.

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

eprints-78
type: Article-Reference
has-url: http://deploy-eprints.ecs.soton.ac.uk/78/1/53c190b947c9f378091dc05fe375b603
has-page-numbers: 207-228
type: Thing
has-title: Frameworks for designing and implementing dependable systems using Coordinated Atomic Actions: A comparative study
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/78
has-date: http://www.aktors.org/ontology/date#2009
has-volume: 82

http://deploy.rkbexplorer.com/id/publishing-house-89c3f1bf8cd2f52b289e523e9a87ec1e
has-title: DEPLOY Project
type: Publishing-House
type: Thing

http://deploy.rkbexplorer.com/id/person-abcead70f0b5ec446831dd965ec1575c-e3ff05e5a40fcb1a2c5033dd7cce7e19
family-name: Samia
given-name: Mireille
full-name: Mireille Samia
type: Person
type: Thing

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

http://lodlaundromat.org/.well-known/genid/d7411f87c87a06e2299f170288045342#5
has-title: International Conference on Formal Engineering Methods - ICFEM 09
has-date: http://www.aktors.org/ontology/date#2009
type: Conference-Proceedings-Reference
type: Thing

http://deploy.rkbexplorer.com/id/journal-f3c24bd91410a93b15c251deb52ea486
has-title: Joint Working IEEE/IFIP Conference on Software Architecture 2009 & European Conference on Software Architecture 2009
type: Publication-Reference
type: Journal
type: Thing

http://deploy.rkbexplorer.com/id/person-451b2f4050dfbf772f9aa45492ff086d-a23031a7e27367e2eaa6abe09294e0e6
family-name: Larsen
given-name: P G
full-name: P G Larsen
type: Person
type: Thing

eprints-107
type: Thing
has-url: http://deploy-eprints.ecs.soton.ac.uk/107/2/CtsCtrl.zip
type: Book-Reference
has-title: Using Event-B Refinement to Verify a Control Strategy
has-url: http://deploy-eprints.ecs.soton.ac.uk/107/4/indexcodes.txt
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/107
has-url: http://deploy-eprints.ecs.soton.ac.uk/107/1/strategyref.pdf
has-date: http://www.aktors.org/ontology/date#2009

eprints-94
has-date: http://www.aktors.org/ontology/date#2009
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/94
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/d7411f87c87a06e2299f170288045342#2
has-abstract: Agent technology offers a number of advantages over traditional distributed systems, such as asynchronous communication, anonymity of individual agents and ability to change operational context. However, it is notoriously difficult to ensure dependability of agent systems. In this paper we present a formal approach for the top-down development of fault tolerant middleware for agent systems. We demonstrate how to develop the middleware that besides providing agent coordination is also able to cope with their failures. We focus on handling agent crushes and transient faults caused by volatile communication environment. We argue that formal development of middleware with integrated fault tolerance mechanisms has potential to enhance dependability of an agent system.
has-title: Fault Tolerant Middleware for Agent Systems: A Refinement Approach
type: Thing
type: Proceedings-Paper-Reference

http://deploy.rkbexplorer.com/id/person-d33fea45a8f080a5608ba42f87a002c6-3ad7dd5a50ae24311ca45c5bda0ca90c
family-name: Woodcock
given-name: Jim
full-name: Jim Woodcock
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

http://deploy.rkbexplorer.com/id/person-179447282825fddaf6ca7b39fb060457-24435d3d521f22a3b351c36d4e881112
family-name: Zorzo
given-name: Avelino
full-name: Avelino Zorzo
type: Person
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

http://deploy.rkbexplorer.com/id/person-99c2a05057e2958d65e131a56105f19a-12f24552670c17461250e723e75941c8
family-name: Jones
given-name: Cliff B
full-name: Cliff B Jones
type: Person
type: Thing

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

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

http://deploy.rkbexplorer.com/id/person-f8a74bf52cfa428f31e85124dfa43eb4-c48428572228004bd7ed1c3417b6cf85
family-name: Metayer
given-name: Christophe
full-name: Christophe Metayer
type: Person
type: Thing

eprints-144
has-date: http://www.aktors.org/ontology/date#2009
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/144
type: Thing
has-abstract: Event-B is a general purpose formal development method suitable for the design and detailed development of safety-critical systems. Being a data-driven formalism, it lacks any control ﬂow constructs. This turns out to be a limitation for systems with rich control ﬂow properties. In Event-B, control ﬂow information has to be embedded into guards and event actions and this results in an entanglement of control ﬂow and functional specification with the additional downside of extra model variables. This paper proposes a method for extending Event-B models with an new viewpoint portraying control ﬂow properties of a model. The novelty of the work is in relying solely on theorem proving to demonstrate the consistency of control ﬂow and main Event-B specification. The focus is placed on the practicality of working with such an extension and also on achieving proof economy. A detailed formal treatment of the method is presented and illustrated with a case study. A proof of concept implementation for the RODIN platform is brieﬂy discussed.
has-url: http://deploy-eprints.ecs.soton.ac.uk/144/1/flows%2Dpaper..pdf
type: Publication-Reference
has-url: http://deploy-eprints.ecs.soton.ac.uk/144/3/indexcodes.txt
has-title: On Event-B and Control Flow

http://deploy.rkbexplorer.com/id/person-eef550d06dcce03b9cde9ff601530c93-5f763fbda32a492226bfc60811bf17b8
family-name: Schieferdecker
given-name: I
full-name: I Schieferdecker
type: Person
type: Thing

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

eprints-89
has-title: Methods, Models and Tools for Fault Tolerance
type: Thing
has-date: http://www.aktors.org/ontology/date#2009
type: Publication-Reference
has-url: http://www.springer.com/computer/programming/book/978-3-642-00866-5
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/89

http://deploy.rkbexplorer.com/id/publishing-house-0843f588c79adf8b3c10504fe18195c3
has-title: Knowledge Systems Institute Graduate School
type: Publishing-House
type: Thing

eprints-110
has-abstract: Distributed information systems are critical to the functioning of many businesses; designing them to be dependable is a challenging but important task. We report our experience in using formal methods to enhance processes and tools for development of business information software based on service-oriented architectures. In our work, which takes place in an industrial setting, we focus on the configuration of middleware, verifying application-level requirements in the presence of faults. In pilot studies provided by SAP, we used the Event-B formalism and the open Rodin tools platform to prove properties of models of business protocols and expose weaknesses of certain middleware configurations with respect to particular protocols. We then extended the approach to use models automatically generated from diagrammatic design tools, opening the possibility of seamless integration with current development environments. Increased automation in the verification process, through domain-specific models and theories, is a goal for future work. KEYWORDS: Verification, Fault Modelling, Service- Oriented Architectures, Event-B, Tool Support
has-url: http://deploy-eprints.ecs.soton.ac.uk/110/3/indexcodes.txt
type: Thing
has-date: http://www.aktors.org/ontology/date#2009
has-url: http://deploy-eprints.ecs.soton.ac.uk/110/1/PublishedVersionOfICECCSpaper.pdf
type: Article-Reference
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/110
has-page-numbers: 68-77
has-title: Formal Modelling and Analysis of Business Information Applications with Fault Tolerant Middleware

http://deploy.rkbexplorer.com/id/person-f365d2ddb0c152b0ec46b98ff5791b30-8a92fe087258d62d245780a3c715932d
family-name: Wieczorek
given-name: S
full-name: S Wieczorek
type: Person
type: Thing

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

http://deploy.rkbexplorer.com/id/person-f365d2ddb0c152b0ec46b98ff5791b30-5f763fbda32a492226bfc60811bf17b8
family-name: Wieczorek
given-name: S
full-name: S Wieczorek
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/journal-d1a941c755725e65bd4417dce5ae726f
has-title: Journal of Systems and Software
type: Publication-Reference
type: Journal
type: Thing

http://deploy.rkbexplorer.com/id/person-2d6231db28f4181af04f0da3297e97c5-3ad7dd5a50ae24311ca45c5bda0ca90c
family-name: Larsen
given-name: Peter Gorm
full-name: Peter Gorm Larsen
type: Person
type: Thing

eprints-160
has-abstract: We examine the the industrial application of formal methods using data gathered in a review of 62 projects taking place over the last 25 years. The review suggests that formal methods are being applied in a wide range of application domains, with increasingly strong tool support. Significant challenges remain in providing usable tools that can be integrated into established development processes; in education and training; in taking formal methods from first use to second use, and in gathering and evidence to support informed selection of methods and tools.
has-url: http://www.springer.com/computer/programming/book/978-3-642-05088-6
has-url: http://deploy-eprints.ecs.soton.ac.uk/160/2/BicarreguiEtAlIdayAuth.pdf
has-date: http://www.aktors.org/ontology/date#2009
has-title: Industrial Practice in Formal Methods: a Review
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/160
type: Thing
has-url: http://deploy-eprints.ecs.soton.ac.uk/160/4/indexcodes.txt
type: Publication-Reference

http://lodlaundromat.org/.well-known/genid/d7411f87c87a06e2299f170288045342#3
has-title: First Nasa Formal Method Symposium
has-date: http://www.aktors.org/ontology/date#2009
type: Conference-Proceedings-Reference
type: Thing

eprints-84
has-abstract: MIDAS (Microprocessor Instruction and Data Abstraction System) is a specification of an Instruction Set Architecture (ISA) capable of executing binary images compiled from the C language. It was developed to demonstrate a methodology for formal construction of various ISAs in Event-B via a generic model. It is intended to be representative of typical microprocessor ISAs, but using a minimal number of defined instructions, in order to make complete refinement practical. The intention is to simplify the number and complexity of the defined instructions at the cost of compiler complexity, run-time performance and code density, without compromising representativeness. There are two variants: a stack-based machine and a randomly accessible register array machine. The two variants employ the same instruction codes, the differences being limited to register file behavior.
type: Publication-Reference
has-title: MIDAS: A Formally Constructed Virtual Machine
has-date: http://www.aktors.org/ontology/date#2009
has-url: http://deploy-eprints.ecs.soton.ac.uk/84/1/MidasBundle.rar
has-url: http://deploy-eprints.ecs.soton.ac.uk/84/4/indexcodes.txt
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/84
type: Thing
has-url: http://deploy-eprints.ecs.soton.ac.uk/84/2/Midas_Deploy.pdf

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-73eaf334d5d5bc4ac57733d461d8d112-8a92fe087258d62d245780a3c715932d
family-name: Kozyura
given-name: V
full-name: V Kozyura
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-89cd3cc208072c24bfa40fdb97f6fb3e-ed640ee6b7826f7d7f1180b0ad4aaf82
family-name: Edmunds
given-name: Andrew
full-name: Andrew Edmunds
type: Person
type: Thing

eprints-105
has-title: Structuring Specifications with Modes
has-abstract: The two dependability means considered in this paper are rigorous design and fault tolerance. It can be complex to rigorously design some classes of systems, including fault tolerant ones, therefore appropriate abstractions are needed to better support system modelling and analysis. The abstraction proposed in this paper for this purpose is the notion of operation mode. Modes are formalised and their relation to a state-based formalism in a refinement approach is established. The use of modes for fault tolerant systems is then discussed and a case study presented. Using modes in state-based modelling allows us to improve system structuring, the elicitation of system assumptions and expected functionality, as well as requirement traceability.
type: Thing
has-url: http://deploy-eprints.ecs.soton.ac.uk/105/1/ladc%2Dfinal.pdf
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/105
has-date: http://www.aktors.org/ontology/date#2009
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/d7411f87c87a06e2299f170288045342#1
type: Proceedings-Paper-Reference

http://deploy.rkbexplorer.com/id/person-00019e64b9bd9223cbe3b30c2c23cb38-5f99ddf6618bf6f9cc67a6625ed9cc53
family-name: Plagge
given-name: Daniel
full-name: Daniel Plagge
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-5cc9c64726103b8a48f3f67342f4f17d-61605da97a72f30dbe474eb6bb8128f0
family-name: Bicarregui
given-name: Juan
full-name: Juan Bicarregui
type: Person
type: Thing

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

http://deploy.rkbexplorer.com/id/person-c4e5fe9940b95b97f6ceccd70cbeff5a-8a92fe087258d62d245780a3c715932d
family-name: Bendisposto
given-name: Jens
full-name: Jens Bendisposto
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-b83b55637c6b2e461388bcc08695852b-44c1d862d1567cdff61f0b65becb95c6
family-name: Wright
given-name: Stephen
full-name: Stephen Wright
type: Person
type: Thing

http://lodlaundromat.org/.well-known/genid/d7411f87c87a06e2299f170288045342#6
has-title: AFM09 (Automated Formal Methods)
has-date: http://www.aktors.org/ontology/date#2009
type: Conference-Proceedings-Reference
type: Thing

http://deploy.rkbexplorer.com/id/person-e0638b0e7a15f30831b459e05bcf422e-24435d3d521f22a3b351c36d4e881112
family-name: Pelliccione
given-name: Patrizio
full-name: Patrizio Pelliccione
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/journal-5f1d81aa0a391f8ff496f76b4f39c213
has-title: The Journal of Systems and Software
type: Publication-Reference
type: Journal
type: Thing

http://deploy.rkbexplorer.com/id/publishing-house-09039ee8dc22cd24c526909663ccb3a3
has-title: ETH Zurich
type: Publishing-House
type: Thing

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

eprints-150
has-url: http://deploy-eprints.ecs.soton.ac.uk/150/2/SharedBufferExample.zip
has-date: http://www.aktors.org/ontology/date#2009
has-url: http://deploy-eprints.ecs.soton.ac.uk/150/5/indexcodes.txt
type: Thing
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/150
type: Publication-Reference
has-title: A Code Generation Example for Event-B: A Shared Channel with Concurrent Read/Writers
has-url: http://deploy-eprints.ecs.soton.ac.uk/150/3/PlenarySharedBuffer.pdf
has-abstract: We present an example involving processes reading and writing to a shared channel. A channel may have at most one reader reading, and at most one writer writing at any one time; however a number of processes may be waiting to read from, or write to, the channel. In our most abstract model data is transferred as a block in a single atomic step. A write event constitutes moving a block from a writing process to a channel buffer; and a read event constitutes moving a block from a channel buffer to a reader. The atomicity of the read and write activity is altered in the refinement - we introduce blocks that are made up of packets, and each packet is written to the channel individually. This allows the reader to begin reading as soon as there is data in the channel - without the writer having to complete the data transfer. We continue with an overview of our implementation notation (OCB), and show the implementation level specification for the concurrent read/writers example. We then present details of the implementation level refinement that results from the translation of the OCB model into Event-B, and also discuss details of the source code generated by the Java translator.

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

http://deploy.rkbexplorer.com/id/person-cbc6a17975d3e80cfa107359e32dc690-b99a02d2c9ff728fc223264257663aa8
family-name: Rubira
given-name: Cecilia
full-name: Cecilia Rubira
type: Person
type: Thing

eprints-108
type: Thing
has-url: http://deploy-eprints.ecs.soton.ac.uk/108/1/cookbook.pdf
type: Book-Reference
has-date: http://www.aktors.org/ontology/date#2009
has-url: http://deploy-eprints.ecs.soton.ac.uk/108/3/indexcodes.txt
has-title: Towards a Cookbook for Modelling and Refinement of Control Problems
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/108

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

eprints-11
has-title: Rodin Manual and Language Definition
type: Thing
has-url: http://deploy-eprints.ecs.soton.ac.uk/11/1/manual%2D2.3.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/11/15/indexcodes.txt
has-url: http://deploy-eprints.ecs.soton.ac.uk/11/14/indexcodes.txt
type: Book-Reference
has-url: http://deploy-eprints.ecs.soton.ac.uk/11/2/mathLanguage%2D2007%2D10%2D26.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/11/4/kernel_lang.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/11/3/notation%2D1.5.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/11/13/indexcodes.txt
has-date: http://www.aktors.org/ontology/date#2009
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/11
has-url: http://deploy-eprints.ecs.soton.ac.uk/11/12/indexcodes.txt

http://deploy.rkbexplorer.com/id/person-8f94cdec2034971294871cb0c2d6e3e8-61605da97a72f30dbe474eb6bb8128f0
family-name: Arenas
given-name: Alvaro
full-name: Alvaro Arenas
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-a099a2f02eef3bfe69ae6bdc4e771651-5f763fbda32a492226bfc60811bf17b8
family-name: Stefanescu
given-name: A
full-name: A Stefanescu
type: Person
type: Thing

eprints-137
has-url: http://deploy-eprints.ecs.soton.ac.uk/137/3/indexcodes.txt
has-title: Rodin User and Developer Workshop 2009 - Extended Abstracts
type: Book-Reference
has-date: http://www.aktors.org/ontology/date#2009
has-url: http://deploy-eprints.ecs.soton.ac.uk/137/1/proceedings.pdf
type: Thing
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/137

http://lodlaundromat.org/.well-known/genid/d7411f87c87a06e2299f170288045342#1
has-title: Fourth Latin-American Symposium on Dependable Computing (LADC)
has-date: http://www.aktors.org/ontology/date#2009
type: Conference-Proceedings-Reference
type: Thing

http://deploy.rkbexplorer.com/id/person-490692ec8bbee956ec6101f12df93f57-5f763fbda32a492226bfc60811bf17b8
family-name: Kraft
given-name: F M
full-name: F M Kraft
type: Person
type: Thing

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

http://deploy.rkbexplorer.com/id/publishing-house-56bfb362d227ccfad724c85fb1eda298
has-title: ECS, University of Southampton
type: Publishing-House
type: Thing

http://deploy.rkbexplorer.com/id/person-a9911e17588535a3dca04a665deef2ea-a23031a7e27367e2eaa6abe09294e0e6
family-name: Fitzgerald
given-name: J S
full-name: J S Fitzgerald
type: Person
type: Thing

http://www.aktors.org/ontology/date#2009
year-of: 2009
has-pretty-name: 2009
type: Calendar-Date
type: Thing

eprints-145
has-url: http://deploy-eprints.ecs.soton.ac.uk/145/1/ecsa09_camera_ready.pdf
type: Thing
has-url: http://deploy-eprints.ecs.soton.ac.uk/145/3/indexcodes.txt
type: Article-Reference
has-abstract: Component integration plays a decisive role in service-oriented architectures (SOAs). The technical implementation must faithfully reflect business and enterprise integration requirements. This implies a good understanding of the globally observable message choreography but also of how messages are handled by the involved components and by the SOA middleware. In this paper we present a solution to the problem of keeping global and local viewpoints in synchronization via a common message choreography metamodel. As main contribution we shape various interpretations of global choreographies, which were left unspecified in state-of-the-art choreography approaches. We have implemented a message choreography modeling (MCM) environment incorporating these contributions. MCM seamlessly complements existing models at SAP. We show how service integration experts, architects, and testers can benefit from our approach that enables model-based integration testing and model verification facilities.
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/145
has-date: http://www.aktors.org/ontology/date#2009
has-title: Viewpoints for Modeling Choreographies in Service-Oriented Architectures

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

http://deploy.rkbexplorer.com/id/person-395ad18a14580a59a0bc58a4ac3ffc37-61605da97a72f30dbe474eb6bb8128f0
family-name: Ponsard
given-name: Christophe
full-name: Christophe Ponsard
type: Person
type: Thing

eprints-90
has-date: http://www.aktors.org/ontology/date#2009
has-title: Step-wise Development of Resilient Ambient Campus Scenarios
type: Book-Section-Reference
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/90
type: Thing
has-url: http://deploy-eprints.ecs.soton.ac.uk/90/3/indexcodes.txt
has-url: http://deploy-eprints.ecs.soton.ac.uk/90/1/54540304.pdf

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-f69773a9f7b219563f6042cba17cba7e-24435d3d521f22a3b351c36d4e881112
family-name: Guelfi
given-name: Nicolas
full-name: Nicolas Guelfi
type: Person
type: Thing

eprints-153
type: Thing
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/153
has-abstract: Operation modes are useful structuring units that facilitate design of several safety-critical systems such as such as avionic, transportation and space systems. Although some support to the construction of modal systems can be found in the literature, modelling abstractions for the formal specification, analysis and correct construction of modal systems are still lacking. This paper discusses existing support for the construction of modal systems and proposes both a formalisation and a reﬁnement notion for modal systems. A modal system, specified using the proposed abstractions, can be realised using different specification languages. Complementing the contribution, we define the requirements for an Event-B model to realise a modal system specification. A case study illustrates the proposed approach.
has-title: Modal Systems: Specification, Reﬁnement and Realisation
type: Proceedings-Paper-Reference
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/d7411f87c87a06e2299f170288045342#5
has-url: http://deploy-eprints.ecs.soton.ac.uk/153/1/paper105%2DICFEM09.pdf
has-date: http://www.aktors.org/ontology/date#2009
has-url: http://deploy-eprints.ecs.soton.ac.uk/153/3/indexcodes.txt

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

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

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

http://deploy.rkbexplorer.com/id/journal-cdb70681d5752108e985384de2a41260
has-title: Proceedings 14th IEEE International Conference on Engineering of Complex Computer Systems ICECCS 2009.
type: Publication-Reference
type: Journal
type: Thing

http://deploy.rkbexplorer.com/id/person-4b91512d970d86a1f3707335a04be0a9-42c34226e0b90947e96c48ab8fb7c5c3
family-name: Iliasov
given-name: Alexei
full-name: Alexei Iliasov
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-f9e8ed400943f912f94afe15236a345a-24435d3d521f22a3b351c36d4e881112
family-name: Capozucca
given-name: Alfredo
full-name: Alfredo Capozucca
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-eea2488aaebeb98b3faff7eee3e1679e-5f99ddf6618bf6f9cc67a6625ed9cc53
family-name: Lopatkin
given-name: Ilya
full-name: Ilya Lopatkin
type: Person
type: Thing

eprints-161
has-url: http://deploy-eprints.ecs.soton.ac.uk/161/2/fmsurvey[1].pdf
has-abstract: Formal methods use mathematical models for analysis and verification at any part of the program life-cycle. We describe the state of the art in the industrial use of formal methods, concentrating on their increasing use at the earlier stages of specification and design. We do this by reporting on a new survey of industrial use, comparing the situation in 2009 with the most significant surveys carried out over the last 20 years. We describe some of the highlights of our survey by presenting a series of industrial projects, and we draw some observations from these surveys and records of experience. Based on this, we discuss the issues surrounding the industrial adoption of formal methods. Finally, we look to the future and describe the development of a Verified Software Repository, part of the worldwide Verified Software Initiative. We introduce the initial projects being used to populate the repository, and describe the challenges they address.
has-page-numbers: 1-36
has-date: http://www.aktors.org/ontology/date#2009
type: Article-Reference
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/161
type: Thing
has-url: http://deploy-eprints.ecs.soton.ac.uk/161/4/indexcodes.txt
has-volume: 41
has-number: 4
has-title: Formal Methods: Practice and Experience

http://lodlaundromat.org/.well-known/genid/d7411f87c87a06e2299f170288045342#4
has-title: Integrated Formal Methods iFM2009
has-date: http://www.aktors.org/ontology/date#2009
type: Conference-Proceedings-Reference
type: Thing

http://deploy.rkbexplorer.com/id/person-395ad18a14580a59a0bc58a4ac3ffc37-50e781599010d56fea9f185edc7635d6
family-name: Ponsard
given-name: Christophe
full-name: Christophe Ponsard
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/journal-e7a31c7afec28c6fdef45d65978df7fc
has-title: ACM Computing Surveys
type: Publication-Reference
type: Journal
type: Thing

http://deploy.rkbexplorer.com/id/person-808377482599bbb2fc48d8780b8ae238-5f763fbda32a492226bfc60811bf17b8
family-name: Charfi
given-name: A
full-name: A Charfi
type: Person
type: Thing

eprints-148
has-url: http://deploy-eprints.ecs.soton.ac.uk/148/3/indexcodes.txt
has-url: http://deploy-eprints.ecs.soton.ac.uk/148/1/seke09_jcre.pdf
type: Thing
type: Book-Section-Reference
has-title: Pie Tree Visualization
has-date: http://www.aktors.org/ontology/date#2009
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/148

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

http://deploy.rkbexplorer.com/id/person-eef550d06dcce03b9cde9ff601530c93-8a92fe087258d62d245780a3c715932d
family-name: Schieferdecker
given-name: I
full-name: I Schieferdecker
type: Person
type: Thing

eprints-106
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/106
type: Thing
has-date: http://www.aktors.org/ontology/date#2009
type: Book-Reference
has-title: Towards Automated Reﬁnement: Patterns in Event B
has-url: http://deploy-eprints.ecs.soton.ac.uk/106/1/main%2Dictac2009.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/106/3/indexcodes.txt

http://deploy.rkbexplorer.com/id/publishing-house-ad54bf1ad9ce4c712ab33869a79fd20b
has-title: DEPLOY
type: Publishing-House
type: Thing

http://deploy.rkbexplorer.com/id/publishing-house-3bc07b0c1b8f7135047c61bf1bd2f041
has-title: RODIN Project
type: Publishing-House
type: Thing

eprints-51
has-title: Decomposition Structures for Event-B
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/d7411f87c87a06e2299f170288045342#4
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/51
has-date: http://www.aktors.org/ontology/date#2009
type: Proceedings-Paper-Reference
type: Thing

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

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/publishing-house-04f9bca8b99137515946893c2bf96a16
has-title: Technical Report
type: Publishing-House
type: Thing

http://deploy.rkbexplorer.com/id/person-00019e64b9bd9223cbe3b30c2c23cb38-8a92fe087258d62d245780a3c715932d
family-name: Plagge
given-name: Daniel
full-name: Daniel Plagge
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-73eaf334d5d5bc4ac57733d461d8d112-5f763fbda32a492226bfc60811bf17b8
family-name: Kozyura
given-name: V
full-name: V Kozyura
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-d5c4f235f9f262879c15081cdf792645-ac38a9c88ff871dce313d7bc26c9d18b
family-name: Mehta
given-name: Farhad
full-name: Farhad Mehta
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-90e5976e32608e938418061ba3ae2d0e-c14e53bd9c90664f489f6c84aa1ae36a
family-name: Roth
given-name: Andreas
full-name: Andreas Roth
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-8e0400974d71894029bdc22f981fc6bd-a32231f47aac9c4cf59b1324f8b9363e
family-name: Riberiro
given-name: Leila
full-name: Leila Riberiro
type: Person
type: Thing

eprints-88
has-page-numbers: 874-890
has-url: http://deploy-eprints.ecs.soton.ac.uk/88/3/indexcodes.txt
type: Article-Reference
has-title: Improving reliability of cooperative concurrent systems with exception flow analysis
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/88
has-volume: 82
has-date: http://www.aktors.org/ontology/date#2009
has-abstract: Developers of fault-tolerant distributed systems need to guarantee that fault tolerance mechanisms they build are in themselves reliable. Otherwise, these mechanisms might in the end negatively affect overall system dependability, thus defeating the purpose of introducing fault tolerance into the system. To achieve the desired levels of reliability, mechanisms for detecting and handling errors should be developed rigorously or formally. We present an approach to modeling and verifying fault-tolerant distributed systems that use exception handling as the main fault tolerance mechanism. In the proposed approach, a formal model is employed to specify the structure of a system in terms of cooperating participants that handle exceptions in a coordinated manner, and coordinated atomic actions serve as representatives of mechanisms for exception handling in concurrent systems. We validate the approach through two case studies: (i) a system responsible for managing a production cell, and (ii) a medical control system. In both systems, the proposed approach has helped us to uncover design faults in the form of implicit assumptions and omissions in the original specifications.
type: Thing
has-url: http://deploy-eprints.ecs.soton.ac.uk/88/1/fernando%2Djss%2D2009.pdf

eprints-151
type: Book-Reference
has-title: Goal-Oriented Requirements Engineering in Action in the Transportation Sector
has-url: http://deploy-eprints.ecs.soton.ac.uk/151/3/indexcodes.txt
has-url: http://deploy-eprints.ecs.soton.ac.uk/151/1/DEPLOY%2DGORE%2Din%2Daction.pdf
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/151
type: Thing
has-date: http://www.aktors.org/ontology/date#2009

eprints-130
type: Book-Reference
type: Thing
has-title: Rodin: An Open Toolset for Modelling and Reasoning in Event-B
has-date: http://www.aktors.org/ontology/date#2009
has-url: http://deploy-eprints.ecs.soton.ac.uk/130/3/indexcodes.txt
has-url: http://deploy-eprints.ecs.soton.ac.uk/130/1/main.pdf
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/130

eprints-109
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/109
has-date: http://www.aktors.org/ontology/date#2009
type: Thing
type: Book-Reference
has-title: Event Model Decomposition
has-url: http://deploy-eprints.ecs.soton.ac.uk/109/1/626.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/109/3/indexcodes.txt

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

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