International audience

Cyber-physical systems allow interactions with the physical world using a network of sensors and actuators. They also form basis of future technologies via engaging in innovating within many crucial fields: health, transport, smart grid, etc. Modeling cyber-physical systems requires handling the evolution of continuous measurements. Generally this evolution is repre-sented by ordinary differential equations where the unknown variable denotes a set of functions that depend on a single independent variable. The aim of our work is to propose a correct-by-construction formal approach, based on the refinement technique of the Event-B method, to model and verify such systems. However, Event-B does not handle the resolution of ordinary differential equations. To overcome this limit, we suggest to combine Event-B with the differential equation solver SageMath. This paper presents our approach by means of the hybrid smart heating system case study.

Abstract Many disciplines have adopted component-based principles to avail themselves of the many advantages they bring, especially component reusability. In a short time, the component-based architecture became a renown branch in the IT world and the center of interest of many researchers. Much work has been conducted in this context for the verification of component-based applications (CBAs). However, the main focus has been on the structural aspect of such compositions, while the behavioral aspect has seldom been dealt with. In this paper, our goal is to close this gap and propose a formal approach to verify the behavioral correctness of CBAs. We first define a set of requirements to be satisfied by the structure and the behavior of a CBA, represented by a set of interactions that may occur between their components. Then, we build a formal Event-B model to represent these requirements in a rigorous and non-ambiguous way. The use of the Event-B refinement technique allows us to master the complexity of CBAs by introducing their elements in an incremental manner. The correctness of the development is ensured by establishing a set of proof obligations, under the Rodin platform, and also by animating it with the ProB animator/model checker. The approach is illustrated by a running example.

International audience

Abstract This paper presents SGAC (Solution de Gestion Automatisée du Consentement / automated consent management solution), a new healthcare access control model and its support tool, which manages patient wishes regarding access to their electronic health records (EHR). This paper also presents the verification of access control policies for SGAC using two first-order-logic model checkers based on distinct technologies, Alloy and ProB. The development of SGAC has been achieved within the scope of a project with the University of Sherbrooke Hospital (CHUS), and thus has been adapted to take into account regional laws and regulations applicable in Québec and Canada, as they set bounds to patient wishes: for safety reasons, under strictly defined contexts, patient consent can be overriden to protect his/her life (break-the-glass rules). Since patient wishes and those regulations can be in conflict, SGAC provides a mechanism to address this problem based on priority, specificity and modality. In order to protect patient privacy while ensuring effective caregiving in safety-critical situations, we check four types of properties: accessibility, availability, contextuality and rule effectivity. We conducted performance tests comparison: implementation of SGAC versus an implementation of another access control model, XACML, and property verification with Alloy versus ProB. The performance results show that SGAC performs better than XACML and that ProB outperforms Alloy by two order of magnitude thanks to its programmable approach to constraint solving.

Nowadays, the usefulness of the formal verification and validation of system specifications is well established, at least for critical systems. However, one of the main obstacles to their adoption lies in obtaining the formal specification of the system, and, in the case of refinement-based formal methods such as B System or Event-B, in obtaining the most abstract specification that heads the development of the system. The SysML/KAOS requirements engineering method is proposed to overcome this difficulty. It includes a goal modeling language to model requirements from stakeholders needs. Translation rules from a goal model to a B System specification have already been defined. They allow to obtain a skeleton of the system specification. To complete it, a language has been defined to express the domain model associated to the goal model. Its translation gives the structural part of the B System specification. However, it very often appears that new elements must be added in the B System specification obtained from SysML/KAOS models, discovered for instance when specifying the body of events and/or by using formal validation and/or verification tools. We have therefore defined a set of rules allowing the back propagation, within domain models, of every newly added element. This paper describes these rules and how they are specified in Event-B. Their consistency is proved using the Rodin tool. We show that they are structure preserving: two related elements within the B System specification remain related within the domain model. This is done by proving various isomorphisms between the B System specification and the domain models.

