Abstract State Machines, Alloy, B and Z

How should a software system be verified? Much research is currently focused on attempts to show that code modules meet their specifications. This is important, but bugs in code are not the weakest link in the chain. The larger problems are identifying and articulating critical properties, and ensuring that the components of a system - not only software modules, but also hardware peripherals, physical environments, and human operators - together establish them. Another common assumption is that verification must take system design and implementation as given. I’ll explain the rationale for, and elements of, a new approach to verification, in which design is driven by verification goals, and verification arguments are structured in a way that exposes the relationship between critical properties and the components that ensure them.

Traditionally, simulation is used to perform probabilistic analysis. However, it provides less accurate results and cannot handle large-scale problems due to the enormous CPU time requirements. Recently, a significant amount of formalization has been done in higher-order logic that allows us to conduct precise probabilistic analysis using theorem proving and thus overcome the limitations of the simulation. Some major contributions include the formalization of both discrete and continuous random variables and the verification of some of their corresponding probabilistic and statistical properties. This paper describes the infrastructures behind these capabilities and their utilization to conduct the probabilistic analysis of real-world systems.

A natural encoding of synchronous message exchange with direct wait-control is proved to be equivalent in a distributed environment to a refinement which uses semaphores to implement wait control. The proof uses a most general scheduler, which is left as abstract and assumed to satisfy a few realistic, explicitly stated assumptions. We hope to provide a scheme that can be implemented by current theorem provers.

Scenario-driven requirement specifications are widely used to capture and represent high-level requirements. Timed Use Case Maps (TUCM) is a high-level scenario based modeling technique that can be used to capture and integrate behavioral and time-related aspects at a high level of abstraction. The Timed Use Case Maps language assumes durational semantics which introduces semantic variation points when dealing with concurrent flows. In this paper, we introduce three AsmL-based operational semantics, making the semantic variation points of TUCM concurrent behavior explicit. The proposed semantics are illustrated using an example.

Scenarios have been used in various stages of the software development process, in particular in requirement elicitation and software validation and testing. In this paper, we present our recent work on the specification, design and implementation of a

CoreASM

plugin, called Bârun, that offers a powerful scripting language on top of the

CoreASM

extensible modeling framework and tool environment for high-level design and analysis of distributed systems. We illustrate the application of Bârun and demonstrate its features using an industrial case study.

This paper presents

AsmetaSMV

, a model checker for Abstract State Machines (ASMs). It has been developed with the aim of enriching the ASMETA (ASM mETAmodeling) toolset – a set of tools for ASMs – with the capabilities of the model checker NuSMV to verify properties of ASM models written in the AsmetaL language. We describe the general architecture of AsmetaSMV and the process of automatically mapping ASM models into NuSMV programs. As a proof of concepts, we report the results of using AsmetaSMV to verify temporal properties of various case studies of different characteristics and complexity.

The SystemC UML profile is a modeling language designed to lift features and abstractions of the SystemC/C++ class library to the UML level with the aim of improving the current industrial System-on-Chip design methodology. Its graphical syntax and static semantics were defined following the “profile” extension mechanism of the UML metamodel, while its behavioral semantics was given in natural language. This paper provides a precise and executable semantics of the

SystemC Process State Machines

that are an extension of the UML state machines and are part of the SystemC UML profile to model the reactive behavior of the SystemC processes. To this purpose, we used the meta-hooking approach of the ASM-based semantic framework, which allows the definition of the dynamic semantics of metamodel-based languages and of UML profiles.

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.

Safety properties of a system may be specified by constraining the sequences of interactions of the system with its environment. This paper shows how to encode specifications in such a style using Alloy.

We extend the Alloy language with the standard imperative constructs; we show the mix of declarative and imperative constructs to be useful in modeling dynamic systems. We present a translation from our extended language to the existing first-order logic of the Alloy Analyzer, allowing for efficient analysis of models.

