Search

International audience; This paper presents a formal model of the case study proposed for the ABZ2018 conference, which concerns the Hybrid ERTMS/ETCS Level 3 Standard. This standard allows trains to communicate with a train supervisor to report their integrity and positions, thanks to an onboard train integrity monitoring system. The supervisor assigns trains a movement authority to control traffic and to avoid collisions. The standard also provides for trains that cannot communicate with the supervisor; these trains are detected by sensors on tracks and obey traffic signals set by the supervisor along the trackside. Using communication allows for a finer grain control of the tracks. Our model is derived using stepwise refinement with the Event-B method. We take into account the main features of the case study (VSS management, timers, ERTMS and non-ERTMS trains). Our model is decomposed into four refinements. All proof obligations have been discharged using the Rodin provers, except those related to the computation of the VSS state machine, which was found to be ambiguous (nondeterministic). Our model has been validated using ProB. The main safety property, which is that ERTMS trains do not collide, is proved. Our model focuses on the discrete control logic aspects of the case study.

International audience; This paper introduces an Event-B formal model of the adaptive exterior light system for cars, a case study proposed in the context of the ABZ2020 conference. The system describes the different provided lights and the conditions under which they are switched on/off in order to improve the visibility of the driver without dazzling the oncoming ones. The system can be viewed as a lights controller that reads different information form the available sensors (key state, exterior luminosity, etc.) and takes the adequate actions by acting on the actuators of the lights in order to ensure a good visibility for the driver according to the information read. Our model is built using stepwise refinement with the Event-B method. We consider all the features of the case study, all proof obligations have been discharged using the Rodin provers. Our model has been validated using ProB by applying the different provided scenarios. This validation has permitted us to point out and correct some mistakes, ambiguities and oversights in the first versions of the case study.

International audience; In this paper, we show the application of ASTDs to intrusion detection. ASTD is an executable, modular and graphical notation that allows for the composition of hierarchical state machines with process algebra operators to model complex attack phases. Overall, ASTD attack specifications are more concise than industrial tools like Snort, Zeek, and other attack languages in the literature. For intrusion detection, iASTD (the ASTD interpreter) and Zeek provided similar results. iASTD produced less false positives and a smaller number of true positives per attack than Snort, which is an important factor to deal with huge amounts of events. The processing time of iASTD on the real-time testbed is slower than Snort and Zeek, but it can be improved by compiling ASTD specifications into Zeek scripts.

Hybrid systems are one of the most common mathematical models for Cyber-Physical Systems (CPSs). They combine discrete dynamics represented by state machines or finite automata with continuous behaviors represented by differential equations. The measurement of continuous behaviors is performed by sensors. When these sensors have a continuous access to these measurements, we call such model an Event-Triggered model. The properties of this model are easier to prove, while its implementation is difficult in practice. Therefore, it is preferable to introduce a more realistic model, called Time-Triggered model, where the sensors take periodic measurements. Contrary to Event-Triggered models, Time-Triggered models are much easier to implement, but much more difficult to verify. Based on the differential refinement logic (dR\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathcal {L}$$\end{document}), a dynamic logic for refinement relations on hybrid systems, it is possible to prove that a Time-Triggered model refines an Event-Triggered model. The major limitation of such logic is that it is not supported by any prover. In this paper, we propose a correct-by-construction approach that implements the reasoning on hybrid programs particularly the reasoning of dR\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathcal {L}$$\end{document} in Event-B to take advantage of its associated tools.

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.