Algebraic State-Transition Diagrams (ASTDs) are extensions of common automata and statecharts that can be combined with process algebra operators like sequence, choice, guard and quantified synchronization. They were previously introduced for the graphical representation, specification and proof of information systems. In an attempt to use ASTDs to specify cyber-attack detection, we have identified a number of missing features in ASTDs. This paper extends the ASTD notation with state variables (attributes), actions on transitions, and a new operator called flow which corresponds to AND states in statecharts and is a compromise between interleaving and synchronization in process algebras. We provide a formal structured operational semantics of these extensions and illustrate its implementation in an OCaml-based interpreter called iASTD and the model checker ProB. Extended ASTDs are illustrated in a case study in cyber attack detection.

Abstract In this paper, we study the information system verification problem as a parameterized verification one. Informations systems are modeled as multi-parameterized systems in a formal language based on the Algebraic State-Transition Diagrams (ASTD) notation. Then, we use the Well Structured Transition Systems (WSTS) theory to solve the coverability problem for an unbounded ASTD state space. Moreover, we define a new framework to prove the effective pred-basis condition of WSTSs, i.e. the computability of a base of predecessors for every states.

Abstract Cloud environments are being increasingly used for the deployment and execution of complex applications and particularly component-based ones. They are expected to provide elasticity, among other characteristics, in order to allow a deployed application to rapidly change the amount of its allocated resources in order to meet the variation in demand while ensuring a given Quality of Service (QoS). However, establishing a correct elastic component-based application is not guaranteed in Cloud. Indeed, applying elasticity mechanisms should preserve functional properties and improve non-functional properties related to QoS, performance and resource consumption. In this paper, we propose an approach for the verification and deployment of elastic component-based applications. Our approach is based on the Event-B formal method. In fact, we formally model the component artifacts using Event-B and we define the Event-B events that model the elasticity mechanisms (scaling up and down) for component-based applications. Furthermore, we formally verify that our approach preserves the semantics of the component-based applications by using the proof obligations and the ProB animator. Once the elastic component-based applications are validated, they can be deployed in a Cloud environment using an elastic deployment framework which we have developed.

Cloud environments are being increasingly used for deploying and executing business processes to provide a high level of performance with low operating cost. Nevertheless, due to the lack of an explicit and formal description of the resource perspective in the existing business processes, the correctness of Cloud resources management can not be verified. The aim of the present work is to offer a formal definition of the resource perspective in business processes as a step towards ensuring a correct and consistent Cloud resource allocation in business process modeling. Concretely, we propose a formalism based on the Event-B language for specifying Cloud resource allocation policies in business process models. This formal specification is used to formally validate the consistency of Cloud resource allocation for process modeling at design time, and to analyze and check its correctness according to user requirements and resource capabilities. In order to show its feasibility, our approach has been tested using a real use case study from an industrial partner.

Nowadays, a growing number of companies are using Cloud Computing to optimize their business processes by using dynamically scalable and often virtualized resources on demand. Nevertheless, due to the lack of explicit and formal description of the resource perspective in existing business processes, Cloud resource allocation behavior cannot be efficiently and correctly managed. In this paper, we aim at formally verifying resource allocation in business processes using Event-B. More precisely, our aim is to specify the resource allocation behavior both at design time and at runtime, and to check its correctness according to users' needs. Our model also takes into account different cloud properties such as elasticity and shareability. In order to show its feasibility, our approach has been tested using a use case study from an industrial partner.

A configurable process model captures a family of similar processes. Such models can be configured to obtain a process variant according to specific requirements. With this aim, several approaches have been proposed for the configuration of process models. Nevertheless, an increasing attention is being paid to achieve this in a sound manner due to the complex inter-dependencies between the configuration decisions. In this work, we aim to guide the process analyst to easily configure process models while preserving soundness. To do so, we propose a formal approach for ensuring correctness of business process configurations while considering structural constraints they have to obey. Specifically, using the Event-B language, we formally define a configurable process model, its correctness-preserving conditions and its configuration constraints.