Despite the rich literature on network architecture and communication system design, the current practice of describing architectures remains informal and idiosyncratic. Such practice has evolved based on idiomatic terminology and hence, it is failing to provide a formal framework for representing and for reasoning about network architectures. This state of affairs has led to the overloading of architectural terms, and to the emergence of a large body of network architecture proposals with no clear indication of their cross similarities, their compatibility points, their unique properties, and their architectural performance and soundness. Formalizing network architectural descriptions is therefore a timely contribution, and this paper presents a first step in that direction. The paper builds upon architectural style modeling concepts from the software engineering field, and applies them to the network architecture space. Our approach is presented through a case study detailing a formal model for a common class of network architectures. The model uses a simple declarative language based on relations and first-order logic.

The Java programming language has been widely described as secure by design. Nevertheless, a number of serious security vulnerabilities have been discovered in Java, particularly in the component known as the Bytecode Verifier. This paper describes a method for representing Java security constraints using the Alloy modeling language. It further describes a system for performing a security analysis on any block of Java bytecodes by converting the bytes into relation initializers in Alloy. Any counterexamples found by the Alloy analyzer correspond directly to insecure code. Analysis of a real world malicious applet is given to demonstrate the efficacy of the approach. This type of analysis represents a significant departure from standard malware detection methods based on signatures or anomaly detection.

Identifying a minimal unsatisfiable core in an Alloy model proved to be a very useful feature in many scenarios. We extend this concept to

hot core

, an approximation to unsat core that enables the user to obtain valuable feedback when the Alloy’s sat-solving process is abruptly interrupted. We present some use cases that exemplify this new feature and explain the applied heuristics. The NP-completeness nature of the verification problem makes hot core specially appealing, since it is quite frequent for users of the Alloy Analyzer to stop the analysis when some time threshold is exceeded. We provide experimental results showing very promising outcomes supporting our proposal.

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.

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.

Smart Card applications usually require reliability and security to avoid incorrect operation or access violation in transactions and corruption or undue access to stored information. A way of reaching these requirements is improving the quality of the development process of these applications. BSmart is a method and a corresponding tool designed to support the formal development of the complete Java Card smart card application, following the B formal method.

Software development in B and Event-B generates proof obligations that have to be discharged using theorem provers. The cost of such developments therefore depends directly on the degree of automation and efficiency of theorem proving techniques for the logics in which these lemmas are expressed. This paper presents and formalizes an approach to transform a class of proof obligations generated in the Rodin platform in a language that can be addressed by state-of-the-art SMT solvers. The work presented in the paper handles proof obligations with Booleans, integer arithmetics and basic sets.

Symmetry reduction is a model checking technique that can help alleviate the problem of state space explosion, by preventing redundant state space exploration. In previous work, we have developed three effective approaches to symmetry reduction for B that have been implemented into the

ProB

model checker, and we have proved the soundness of our state symmetries. However, it is also important to show our techniques are sound with respect to standard model checking, at the algorithmic level. In this paper, we present a retrospective B development that addresses this issue through a series of B refinements. This work also demonstrates the valuable insights into a system that can be gained through formal modelling.

We study the definition and the mapping of an AADL subset: the so called synchronous subset. We show that the data port protocol used for delayed and immediate connections between periodic threads can be interpreted in a synchronous way. In this paper, we formalize this interpretation and study the development of its mapping such that the original synchronous semantics is preserved. For that purpose, we use refinements through the Event B method.

This paper presents

Matelas

, a B predicate calculus definition for social networking, modelling social-network content, privacy policies, social-networks friendship relations, and how these relations effect users’ policies. The work presented in this paper is part of an ongoing work that aims at using several formal methods tools and techniques to develop a full-fledged social-network service implementing stipulated policies. Although we employed Atelier B to write

Matelas

, plans are to port it to Event B and to use Rodin to implement the social-network application.

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.

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.

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.

We present here a case study developing a parallel program. The approach that we use combines

refinement

and

decomposition

techniques. This involves in the first step to abstractly specify the aim of the program, then subsequently introduce shared information between sub-processes via refinement. Afterwards, decomposition is applied to split the resulting model into sub-models for different processes. These sub-models are later independently developed using refinement. Our approach aids the understanding of parallel programs and reduces the complexity in their proofs of correctness.