International audience; This paper describes a case study of the SysML/KAOS method for a road transportation system for the City of Montreal (VdM), the second-largest city in Canada. The transportation system was developed from unstructured requirements represented in textual and schematic documents. Therefore, the VdM wanted to investigate new ways of organising and analysing the requirements of traffic projects, in order to increase the level of confidence in their safety, usability and reusability. This paper describes the formal specification, verification and validation of system requirements and provides an appraisal of the SysML/KAOS requirements engineering method on an industrial-scale case study. SysML/KAOS is designed within the ANR FORMOSE project to bridge the gap between stakeholder needs and the formal specification of system functionalities and domain constraints. The method has proven useful to deal with the seven refinement levels, twelve components (human, hardware, software and cyber-physical) and a hundred functional and non-functional goals that constitute the specification of the road transportation system, mainly focused on the safe movement of vehicles on road. It especially facilitated their validation with VdM stakeholders who had never dealt with formal methods and requirements engineering. Animation tools (ProB and B-Motion Studio) were also used to validate the formal specification with VdM stakeholders. This paper also reports improvements identified to enhance the expressiveness of SysML/KAOS goal modeling languages during validation sessions with VdM stakeholders. This includes the introduction of a non-functional goal refinement strategy based on logical formulas and of an obstacle modeling language.

International audience; Nowadays, network technologies are essential for transferring and storing various information of users, companies, and industries. However, the growth of the information transfer rate expands the attack surface, offering a rich environment to intruders. Intrusion detection systems (IDSs) are widespread systems able to passively or actively control intrusive activities in a defined host and network perimeter. Recently, different IDSs have been proposed by integrating various detection techniques, generic or adapted to a specific domain and to the nature of attacks operating on. The cybersecurity landscape deals with tremendous diverse event streams that exponentially increase the attack vectors. Event stream processing (ESP) methods appear to be solutions that leverage event streams to provide actionable insights and faster detection. In this paper, we briefly describe domains (as well as their vulnerabilities) on which recent papers were-based. We also survey standards for vulnerability assessment and attack classification. Afterwards, we carry out a classification of IDSs, evaluation metrics, and datasets. Next, we provide the technical details and an evaluation of the most recent work on IDS techniques and ESP approaches covering different dimensions (axes): domains, architectures, and local communication technologies. Finally, we discuss challenges and strategies to improve IDS in terms of accuracy, performance, and robustness.

International audience; 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.

International audience; We validate the RBAC ANSI 2012 standard using the B method. Numerous problems are identified: logical errors, inconsistencies, ambiguities, typing errors, missing preconditions, invariant violation, inappropriate specification notation. A clean version of the standard written in the B notation is proposed. We argue that the ad hocmathematical notation used in the standard is inappropriate and we propose that a more methodological and tool-supported approach must definitely be used for writing standards, in order to avoid the issues identified in the paper. Human reviewing is insufficient to produce error-free international standards

HighlightsWe propose to merge a set of business process fragments to construct new processes.We extend path matrices to systematically compile fragments' components.We ensure that the behavior of initial fragments is preserved.We ensure that the designer is alerted of undesirable behaviors.We prove the effectiveness of our approach through experimentations. In the field of business process management, adopting efficient building strategies can improve the quality of companies' business processes. The reuse of existing business processes or even fragments of them is a practical approach to build complete business processes or coarser-grained process fragments. In the present paper, we deal with the merge of a set of business process fragments for the construction of new complete processes. Our merge mechanism relies on a particular path matrix, that we call gateway path matrix. We use gateway path matrices to represent business process fragments to systematically compose shared components with individual ones. Moreover, our approach ensures that the resulting business process fragments subsume the behavior of initial ones and allows for adding new execution scenarios while controlling undesirable ones. In fact, we detect newly generated behaviors, and alert process designers of undesirable ones through behavioral constraints. We provide extensive experimental results derived from an implementation of our approach applied on a well-known industrial library of business process fragments.

