Abstract Cloud computing is a conceptual paradigm that is receiving a great deal of interest from a variety of major commercial organisations. By building systems which run within cloud computing infrastructures, problems related to scalability and availability can be reduced. At the time of writing, Amazon Web Services (AWS) [1] is one of the most widely used infrastructures. AWS consists of a number of different components, which can be used in combination or alone. One usage model is to use Elastic Compute Cloud instances to process information and to use the Simple Queue Service (SQS) to handle requests and responses.
Abstract Alloy [Jac02a] is a widely adopted relational modeling language. Its appealing syntax and the support provided by the Alloy Analyzer [Jac02b] tool make model analysis accessible to a public of non-specialists. A model and property are translated to a propositional formula, which is fed to a SAT-solver to search for counterexamples. The translation strongly depends on user-provided bounds for data domains called scopes - the larger the scopes, the more confident the user is about the correctness of the model. Due to the intrinsic complexity of the SAT-solving step, it is often the case that analyses do not scale well enough to remain feasible as scopes grow.
Abstract We propose what is essentially a recasting of Circus, the Z-and-CSP-based concurrent language for refinement, into a B context by means of a modest extension of classical B which introduces a new structural component called a reactive-B process. This specifies the channels via which the process can communicate with its environment, and actions by which its behaviour is specified. Such actions are expressed in a new action notation in the same syntactic spirit as B’s Abstract Machine Notation, but with a similar Unifying Theories of Programming relational semantics to that of the actions of Circus. Crucially, by including ordinary abstract machines these reactive-B processes can also acquire persistent state, which their actions can manipulate by invoking the operations of those included machines.
Abstract The activities of formal modelling and reasoning are closely related. But while the rigour of building formal models brings significant benefits, formal reasoning remains a major barrier to the wider acceptance of formalism within design. Here we propose reasoned modelling critics – a technique which aims to abstract away from the complexities of low-level proof obligations, and provide high-level modelling guidance to designers when proofs fail. Inspired by proof planning critics, the technique combines proof-failure analysis with modelling heuristics. Here, we present the details of our proposal and outline future plans.
Abstract We provide a detailed description of refinement in Event-B, both as a contribution in itself and as a foundation for the approach to simultaneous animation of multiple levels of refinement that we propose. We present an algorithm for simultaneous multi-level animation of refinement, and show how it can be used to detect a variety of errors that occur frequently when using refinement. The algorithm has been implemented in ProB and we applied it to several case studies, showing that multi-level animation is tractable also on larger models.
Abstract This paper introduces the subject of secrecy models development by transformation, with formal validation. In an enterprise, constructing a secrecy model is a participatory exercise involving policy makers and implementers. Policy makers iteratively provide business governance requirements, while policy implementers formulate rules of access in computer-executable terms. The process is error prone and may lead to undesirable situations thus threatening the security of the enterprise. At each iteration, a security officer (SO) needs to guarantee business continuity by ensuring property preservation; as well, he needs to check for potential threats due to policy changes. This paper proposes a method that is meant to address both aspects: the formal analysis of transformation results and the formal proof that transformations are property preserving. UML is used for expressing and transforming models [1], and the Alloy analyzer is used to perform integrity checks [3]. Governance requirements dictate a security policy, that regulates access to information. This policy is implemented by means of secrecy models. Hence, the SO defines the mandatory secrecy rules as a part of enterprise governance model in order to implement security policy. For instance, a secrecy rule may state: higher-ranking officers have read rights to information at lower ranks. Automation helps reduce design errors of combined and complex secrecy models [2]. However, current industry practices do not include precise methods for constructing and validating enterprise governance models. Our research proposes a formal transformation method to construct secrecy models by way of applying transformations to a base UML model (BM). For example, starting from the BM, with only three primitives: Subject/Verb/Object, we can generate RBAC0 in addition to SecureUML [2] model. By way of examples and by means of formal analysis we intend to show that, using our method, a SO is able to build different types of secrecy models and validate them for consistency, in addition to detecting scenarios resulting from unpreserved properties.
Abstract One of the key research challenges in autonomic computing is to define rigorous mathematical models for specifying, analyzing, and verifying high-level self-* policies. This paper presents the FracToy formal methodology to specify self-configurable component-based systems, and particularly both their component-based architectural description and their self-configuration policies. This rigorous methodology is based on the first-order relational logic, and is implemented with the Alloy formal specification language. The paper presents the different steps of the FracToy methodology and illustrates them on a self-configurable component-based example.
Abstract The B method [1] is gaining visibility in formal methods community due to excellent support for refinement. However, the traceability between the requirements and the formal model is still an issue of this method. To overcome this issue, different solutions have been proposed by researchers. In [2], the authors have presented a traceability between KAOS requirements and B. A mixed solution using natural language and UML-B has been proposed by [3]. However, these approaches use non-standard artifacts for requirement specifications, which we consider a disincentive for convincing designers to adopt formal methods since they must spend time to learn them. So, we propose an approach for mapping requirements to B models from use cases [4], which can be considered as the de-facto industry standard for requirement specifications. We propose that use case scenario sentences must be written using a controlled natural language (CNL) described according our use case transaction definition, which is based on Ochodek’s transaction model [5]. We consider that a transaction is a sequence of four steps actions in a scenario, which starts from the actors request (U) and finishes with the system response (SR). The system validation (SV) and system expletive (SE) actions must also occur within the starting and ending action. The actions help to find out the B components. So, from SV actions we extract the preconditions and from SE actions we derive the operations names and the postconditions. We are not interested in the automatic translation of use cases for formal specifications since there are many natural language ambiguity problems. The intention of our work is to take the use cases as a guideline for starting B specifications. Our main goal is to create a new and complete development process (including deliverables artifacts), namely Be Velopment, for B focusing on agility/usability and we believe that use cases seem to be a good start point.
Abstract Event-B does not provide specific support for the modelling of problems that require some structuring, such as, local variables or sequential ordering of events. All variables need to be declared globally and sequential ordering of events can only be achieved by abstract program counters. This has two unfortunate consequences: such models become less comprehensible — we have to infer sequential ordering from the use of program counters; proof obligation generation does not consider ordering — generating too many proof obligations (although these are usually trivially discharged). In this article we propose a method for specifying structured models avoiding, in particular, the use of abstract program counters. It uses a notation that mainly serves to drive proof obligation generation. However, the notation also describes the structure of a model explicitly. A corresponding graphical notation is introduced that visualises the structure of a model.
Abstract Recently, Space Systems Finland has undertaken formal Event B development of a part of the on-board software for the BepiColombo space mission. As a result, lack of modularisation mechanisms in Event B has been identified as a serious obstacle to scalability. One of the main benefits of modularisation 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, modularisation 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 modularisation. We demonstrate how our approach can support reuse in the formal development in the space domain.