We investigate the use of ClawZ, a suite of tools for the verification of implementations of control laws, to construct formal models for control systems in the area of communications and signal-processing intensive applications. Whereas ClawZ has been successfully applied to verify control components in avionic systems, special requirements need to be identified and addressed to extend its use to the aforementioned application domain. This gives rise to several extensions, which we explain and subsequently validate by constructing the Z model of a software-defined radio communication device. The experience reported provides insight into general issues surrounding the use and extension of ClawZ.

The topic of

access control

has received a new lease of life in recent years as the need for assurance that the

correct

access control policy is in place is seen by many as crucial to providing assurance to individuals that their data is being treated appropriately. This trend is likely to continue with the increase in popularity of social networking sites and shifts to ‘cloud’-like commercial services: in both contexts, a clear statement of “who can do what” to one’s data is key in engendering trust. While approaches such as role-based access control (RBAC) provide a degree of abstraction, therefore increasing manageability and accessibility, policy languages such as the XML-based XACML provide greater degrees of expressibility—and, as a result, increased complexity. In this paper we explore how the mutual benefits of both RBAC and XACML, and Alloy and Z, may be used to best effect. RBAC is used as an accessible conceptual model; XACML is used as a language of implementation. Our concern is to facilitate the construction and reuse of role-based policies, which may subsequently be deployed in terms of XACML. We wish to provide assurance that these representations and transformations are, in some sense, correct. To this end, we consider formal models of both RBAC and XACML in terms of Z. We also describe how we have taken initial steps in utilising the Alloy Analyzer tool to provide a level of assurance that the two representations are consistent.

Many authors have drawn parallels between the relational model of data and the formal description technique Z, yet none of these contributions have managed to be both close to the relational model in terms of providing a practical means of database design and fully formal in terms of providing an appropriate metamodel. We compare these various formalisms, and suggest how the use of the formal template approach of Amálio

et al

might help to overcome some of the issues faced. We demonstrate the application of this work via a short case study, and suggest further enhancements to the template language.

Few tools are available to help with the difficult task of validating that a Z specification captures its intended meaning. One tool that has been proven to be useful for validating specifications is the Alloy Analyzer, an interactive tool for checking and visualising Alloy models. However, Z specifications need to be translated to Alloy notation to make use of the Alloy Analyzer. These translations have been performed manually so far, which is a cumbersome and error-prone activity. The aim of this paper is to explore to what extent this process can be automated.

The paper identifies a subset of Z that can be straightforwardly translated to Alloy, and the translation for this subset is formalised. More complex constructs, like schemas, are harder to translate. The paper gives a brief overview of the problems, and discusses alternative translation approaches.

We aim at extending the B language in order to build ASM programs which are correct with respect to B-like logical specifications. On the one hand, the main strengths of the B formal method are: i) the ability to express logical statements, and ii) the construction of a correct implementation by refinement. On the other hand, from our viewpoint, the striking aspects of ASM are the non-bounded outer loop that can reach the fixed point of a program and the power to express naturally any kind of (sequential) algorithms.

In software verification,

scope-bounded

checking of programs has become an effective technique for finding subtle bugs. Given bounds (that are iteratively relaxed) on input size and length of execution paths, a program and its correctness specifications are translated into a formula, which is solved using off-the-shelf solvers – a solution to the formula is a counterexample to the correctness specification.

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.

Software architecture researchers have long assumed that architecture independent application descriptions can be mapped to architectures in many styles, that results vary in quality attributes, and that the choice of a style is driven by consideration of such attributes. In our previous work [1],

we