International audience; Cloud computing is a new computing paradigm used for building on demand free and open source software (FOSS) applications. However, due to the lack of an explicit and formal description of the resource perspective in the existing FOSS applications, the correctness of Cloud resources management cannot be verified. The main objective of this paper is to propose a formal definition of the resource perspective in FOSS applications as a step towards ensuring a correct and consistent Cloud resource allocation in FOSS application modeling. Hence, we developed a Cloud Resources Allocation Model (CRAM4FOSS) for FOSS applications using the Event-B method. This model is used to formally validate the consistency of Cloud resource allocation for FOSS applications at design time, and to analyze and check its correctness according to the user’s requirements and the resource’s capabilities. The correctness and the consistency of our CRAM4FOSS model have been established into two phases : first, the ProB model-checker is used to detect the most obvious errors and validate the Event-B model by playing some scenarios, then a proof activity is performed to discharge the generated proof obligations that ensure the correctness of the model.

International audience; 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

International audience; 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

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.

International audience; This paper is about the extension of the SysML/KAOS requirements engineering method with domain models expressed as ontologies. More precisely, it concerns the translation of these ontologies into B System for system construction. The contributions of this paper are twofold. The first one is a formal semantics for the ontology modeling language. The second one is the formal definition of translation rules between ontologies and B system specifications in order to provide the structural part of the formal specification. These translation rules are modeled in Event-B. Their consistency and completeness are proved using Rodin. We show that they are structure preserving (two related elements within the source model remain related within the target model), by proving various isomorphisms between the ontology and the B System specification

International audience; This paper presents a specification of the hybrid ERTMS/ ETCS level 3 standard in the framework of the case study proposed for the 6th edition of the ABZ conference. The specification is based on the method and tools, developed in the ANR FORMOSE project, for the modeling and formal verification of critical and complex system requirements. The requirements are specified with SysML/KAOS goal diagrams and are automatically translated into B System specifications, in order to obtain the architecture of the formal specification. Domain properties are specified by ontologies with the SysML/KAOS domain modeling language, based on OWL and PLIB. Their automatic translation completes the structural part of the formal specification. The only part of the specification, which must be manually completed, is the body of events. The construction is incremental, based on the refinement mechanisms existing within the involved methods. The formal specification of the case study is composed of seven refinement levels and all the proofs have been discharged with the Rodin prover

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.

International audience; The use of formal methods for verification and validation of critical and complex systems is important, but can be extremely tedious without modularisation mechanisms. SysML/KAOS is a requirements engineering method. It includes a goal modeling language to model requirements from stakeholder's needs. It also contains a domain modeling language for the representation of system application domain using ontologies. Translation rules have been defined to automatically map SysML/KAOS models into B System specifications. Moreover, since the systems we are interested in naturally break down into subsystems (enabling the distribution of work between several agents: hardware, software and human), SysML/KAOS goal models allow the capture of assignments of requirements to agents responsible of their achievement. Each agent is associated with a subsystem. The contribution of this paper is an approach to ensure that a requirement assigned to a subsystem is well achieved by the subsystem. A particular emphasis is placed on ensuring that system invariants persist in subsystems specifications

International audience; This paper presents an Event-B model of the ABZ2018 case study on the European Rail Trac Management System (ERTMS) standard. The case study focusses on the management of xed virtual sub-sections (VSS). We model the hybrid level 3 of the standard, which assumes that trains may be either equipped with an on-board train integrity monitoring system (TIMS) and that they report their position and integrity, ERTMS trains not tted with TIMS that report only their front position or non-ERTMS trains that do not report any information about their position. We take into account most of the main features of the case study. Our model is decomposed into four renements. All proof obligations have been discharged using the Rodin provers, except those related to the computation of the VSS state machine, which was found to be ambiguous (nondeterministic). Our model has been validated using ProB. The main safety property, which is that ERTMS trains do not collide, is proved

