http://deploy.rkbexplorer.com/id/person-100f498ae268dd4869470f10ff7f0d1c-7cd32e7c2c44839d94bf9fabd3843354
family-name: Dony
given-name: Christophe
full-name: Christophe Dony
type: Person
type: Thing

eprints-33
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/33
has-date: http://www.aktors.org/ontology/date#2008
type: Thing
type: Proceedings-Paper-Reference
has-title: Formal Refinement Automation
has-url: http://deploy-eprints.ecs.soton.ac.uk/33/1/iliavocs.pdf
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#5
has-url: http://deploy-eprints.ecs.soton.ac.uk/33/3/indexcodes.txt

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

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

http://deploy.rkbexplorer.com/id/person-8768095c4772f9a39faa2cf2cf37d1ee-614513275406bc0b0ddb6f4cb1edf313
family-name: Gorbenko
given-name: Anatoliy
full-name: Anatoliy Gorbenko
type: Person
type: Thing

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

http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#7
has-date: http://www.aktors.org/ontology/date#2008
has-title: Abstract State Machines, B and Z, First International Conference ABZ 2008
type: Conference-Proceedings-Reference
type: Thing

eprints-41
type: Proceedings-Paper-Reference
has-url: http://deploy-eprints.ecs.soton.ac.uk/41/3/indexcodes.txt
has-title: Precise Steps for Choreography Modeling for SOA Validation and Verification
has-date: http://www.aktors.org/ontology/date#2008
type: Thing
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#1
has-url: http://deploy-eprints.ecs.soton.ac.uk/41/1/sose%2Dcamera%2Dready.pdf
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/41

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

http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#13
has-date: http://www.aktors.org/ontology/date#2008
has-title: EDCC 7: the Seventh European Dependable Computing Conference (EDCC-7)
type: Conference-Proceedings-Reference
type: Thing

http://deploy.rkbexplorer.com/id/person-d009963a40cdcfb0f850852db8d63cd0-3ddfec4adbae5ba5209cf2451a0c1a30
family-name: Greathead
given-name: David
full-name: David Greathead
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/journal-ac8cac4f0369b412cc8298d33cd05c2e
has-title: Formal Aspects of Computing
type: Publication-Reference
type: Journal
type: Thing

eprints-49
type: Book-Section-Reference
has-title: Incremental Design of Distributed Systems with Event-B
type: Thing
has-url: http://deploy-eprints.ecs.soton.ac.uk/49/2/marktoberdorf2.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/49/4/indexcodes.txt
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/49
has-date: http://www.aktors.org/ontology/date#2008

http://deploy.rkbexplorer.com/id/person-5229f5509fa97145597cd2bde6ea4341-614513275406bc0b0ddb6f4cb1edf313
family-name: Kharchenko
given-name: Vyacheslav
full-name: Vyacheslav Kharchenko
type: Person
type: Thing

eprints-28
has-abstract: The construction of formal models of real-time distributed systems is a considerable practical challenge. We propose and illustrate a pragmatic incremental approach in which detail is progressively added to abstract system-level specifications of functional and timing properties via intermediate models that express system architecture, concurrency and timing behaviour. The approach is illustrated by developing a new formal model of the cardiac pacemaker system proposed as a “grand challenge” problem in 2007. The models are expressed using the Vienna Development Method (VDM) and are validated primarily by scenario-based tests, including the analysis of timed traces. We argue that the insight gained using this staged modelling approach will be valuable in the subsequent development of implementations, and in detecting potential bottlenecks within suggested implementation architectures.
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/28
has-page-numbers: 181-197
has-title: Incremental Development of a Distributed Real-Time Model of a Cardiac Pacing System using VDM
type: Thing
has-url: http://deploy-eprints.ecs.soton.ac.uk/28/1/pacemaker.pdf
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#15
has-date: http://www.aktors.org/ontology/date#2008
has-url: http://deploy-eprints.ecs.soton.ac.uk/28/3/indexcodes.txt
type: Proceedings-Paper-Reference

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