demonstrated the feasibility of formally treating architectural style as an independent variable. Given an application description and architectural style description in Alloy [3], we map them to software architecture description that refines the given application in conformance with the given style. To represent a map, we extend a traditional architectural style description (in Alloy) with predicates for mapping application descriptions in a given style to architectural descriptions in the given style. These predicates take application descriptions as parameters and define relationships required to hold between them and computed architectural descriptions. Given an application description, and a map, Alloy computes corresponding architectural descriptions guaranteed to conform to the given architectural style. This paper extends our earlier work to aspect-oriented structures. In doing so, we describe an aspect-enabled application description style and a map taking application descriptions in this style to pipe-and-filter architectures. We use the Alloy Analyzer to compute architecture descriptions, represented as satisfying solutions to the constraints of a map given an application description. The

A2A

transformer application, developed in our research group, then converts the Alloy-computed architecture to an architecture description in a traditional architecture description language (ADL): here, AspectualACME[2].

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.

While several different techniques utilize specifications to check correctness of programs before they are deployed, the use of specifications in deployed software is more limited, largely taking the form of runtime checking where assertions form a basis for detecting erroneous program states and terminating erroneous executions in failures. Recent approaches [1] proposed constraint-based repair where data structure constraints are used to repair erroneous states. However, data structure constraints are too weak a form of specification for error recovery in general. We have developed a specification-based approach for data structure repair, which allows repairing erroneous executions in deployed software by repairing erroneous states. The key novelty is our support for rich behavioral specifications, such as those that relate pre-states with post-states to accurately specify expected behavior and hence to enable precise repair.

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.

The aim of this paper is to give some feedback about the B specification [1] of a localization software component which is one of the most critical parts in the land transportation system. The main difficulties when we develop a localization component is: (i) to find the correct algorithm that merges positioning data (ii) to take into account all the properties we have to deal with. At this stage, we think that a semi formal model such as KAOS [2], a goal-based requirements engineering method, will be very useful in order to have guidelines on how to do. For that, we will just focus on the architecture of the B specifications and how using KAOS help us to build it. Since goals play an important role in requirements engineering process, rather than establishing traceability from the KAOS requirements model as a whole, we propose to establish traceability from individual goals that are part of the KAOS goal model. The main idea is to specify a correspondence rule between each concept of the goal model and B elements. Up to now, we consider only functional goals of type Achieve [2]. A B machine is associated to each goal. This machine contains an operation that “realizes” the goal; i.e. it describes the “work” to perform to reach the goal, in terms of generalized substitutions. The refinement of a goal is represented by a B refinement machine that refines the machine; the abstract operation is refined by a concrete one. This operation is built by combining operations of the machines that correspond to the sub-goals of the more abstract goal and are included in the B machine via the inclusion relationship. The nature of the combination depends on the goal refinement pattern (Milestone, AND, OR). The reader can refer to [3] for more details. The main contribution of our approach is that it establishes the first brick toward the construction of the bridge between the nonformal and the formal worlds as narrow and concise as possible. Furthermore, by discharging the proof obligations generated by the B refinement process, we can prove some properties of consistency on the goal model. Regarding the different KAOS goal model concepts, we need now to consider the translation of the concepts of domain properties and non functional goals.

There are two available approaches to automatically generate implementation code from timed automata model. The first approacch is implemented and attached to TIMES tool [1]. We will call this approach “TIMES approach”. While the second approach is based on using B-method [2] and its available code generation tool [3]. We will call this approach “B-method approach”. We select the model of the production cell to be used as a case study for the comparison between these two approaches. The same production cell model has been used against both approaches. The B-method approach generates platform independent code [4]. So we select the generated code using TIMES to be platform independent too for the comparison purpose. For the B-method approach, we use the deterministic semantic of timed automata which is used for TIMES code generation as given in [5]. This semantic controls the selection of the next executed function. The using of this deterministic mechanism is generally not needed for the code generated by the B-method approach. But we use it as it is the implemented mechanism for the TIMES approach. So we select to use it for comparison purpose. By running the implementation code generated using the B-method approach, it works fine as far as we run and no property violation could be found. On the other hand the code generated using TIMES approach runs successfully for the first 10 action transitions and then it progresses the time infinitely. This means that the system deadlocked, so it violates the first property of the model. While the first property is to guarantee that the system is deadlock free. This deadlock is due to the mishandling of the committed and urgent states [6]. The introduced comparison gave a result that the approach based on the using of B-method generates a verified code (by mean of simulation) and handles more timed automata features.