Context: Nowadays, Information Systems (IS) are at the heart of most companies and constitute then a critical element that needs an adequate attention regarding security issues of sensitive data it manages. Objective: This paper presents a formal approach for the development of a filter to secure access to sensitive resources of information systems. Method: The proposed approach consists of three complementary steps. Designers start by modeling the functionalities of the system and its security requirements using dedicated UML diagrams. These diagrams are then automatically translated into a formal B specification suitable not only for reasoning about data integrity checking but also for the derivation of a trustworthy implementation. Indeed, a formal refinement process is applied on the generated B specification to obtain a relational-like B implementation which is then translated into an AspectJ implementation, connected to a SQL Server (release 2014) relational database system. Such a generation is performed following the aspect oriented programming paradigm which permits a separation of concerns by making a clear distinction between functional and security aspects. Results: A systematic formal approach to derive a secure filter that regulates access to the sensitive data of an information system. The filter considers both static and dynamic access rules. A tool that supports the proposed approach is also provided. Conclusion: The approach has been applied on several case studies that demonstrate that the development of a tool permits to free the developers from tedious and error-prone tasks since they have just to push a button to generate the AspectJ code of an application.

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.

International audience; Modeling the domain of a system to be implemented is a very critical and often neglected activity during requirements engineering. In this paper, we set the scene for an approach to complement the SysML/KAOS goal model of a system by adding an ontological representation of its domain knowledge. We think that an Event-B formalization of that domain representation can be used to enrich the formal specifications obtained from the goal model. This paper describes the metamodel that we propose for the representation of domain knowledge and illustrates the proposal through a Landing Gear System case study

International audience; This paper investigates the verification ofaccess control policies for SGAC, a new healthcare access-control model, using Alloy and ProB, two first orderlogic model checkers based on distinct technologies.SGAC supports permission and prohibition, ruleinheritance among subjects and resources and conflictsresolution. In order to protect patient privacy while ensuringeffective caregiving in safety-critical situations, we check different properties such as accessibility, ineffectiverule detection. Our performance results showthat ProB performs two orders of magnitude betterthan Alloy. Results are promising enough to considerProB for verifying patient policies in SGAC.

International audience; Configurable process models are recently gaining momentum as a basis for process design by reuse. Such models are designed in a generic manner to group common and variable parts of similar processes. Since these processes are usually large and complex, their configuration becomes manifestly a difficult task. This is why, an increasing attention is being paid to help achieving the process models configuration in a correct and domain-compliant manner. In this work, we propose an Event-B based formal approach that guides the process analyst to easily derive correct process variants while considering business domain constraints provided by configuration guidelines. To show the effectiveness of our approach, we conduct experiments on a case study

International audience; 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