eprints-99
type: Thing
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#13
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/99
has-title: Refinement Patterns for Fault Tolerant Systems
has-abstract: The paper puts forward the idea of using fault tolerance refinement patterns to assist system developers in disciplined application of software fault tolerance mechanisms in rigorous system design. Two patterns are proposed to support a correct introduction of recovery blocks and N-version programming into a system model; these are formally defined and their correctness proven. We also discuss several important issues involved in the use of these patterns in engineering systems, including tool support and pattern composition.design) as a major means for improving the quality of products.
has-url: http://deploy-eprints.ecs.soton.ac.uk/99/1/edcc%2Dfinal.pdf
has-date: http://www.aktors.org/ontology/date#2008
has-url: http://deploy-eprints.ecs.soton.ac.uk/99/3/indexcodes.txt
type: Proceedings-Paper-Reference

http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#2
has-date: http://www.aktors.org/ontology/date#2008
has-title: 4th International Workshop on Exception Handling (WEH.08), at ACM SIGSOFT 2008/FSE 16
type: Conference-Proceedings-Reference
type: Thing

http://deploy.rkbexplorer.com/id/person-f5b77b4bebe6bd27daa19aef96415799-8806e8c24f5928c142562d222e11cd15
family-name: Macedo
given-name: Hugo Daniel
full-name: Hugo Daniel Macedo
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-c4dd288a064650fdfba7361c844597db-3ddfec4adbae5ba5209cf2451a0c1a30
family-name: Payne
given-name: Richard
full-name: Richard Payne
type: Person
type: Thing

eprints-44
type: Thing
has-url: http://deploy-eprints.ecs.soton.ac.uk/44/3/indexcodes.txt
has-title: Probing the Depths of CSP-M: A New FDR-Compliant Validation Tool
has-date: http://www.aktors.org/ontology/date#2008
has-url: http://deploy-eprints.ecs.soton.ac.uk/44/1/main.pdf
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/44
type: Book-Section-Reference

http://deploy.rkbexplorer.com/id/person-205632f059d5323f42cbd0d8934c7019-94a37a77106d67d5ab3a4a60529beed2
family-name: Dallons
given-name: Gautier
full-name: Gautier Dallons
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-425e7481d43dda1ef7d067c8dd1b2ec6-2fb92fcd66cdcd34eca78db11da4f58e
family-name: Andreas
given-name: Roth
full-name: Roth Andreas
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-f9579eae1c06dbfedbaedf003c91e8a4-ff87ee2176dffad660019ef2d847b44e
family-name: Spermann
given-name: Corinna
full-name: Corinna Spermann
type: Person
type: Thing

eprints-52
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/52
has-url: http://deploy-eprints.ecs.soton.ac.uk/52/1/Bryans%2Det%2Dal.pdf
has-title: Formal Modelling and Analysis of Business Information Applications with Fault Tolerant Middleware
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.
type: Publication-Reference
has-url: http://deploy-eprints.ecs.soton.ac.uk/52/3/indexcodes.txt
type: Thing
has-date: http://www.aktors.org/ontology/date#2008

http://deploy.rkbexplorer.com/id/person-7a1c3a15cf48ae2e2d94f7783db8a9e8-94a37a77106d67d5ab3a4a60529beed2
family-name: Philippe
given-name: Massonet
full-name: Massonet Philippe
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-cc022198c36492e90ad98b8f45847def-ba99479eec96bb647d10645e41cde1c6
family-name: Muccini
given-name: Henry
full-name: Henry Muccini
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/publishing-house-382b0f5185773fa0f67a8ed8056c7759
has-title: N/A
type: Publishing-House
type: Thing

www.aktors.org
site name: Aktors
locale: en_US
title: Turning Shoe Information to Knowledge of Technology and Deals
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://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#5
has-date: http://www.aktors.org/ontology/date#2008
has-title: Eighth International Workshop on Automated Verification of Critical Systems
type: Conference-Proceedings-Reference
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

