The quality of a system depends on the degree to which it fulfills its requirements. Requirements traceability is broadly recognized as a crucial element of any rigorous system development process, especially for the design of critical complex systems. The paper proposes a model-based approach to support traceability by defining several kinds of alignment links between requirements models and high-level architecture models. We have already defined these models using a combination of graphical notations based on SysML and the formal method Event-B, hence alignment links are first graphically specified by refining the Dependency concept of SysML. Then they are translated into Event-B specifications. The main idea is to use the formal refinement concept to prove their correctness. As the semantics of this refinement is not the same as the standard Event-B refinement, we have defined new proof obligations to express it, which can be discharged using Atelier B. Finally we illustrate our approach on a case study from the railway domain.

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.

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.

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.

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.

Abstract This paper introduces three refinement patterns for algebraic state-transition diagrams ( astds ): state refinement, transition refinement and loop-transition refinement. These refinement patterns are derived from practice in using astds for specifying information systems and security policies in two industrial research projects. Two refinement relations used in these patterns are formally defined. For each pattern, proof obligations are proposed to ensure preservation of behaviour through refinement. The proposed refinement relations essentially consist in preserving scenarios by replacing abstract events with concrete events, or by introducing new events. Deadlocks cannot be introduced; divergence over new events is allowed in one of the refinement relation. We prove congruence-like properties for these three patterns, in order to show that they can be applied to a subpart of a specification while preserving global properties. These three refinement patterns are illustrated with a simple case study of a complaint management system.

To develop quality software and systems, both functional and non-functional requirements need to be taken into account at the highest level of abstraction. However the issue of relationships between non-functional requirements and functional requirements has been rarely addressed. In this article, we outline an extension of the SysML requirements meta-model with relevant concepts of commonly used goal-oriented requirements engineering approaches. The main contribution of our approach is to analyse and describe the impact of non-functional requirements on functional requirements.

With most of formal methods, an initial formal model can be refined in multiple steps, until the final refinement contains enough details for an implementation. Most of the time, this initial model is built from the description obtained by the requirements analysis. Unfortunately, this transition from the requirements phase to the formal specification phase is one of the most painful steps and is still ambiguous. In fact, building this initial model requires a high level of competence and a lot of practice, especially as there is no well-defined process to assist designers. For that purpose, we propose a goal-based approach in which initial formal models (in Event-B) are built incrementally driven by a goal-oriented requirements engineering (GORE) paradigm.

This paper addresses the problem of introducing variability in goal-based requirements. The proposed approach adopts and extends the KAOS goal oriented metamodel with variability concepts. The resulting metamodel is then used to model common and variable requirements at goal level. The application domain is the Cycab, a public vehicle with fully automated driving capability.

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.

EB3is a trace-based formal language created for the specification of information systems (IS). Attributes, linked to entities and associations of an IS, are computed in EB3by recursive functions on the valid traces of the system. We aim at synthesizing relational database transactions that correspond to EB3attribute definitions. Each EB3action is translated into a transaction. EB3attribute definitions are analysed to determine the key values affected by each action. Some key values are retrieved from SELECT statements that correspond to first-order predicates in EB3attribute definitions. To avoid problems with the sequencing of SQL statements in the transactions, temporary variables and/or tables are introduced for these key values. Generation of DELETE statements is straightforward, but distinguishing updates from insertions of tuples requires more analysis

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.