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

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

http://deploy.rkbexplorer.com/id/publishing-house-42323f69e76b548d6c4e37823e1800d8
has-title: Space Systems Finland Ltd
type: Publishing-House

eprints-209
has-url: http://deploy-eprints.ecs.soton.ac.uk/209/1/cookbookCC.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/209/3/indexcodes.txt
has-title: Evaluation of a Guideline by Formal Modelling of Cruise Control System in Event-B
type: Article-Reference
has-date: http://www.aktors.org/ontology/date#2010

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#24
has-date: http://www.aktors.org/ontology/date#2010
has-title: ABZ 2010
type: Conference-Proceedings-Reference

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

eprints-280
has-url: http://deploy-eprints.ecs.soton.ac.uk/280/1/1210.pdf
has-date: http://www.aktors.org/ontology/date#2010
has-title: Ideas for a high-level proof strategy language
has-url: http://deploy-eprints.ecs.soton.ac.uk/280/3/indexcodes.txt
type: Book-Reference

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

http://deploy.rkbexplorer.com/id/person-d7dbb6233258a2c325b71f5c9950a942-c6121c94b8a1721fd1f5cb7a3468f699
family-name: Pierce
full-name: Ken G Pierce
given-name: Ken G
type: Person

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

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

http://deploy.rkbexplorer.com/id/publishing-house-b62ba5c6efe74dec9dee2d6a295782fa
has-title: Good Friends Publishing Company
type: Publishing-House

eprints-259
has-url: http://deploy-eprints.ecs.soton.ac.uk/259/3/indexcodes.txt
type: Book-Section-Reference
has-title: Patterns for Refinement Automation
has-url: http://deploy-eprints.ecs.soton.ac.uk/259/1/main%2Dfmco%2Dbook%2D2010.pdf
has-date: http://www.aktors.org/ontology/date#2010

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

http://deploy.rkbexplorer.com/id/person-ae957c2a39fb378f7a574cdf93007f64-464ffb6358c731ae1f29dea088b5a48a
family-name: Jones
full-name: C B Jones
given-name: C B
type: Person

http://deploy.rkbexplorer.com/id/person-8a80d4a207a35942ab527c105c8c1118-b484af6b452fe58c721bccc325b8be40
family-name: Wendland
full-name: Marc-Florian Wendland
given-name: Marc-Florian
type: Person

http://deploy.rkbexplorer.com/id/person-e10b16a7536dd9758fd467c8103109f1-425c9eaf03e275ffac7f26894a88af35
family-name: Ireland
full-name: Andrew Ireland
given-name: Andrew
type: Person

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

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

eprints-167
has-abstract: An executable "DEPLOY Satellite" specification in the form of Ada source code that has statement numbering comments. The presence of statement numbering comments is the only difference with respect to http://deploy-eprints.ecs.soton.ac.uk/166/.
has-url: http://deploy-eprints.ecs.soton.ac.uk/167/1/depsat_v15_01%2D01%2D2010numbered.zip
has-date: http://www.aktors.org/ontology/date#2010
has-title: DEPLOY Satellite (an Attitude and Orbit Control System) Specification, Version 15
type: Publication-Reference

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#11
has-date: http://www.aktors.org/ontology/date#2010
has-title: ABZ2010
type: Conference-Proceedings-Reference

http://deploy.rkbexplorer.com/id/person-f8358d7a10e754fecb1022af45e3a82f-7761785b67e20f13f0de88bceba84ded
family-name: Stefanescu
full-name: Alin Stefanescu
given-name: Alin
type: Person

http://deploy.rkbexplorer.com/id/publishing-house-73b36f5d83a8104b94dc3bfb0a6a5ea0
has-title: School of Computing Science, Newcastle University
type: Publishing-House

eprints-267
has-abstract: Event-B is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. In this article we present the Rodin modelling tool that seamlessly integrates modelling and proving. We outline how the Event-B language was designed to facilitate proof and how the tool has been designed to support changes to models while minimising the impact of changes on existing proofs. We outline the important features of the prover architecture and explain how well-definedness is treated. The tool is extensible and configurable so that it can be adapted more easily to different application domains and development methods.
has-date: http://www.aktors.org/ontology/date#2010
type: Article-Reference
has-title: Rodin: An Open Toolset for Modelling and Reasoning in Event-B

http://deploy.rkbexplorer.com/id/person-dbc218bd8f9016ee59e4ef694cdd767b-10a3c9ebf1c83daf50e78d053d482570
family-name: de Boer
full-name: Frank S de Boer
given-name: Frank S
type: Person

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

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

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

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#19
has-date: http://www.aktors.org/ontology/date#2010
has-title: Workshop on B Dissemination [WOBD] Satellite event of SBMF 2010
type: Conference-Proceedings-Reference

eprints-325
has-date: http://www.aktors.org/ontology/date#2010
has-title: Augmenting Formal Development of Control Systems with Quantitative Reliability Assessment
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#8
type: Proceedings-Paper-Reference

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

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#6
has-date: http://www.aktors.org/ontology/date#2010
has-title: FMCO Formal Methods for Components and Objects
type: Conference-Proceedings-Reference

eprints-254
has-url: http://deploy-eprints.ecs.soton.ac.uk/254/1/bio9_5.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/254/3/indexcodes.txt
has-date: http://www.aktors.org/ontology/date#2010
has-title: Insight, inspiration and collaboration
type: Book-Section-Reference

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

http://deploy.rkbexplorer.com/id/person-d29b58142ad13b6399b3197e61489c5e-b484af6b452fe58c721bccc325b8be40
family-name: Wieczorek
full-name: Sebastian Wieczorek
given-name: Sebastian
type: Person

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

http://deploy.rkbexplorer.com/id/person-a332837300e6dc253f974243adc47f02-b484af6b452fe58c721bccc325b8be40
family-name: Bauer
full-name: Thomas Bauer
given-name: Thomas
type: Person

http://deploy.rkbexplorer.com/id/person-bc0a824c56e4d5cff78f3e2341193260-c9b3d688f9eb36b538eba6aaf9ec0f1c
family-name: Roscoe
full-name: A W Roscoe
given-name: A W
type: Person

eprints-183
has-url: http://deploy-eprints.ecs.soton.ac.uk/183/1/From_Problem_Frames_to_HJJ.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/183/3/indexcodes.txt
has-url: http://www.cs.ncl.ac.uk/research/pubs/trs/papers/1163.pdf
has-date: http://www.aktors.org/ontology/date#2010
has-title: From problem frames to HJJ
type: Book-Section-Reference

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#27
has-date: http://www.aktors.org/ontology/date#2010
has-title: Proceedings of the 7th International Conference on the Quality of Information and Communications Technology
type: Conference-Proceedings-Reference

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

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