eprints-39
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#10
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/39
has-date: http://www.aktors.org/ontology/date#2008
has-title: Linking Event-B and Concurrent Object-Oriented Programs
type: Proceedings-Paper-Reference
type: Thing

http://deploy.rkbexplorer.com/id/journal-2ebe291112ec3a2a7997875ef4ff0fca
has-title: ERCIM News
type: Publication-Reference
type: Journal
type: Thing

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

http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#11
has-date: http://www.aktors.org/ontology/date#2008
has-title: Seventh European Dependable Computing Conference (EDCC-7)
type: Conference-Proceedings-Reference
type: Thing

http://deploy.rkbexplorer.com/id/journal-74200623372329bb066a12b79ba089b6
has-title: SIGSOFT Software Engineering Notes
type: Publication-Reference
type: Journal
type: Thing

eprints-47
has-date: http://www.aktors.org/ontology/date#2008
type: Thing
has-url: http://deploy-eprints.ecs.soton.ac.uk/47/1/teaching_animation.pdf
has-title: Easy Graphical Animation and Formula Visualisation for Teaching B
type: Proceedings-Paper-Reference
has-abstract: ProB is being used for teaching the B-method. In this paper, we present two new features of ProB that we have introduced while teaching B. One feature allows a student (or an expert user) to graphically visualise any predicate as a tree. The underlying algorithm can deal with undefined subformulas and tries to provide useful feedback even for existentially quantified formulas which are false. This feature is especially useful to inspect unexpected invariant violations or operations which are unexpectedly enabled or disabled. The other feature enables a student or lecturer to easily and quickly write custom graphical state representations, to provide a better understanding of the model. With this method, one simply has to assemble a series of pictures and to write an animation function in B itself, which stipulates which pictures should be shown where depending on the current state of the model. As an additional side-benefit, writing the animation function in B itself is a good exercise for students.
has-url: http://deploy-eprints.ecs.soton.ac.uk/47/3/indexcodes.txt
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/47
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#14

eprints-26
has-url: http://deploy-eprints.ecs.soton.ac.uk/26/1/evtbena.pdf
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/26
has-title: On the Purpose of Event-B Proof Obligations
has-url: http://deploy-eprints.ecs.soton.ac.uk/26/3/indexcodes.txt
type: Thing
has-date: http://www.aktors.org/ontology/date#2008
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#9
type: Proceedings-Paper-Reference
has-abstract: Event-B is a formal modelling method which is claimed to be suitable for diverse modelling domains, such as reactive systems and sequential program development. This claim hinges on the fact that any particular model has an appropriate semantics. In Event-B this semantics is provided implicitly by proof obligations associated with a model. There is no fixed semantics though. In this article we argue that this approach is beneficial to modelling because we can use similar proof obligations across a variety of modelling domains. By way of two examples we show how similar proof obligations are linked to different semantics. A small set of proof obligations is thus suitable for a whole range of modelling problems in diverse modelling domains.

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

http://deploy.rkbexplorer.com/id/person-82dea5ee2addc7475e6d3250e82b4836-0a46f594e90a013357fd0d1a7f0bfbd4
family-name: Snook
given-name: Colin
full-name: Colin Snook
type: Person
type: Thing