This paper presents SGAC(Solution de Gestion Automatisée du Consentement, automatised consent management solution), a new healthcare access control model and its support tool, that manages patient wishes regarding access to their electronic health record (EHR). The development of this model has been achieved in the scope of a project with the Sherbrooke University Hospital, and thus has been adapted to take into account laws and regulations applicable in Québec and Canada, as they set bounds to patient wishes: under strictly defined contexts, patient consent can be overridden to protect his/her life. Moreover, since patient wishes and laws can be in conflict, SGAC provides a mechanism to address this problem. Besides, laws do not cover all cases where consent should be overridden to ensure patient safety. To this end, we define a formal model of SGAC which allows for property verification, making it possible to detect these cases. A performance comparison with XACML (WSO2/Balana) is presented and demonstrates the superior performances of SGAC.

Currently, it is well recognized that coupling graphical and formal notations offers several advantages. Indeed, even if a graphical representation permits to design a visual, synthetic and user-friendly view of the system, it may be source of ambiguity and does not permit any formal verification. Formal methods help to remedy these shortcomings by giving a precise semantics to graphical notations such that it becomes possible to verify a large range of properties and even to generate correct implementations. Nevertheless, users cannot take a full advantage of the benefits of such a combination if it is not supported by an automatic tool that liberates them from the tedious translation activity. Following this direction, the present paper describes the main functionalities of a tool that automatically generates a formal secure access control filter for information systems. The goal of the filter is to regulate the access to data of an information system according to a set of static and dynamic rules. Data are described using a UML class diagram, whereas the static and dynamic rules are modeled using SECUREUML and UML activity diagrams respectively. Basically, the tool automatically generates the B formal specification corresponding to these diagrams and the filter.

Abstract This paper proposes a formal approach for generating necessary and sufficient proof obligations to demonstrate a set of dynamic properties using the B method. In particular, we consider reachability, non-interference and absence properties. Also, we show that these properties permit a wide range of property patterns introduced by Dwyer to be expressed. An overview of a tool supporting these approaches is also provided.

In UML modeling, class diagrams permit to capture the entities involved in a system but also the associations they have with each other. These associations are characterized by a multiplicity on each role to state the min-max number of instances of the opposite class that can be linked to each instance of the class associated with the role. Since these multiplicities may be conflicting, it becomes necessary to check the global consistency of a class diagram. Such verification will ensure that it is possible to find an instantiation of the diagram that satisfies all the multiplicities. In this paper, we describe an automatized approach that permits to validate a class diagram by exhibiting a particular instance. Basically, this approach proceeds in two main steps: first, the multiplicities are represented as a mathematical model, then a constraint solver is used to determine whether it has at least one solution. The correctness of the approach, which is supported by an automatic tool, has been carried out using the B formal method.

Recent researches have proposed to retrieve relevant fragments out from whole business processes to build new ones. Although they avoid building business processes from scratch, this task has been performed independently for each process, thus, making resulting fragments handling complicated. In this paper, we propose to merge some given business process fragments in order to facilitate the fragment-based business process design. At the same time, the obtained fragment must keep the behavior of original fragments so as to avoid paths execution blockage while the obtained fragments are integrated as part of a complete process. Our approach presents a systematic merge revolving around the so-called adjacency matrices. Typically used to handle graphs, this mechanism is adapted to business process fragments. We also present some rules to provide the obtained fragments with the behavior of original fragments and avoid inconsistent behaviors that were newly added after the merge.

Two major concerns are emerging, while dealing with building new process functionalities: shortening the development periods and eliminating the risks related to sensitive information leakages and privacy breaches. Indeed, managing business processes in a modern fashion may increase their quality. An effective solution consists in reusing specific fragments of existing business processes. Moreover, the produced fragments need to be declared as safe from a privacy perspective.

Temporal properties are very common in various classes of systems, including information systems and security policies. This paper investigates two verification methods, proof and model checking, for one of the most frequent patterns of temporal property, the absence pattern. We explore two model-based specification techniques, B and Alloy, because of their adequacy for easily specifying systems with complex data structures, like information systems. We propose a first-order, assertion-based, sound and complete strategy to verify the absence pattern. This enables the proof of the absence pattern using conventional first-order provers. We show that the use of assertions significantly increases the size of the models that can be checked, when compared to traditional LTL model checking techniques. The approach is illustrated throughout a case study.