The use of formal methods for software development is escalating over the period of time. The input to this formal specification phase is often the documents obtained during the requirements analysis activity which are either textual or semi-formal. Now there is a traceability gap between analysis and specification phases as verification of the semi-formal analysis model is difficult because of poor understandability of lower level of formalism of verification tools and validation of the formal specification is difficult for customers due to their inability to understand formal models. Our objective is to bridge this gap by a gradual introduction of formalism into the requirement model in order to facilitate its validation.We analyse our requirements with KAOS (Knowledge Acquisition in autOmated Specification) [1] which is a goal-oriented methodology for requirements modeling, then we translate the KAOS goal model, following our derived precise semantics [3], into an Event-B [2] formal specification, and finally we rigourously animate the obtained specification in order to validate its conformance to original requirements with the approach defined in [4].

The Service-Oriented Architectures (SOA) are increasingly used in various application domains. Nowadays various Services operate on the Web and access various critical resources such as databases. These services are called transactional web services when they perform transactional actions. This kind of Services must verify the relevant constraints related to transactional systems. In our work, we focus on web services described with BPEL [1].

Event-B [1] is a formalism for discrete system modelling. The Rodin platform [2] 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 theory developer with deciding whether a given rule should be applied automatically.

In a model-based testing approach as well as for the verification of properties by model-checking, B models provide an interesting solution. But for industrial applications, the size of their state space often makes them hard to handle. To reduce the amount of states, an abstraction function can be used, often combining state variable elimination and domain abstractions of the remaining variables. This paper illustrates a computer aided abstraction process that combines syntactic and semantic abstraction functions. The first function syntactically transforms a B event system

M

into an abstract one

A

, and the second one transforms a B event system into a Symbolic Labelled Transition System (SLTS). The syntactic transformation suppresses some variables in

M

. This function is correct in the sense that

A

is refined by

M

. A process that combines the syntactic and semantic abstractions has been experimented. It significantly reduces the time cost of semantic abstraction computation. This abstraction process allows for verifying safety properties by model-checking or for generating abstract tests. These tests are generated by a coverage criteria such as all states or all transitions of an SLTS.

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-off development since much effort 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.

Component-based software engineering is a practical approach to address the issue of building large software by combining existing and new components. However, building reliable software systems from components requires to verify the consistency of components and the correctness of their assemblies.

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.

An important frequent task in both Z and B is the proof of verification conditions (VCs). In Z and B, VCs can be predicates to be discharged as a result of refinement steps, some proof about initialization properties or domain checking. Ideally, a tool that supports any Z and B technique should automatically discharge as many VCs as possible. Here, we present

ZB2SMT

, a Java package designed to clearly and directly integrate both Z and B tools to the satisfiability module theory (SMT) solvers such as veriT [1], a first-order logic (FOL) theorem prover that accepts the SMT syntax [4] as input. By having the SMT syntax as target we are able to easily integrate with further eleven automatic theorem provers.

ZB2SMT

is currently used by Batcave [2], an open source tool that generates VCs for the B method and

CRefine

[3], a tool that supports the Circus refinement calculus. Much of the VCs generated to validate the refinement law applications, are based on FOL predicates. Hence,

CRefine

uses the

ZB2SMT

package to automatically prove such predicates. The package integrates elements of Z and B predicates in a common language and transforms these predicates into SMT syntax. In this process, a SMT file is generated containing the predicate and some definitions. It is sent to a chosen SMT solver which yields a Boolean value for the predicate or it can be sent to several SMT solvers in a parallel approach. In order to improve the performance of the proof system,

ZB2SMT

has a module that can call different instances of solvers at different computers, according to a configuration file. It improves the proof process by allowing different strategies to be performed in parallel, reducing the verification time.

Software engineering diagrams are hard to verify and formally analyse, often due to inadequately defined diagram semantics: the semantics often does not enable formal analysis, or may be under specified to a degree that does not allow useful properties to be checked.