eprints-76
type: Thing
type: Publication-Reference
has-url: http://deploy-eprints.ecs.soton.ac.uk/76/3/indexcodes.txt
has-date: http://www.aktors.org/ontology/date#2008
has-url: http://deploy-eprints.ecs.soton.ac.uk/76/1/WP3_intro.pdf
has-title: Deployment in the Space Sector (Slides for DEPLOY Newcastle Kick-off Meeting)
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/76

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-34
has-url: http://deploy-eprints.ecs.soton.ac.uk/34/1/serene6%2Dfinal.pdf
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#3
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/34
type: Proceedings-Paper-Reference
has-url: http://deploy-eprints.ecs.soton.ac.uk/34/3/indexcodes.txt
type: Thing
has-abstract: Mobile agent systems often require sophisticated cooperation and coordination during error detection and recovery. In this paper we propose novel fault tolerance mechanisms that support co-operative exception handling in such systems. The paper demonstrates how mechanisms like these can be formally developed and analysed. We start with identifying the typical modes of failures in agents and analysing possible failure and recovery scenarios in mobile systems. Stepwise refinement is used as our formal framework for top-down development and verification. Using the framework we formally verify the essential model properties, such as interoperability, local and global state consistency and termination of error recovery. Our approach provides developers with formal generic patterns for incorporating fault- tolerance mechanisms into mobile agent systems. We also demonstrate how the results of our formal development can be instantiated and reused in developing real-world agent software.in a search for resources or other agents. Openness allows a number of agents from different administration domains to form multi-agent applications. Anonymity is collateral to openness and equally essential for decoupling, security and scalability. Agents are autonomous because they participate in a multi-agent application to achieve their own goals, so they do not have to follow protocols enforced by the third parties.
has-date: http://www.aktors.org/ontology/date#2008
has-title: Formal development of cooperative exception handling for mobile agent systems

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

http://deploy.rkbexplorer.com/id/person-67d71eedbc5ef09b046b2e8fbcfaafcd-f887968656cb3615ccbf1cecdcc28756
family-name: Ligot
given-name: Olivier
full-name: Olivier Ligot
type: Person
type: Thing

http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#8
has-date: http://www.aktors.org/ontology/date#2008
has-title: Abstract State Machines, B and Z, First International Conference ABZ 2008
type: Conference-Proceedings-Reference
type: Thing

eprints-42
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/42
type: Book-Section-Reference
has-title: Declarative Programming for Verification: Lessons and Outlook
has-date: http://www.aktors.org/ontology/date#2008
type: Thing
has-url: http://deploy-eprints.ecs.soton.ac.uk/42/1/ppdp8k%2Dleuschel.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/42/3/indexcodes.txt

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://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#14
has-date: http://www.aktors.org/ontology/date#2008
has-title: The B Method : From Research to Teaching
type: Conference-Proceedings-Reference
type: Thing

eprints-71
has-date: http://www.aktors.org/ontology/date#2008
has-title: Proceedings of the Fourth International Workshop on Exception Handling Co-located with the Sixteenth ACM SIGSOFT International Symposium on the Foundations of Software Engineering. Atlanta, USA
type: Book-Reference
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/71
type: Thing

eprints-29
has-page-numbers: 128-132
has-url: http://deploy-eprints.ecs.soton.ac.uk/29/1/final.pdf
has-number: 3-4
has-date: http://www.aktors.org/ontology/date#2008
type: Article-Reference
has-title: The connection between two ways of reasoning about partial functions
has-abstract: Undefined terms involving the application of partial functions and operators are common in program specifications and in discharging proof obligations that arise in design. One way of reasoning about partial functions with classical First-order Predicate Calculus (FoPC) is to use a non-strict equality notion so as to insulate logical operators from undefined operands. An alternative approach is to work only with strict (weak) equality but use an alternative Logic of Partial Functions (LPF)—a logic in which the “Law of the Excluded Middle” does not hold. This paper explores the relationships between the theorems that can be proved in the two approaches. The main result is that theorems in LPF using weak equality can be straightforwardly translated into ones that are true in FoPC; translation in the other direction results, in general, in more complicated expressions but in many cases these can be readily simplified. Such results are important if the laudable move towards interworking of formal methods tools is to be sound.
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/29
type: Thing
has-volume: 107
has-url: http://deploy-eprints.ecs.soton.ac.uk/29/3/indexcodes.txt

eprints-79
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/79
has-date: http://www.aktors.org/ontology/date#2008
has-url: http://deploy-eprints.ecs.soton.ac.uk/79/1/Deployment_in_the_Space_Sector.ppt
has-title: Deployment in the Space Sector (WP3 Meeting in Newcastle)
type: Publication-Reference
type: Thing