eprints-283
has-url: http://deploy-eprints.ecs.soton.ac.uk/283/1/1185.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/283/3/indexcodes.txt
has-date: http://www.aktors.org/ontology/date#2010
has-title: What Can the pi-calculus Tell Us About the Mondex Purse System?
type: Book-Reference

http://deploy.rkbexplorer.com/id/publishing-house-453543ec8eb93a87a1ba4719815efc54
has-title: CEA
type: Publishing-House

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

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

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

http://deploy.rkbexplorer.com/id/person-d79d639c5d728e947411eacd4bc6b69f-a332b9a35de579f148d1f388140cadc7
family-name: Maamria
full-name: Issam Maamria
given-name: Issam
type: Person

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

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#14
has-date: http://www.aktors.org/ontology/date#2010
has-title: First Deploy Technical Workshop
type: Conference-Proceedings-Reference

http://deploy.rkbexplorer.com/id/person-2e8cc9ad2f615dd5401ac36ec7ba34eb-cd604f0ec3d7df4762fb1ce8f777d4ed
family-name: Olszewska
full-name: Marta Olszewska
given-name: Marta
type: Person

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#1
has-date: http://www.aktors.org/ontology/date#2010
has-title: Integrated Formal Methods iFM 2010
type: Conference-Proceedings-Reference

eprints-270
has-url: http://deploy-eprints.ecs.soton.ac.uk/270/1/stv10.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/270/3/indexcodes.txt
has-title: Improving Testing of Enterprise Systems by Model-based Testing on Graphical User Interfaces
has-abstract: Software development and testing of Enterprise Resource Planning (ERP) systems demands dedicated methods to tackle its special features. As manual testing is not able to systematically test ERP systems due to the involved complexity, an efficient testing approach should be automatic. Since the underlying business processes of enterprise systems are realized at the level of the user interface (UI), system level testing is the dominant testing approach. The recent architectural shift to service-based enterprise systems demands to apply blackbox testing techniques. Model-based testing is a method that enables a high degree of automation for black-box testing, but the current research and practice usually does not address the UI. In this paper we describe the state of the art and state of the practice in order to motivate further research activities in this area.
type: Proceedings-Paper-Reference
has-page-numbers: 352 - 357
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#25
has-date: http://www.aktors.org/ontology/date#2010

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

eprints-249
type: Proceedings-Paper-Reference
has-title: Specification Metrics for Event-B Developments
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#3
has-url: http://deploy-eprints.ecs.soton.ac.uk/249/1/OlSe_Conquest2010.pdf
has-page-numbers: 1-12
has-date: http://www.aktors.org/ontology/date#2010
has-abstract: In this paper we define several metrics for Event-B specifications in order to as-sess the maintainability of a rigorous system in its early development stage. We perform measurements of physical features of the specification. Moreover, we derive metrics like difficulty of constructing a specification or effort needed for its creation. The specification is investigated in the perspective of its syntactical characteristics. We base our metrics on the Event-B language primitives, namely operators and operands that we regard meaningful for our measurement model. We also use statistics about proof obligations in our metrics, as we consider the proving activity as a vital element in the process of creating a specification. Presented metrics are applied to a number of Event-B specifications, both their dynamic and static parts. They are examined in order to empirically con-firm appropriateness for management purposes. Obtained results are analysed in a perspective of an abstract specification and its consecutive refinements.
has-url: http://deploy-eprints.ecs.soton.ac.uk/249/3/indexcodes.txt

eprints-228
has-url: http://www.inf.ethz.ch/research/disstechreps/techreports
has-date: http://www.aktors.org/ontology/date#2010
has-title: How to Interpret Failed Proofs in Event-B
type: Book-Reference

eprints-207
has-url: http://deploy-eprints.ecs.soton.ac.uk/207/1/final%2Diceccs2010.pdf
has-date: http://www.aktors.org/ontology/date#2010
type: Book-Section-Reference
has-url: http://deploy-eprints.ecs.soton.ac.uk/207/3/indexcodes.txt
has-title: Patterns for Modelling Time and Consistency in Business Information Systems

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

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

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#22
has-date: http://www.aktors.org/ontology/date#2010
has-title: VSTTE’10 Verified Software: Theories, Tools and Experiments
type: Conference-Proceedings-Reference

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#9
has-date: http://www.aktors.org/ontology/date#2010
has-title: Workshop on Tool Building in Formal Methods - ABZ Conference
type: Conference-Proceedings-Reference

www.aktors.org
locale: en_US
type: website
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
site name: Aktors

eprints-257
has-date: http://www.aktors.org/ontology/date#2010
has-title: Elucidating concurrent algorithms via layers of abstraction and reification
has-volume: online
type: Article-Reference

eprints-236
has-url: http://deploy-eprints.ecs.soton.ac.uk/236/4/indexcodes.txt
has-title: An Approach of Requirements Tracing in Formal Refinement
has-abstract: Formal modeling of computing systems yields models that are intended to be correct with respect to the requirements that have been formalized. The complexity of typical computing systems can be addressed by formal refinement introducing all the necessary details piecemeal. We report on preliminary results that we have obtained for tracing informal natural-language requirements into formal models across refinement levels. The approach uses the WRSPM reference model for requirements modeling, and Event-B for formal modeling and formal refinement. The combined use of WRSPM and Event-B is facilitated by the rudimentary refinement notion of WRSPM, which provides the foundation for tracing requirements to formal refinements. We assume that requirements are evolving, meaning that we have to cope with frequent changes of the requirements model and the formal model. Our approach is capable of dealing with frequent changes, making use of corresponding techniques already built into the Event-B method.
type: Proceedings-Paper-Reference
has-date: http://www.aktors.org/ontology/date#2010
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#22
has-url: http://deploy-eprints.ecs.soton.ac.uk/236/2/2010%2D03_Formal_Modelling_of_Requirements.pdf

http://deploy.rkbexplorer.com/id/person-b3230d099e907edf021055aaaa9a1b86-5d2a834c3bd05f50fd232768499fb5be
family-name: Woodcock
full-name: Jim C P Woodcock
given-name: Jim C P
type: Person

http://deploy.rkbexplorer.com/id/person-d79d639c5d728e947411eacd4bc6b69f-de771e8b33afa6400c994123cadbcdb2
family-name: Maamria
full-name: Issam Maamria
given-name: Issam
type: Person

http://deploy.rkbexplorer.com/id/person-7b5547cabfe90d04bd0ffaffb7a5c374-5b128804bba3eaaed06a0df9ce8fb5ec
family-name: Pierce
full-name: K G Pierce
given-name: K G
type: Person

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

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

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