International audience; This paper presents SGAC (\textit{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

International audience; 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 \textsc{SecureUML} and UML activity diagrams respectively. Basically, the tool automatically generates the B formal specification corresponding to these diagrams and the filter

International audience; 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

International audience; With the advent of the internet, most organizations offer more and more access to their information systems in order to increase their benefits. However, such an opening may cause security issues if sufficient precautions are not taken. An adequate solution to secure access to information systems consists in (1) defining the sufficient security policies and (2) ensuring their correct deployment on a given technological infrastructure. The present paper deals with the first point by introducing a formal approach that permits to develop a secure filter for an information system that respects different kinds of security rules: functional, static and dynamic rules. The proposed approach uses the \texttt{SecureUML} language to express the static rules and adapts the UML activity diagrams for dynamic ones while the structure of the manipulated data and the functionalities are expressed using a UML class diagram. Starting from these graphical notations, the approach consists in mapping them into a B formal specification to ensure their consistency and validate the system. Finally, a proved filter, which permits to take into account different security rules, is formally derived using the B refinement technique

International audience; 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

This article describes the Event-B modeling of a landing gear system of an aircraft whose complete description can be found in Boniol and Wiels (The Landing Gear System Case Study, ABZ Case Study, Communications in Computer Information Science, vol 433, Springer, Berlin, 2014). This real-life case study has been proposed by the ABZ'2014 track that took place in Toulouse, the European capital of the aeronautic industry. Our modeling is based on the Parnas and Madey's 4-Variable Model that permits to consider the different parts of a system. These parts are incrementally introduced using the Event-B refinement technique. The entire development has been carried out with the Rodin toolset. To ensure the correctness of the different components, we use several verification techniques (animation, model checking and proof) depending on the complexity and the kind of the properties to verify. Basically, prior to the proof phase that can be tedious and complex, we use the animator AnimB and the model checker ProB that permit to discover some trivial inconsistencies. Once no error is reported, we start the proof phase by using the Atelier B and SMT provers which we installed on Rodin. We conclude the article by drawing up some key findings of and lessons learned from this experience.

International audience; In the present work, we propose an approach to merge business process fragments in order to facilitate the reuse of fragments in business process designs. The approach relies on the so-called adjacency matrices. Typically used to handle graphs, this concept represents a new way to systematically merge fragments through their corresponding matrices. At the same time, fragments merging must keep the behavior of the original fragments consisting of their execution scenarios and rule out undesirable ones that may be generated during the merge task. Indeed, such behaviors probably lead to process execution blocking. The proposed approach has been implemented and tested on a collection of fragments and experimental results are provided

International audience; 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

International audience; 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. This paper presents a design-time approach to decompose existing business processes. This approach provides ready-for-reuse and privacy-aware fragments that are conform to given semantics specifications. It is based on the so-called FCA technique handling semantic clustering while dealing with the privacy constraints

International audience; 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.

Dynamic properties are very useful in the specification of Information Systems (IS) and security policies. They allow the user to express properties that involve several states of a system. Indeed, invariance properties do not permit to cover such kind of properties. In this paper, we suggest a formal approach, based on the use of the B method, to verifying absence properties of the form $\mathsf{Abs}(P_2, \ \mathsf{From}\ P_1\ \mathsf{Until}\ P_3)$ that express that some states, represented by predicate $P_2$, should not be reached starting from a state that satisfies $P_1$ until a state satisfies $P_3$ is reached. Our proposal consists in defining two proof obligations based on weakest preconditions that are sufficient and necessary to prove that a system verifies such a property.

International audience; Context: Formal methods are very useful in the software industry and are becoming of paramount importance in practical engineering techniques. They involve the design and modeling of various system aspects expressed usually through different paradigms. These different formalisms make the verification of global developed systems more difficult. Objective: In this paper, we propose to combine two modeling formalisms, in order to express both functional and security timed requirements of a system to obtain all the requirements expressed in a unique formalism. Method: First, the system behavior is specified according to its functional requirements using Timed Extended Finite State Machine (TEFSM) 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 adapted to express security properties such as permissions, prohibitions and obligations with time considerations. Results: The proposed algorithms produce a global TEFSM specification of the system that includes both its functional and security timed requirements. Conclusion: It is concluded that it is possible to merge several requirement aspects described with different formalisms into a global specification that 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 Travel service to demonstrate its scalability and feasibility.

International audience; This paper proposes an approach to prove interference freedom for a reach ability property of the form AG (psi => EF phi) 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 (psi => EF phi). 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

International audience; This paper presents a technique for vulnerability detection in C programs. It is based on a vulnerability formal model called "Vulnerability Detection Conditions" (VDCs). This model is used together with passive testing techniques for the automatic detection of vulnerabilities. The proposed technique has been implemented in a dynamic code analysis tool, TestInv-Code, which detects the presence of vulnerabilities on a given code, by checking dynamically the VDCs on the execution traces of the given program. The tool has been applied to several C applications containing some well known vulnerabilities to illustrate its effectiveness. It has also been compared with existing tools in the market, showing promising performances

International audience; Traditionally, a security policy is defined from an informal set of requirements, generally written using natural language. It is then difficult to appreciate the compatibility degree of the manually generated security policy with the informal requirements definition. The idea of this paper is to automate the process of deriving the formal security policy, using a more structured specification of the security objectives issued by the administrator of the information system to be secured. We chose the goal-oriented methodology KAOS to express the functional objectives, then based on the results of a risk analysis, we integrate the security objectives to the obtained KAOS framework. Finally, through a process of transformation applied to this structured security objectives specification, we automatically generate the corresponding security policy. This policy is consistent with the access control model OrBAC (Organization Access Control).

International audience; This paper gives an overview of a formal approach for detecting vulnerabilities in C programs using the B formal method. Vulnerabilities denote faults that may be introduced unintentionally into programs making them behave incorrectly. Such faults (or programing errors) may lead to unpredictable behavior and even worse well-motivated attackers may exploit them later to cause real damages. Basically, the proposed approach consists in translating the vulnerable aspects of a C program into a B specification. On this B specification proof and model checking activities are performed in order to detect the presence or absence of vulnerabilities. Compared to the existing vulnerability detection techniques, a proof-based approach permits to eliminate false alarms and denial of service attacks

International audience; This paper presents a formal approach to proving temporal reachability properties, expressed in CTL, on B systems. We are particularly interested in demonstrating that a system can reach a given state by executing a sequence of actions (or operation calls) called a path. Starting with a path, the proposed approach consists in calculating the proof obligations to discharge in order to prove that the path allows the system to evolve in order to verify the desired property. Since these proof obligations are expressed as first logic formulas without any temporal operator, they can be discharged using the prover of AtelierB. Our proposal is illustrated through a case study

International audience; This paper proposes an approach to prove reachability properties of the form AG psi => EF phi using substitution refinement in classical B. Such properties denote that there exists an execution path for each state satisfying psi to a state satisfying phi. These properties frequently occur in security policies and information systems. We show how to use Morgan's specification statement to represent a property and refinement laws to prove it. The idea is to construct by stepwise refinement a program whose elementary statements are operation calls. Thus, the execution of such a program provides an execution satisfying AG psi => EF phi. Proof obligations are represented using assertions (ASSERT clause of B) and can be discharged using Atelier B

International audience; Maintaining integrity constraints in information systems is a real issue. In our previous work, we have defined a formal approach that derives B formal specifications from a UML description of the system. Basically, the generated B specification is composed of a set of variables modeling data and a set of operations representing transactions. The integrity constraints are directly specified as B invariant properties. So far, the operations we generate establish only a reduced class of constraints. In this paper, we describe a systematic approach to identify preconditions that take a larger class of invariants into account. The key idea is the definition of rewriting and simplification rules that we apply to the B invariants.

International audience; 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

International audience; 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 StateMachine) 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 Telecom1 Travel system as a case study to demonstrate the reliability of our framework

International audience; This paper describes the formal verification of an interlocking system. We have formally proved the non-derailing and non-collision safety properties for an existing interlocking system operating on Paris Metro's line 3Bis. These high-level properties have first been refined to an intermediate level permitting their expression in terms of the control system's inputs and outputs. The resulting properties have then been formalised in the Prover iLock Verifier engine's internal language. The Prover iLock Verifier engine is a COTS commercialised by Prover Technology. For this project some specific features have been added to the engine to provide certified proofs that can be used, instead of testing, in the SIL-4 qualification process of interlocking systems.

This paper presents a formal approach for the development of trustworthy database applications. This approach consists of three complementary steps. Designers start by modeling applications using UML diagrams dedicated to database applications domain. These diagrams are then automatically translated into B specifications suitable not only for reasoning about data integrity checking but also for the derivation of trustworthy implementations. In this paper, we present a process based on the B refinement technique for the derivation of a SQL relational implementation, embedded in the JAVA language (JAVA/SQL), from a B specification obtained by the first translation phase.

International audience; 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

International audience; This article describes a formal approach to specify and develop database applications. This approach consists of two complementary phases. In the first phase, B specifications are automatically generated from UML class, state and collaboration diagrams describing the data and the transactions of the system we are developing. In the second phase, these specifications are successively refined until they become close enough to a relational implementation. The tool supporting this approach is implemented as an extension of the Rational Rose tool to develop and visualize graphical (UML) and formal (B) notations in a single environment.