http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#3
has-date: http://www.aktors.org/ontology/date#2008
has-title: 1st Int. workshop on Software Engineering for Resilient Systems - SERENE 2008
type: Conference-Proceedings-Reference
type: Thing

eprints-37
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/37
type: Proceedings-Paper-Reference
type: Thing
has-title: A Roadmap for the Rodin Toolset
has-date: http://www.aktors.org/ontology/date#2008
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#7
has-page-numbers: 347

http://deploy.rkbexplorer.com/id/person-811a0dd5a16686c64d45155d8fd38429-f1d47c7c5714444e8ab0eea86567945f
family-name: Langbacka
given-name: Thomas
full-name: Thomas Langbacka
type: Person
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-e0638b0e7a15f30831b459e05bcf422e-24435d3d521f22a3b351c36d4e881112
family-name: Pelliccione
given-name: Patrizio
full-name: Patrizio Pelliccione
type: Person
type: Thing

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

eprints-45
has-url: http://deploy-eprints.ecs.soton.ac.uk/45/3/indexcodes.txt
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/45
type: Thing
has-title: ProB gets Nauty: Effective Symmetry Reduction for B and Z Models
has-date: http://www.aktors.org/ontology/date#2008
type: Book-Section-Reference
has-url: http://deploy-eprints.ecs.soton.ac.uk/45/1/nauty_symIEEE.pdf

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

eprints-24
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/24
has-page-numbers: 3-6
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#11
has-abstract: While pervasive systems offer versatile computing environment, their complexity poses a significant challenge to their developers. Hence ensuring resilience of pervasive systems is an important issue, which should be tackled by adopting rigorous design methods and systems approach. In this short paper we identify the key research directions in engineering pervasive resilient systems and our experience in rigorous development of a multi-agent application called Ambient Campus.
type: Thing
has-title: Towards Rigorous Engineering of Resilient Pervasive Systems
type: Proceedings-Paper-Reference
has-date: http://www.aktors.org/ontology/date#2008

http://deploy.rkbexplorer.com/id/journal-acda9a1406f8212b23b4358bb3b53bf6
has-title: Computer Systems Science and Engineering
type: Publication-Reference
type: Journal
type: Thing

http://deploy.rkbexplorer.com/id/person-f365d2ddb0c152b0ec46b98ff5791b30-60a150c2dda73bc08b136204624e9581
family-name: Wieczorek
given-name: S
full-name: S Wieczorek
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-74
has-url: http://deploy-eprints.ecs.soton.ac.uk/74/3/indexcodes.txt
has-url: http://deploy-eprints.ecs.soton.ac.uk/74/1/Minipilot.pdf
has-title: A Description of a Smallish Part of the BepiColombo (BC) MIXS/SIXS Onboard Instrument SW
type: Thing
has-date: http://www.aktors.org/ontology/date#2008
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/74
type: Book-Reference

http://deploy.rkbexplorer.com/id/publishing-house-760cd418fa57316dffcd1d893e2dc485
has-title: ACM Press
type: Publishing-House
type: Thing

eprints-32
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#2
has-date: http://www.aktors.org/ontology/date#2008
type: Thing
type: Proceedings-Paper-Reference
has-abstract: Exception handling is one of the popular means used for improving dependability and supporting recovery in the Service-Oriented Architecture (SOA). This practical experience paper presents the results of error and fault injection into Web Services. We summarize our experiments with the SOA-specific exception handling features provided by the two development kits: the Sun Microsystems JAX-RPC and the IBM WebSphere Software Developer Kit for Web Services. The main focus of the paper is on analyzing exception propagation and performance as the major factors affecting fault tolerance (in, particular, error handling, and fault diagnosis) in Web Services.
has-title: Experimenting with Exception Propagation Mechanisms in Service-Oriented Architectures
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/32
has-url: http://deploy-eprints.ecs.soton.ac.uk/32/1/WEH08%2Dfinal%2Dgorbenko%2Dnew.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/32/3/indexcodes.txt