http://deploy.rkbexplorer.com/id/person-f8358d7a10e754fecb1022af45e3a82f-fc06490f81290a4427a6e7ad4e46811c
family-name: Stefanescu
full-name: Alin Stefanescu
given-name: Alin
type: Person

http://deploy.rkbexplorer.com/id/person-17f57da6ab69267347b65cce2409647d-1920b6efd7de8655de69462b3d80ac8f
family-name: Silva
full-name: Renato Silva
given-name: Renato
type: Person

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

http://deploy.rkbexplorer.com/id/person-a92002e83db2fd767482e4c50871173f-b566d540334e4e76092eaa9d7d5185df
family-name: Bundy
full-name: Alan Bundy
given-name: Alan
type: Person

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

eprints-202
has-abstract: The Rodin platform for Event-B formal modelling is based on a bespoke model repository. While this approach has some advantages it also means that the platform does not benefit from the host of emerging technologies and supporting packages that are freely available for open source modelling frameworks. The Eclipse Modelling Framework (EMF) has emerged as the de-facto standard package upon which to build any Eclipse based modelling tool. In order to make this support available for our Rodin tools we have now engineered a front-end EMF based representation of Event-B.
has-date: http://www.aktors.org/ontology/date#2010
has-title: An EMF Framework for Event-B
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#9
type: Proceedings-Paper-Reference

eprints-194
has-date: http://www.aktors.org/ontology/date#2010
has-title: A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#24
type: Proceedings-Paper-Reference

http://deploy.rkbexplorer.com/id/person-ae957c2a39fb378f7a574cdf93007f64-5b128804bba3eaaed06a0df9ce8fb5ec
family-name: Jones
full-name: C B Jones
given-name: C B
type: Person

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#17
has-date: http://www.aktors.org/ontology/date#2010
has-title: Abstract State Machines (ASM), Alloy, B and Z Conference (ABZ 2010)
type: Conference-Proceedings-Reference

eprints-294
has-date: http://www.aktors.org/ontology/date#2010
has-title: Rewriting and Well-Definedness within a Proof System
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#4
type: Proceedings-Paper-Reference

http://deploy.rkbexplorer.com/id/person-e340f053d2703f779131f30017fe3621-80f5c1e394c5f90940b224daf13bcb60
family-name: Jastram
full-name: Michael Jastram
given-name: Michael
type: Person

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#4
has-date: http://www.aktors.org/ontology/date#2010
has-title: Partiality and Recursion in Interactive Theorem Provers PAR-10
type: Conference-Proceedings-Reference