This paper proposes an approach to prove interference freedom for a reach ability property of the form AG (ψ =>; EF Φ) in a B specification. Such properties frequently occur in security policies and information systems. Reach ability is proved by constructing using stepwise algorithmic refinement an abstract program that refines AG (ψ =>; EF Φ). We propose proof obligations to show non-interference, ie, to prove that other operations can be executed in interleaving with this program while preserving the reach ability property, to cater for the multi-user aspect of information systems. Proof obligations are discharged using conventional B provers (eg, Atelier B). Since refinement preserves these reach ability properties and non-interference, proofs can be conducted on abstract machines rather than implementation code.

Formal methods are very useful in software industry and are becoming of paramount importance in practical engineering techniques. They involve the design and the modeling of various system aspects expressed usually through different paradigms. In this paper, we propose to combine two modeling formalisms in order to express both functional and security timed requirements of a system. First, the system behavior is specified based on its functional requirements using TEFSM (timed extended finite state machine) formalism. Second, this model is augmented by applying a set of dedicated algorithms to integrate timed security requirements specified in Nomad language. This language is well adapted to express security properties such as permissions, prohibitions and obligations with time considerations. The resulting secure model can be used for several purposes such as code generation, specification correctness proof, model checking or automatic test generation. In this paper, we applied our approach to a France Telecom(France Telecom is the main telecommunication company in France) Travel service in order to demonstrate its feasibility.

Security and reliability are of paramount importance in designing and building real-time systems because any security failure can put the public and the environment at risk. In this paper, we propose a framework to take timed security requirements into account from the design stage of the system building. Our approach consists of two main steps. First, the system behavior is specified based on its functional requirements using TEFSM (Timed Extended Finite State Machine) formalism. Second, this model is augmented by applying a set of dedicated algorithms to integrate timed security properties specified in Nomad language. Nomad is a formal language well adapted to express timed security properties with timed constraints. We also briefly present a France Telecom Travel system as a case study to demonstrate the reliability of our framework.

UB2SQL is a tool for designing and developing database applications using UML and B formal method. The approach supported by UB2SQL consists of two successive phases. In the first phase, with the design of applications using class, state and collaboration diagrams, B specifications are automatically generated from UML diagrams; the diagrams are then augmented with these B specifications in place. The second phase deals with the refinement of these B specifications into a relational database implementation, for which UML representation is constructed. In both phases, proofs are achieved to ensure correctness of the obtained B specification and correctness of the refinement process. To overcome the lack of rules and tactics in the B prover, UB2SQL defines specific rules and tactics making the proof task seem like a push-button activity. To increase the usability of UB2SQL in both academic and industrial contexts, the tool has been integrated as a plug-in to the Rational Rose CASE tool. Such integration allows users to develop and be able to visualize graphical UML diagrams and formal B notation in a single environment.

The lack of a precise semantics for UML activity diagrams makes the reasoning on models constructed using such diagrams infeasible. However, such diagrams are widely used in domains that require a certain degree of confidence. Due to economical interests, the business domain is one of these. To enhance confidence level of UML activity diagrams, this paper provides a formal definition of their syntax and semantics. The main interest of our approach is that we chose UML activity diagrams, which are recognized to be more tractable by engineers, and we extend them with timing constraints. We outline the translation of our semantics into the PROMELA input language of the SPIN model checker which can be used to check several properties.

This paper presents, through an example, an overview of our method which generates B specifications from an application described using UML notations. We are interested in data intensive applications. This allows us to automatically generate basic update operations from class diagrams. Then these operations are combined to elaborate more complex transactions described in UML by state and collaboration diagrams. The obtained B machines are directly usable in AtelierB and proofs can be performed allowing the consistency of the application to be checked. Finally the outlines of the prototype support tool are described.