http://deploy.rkbexplorer.com/id/person-4b0e2fe4dc9536c172ce5ffde97a60e1-8806e8c24f5928c142562d222e11cd15
family-name: Fitzgerald
given-name: John
given-name: John S
full-name: John S Fitzgerald
full-name: John Fitzgerald
type: Person
type: Thing

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

eprints-3
type: Thing
has-date: http://www.aktors.org/ontology/date#2008
has-url: http://deploy-eprints.ecs.soton.ac.uk/3/4/indexcodes.txt
has-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.
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#12
type: Proceedings-Paper-Reference
has-title: UML-B and Event-B: an integration of languages and tools
has-url: http://deploy-eprints.ecs.soton.ac.uk/3/1/SnBu08.pdf
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/3

http://deploy.rkbexplorer.com/id/person-11bb90b850ca37883e6ec5b20277dfbc-7cd32e7c2c44839d94bf9fabd3843354
family-name: Kienzle
given-name: Joerg
full-name: Joerg Kienzle
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/person-3fb4896f644bd36a8d0fceccbf36cffb-dc13195dc4195f8b7bfc38cec60f5f11
family-name: Yadav
given-name: Divakar
full-name: Divakar Yadav
type: Person
type: Thing

http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#6
has-date: http://www.aktors.org/ontology/date#2008
has-title: ICFEM 2008
type: Conference-Proceedings-Reference
type: Thing

http://deploy.rkbexplorer.com/id/person-996b1d7634e684278c8f31402f3cde4b-614513275406bc0b0ddb6f4cb1edf313
family-name: Mikhaylichenko
given-name: Alexey
full-name: Alexey Mikhaylichenko
type: Person
type: Thing

eprints-40
type: Thing
has-url: http://deploy-eprints.ecs.soton.ac.uk/40/3/indexcodes.txt
has-number: 75
has-title: From Rigorous Requirements Engineering to Formal System Design of Safety-Critical Systems
has-date: http://www.aktors.org/ontology/date#2008
has-url: http://deploy-eprints.ecs.soton.ac.uk/40/1/EN75%2DCETIC.pdf
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/40
type: Article-Reference
has-page-numbers: 22-23

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-abcead70f0b5ec446831dd965ec1575c-89409d45bc48e9c6b4f92d78e4f48d38
family-name: Samia
given-name: Mireille
full-name: Mireille Samia
type: Person
type: Thing

http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#12
has-date: http://www.aktors.org/ontology/date#2008
has-title: The IASTED International Conference on Software Engineering - SE2008
type: Conference-Proceedings-Reference
type: Thing

http://deploy.rkbexplorer.com/id/person-62d22a3b5022b714fa1353f356f87f63-f75143588b8fae0ff978c098c09eb14b
family-name: Fontaine
given-name: Marc
full-name: Marc Fontaine
type: Person
type: Thing

eprints-69
has-date: http://www.aktors.org/ontology/date#2008
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/69
type: Thing
has-title: SERENE '08: Proceedings of the 2008 RISE/EFTS Joint International Workshop on Software Engineering for Resilient Systems. Newcastle upon Tyne, United Kingdom
type: Book-Reference

eprints-27
has-url: http://deploy-eprints.ecs.soton.ac.uk/27/1/deploy%2Dercim%2Dnews.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/27/3/indexcodes.txt
has-date: http://www.aktors.org/ontology/date#2008
has-title: DEPLOY: industrial deployment of advanced system engineering methods for high productivity and dependability
type: Article-Reference
has-title: DEPLOY: Industrial Deployment of Advanced System Engineering Methods for High Productivity and Dependability
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#4
type: Proceedings-Paper-Reference
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/68
has-volume: 33
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/65
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/27
has-page-numbers: 54-55
has-number: 74
type: Thing
has-number: 6

