12th European Workshop on Dependable Computing (EWDC 2009)
21st IFIP Int. Conference on Testing of Communicating Systems and the 9th Int. Workshop on Formal Approaches to Testing of Software TESTCOM/FATES 2009
Applying Model Checking to Generate Model-based Integration Tests from Choreography Models
Choreography models describe the communication protocols between services. Testing of service choreographies is an important task for the quality assurance of service-based systems as used e.g. in the context of service-oriented architectures (SOA). The formal modeling of service choreographies enables a model-based integration testing (MBIT) approach. We present MBIT methods for our service choreography modeling approach called Message Choreography Models (MCM). For the model-based testing of service choreographies, MCMs are translated into Event-B models and used as input for our test generator which uses the model checker ProB.
Publication export from Deploy
This ontology contains information detailing publications held by Deploy
From Goal-Oriented Requirements to Event-B Specifications
In goal-oriented requirements engineering methodologies, goals are structured into refinement trees from high-level system-wide goals down to fine-grained requirements assigned to specific software/ hardware/human agents that can realise them. Functional goals assigned to software agents need to be operationalised into specification of services that the agent should provide to realise those requirements. In this paper, we propose an approach for operationalising requirements into specifications expressed in the Event-B formalism. Our approach has the benefit of aiding software designers by bridging the gap between declarative requirements and operational system specifications in a rigorous manner, enabling powerful correctness proofs and allowing further refinements down to the implementation level. Our solution is based on verifying that a consistent Event-B machine exhibits properties corresponding to requirements.
SAL, Kodkod, and BDDs for Validation of B Models. Lessons and Outlook.
PROB is a model checker for high-level B and Event-B models based on constraint-solving. In this paper we investigate alternate approaches for validating high-level B models using alternative techniques and tools based on using BDDs, SAT-solving and SMT-solving. In particular, we examine whether PROB can be complemented or even supplanted by using one of the tools BDDBDDB, Kodkod or SAL.
Frameworks for designing and implementing dependable systems using Coordinated Atomic Actions: A comparative study
International Conference on Formal Engineering Methods - ICFEM 09
Joint Working IEEE/IFIP Conference on Software Architecture 2009 & European Conference on Software Architecture 2009
Using Event-B Refinement to Verify a Control Strategy
Agent technology offers a number of advantages over traditional distributed systems, such as asynchronous communication, anonymity of individual agents and ability to change operational context. However, it is notoriously difficult to ensure dependability of agent systems. In this paper we present a formal approach for the top-down development of fault tolerant middleware for agent systems. We demonstrate how to develop the middleware that besides providing agent coordination is also able to cope with their failures. We focus on handling agent crushes and transient faults caused by volatile communication environment. We argue that formal development of middleware with integrated fault tolerance mechanisms has potential to enhance dependability of an agent system.
Fault Tolerant Middleware for Agent Systems: A Refinement Approach
Turning Shoe Information to Knowledge of Technology and Deals
Aktors
en_US
Take a look at Nike and Adidas Shoe technology, and use Finish Line coupons to save money on athletic shoes and performance apparel
website
Event-B is a general purpose formal development method suitable for the design and detailed development of safety-critical systems. Being a data-driven formalism, it lacks any control ﬂow constructs. This turns out to be a limitation for systems with rich control ﬂow properties. In Event-B, control ﬂow information has to be embedded into guards and event actions and this results in an entanglement of control ﬂow and functional specification with the additional downside of extra model variables. This paper proposes a method for extending Event-B models with an new viewpoint portraying control ﬂow properties of a model. The novelty of the work is in relying solely on theorem proving to demonstrate the consistency of control ﬂow and main Event-B specification. The focus is placed on the practicality of working with such an extension and also on achieving proof economy. A detailed formal treatment of the method is presented and illustrated with a case study. A proof of concept implementation for the RODIN platform is brieﬂy discussed.
Methods, Models and Tools for Fault Tolerance
Knowledge Systems Institute Graduate School
Distributed information systems are critical to the functioning of many businesses; designing them to be dependable is a challenging but important task. We report our experience in using formal methods to enhance processes and tools for development of business information software based on service-oriented architectures. In our work, which takes place in an industrial setting, we focus on the configuration of middleware, verifying application-level requirements in the presence of faults. In pilot studies provided by SAP, we used the Event-B formalism and the open Rodin tools platform to prove properties of models of business protocols and expose weaknesses of certain middleware configurations with respect to particular protocols. We then extended the approach to use models automatically generated from diagrammatic design tools, opening the possibility of seamless integration with current development environments. Increased automation in the verification process, through domain-specific models and theories, is a goal for future work. KEYWORDS: Verification, Fault Modelling, Service- Oriented Architectures, Event-B, Tool Support
Formal Modelling and Analysis of Business Information Applications with Fault Tolerant Middleware
We examine the the industrial application of formal methods using data gathered in a review of 62 projects taking place over the last 25 years. The review suggests that formal methods are being applied in a wide range of application domains, with increasingly strong tool support. Significant challenges remain in providing usable tools that can be integrated into established development processes; in education and training; in taking formal methods from first use to second use, and in gathering and evidence to support informed selection of methods and tools.
Industrial Practice in Formal Methods: a Review
MIDAS (Microprocessor Instruction and Data Abstraction System) is a specification of an Instruction Set Architecture (ISA) capable of executing binary images compiled from the C language. It was developed to demonstrate a methodology for formal construction of various ISAs in Event-B via a generic model. It is intended to be representative of typical microprocessor ISAs, but using a minimal number of defined instructions, in order to make complete refinement practical. The intention is to simplify the number and complexity of the defined instructions at the cost of compiler complexity, run-time performance and code density, without compromising representativeness. There are two variants: a stack-based machine and a randomly accessible register array machine. The two variants employ the same instruction codes, the differences being limited to register file behavior.
MIDAS: A Formally Constructed Virtual Machine
The two dependability means considered in this paper are rigorous design and fault tolerance. It can be complex to rigorously design some classes of systems, including fault tolerant ones, therefore appropriate abstractions are needed to better support system modelling and analysis. The abstraction proposed in this paper for this purpose is the notion of operation mode. Modes are formalised and their relation to a state-based formalism in a refinement approach is established. The use of modes for fault tolerant systems is then discussed and a case study presented. Using modes in state-based modelling allows us to improve system structuring, the elicitation of system assumptions and expected functionality, as well as requirement traceability.
A Code Generation Example for Event-B: A Shared Channel with Concurrent Read/Writers
We present an example involving processes reading and writing to a shared channel. A channel may have at most one reader reading, and at most one writer writing at any one time; however a number of processes may be waiting to read from, or write to, the channel. In our most abstract model data is transferred as a block in a single atomic step. A write event constitutes moving a block from a writing process to a channel buffer; and a read event constitutes moving a block from a channel buffer to a reader. The atomicity of the read and write activity is altered in the refinement - we introduce blocks that are made up of packets, and each packet is written to the channel individually. This allows the reader to begin reading as soon as there is data in the channel - without the writer having to complete the data transfer. We continue with an overview of our implementation notation (OCB), and show the implementation level specification for the concurrent read/writers example. We then present details of the implementation level refinement that results from the translation of the OCB model into Event-B, and also discuss details of the source code generated by the Java translator.
Towards a Cookbook for Modelling and Refinement of Control Problems
Rodin User and Developer Workshop 2009 - Extended Abstracts
Fourth Latin-American Symposium on Dependable Computing (LADC)
Component integration plays a decisive role in service-oriented architectures (SOAs). The technical implementation must faithfully reflect business and enterprise integration requirements. This implies a good understanding of the globally observable message choreography but also of how messages are handled by the involved components and by the SOA middleware. In this paper we present a solution to the problem of keeping global and local viewpoints in synchronization via a common message choreography metamodel. As main contribution we shape various interpretations of global choreographies, which were left unspecified in state-of-the-art choreography approaches. We have implemented a message choreography modeling (MCM) environment incorporating these contributions. MCM seamlessly complements existing models at SAP. We show how service integration experts, architects, and testers can benefit from our approach that enables model-based integration testing and model verification facilities.
Viewpoints for Modeling Choreographies in Service-Oriented Architectures
Step-wise Development of Resilient Ambient Campus Scenarios
Operation modes are useful structuring units that facilitate design of several safety-critical systems such as such as avionic, transportation and space systems. Although some support to the construction of modal systems can be found in the literature, modelling abstractions for the formal specification, analysis and correct construction of modal systems are still lacking. This paper discusses existing support for the construction of modal systems and proposes both a formalisation and a reﬁnement notion for modal systems. A modal system, specified using the proposed abstractions, can be realised using different specification languages. Complementing the contribution, we define the requirements for an Event-B model to realise a modal system specification. A case study illustrates the proposed approach.
Modal Systems: Specification, Reﬁnement and Realisation
Proceedings 14th IEEE International Conference on Engineering of Complex Computer Systems ICECCS 2009.
Formal methods use mathematical models for analysis and verification at any part of the program life-cycle. We describe the state of the art in the industrial use of formal methods, concentrating on their increasing use at the earlier stages of specification and design. We do this by reporting on a new survey of industrial use, comparing the situation in 2009 with the most significant surveys carried out over the last 20 years. We describe some of the highlights of our survey by presenting a series of industrial projects, and we draw some observations from these surveys and records of experience. Based on this, we discuss the issues surrounding the industrial adoption of formal methods. Finally, we look to the future and describe the development of a Verified Software Repository, part of the worldwide Verified Software Initiative. We introduce the initial projects being used to populate the repository, and describe the challenges they address.
Towards Automated Reﬁnement: Patterns in Event B
Improving reliability of cooperative concurrent systems with exception flow analysis
Developers of fault-tolerant distributed systems need to guarantee that fault tolerance mechanisms they build are in themselves reliable. Otherwise, these mechanisms might in the end negatively affect overall system dependability, thus defeating the purpose of introducing fault tolerance into the system. To achieve the desired levels of reliability, mechanisms for detecting and handling errors should be developed rigorously or formally. We present an approach to modeling and verifying fault-tolerant distributed systems that use exception handling as the main fault tolerance mechanism. In the proposed approach, a formal model is employed to specify the structure of a system in terms of cooperating participants that handle exceptions in a coordinated manner, and coordinated atomic actions serve as representatives of mechanisms for exception handling in concurrent systems. We validate the approach through two case studies: (i) a system responsible for managing a production cell, and (ii) a medical control system. In both systems, the proposed approach has helped us to uncover design faults in the form of implicit assumptions and omissions in the original specifications.
Goal-Oriented Requirements Engineering in Action in the Transportation Sector
Rodin: An Open Toolset for Modelling and Reasoning in Event-B