eprints-273
has-url: http://deploy-eprints.ecs.soton.ac.uk/273/2/indexcodes.txt
has-url: http://deploy-eprints.ecs.soton.ac.uk/273/1/Motip2010_proceedings.pdf
has-date: http://www.aktors.org/ontology/date#2010
has-title: Proc. of 3rd Workshop on Model-based Testing in Practice (MOTIP'10)
type: Book-Reference

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

eprints-252
type: Publication-Reference
has-title: A Basis for Feature-Oriented Modelling in Event-B
has-url: http://deploy-eprints.ecs.soton.ac.uk/252/3/indexcodes.txt
has-url: http://deploy-eprints.ecs.soton.ac.uk/252/1/paper_53%2D1.pdf
has-date: http://www.aktors.org/ontology/date#2010
has-abstract: Feature-oriented modelling is a well-known approach for Software Product Line (SPL) development. It is a widely used method when developing groups of related software. With an SPL approach, the development of a software product is quicker, less expensive and of higher quality than a one-oﬀ development since much eﬀort is re-used. However, this approach is not common in formal methods development, which is generally high cost and time consuming, yet crucial in the development of critical systems. With the increase of more complex critical systems, it becomes more important to apply formal methods to the development cycle, and we propose a method that allows the application of SPL development techniques to formal methods. This results in faster and cheaper development of formal systems. Our method combines Event-B [1] and feature models [2]. A feature in a feature model represents a requirement of the product family and is formally described in Event-B using special feature modelling patterns. A feature repre- sented in Event-B is referred to as component. We develop composition rules, which allow components to be composed. Special composition proof obligations allow the veriﬁcation of the composition. The feature model is formed by features which may be associated with Event- B components. A subset of features from the feature model can be selected to form a feature model instance, thereby selecting several of these Event-B com- ponents. These components are composed pair-wise, and composition POs can be discharged to prove properties and to ensure consistency of the composition. The ﬁnal Event-B machine represents the formal speciﬁcation which is associated with the feature model instance and is obtained by composing these components. The motivation of our work is to allow product line development for critical systems. We use traditional product line methods, i.e. feature modelling, and link it with the formal method Event-B. Future work is focussed on amending feat…

http://deploy.rkbexplorer.com/id/person-f78a1026fb4955f88dead8d35bd4695f-10a3c9ebf1c83daf50e78d053d482570
family-name: Bonsangue
full-name: Marcello M Bonsangue
given-name: Marcello M
type: Person

eprints-231
type: Proceedings-Paper-Reference
has-url: http://deploy-eprints.ecs.soton.ac.uk/231/1/cetic%2Dhopes%2Dv2.pdf
has-title: Comparison of the AADL and Event-B Model-Based Tool Chains for Designing Embedded Systems
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#5
has-date: http://www.aktors.org/ontology/date#2010
has-abstract: This paper compares two model-based tool chains support- ing the design of embedded systems. The first one relies on an architecture description language called AADL (Architecture Analysis and Design Language) specially targeting embedded system. The second one is based on a generic notation for system modelling called Event-B which is being deployed in the design of embedded systems, e.g. in the transportation sector. A number of tools supporting similar activities arehighlighted as well as the impact of the characteristics of the respective underlying languages on the global design activity.
has-url: http://deploy-eprints.ecs.soton.ac.uk/231/3/indexcodes.txt

http://deploy.rkbexplorer.com/id/person-e3fec723327ea3df2d744f9feb2e470e-5d2a834c3bd05f50fd232768499fb5be
family-name: Joshi
full-name: Rajev Joshi
given-name: Rajev
type: Person

http://deploy.rkbexplorer.com/id/person-ff2363b46400bb1099d35b70c8ba1942-d31c73297c7f716770acd72786eac9ff
family-name: Rezazadeh
full-name: Abdolbaghi Rezazadeh
given-name: Abdolbaghi
type: Person

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

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

http://deploy.rkbexplorer.com/id/person-11326e7891f57db00e9b0494784be0b5-b484af6b452fe58c721bccc325b8be40
family-name: Eichler
full-name: Hajo Eichler
given-name: Hajo
type: Person

http://deploy.rkbexplorer.com/id/person-55b699e46e50872724b309f9ceeeab1b-cf2c445dce10f3a43a9b40f34aaa026b
family-name: Sorge
full-name: Jennifer Sorge
given-name: Jennifer
type: Person

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

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#25
has-date: http://www.aktors.org/ontology/date#2010
has-title: in Proceedings of 7th Workshop on Systems Testing and Validation
type: Conference-Proceedings-Reference

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

eprints-281
has-url: http://deploy-eprints.ecs.soton.ac.uk/281/1/1220.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/281/3/indexcodes.txt
has-date: http://www.aktors.org/ontology/date#2010
has-title: Semantic Models for a Logic of Partial Functions
type: Book-Reference

http://deploy.rkbexplorer.com/id/person-f8358d7a10e754fecb1022af45e3a82f-cfe0be318da8608234a52a4a42e1f9fd
family-name: Stefanescu
full-name: Alin Stefanescu
given-name: Alin
type: Person

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

eprints-239
has-url: http://deploy-eprints.ecs.soton.ac.uk/239/1/Safecomp_CR.pdf
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#18
type: Proceedings-Paper-Reference
has-date: http://www.aktors.org/ontology/date#2010
has-title: Verifying Mode Consistency for On-Board Satellite Software
has-url: http://deploy-eprints.ecs.soton.ac.uk/239/3/indexcodes.txt
has-abstract: Space satellites are examples of complex embedded systems. Dynamic behaviour of such systems is typically described in terms of operational modes that correspond to the different stages of a mission and states of the components. Components are susceptible to various faults that complicate the mode transition scheme. Yet the success of a mission depends on the correct implementation of mode changes. In this paper we propose a formal approach that ensures consistency of mode changes while developing a system architecture by refinement. The approach relies on recursive application of modelling and refinement patterns that enforce correctness while implementing the mode transition scheme. The proposed approach is exemplified by the development of an Attitude and Orbit Control System undertaken within the ICT DEPLOY project.

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

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

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

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

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#12
has-date: http://www.aktors.org/ontology/date#2010
has-title: ABZ2010
type: Conference-Proceedings-Reference

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

http://deploy.rkbexplorer.com/id/person-3716011872eba04cce281710390d712e-d56122e30820a4a6da448191c6f240aa
family-name: Bryans
full-name: Jeremy Bryans
given-name: Jeremy
type: Person

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

http://deploy.rkbexplorer.com/id/person-5eac220d5f46b0b50a347acb59d26d63-c6121c94b8a1721fd1f5cb7a3468f699
family-name: Verhoef
full-name: Marcel Verhoef
given-name: Marcel
type: Person

http://deploy.rkbexplorer.com/id/person-9322c5c217870fd8dbd7900d50d24533-dceee8401647649976a72d922acc4b47
family-name: Tarasyuk
full-name: Anton Tarasyuk
given-name: Anton
type: Person

eprints-197
has-url: http://deploy-eprints.ecs.soton.ac.uk/197/3/indexcodes.txt
type: Proceedings-Paper-Reference
has-date: http://www.aktors.org/ontology/date#2010
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#10
has-url: http://deploy-eprints.ecs.soton.ac.uk/197/1/wstbfm2010_submission_13.pdf
has-abstract: The Event-B method is a formal approach to modelling systems, using refinement. Initial specification is done at a high level of abstraction; detail is added in refinement steps as the development proceeds toward implementation. In previous work we developed an approach to bridge the gap between abstract specifications and implementations using an implementation level specification notation. In this paper we present details of the tool support for our notation and some of our experiences using the tool.
has-title: Tool Support for Event-B Code Generation

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

http://deploy.rkbexplorer.com/id/person-ff2363b46400bb1099d35b70c8ba1942-b5442c3b3010cbf60a58ac86621b38d0
family-name: Rezazadeh
full-name: Abdolbaghi Rezazadeh
given-name: Abdolbaghi
type: Person

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#20
has-date: http://www.aktors.org/ontology/date#2010
has-title: Workshop on B Dissemination [WOBD] Satellite event of SBMF 2010
type: Conference-Proceedings-Reference

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

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#7
has-date: http://www.aktors.org/ontology/date#2010
has-title: Eighth European Dependable Computing Conference (Fast Abstract Track)
type: Conference-Proceedings-Reference

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

eprints-255
has-url: http://deploy-eprints.ecs.soton.ac.uk/255/1/CBJ%2Dfinal.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/255/3/indexcodes.txt
has-date: http://www.aktors.org/ontology/date#2010
has-title: The role of auxiliary variables in the formal development of concurrent programs
type: Book-Section-Reference

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

http://deploy.rkbexplorer.com/id/person-b38a96a0c3cb2ea288ff8e0a97f94406-bfc0a4cf15c8a22276a435be32b36bbc
family-name: Turner
full-name: Edd Turner
given-name: Edd
type: Person

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

http://deploy.rkbexplorer.com/id/person-eea2488aaebeb98b3faff7eee3e1679e-64c1a5ce5d80419fdeb69a63ec213759
family-name: Lopatkin
full-name: Ilya Lopatkin
given-name: Ilya
type: Person

http://deploy.rkbexplorer.com/id/person-3f9dbc1c4664bdce55454d5776713d96-c9b3d688f9eb36b538eba6aaf9ec0f1c
family-name: Wood
full-name: Ken Wood
given-name: Ken
type: Person

http://deploy.rkbexplorer.com/id/person-b2507ee03dd851e13e36574d0016852b-388bdf18dd3ccec3ba0592e5a069c906
family-name: Sere
full-name: Kaisa Sere
given-name: Kaisa
type: Person

http://deploy.rkbexplorer.com/id/person-84b502de5fe7665d5666bdc31b979c52-94a6318e4501b9a2304f3f7c00fe693d
family-name: De Landtsheer
full-name: Renaud De Landtsheer
given-name: Renaud
type: Person

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

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

http://deploy.rkbexplorer.com/id/person-4c40149d161949fd0dfeb816c9c62d3d-0f00d12e589fe9c190b20815a29b4469
family-name: Fritz
full-name: Fabian Fritz
given-name: Fabian
type: Person

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

http://deploy.rkbexplorer.com/id/person-0876bf55e97cc87d2e43e0292d8bce32-cf2c445dce10f3a43a9b40f34aaa026b
family-name: Poppleton
full-name: Michael Poppleton
given-name: Michael
type: Person

http://deploy.rkbexplorer.com/id/person-c75de35a2b84dc01c88344c450ee23c9-b5442c3b3010cbf60a58ac86621b38d0
family-name: Yeganefard
full-name: Sanaz Yeganefard
given-name: Sanaz
type: Person

http://deploy.rkbexplorer.com/id/person-5f21e4fd2affb33edaa81057b9930156-febd64ae63ff8022c3ff65cb6bc26754
family-name: Väisänen
full-name: Pauli Väisänen
given-name: Pauli
type: Person

http://deploy.rkbexplorer.com/id/person-78c8ef309e36dc4082cf46e29ce685cb-0f00d12e589fe9c190b20815a29b4469
family-name: Illisaov
full-name: Alexei Illisaov
given-name: Alexei
type: Person

eprints-284
has-url: http://deploy-eprints.ecs.soton.ac.uk/284/1/1216.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/284/3/indexcodes.txt
has-date: http://www.aktors.org/ontology/date#2010
has-title: AI4FM: A New Project Seeking Challenges!
type: Book-Reference

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

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

http://deploy.rkbexplorer.com/id/person-530f1bd7939a7fe813d67a09e390e47c-c6121c94b8a1721fd1f5cb7a3468f699
family-name: Wolff
full-name: Sune Wolff
given-name: Sune
type: Person

eprints-263
has-url: http://deploy-eprints.ecs.soton.ac.uk/263/1/modules_wobd.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/263/3/indexcodes.txt
has-date: http://www.aktors.org/ontology/date#2010
has-title: Tutorial on the modularization plugin for Event-B
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#20
type: Proceedings-Paper-Reference

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

eprints-242
type: Proceedings-Paper-Reference
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#1
has-abstract: This paper presents initial results of research aimed at developing methods and tools for multidisciplinary collaborative development of dependable embedded systems. We focus on the construction and analysis by co-simulation of formal models that combine discrete-event specifications of computer-based controllers with continuous-time models of the environment with which they interact. Basic concepts of collaborative modelling and co-simulation are presented. A pragmatic realisation using the VDM and Bond Graph formalisms is described and illustrated by means of an example, which includes the modelling of both normal and faulty behaviour. Consideration of a larger-scale example from the personal transportation domain suggests the forms of support needed to explore the design space of collaborative models. Based on experience so far, challenges for future research in this area are identified.
has-page-numbers: 12-26
has-date: http://www.aktors.org/ontology/date#2010
has-url: http://deploy-eprints.ecs.soton.ac.uk/242/3/indexcodes.txt
has-title: Collaborative Modelling and Co-simulation in the Development of Dependable Embedded Systems
has-url: http://deploy-eprints.ecs.soton.ac.uk/242/1/IFM2010invited.pdf

eprints-200
type: Proceedings-Paper-Reference
has-url: http://deploy-eprints.ecs.soton.ac.uk/200/3/indexcodes.txt
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#13
has-url: http://deploy-eprints.ecs.soton.ac.uk/200/1/decomposition_tool.pdf
has-date: http://www.aktors.org/ontology/date#2010
has-title: Decomposition Tool for Event-B
has-abstract: Two methods have been identified for Event-B model decomposition: shared variable and shared event. The purpose of this paper is to introduce the two approaches and the respective tool support in the Rodin platform. Besides alleviating the complexity for large systems and respective proofs, decomposition allows team development in parallel over the same model which is very attractive in the industrial environment.

eprints-192
has-abstract: Event-B is a formalism for discrete system modelling. The Rodin platform provides a toolset to carry out specification, refinement and proof in Event-B. The importance of proofs as part of formal modelling cannot be emphasised enough, and as such, it is imperative to provide effective tool support for it. An important aspect of this support is the extensibility of the prover, and more pressingly, how its soundness is preserved while allowing extensibility. Rodin has a limited support for adding rules as this requires (a) a deep understanding of the internal architecture and (b) knowledge of the Java language. Our approach attempts to provide support for user-defined proof rules. We initially focus on supporting rewrite rules to enhance the rewriting capabilities of Rodin. To achieve this objective, we introduce a theory construct distinct from contexts and machines. The theory construct provides a platform for the users to define rewrite rules both conditional and unconditional. As part of rule definition, users decide whether the rule is to be applied automatically or interactively. Each defined rule gives rise to proof obligations that serve to verify its conservativity. In this respect, it is required that validity and well-definedness are preserved by rules. After the conservativity of all rules contained in a theory is established, the theory can then be deployed and available to the proving activity. In order to apply rewrite rules, it is necessary to single out applicable rules to any given sequent. This is achieved through a pattern matching mechanism which is implemented as an extension to Rodin. Our approach has two advantages. Firstly, it offers a uniform mechanism to add proof rule without the need to write Java code. Secondly, it provides a means to verify added rules using proof obligations. Our work is still in progress, and research has to be carried out to (a) cover a larger set of rewrite and inference rules, and (b) provide guidelines to help the …
has-date: http://www.aktors.org/ontology/date#2010
has-title: On an Extensible Rule-based Prover for Event-B
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#12
type: Proceedings-Paper-Reference

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

http://deploy.rkbexplorer.com/id/person-ae957c2a39fb378f7a574cdf93007f64-909c9137fa6b956ac7a14fcfd54bcc52
family-name: Jones
full-name: C B Jones
given-name: C B
type: Person

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

http://deploy.rkbexplorer.com/id/person-5f21e4fd2affb33edaa81057b9930156-4700b1e89ef16fa2c5ede9a6ddbf369c
family-name: Väisänen
full-name: Pauli Väisänen
given-name: Pauli
type: Person

http://deploy.rkbexplorer.com/id/person-d29b58142ad13b6399b3197e61489c5e-7761785b67e20f13f0de88bceba84ded
family-name: Wieczorek
full-name: Sebastian Wieczorek
given-name: Sebastian
type: Person

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#15
has-date: http://www.aktors.org/ontology/date#2010
has-title: Formal Methods for Industrial Critical Systems 2010
type: Conference-Proceedings-Reference

http://deploy.rkbexplorer.com/id/person-9322c5c217870fd8dbd7900d50d24533-1f7b40667c626e58819a97d6a15aa06c
family-name: Tarasyuk
full-name: Anton Tarasyuk
given-name: Anton
type: Person

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

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#2
has-date: http://www.aktors.org/ontology/date#2010
has-title: IFM 2010
type: Conference-Proceedings-Reference

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

eprints-250
has-abstract: In this paper we describe our ongoing research on Event-B specification metrics. We focus on the physical features of specification, such as its vocabulary or length for the Event-B machines. We base our metrics on the syntactic properties of the Event-B language, namely operators and operands that we consider meaningful for our measurement model. Presented metrics are applied for a number of Event-B machines. Obtained results can be analysed in a perspective of an abstract machine and its refinements.
type: Proceedings-Paper-Reference
has-title: Towards Event-B Specification Metrics
has-date: http://www.aktors.org/ontology/date#2010
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#14
has-url: http://deploy-eprints.ecs.soton.ac.uk/250/1/Towards_Event%2DB_Specification_Metrics.pdf
has-page-numbers: 81-86
has-url: http://deploy-eprints.ecs.soton.ac.uk/250/2/indexcodes.txt

http://deploy.rkbexplorer.com/id/person-70d8d3a97bb942b9aaff707b21293cec-50c3c5edb895958c46de2a2a1c2c1851
family-name: Grov
full-name: Gudmund Grov
given-name: Gudmund
type: Person

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

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#23
has-date: http://www.aktors.org/ontology/date#2010
has-title: 2nd International Workshop on Software Engineering for Resilient Systems
type: Conference-Proceedings-Reference

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

http://deploy.rkbexplorer.com/id/publishing-house-16a245ab756c0380be53ee4cd9366711
has-title: Newcastle University
type: Publishing-House

http://deploy.rkbexplorer.com/id/person-d7dbb6233258a2c325b71f5c9950a942-e7ebba7cceeb0436f600e0ce29c813cf
family-name: Pierce
full-name: Ken G Pierce
given-name: Ken G
type: Person

eprints-237
has-title: Formal Analysis of BPMN Models using Event-B
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#15
has-url: http://deploy-eprints.ecs.soton.ac.uk/237/3/indexcodes.txt
type: Proceedings-Paper-Reference
has-url: http://deploy-eprints.ecs.soton.ac.uk/237/1/root.pdf
has-date: http://www.aktors.org/ontology/date#2010
has-abstract: The use of business process models has gone far beyond documentation purposes. In the development of business applications, they can play the role of an artifact on which high level properties can be verified and design errors can be revealed in an effort to reduce overhead at later software development and diagnosis stages. This paper demonstrates how formal verification may add value to the specification, design and development of business process models in an industrial setting. The analysis of these models is achieved via an algorithmic translation from the de-facto standard business process modeling language BPMN to Event-B, a widely used formal language supported by the Rodin platform which offers a range of simulation and verification technologies.

http://deploy.rkbexplorer.com/id/publishing-house-68c42c1d0eb8417f33cc29f97b1e4c76
has-title: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany
type: Publishing-House

http://deploy.rkbexplorer.com/id/publishing-house-7eb63c84fd7ce029d6112873054bb3ca
has-title: IEEE Computer Society
type: Publishing-House

http://deploy.rkbexplorer.com/id/journal-e6582f26e38de84a4a66228900f5b842
has-title: NASA Formal Methods Symposium 2010
type: Journal
type: Publication-Reference

http://deploy.rkbexplorer.com/id/person-d79d639c5d728e947411eacd4bc6b69f-d31c73297c7f716770acd72786eac9ff
family-name: Maamria
full-name: Issam Maamria
given-name: Issam
type: Person

eprints-187
has-date: http://www.aktors.org/ontology/date#2010
has-title: 09381 Extended Abstracts Collection — Refinement Based Methods for the Construction of Dependable Systems
type: Book-Reference

eprints-166
has-abstract: An executable "DEPLOY Satellite" specification in the form of Ada source code without any statement numbering comment. The absence of statement numbering comments is the only difference with respect to http://deploy-eprints.ecs.soton.ac.uk/167/.
has-url: http://deploy-eprints.ecs.soton.ac.uk/166/1/depsat_v15_01%2D01%2D2010.zip
has-date: http://www.aktors.org/ontology/date#2010
has-title: DEPLOY Satellite (an Attitude and Orbit Control System) Specification, Version 15 without statement numbering
type: Publication-Reference

http://deploy.rkbexplorer.com/id/person-9d9d92c028217f9fcd5cff3f4f79d45e-1920b6efd7de8655de69462b3d80ac8f
family-name: Hoang
full-name: T Son Hoang
given-name: T Son
type: Person

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#10
has-date: http://www.aktors.org/ontology/date#2010
has-title: WS-TBFM2010
type: Conference-Proceedings-Reference

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

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

http://deploy.rkbexplorer.com/id/person-70d8d3a97bb942b9aaff707b21293cec-425c9eaf03e275ffac7f26894a88af35
family-name: Grov
full-name: Gudmund Grov
given-name: Gudmund
type: Person

eprints-266
has-url: http://deploy-eprints.ecs.soton.ac.uk/266/1/DEP_RP_SSF_R_005_AOCS_SRD_1_0.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/266/3/indexcodes.txt
has-date: http://www.aktors.org/ontology/date#2010
has-title: DEPLOY Work Package 3 Attitude and Orbit Control System Software Requirements Document (DEP-RP-SSF-R-005, Issue 1.0)
type: Book-Reference

http://deploy.rkbexplorer.com/id/person-513e0b6a6151a33e7dd20181746a63ea-1920b6efd7de8655de69462b3d80ac8f
family-name: Pascal
full-name: Carine Pascal
given-name: Carine
type: Person

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

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#18
has-date: http://www.aktors.org/ontology/date#2010
has-title: The 29th International Conference on Computer Safety, Reliability and Security (Safecomp 2010)
type: Conference-Proceedings-Reference

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

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

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

eprints-295
has-date: http://www.aktors.org/ontology/date#2010
has-title: Applying Event-B Atomicity Decomposition to a Multi Media Protocol
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#6
type: Proceedings-Paper-Reference

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

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#5
has-date: http://www.aktors.org/ontology/date#2010
has-title: First Workshop on Hands-on Platforms and tools for model-based engineering of Embedded Systems
type: Conference-Proceedings-Reference

http://deploy.rkbexplorer.com/id/person-2e8cc9ad2f615dd5401ac36ec7ba34eb-388bdf18dd3ccec3ba0592e5a069c906
family-name: Olszewska
full-name: Marta Olszewska
given-name: Marta
type: Person

http://deploy.rkbexplorer.com/id/person-70d8d3a97bb942b9aaff707b21293cec-b566d540334e4e76092eaa9d7d5185df
family-name: Grov
full-name: Gudmund Grov
given-name: Gudmund
type: Person

http://deploy.rkbexplorer.com/id/person-eacb6521b9b182d81d6563e70e5ef802-f440cd04ca8a411bcf9615ecd1babf25
family-name: Fathabadi
full-name: Asieh Salehi Fathabadi
given-name: Asieh Salehi
type: Person

eprints-253
has-abstract: Complex modern applications have to be developed to be dependable to meet their requirements and expectations of their users. An important part of this is their ability to deal with various threats (such as faults in the system environment, operator's mistakes, underlying hardware and software support problems). Development of modern applications is complicated by the need for systematic and rigorous integration of fault tolerance measures. The paper focuses on reuse of fault tolerance modelling. First, it introduces the idea of general modelling templates reflecting abstract views on system behaviour with respect to faults. These templates are used during system detalisation (re�finement) to capture the user's view on system external behaviour. Secondly, it proposes to use a library of concrete modelling patterns allowing developers to systematically integrate speci�c fault tolerance mechanisms (e.g. recovery blocks, checkpoints, exception handling) into the models. The proposed solutions are linked to the Event-B method and demonstrated using a case study.
has-url: http://deploy-eprints.ecs.soton.ac.uk/253/1/serene2010paper.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/253/3/indexcodes.txt
type: Proceedings-Paper-Reference
has-title: On Fault Tolerance Reuse during Reﬁnement
has-date: http://www.aktors.org/ontology/date#2010
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#23

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

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

http://deploy.rkbexplorer.com/id/person-e8b47d23684f76b890def7746877736f-30788a593c3c323c4fc67dc0bd734e4d
family-name: Nummila
full-name: Laura Nummila
given-name: Laura
type: Person

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

http://deploy.rkbexplorer.com/id/person-88ac9e7c52a1f46a46d7512b5a33259e-30788a593c3c323c4fc67dc0bd734e4d
family-name: Räsänen
full-name: Tuomas Räsänen
given-name: Tuomas
type: Person

http://deploy.rkbexplorer.com/id/journal-0ebc61ba8f8d97f30e5ad4992651d384
has-title: International Journal on Software Tools for Technology Transfer (STTT)
type: Journal
type: Publication-Reference

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#26
has-date: http://www.aktors.org/ontology/date#2010
has-title: Dagstuhl-Seminar 10421 "Model-Based Testing in Practice"
type: Conference-Proceedings-Reference

http://deploy.rkbexplorer.com/id/journal-e53391c0707a64727157af4162c14849
has-title: Proceedings of the 15th International Workshop on Formal Methods for Industrial Critical Systems
type: Journal
type: Publication-Reference

eprints-282
has-url: http://deploy-eprints.ecs.soton.ac.uk/282/1/1186.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/282/3/indexcodes.txt
has-date: http://www.aktors.org/ontology/date#2010
has-title: Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification
type: Book-Reference

eprints-261
has-url: http://deploy-eprints.ecs.soton.ac.uk/261/1/flow_plugin.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/261/3/indexcodes.txt
has-date: http://www.aktors.org/ontology/date#2010
has-title: Tutorial on the Flow plugin for Event-B
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#19
type: Proceedings-Paper-Reference

http://deploy.rkbexplorer.com/id/person-ae957c2a39fb378f7a574cdf93007f64-730955c99c8702806ab8c87aa536a990
family-name: Jones
full-name: C B Jones
given-name: C B
type: Person

eprints-240
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#16
type: Proceedings-Paper-Reference
has-url: http://deploy-eprints.ecs.soton.ac.uk/240/1/FMICS_CR.pdf
has-title: Developing Mode-Rich Satellite Software by Refinement in Event B
has-abstract: To ensure dependability of on-board satellite systems, the designers should, in particular, guarantee correct implementation of the mode transition scheme, i.e., ensure that the states of the system components are consistent with the global system mode. However, there is still a lack of scalable approaches to formal verification of correctness of complex mode transitions. In this paper we present a formal development of an Attitude and Orbit Control System (AOCS) undertaken within the ICT DEPLOY project. AOCS is a complex mode-rich system, which has an intricate mode-transition scheme. We show that re�finement in Event B provides the engineers with a scalable formal technique that enables both development of mode-rich systems and proof-based verification of their mode consistency.
has-date: http://www.aktors.org/ontology/date#2010
has-url: http://deploy-eprints.ecs.soton.ac.uk/240/3/indexcodes.txt

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

http://deploy.rkbexplorer.com/id/person-6f9ec19d217e644e673d626ed48a46ac-2b9f533aafca07c81077b8dfbc508221
family-name: Jones
full-name: C B Jones
given-name: C B
type: Person

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

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

http://deploy.rkbexplorer.com/id/person-d29b58142ad13b6399b3197e61489c5e-fc06490f81290a4427a6e7ad4e46811c
family-name: Wieczorek
full-name: Sebastian Wieczorek
given-name: Sebastian
type: Person

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#13
has-date: http://www.aktors.org/ontology/date#2010
has-title: Workshop on Tool Building in Formal Methods - ABZ Conference
type: Conference-Proceedings-Reference

eprints-269
has-page-numbers: 11-11
has-url: http://deploy-eprints.ecs.soton.ac.uk/269/3/indexcodes.txt
has-url: http://deploy-eprints.ecs.soton.ac.uk/269/1/10421_abstracts_collection.2924.pdf
has-title: Model-based testing in the enterprise software domain - past and future initiatives
has-abstract: The testing of enterprise software poses various challenges that require a lot of effort using classical testing approaches. Model-based testing (MBT) showed its potential to improve this on several dimensions including better coverage and increased productivity both on system integration and UI-based scenario testing. In this talk we describe SAP’s recent history of MBT initiatives. A special focus is put on the identified industrial challenges, future directions inside SAP, and proposals for a global alignment of industry and academia.
has-date: http://www.aktors.org/ontology/date#2010
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#26
type: Proceedings-Paper-Reference

eprints-248
has-date: http://www.aktors.org/ontology/date#2010
has-page-numbers: 33-49
has-title: Formal Analysis of BPMN Models Using Event-B
type: Article-Reference

http://deploy.rkbexplorer.com/id/person-5f21e4fd2affb33edaa81057b9930156-5b208005142146151c0f6bf70fced580
family-name: Väisänen
full-name: Pauli Väisänen
given-name: Pauli
type: Person

eprints-206
has-abstract: We present here a case study developing a parallel program. The approach that we use combines reﬁnement and decomposition techniques. This involves in the ﬁrst step to abstractly specify the aim of the program, then subsequently introduce shared information between sub-processes via reﬁnement. Afterwards, decomposition is applied to separate the resulting model into sub-models for different processes. These sub-models are later independently developed using reﬁnement. Our approach aids the understanding of parallel programs and reduces the complexity in their proofs of correctness.
has-date: http://www.aktors.org/ontology/date#2010
has-title: Event-B Decomposition for Parallel Programs
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#11
type: Proceedings-Paper-Reference

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

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

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

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

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#21
has-date: http://www.aktors.org/ontology/date#2010
has-title: ABZ 2010
type: Conference-Proceedings-Reference

eprints-327
has-date: http://www.aktors.org/ontology/date#2010
has-title: Towards Probabilistic Modelling in Event-B
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#2
type: Proceedings-Paper-Reference

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

http://deploy.rkbexplorer.com/id/person-bc0a824c56e4d5cff78f3e2341193260-2b9f533aafca07c81077b8dfbc508221
family-name: Roscoe
full-name: A W Roscoe
given-name: A W
type: Person

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#8
has-date: http://www.aktors.org/ontology/date#2010
has-title: SERENE 2010
type: Conference-Proceedings-Reference

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

eprints-256
has-date: http://www.aktors.org/ontology/date#2010
has-title: Reflections on the work of C.A.R. Hoare
type: Book-Reference

eprints-214
type: Proceedings-Paper-Reference
has-title: System Architecture, Dependability and Modes
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#7
has-url: http://deploy-eprints.ecs.soton.ac.uk/214/1/edcc%2Dfa%2Dfinal.pdf
has-date: http://www.aktors.org/ontology/date#2010
has-url: http://deploy-eprints.ecs.soton.ac.uk/214/3/indexcodes.txt
has-abstract: The mode, defining the specific type of functional behaviour that a system exhibits during its operation, is an important architectural level concept, which has a significant impact on system design, verification and dependability. The notions of modes and mode changes are widely used by the industrial engineers to structure reasoning about different conditions of system functioning. Even though there has been some work on developing modal systems, we still lack a general understanding of how to architect, verify and ensure dependability of such systems. In our work we rely on formal modelling and verification to study intricate relationships between fault tolerance, operation modes and architectural design.

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

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

http://deploy.rkbexplorer.com/id/publishing-house-6ef29839970e95441bb7def816f9f88d
has-title: Deploy Project
type: Publishing-House

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

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

eprints-314
has-url: http://deploy-eprints.ecs.soton.ac.uk/314/1/learning_report_new.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/314/3/indexcodes.txt
has-date: http://www.aktors.org/ontology/date#2010
has-title: DEPLOY Training Evaluation Document
type: Book-Reference

eprints-285
has-abstract: We give a formal development and proof of a known consensus algorithm using stepwise refinement. We begin with an abstract specification of the intended result of the algorithm. The algorithm is developed and proved correct over a number of refinement steps. The proof of correctness is performed concurrently with the development. The development and proof make use of key fault and failure assumptions. The stepwise refinement approach allows us to introduce and prove each property at the most appropriate stage in the development, before detail irrelevant to that property has been added to the model. Finally we introduce an abstract model of a possible network on which the algorithm could be executed.
has-url: http://deploy-eprints.ecs.soton.ac.uk/285/1/root.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/285/3/indexcodes.txt
has-date: http://www.aktors.org/ontology/date#2010
has-title: Developing a Consensus Algorithm using Stepwise Refinement
type: Publication-Reference

http://deploy.rkbexplorer.com/id/person-d29b58142ad13b6399b3197e61489c5e-cfe0be318da8608234a52a4a42e1f9fd
family-name: Wieczorek
full-name: Sebastian Wieczorek
given-name: Sebastian
type: Person

http://deploy.rkbexplorer.com/id/person-db5ab8b84b44d90812c3df7b2c582901-d56122e30820a4a6da448191c6f240aa
family-name: Wei
full-name: Wei Wei
given-name: Wei
type: Person

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

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

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

eprints-193
has-date: http://www.aktors.org/ontology/date#2010
has-title: Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidance
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#21
type: Proceedings-Paper-Reference

eprints-172
has-date: http://www.aktors.org/ontology/date#2010
has-title: Supporting Reuse in Event B Development: Modularisation Approach
has-page-numbers: 174-188
has-url: http://deploy-eprints.ecs.soton.ac.uk/172/3/indexcodes.txt
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#17
type: Proceedings-Paper-Reference
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 benifits 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/172/1/Modules_paper%2Dsubmitted.pdf

http://deploy.rkbexplorer.com/id/person-b4a636d05632d2b81fd95a3b23076612-80f5c1e394c5f90940b224daf13bcb60
family-name: Russo Jr
full-name: Aryldo G Russo Jr
given-name: Aryldo G
type: Person

http://deploy.rkbexplorer.com/id/person-db5ab8b84b44d90812c3df7b2c582901-ca2f57f83de8e826bfd170f765beb365
family-name: Wei
full-name: Wei Wei
given-name: Wei
type: Person

http://deploy.rkbexplorer.com/id/person-fc0e1940b9caed7d31afb39689fed8b4-730955c99c8702806ab8c87aa536a990
family-name: Lovert
full-name: M J Lovert
given-name: M J
type: Person

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#16
has-date: http://www.aktors.org/ontology/date#2010
has-title: 15th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2010)
type: Conference-Proceedings-Reference

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

http://deploy.rkbexplorer.com/id/person-7b5547cabfe90d04bd0ffaffb7a5c374-464ffb6358c731ae1f29dea088b5a48a
family-name: Pierce
full-name: K G Pierce
given-name: K G
type: Person

http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#3
has-date: http://www.aktors.org/ontology/date#2010
has-title: CONQUEST 2010
type: Conference-Proceedings-Reference

eprints-272
has-url: http://deploy-eprints.ecs.soton.ac.uk/272/1/quatic10_camera_ready_version.pdf
has-title: Model-driven Service Integration Testing - A Case Study
type: Proceedings-Paper-Reference
has-date: http://www.aktors.org/ontology/date#2010
paper-in-proceedings: http://lodlaundromat.org/.well-known/genid/e42e1a6a58124c8e44ecd27fad666808#27
has-page-numbers: 292 - 297
has-abstract: This paper presents a case study for the modeling and model-based testing (MBT) of enterprise service choreographies. Our proposed MBT approach uses poprietary models called Message Choreography Models (MCM) as test models. The case study illustrates how MCM-based service integration testing allows to formalize design decisions and enables full integration into an existing industrial test infrastructure by using the concepts of domain specific languages and model transformations. Further, the MBT tools integrated into the testing framework have been compared based on one concrete use case.
has-url: http://deploy-eprints.ecs.soton.ac.uk/272/3/indexcodes.txt

http://deploy.rkbexplorer.com/id/publishing-house-887eab74bfcdae6caf4ae3ee09c939ce
has-title: ETH Zurich, Switzerland
type: Publishing-House

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

eprints-251
has-url: http://deploy-eprints.ecs.soton.ac.uk/251/1/MathExtnSummary.pdf
has-url: http://deploy-eprints.ecs.soton.ac.uk/251/3/indexcodes.txt
has-date: http://www.aktors.org/ontology/date#2010
has-title: Mathematical Extension in Event-B through the Rodin Theory Component
type: Book-Reference