http://deploy.rkbexplorer.com/id/journal-909da9e25c4eb9f11c4cce95ab4e96fb
has-title: Information Processing Letters
type: Publication-Reference
type: Journal
type: Thing

http://deploy.rkbexplorer.com/id/person-f69773a9f7b219563f6042cba17cba7e-24435d3d521f22a3b351c36d4e881112
family-name: Guelfi
given-name: Nicolas
full-name: Nicolas Guelfi
type: Person
type: Thing

http://deploy.rkbexplorer.com/id/publishing-house-0d8f980802951b40c8fa9e3d5de6d587
has-title: ACM
type: Publishing-House
type: Thing

http://deploy.rkbexplorer.com/id/person-35afd411ed3300230573bf5e14dbf722-89409d45bc48e9c6b4f92d78e4f48d38
family-name: Leuschel
given-name: Michael
full-name: Michael Leuschel
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

http://deploy.rkbexplorer.com/id/person-2d6231db28f4181af04f0da3297e97c5-8806e8c24f5928c142562d222e11cd15
family-name: Larsen
given-name: Peter Gorm
full-name: Peter Gorm Larsen
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://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#1
has-date: http://www.aktors.org/ontology/date#2008
has-title: Proceedings of the Fourth IEEE International Symposium on Service-Oriented System Engineering
type: Conference-Proceedings-Reference
type: Thing

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

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

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

eprints-35
has-date: http://www.aktors.org/ontology/date#2008
type: Thing
type: Proceedings-Paper-Reference
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/35
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#8
has-title: UML-B: A plug-in for the Event-B tool set
has-page-numbers: 347

http://deploy.rkbexplorer.com/id/journal-6a83bff266dcda6cb1b64eb9827bad26
has-title: Electronic Workshops in Computing
type: Publication-Reference
type: Journal
type: Thing

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

http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#9
has-date: http://www.aktors.org/ontology/date#2008
has-title: ABZ2008
type: Conference-Proceedings-Reference
type: Thing

eprints-43
type: Thing
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/43
type: Book-Section-Reference
has-date: http://www.aktors.org/ontology/date#2008
has-url: http://deploy-eprints.ecs.soton.ac.uk/43/3/indexcodes.txt
has-url: http://deploy-eprints.ecs.soton.ac.uk/43/1/abz08_invited.pdf
has-title: The High Road to Formal Validation: Model Checking High-Level versus Low-Level Specifications

eprints-22
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/22
has-title: Modelling and proof of a Tree-structured File System
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#6
has-url: http://deploy-eprints.ecs.soton.ac.uk/22/1/TreeFileSys.zip
type: Proceedings-Paper-Reference
type: Thing
has-date: http://www.aktors.org/ontology/date#2008

http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#15
has-date: http://www.aktors.org/ontology/date#2008
has-title: Formal Methods 2008
type: Conference-Proceedings-Reference
type: Thing

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

eprints-72
has-url: http://deploy-eprints.ecs.soton.ac.uk/72/3/indexcodes.txt
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/72
has-url: http://deploy-eprints.ecs.soton.ac.uk/72/1/BepiColombo_%2D_Modelling_Approach.pdf
type: Publication-Reference
has-title: BepiColombo - Modelling Approach (Issue I)
has-date: http://www.aktors.org/ontology/date#2008
type: Thing

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

eprints-30
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/30
has-url: http://deploy-eprints.ecs.soton.ac.uk/30/3/indexcodes.txt
has-title: Animation-based Validation of a Formal Model of Dynamic Virtual Organisations
has-date: http://www.aktors.org/ontology/date#2008
has-url: http://deploy-eprints.ecs.soton.ac.uk/30/1/ewic_fm07_paper3.pdf
type: Thing
has-abstract: We describe a study of the industrial use of animation in the analysis of a formal model of information flow in dynamic virtual organisations (VOs). A generic formal model of a VO structure composed of autonomous agents sharing information was developed using the Vienna Development Method (VDM). An exploratory environment was also developed in which the model was animated via an interpreter running an application-specific script developed with domain experts. A user interface encouraged interaction with the model without requiring exposure to the formalism. The use of the interface and model by domain experts was observed and recorded before debrief, allowing us to draw conclusions about the suitability of formal models for exploring, in an industrial setting, the design of policies governing VOs.
type: Article-Reference
has-volume: http:/

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-0c4837098db3478289c268a564772ec1-1877e60711d1072ffc125775995a8f18
family-name: Voisin
given-name: Laurent
full-name: Laurent Voisin
type: Person
type: Thing

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

http://deploy.rkbexplorer.com/id/publishing-house-24bf203b7782e726523348726c757595
has-title: IEEE Press
type: Publishing-House
type: Thing

http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#4
has-date: http://www.aktors.org/ontology/date#2008
has-title: SERENE '08: Proceedings of the 2008 RISE/EFTS Joint International Workshop on Software Engineering for Resilient Systems
type: Conference-Proceedings-Reference
type: Thing

eprints-38
type: Article-Reference
has-title: An Incremental Development of the Mondex System in Event-B
type: Thing
has-page-numbers: 61-77
has-volume: 20
has-date: http://www.aktors.org/ontology/date#2008
has-number: 1
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/38

http://deploy.rkbexplorer.com/id/person-b2507ee03dd851e13e36574d0016852b-42c34226e0b90947e96c48ab8fb7c5c3
family-name: Sere
given-name: Kaisa
full-name: Kaisa Sere
type: Person
type: Thing

http://lodlaundromat.org/.well-known/genid/92cd0210a83f25cb7ae720b2c8f2d65e#10
has-date: http://www.aktors.org/ontology/date#2008
has-title: Refine 2008 - International Refinement Workshop
type: Conference-Proceedings-Reference
type: Thing

http://deploy.rkbexplorer.com/id/person-94ed68858b7a9f61c035225dfc72b6e9-7cd32e7c2c44839d94bf9fabd3843354
family-name: Garcia
given-name: Alessandro
full-name: Alessandro Garcia
type: Person
type: Thing

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

eprints-67
has-number: 5
type: Article-Reference
has-date: http://www.aktors.org/ontology/date#2008
type: Thing
has-title: Engineering Fault Tolerant Systems (Special issue)
has-volume: 23
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/67
has-page-numbers: 1-3

eprints-46
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/46
has-date: http://www.aktors.org/ontology/date#2008
has-url: http://deploy-eprints.ecs.soton.ac.uk/46/1/afadl07_french_tsi.pdf
has-page-numbers: 1065-1084
has-url: http://deploy-eprints.ecs.soton.ac.uk/46/3/indexcodes.txt
type: Article-Reference
has-title: La validation de modèles Event-B avec le plug-in ProB pour RODIN
type: Thing
has-abstract: The B-method, as well as its offspring Event-B, are both formal methods used for the development of critical computer systems whose correctness has to be formally established. Event-B now spurs the Rodin platform, which is based on Eclipse and can be extended via plug-ins. In this paper, we present two such plug-ins; one for animation and one for interactive proof support, called a disprover. Both plug-ins are based on the ProB tool as well as a translation of Event-B to classical B. With our new plug-ins, Rodin has now become a platform where a user can animate, prove and disprove formal models in an integrated fashion.

http://deploy.rkbexplorer.com/id/journal-f1d129854777266fc2757df0224eae5c
has-title: TSI
type: Publication-Reference
type: Journal
type: Thing

eprints-75
has-web-address: http://deploy-eprints.ecs.soton.ac.uk/id/eprint/75
has-date: http://www.aktors.org/ontology/date#2008
has-url: http://deploy-eprints.ecs.soton.ac.uk/75/1/RodinPlatformExperience.html
has-title: Problems in using RODIN platform in DEPLOY WP3
type: Book-Reference
type: Thing