The systems become increasingly complex and their implementation asks for more rigorous conception approaches. To develop reliable systems, some software engineering approaches have been proposed and particularly top-down approach, which allows building a system, step by step from high abstract speciications, like in [Wir71, CL02, AaDB + 02, vL03, LNRT10]. This approach has been used to design Component-Based Systems (CBS) [START_REF] Szyperski | Component Software: beyond Object-Oriented Programming[END_REF] constituted by communicating entities. It allows efectively to enhance development process reliability and reduce development costs.

CBS are widely used in the industrial ield, and they are built by assembling various reusable components. Its success is due, generally, to the development of complex systems by assembling smaller and simpler components and its reduced development cost. However, this approach of development leads to construct CBS generally even bigger, therefore more complex. Consequently the question of their reliability is not always guaranteed. Hence the need to integrate more formal approaches in the development process of the CBS.

To ease the communication between the various stakeholders in a CBS development project, one of the widely used modeling language is SysML [START_REF] Omg | Systems Modeling Language (SysML) Version 1.3[END_REF], which besides allowing modeling of structure and behavior, it has capabilities to model requirements. It ofers a standard for modeling, specifying and documenting systems. Therefore, in this thesis, we propose to exploit it. The improvements, brought by SysML, have allowed increasing its popularity in the industrial and academic environment. A SysML speciication of a system is described by structural diagrams and behavioral diagrams. The architecture reinement of a system is an important concept in SysML, and it is based in a development process that can start from an abstract level and evoluates towards more detailed levels which can end in an implementation.

In this context, we have identiied two main challenges:

The irst one concerns the development by reinement of a CBS, which is modeled only by its SysML interfaces and behavior protocols. In this case, it is a question of replacing an abstract speciication by a composition of blocks preserving its structural properties and its behavioral properties. Structural diagrams of SysML describe the system in static mode, and behavioral diagrams describe the dynamic operation of the system. The blocks are modeled by two diagrams, the Block Deinition Diagram (BDD), which deines the architecture of the blocks and their performed operations, and the internal block diagram used to deine the ports of each block and connectors between them linking their ports.

diagrams as proposed in [START_REF] Chouali | Formal veriication of components assembly based on SysML and interface automata[END_REF]. This approach aims to formalize the decomposition process, by deining reinement relations between blocks, and by focusing on the veriication of architectural and behavioral aspects of SysML blocks. In this contribution we exploit the tools: Ptolemy II for verifying compatibility between the assembled components, and the MIO Workbench tool to verify reinement.

Secondly, based on SysML requirement diagram and component interfaces, speciied with SD, we propose a formal and methodological approach to specify incrementally the system architecture that preserves all the system requirements (see Contribution 3 on Figure 1.1). Therefore, we propose to treat, one by one, atomic requirements, extracted from the requirement diagram (provided by the speciier), to construct a partial architecture, of the system, composed of atomic components and composite components. At each step, we propose to select an atomic requirement from a SysML requirement diagram, and choose a component from a library that should satisfy the selected requirement. Then we verify whether the component satisies the requirement thanks to the LTL formula which speciies the requirement and the Promela program which speciies the component SD (see Contribution 2 on Figure 1.1). After that, we verify the compatibility between the selected components, and the selected one in the precedent step, and we verify also the preservation of the requirements treated in the precedent steps. This process ends when all atomic requirements are treated, or when we detect incompatibility between components, or the non preservation of the requirements by component composition. When the process ends correctly, we guarantee the architecture consistency of the inal CBS which then fulills all the requirements.

In this context, this thesis presents new contributions which are:

• The exploitation of SysML requirement diagram to specify the requirements of CBS [START_REF] Chouali | Specifying System Architecture from SysML Requirements and Component Interfaces[END_REF][START_REF] Carrillo | Incremental Modeling of System Architecture Satisfying SysML Functional Requirements[END_REF].

• The speciication of SysML requirements with LTL (Linear Temporal Logic) formulae for their veriication on components [START_REF] Carrillo | Incremental Modeling of System Architecture Satisfying SysML Functional Requirements[END_REF], thanks to their SD which are translated to Promela by adapting the approach proposed in [LTM + 09].

• The veriication of components compatibility by exploiting the interface automata formalism [START_REF] De Alfaro | Interface automata[END_REF], obtained from SD of components, thanks to the approach proposed in [START_REF] Chouali | Formal veriication of components assembly based on SysML and interface automata[END_REF]. In this work we adapted the compatibility veriication algorithm to handle SysML requirements and to verify also their preservation by the composition [START_REF] Carrillo | Formalizing and verifying compatibility and consistency of SysML blocks[END_REF][START_REF] Carrillo | Vériication de la consistence et de la compatibilité entre blocs SysML[END_REF][START_REF] Carrillo | Veriication of a SysML Block Decomposition in a Reinement Process[END_REF].

• The veriication of components behavior reinement by applying alternating simulation in interface automata [START_REF] Carrillo | Veriication of a SysML Block Decomposition in a Reinement Process[END_REF].

• The proposition of an incremental approach to construct CBS and to verify their requirements in order to avoid the problem of the combinatorial explosion of the number of states of the veriied components. Indeed, the requirement veriication is performed on elementary (generally small) components, so we avoid the veriication on composite components thanks to the requirements preservation by the composition. This contribution allows obtaining the CBS architecture that fulills all the requirements. Indeed, this architecture is constructed incrementally and also validated incrementally against to SysML requirements at each step [START_REF] Chouali | Specifying System Architecture from SysML Requirements and Component Interfaces[END_REF][START_REF] Carrillo | Incremental Modeling of System Architecture Satisfying SysML Functional Requirements[END_REF].

.

/ T

In this section, we describe the tools that we used to model and verify the CBS in this thesis.

Papyrus This plugin made by Lanusse et al. [LTE + 09, GDTS10], it is designed to work in the Eclipse Modeling Framework (EMF) [START_REF] Steinberg | EMF: Eclipse Modeling Framework[END_REF] to model any kind of EMF model, one of them is SysML. We used this modeling tool to design the SysML models in this thesis.

Besides of being a free and open source software, it has a growing community of users in the industrial and academic ield [LST + 11].

MIO Workbench This tool is a plugin made by Bauer et al. [START_REF] Bauer | On Weak Modal Compatibility, Reinement, and the MIO Workbench[END_REF], it is an Eclipse-based editor and veriication tool for modal I/O automata. We used it in this thesis, to verify behavioral reinement of CBS.

Ptolemy II This is a tool for modeling, simulate and design concurrent, real-time and embedded systems [BLL + 05]. It integrates a module to work with interface automata [START_REF] Lee | A behavioral type system and its application in Ptolemy II[END_REF].

It represents the interaction between components as actors and evaluates their compatibility by various means, and one of those is the compatibility veriication by interface automata. We used this tool to validate the compatibility between components in a CBS.

SPIN This is a popular open-source model-checker that supports the design and veriication of asynchronous process systems. SPIN veriication models are focused on proving the correctness of process interactions, and they attempt to abstract as much as possible from internal procedures [START_REF] Gerard | The Model Checker[END_REF]. SPIN veriies design speciication written in the veriication language Promela (Process Meta Language) [START_REF] Holzmann | Design and validation of computer protocols[END_REF], and it accepts correctness claims (properties) speciied in the syntax of standard Linear Temporal Logic (LTL) [START_REF] Pnueli | The Temporal Logic of Programs[END_REF]. We used this model-checker to verify if a component satisies a given requirement.

.

/ C S

In this section, we present a safety vehicle system as the case study, which we will use as the pivot case study during this thesis.

The system presented here is a case study inspired from the study of Barnes et al. [START_REF] Barnes | Airbag efectiveness in real world crashes[END_REF] and the safety requirements dictated by the American Department of Transportation to improve protection of vehicle occupants [Adm98]. There, the authors deine the conditions to activate automatically the safety devices in a car.

Figure 1.2 shows a safety system that consists of several sensors all around a vehicle (accelerometers, impact sensors, pressure sensors, tachometers, brake pressure sensors, gyroscopes, etc.) that detect whether a collision occurred. When a car collides with a barrier or the breaks are pressed, there will be a speed deceleration. The sensors will detect the acceleration/deceleration values and will send them to a central unit, which is marked with number 1 in the image. This center unit must decide whether to inlate the airbags (front, side, knee, etc.), which are marked with number 2 in the igure, and/or lock the seat-belts (marked with number 3 in the igure). From the directives in [Adm98], we assume that the maximum deceleration that the chest can accept is 60G, and therefore, the airbag must be deployed. In the same way we assume that every time the vehicle decelerates at more than 3G, the seat-belts must be locked. The work presented in this thesis has been already published in national and international conferences, in the following, we list the references for the published articles: .

/ D O

In this section we give a summary of the content of this thesis, which is structured in three parts and composed of nine chapters as follows:

In Part I, we introduce the scientiic context of this work, there, we irst give, in Chapter 2, an overview of Component-Based Systems and the key concepts to describe them. Then in Chapter 3, we present the SysML modeling language and the diagrams that we will use to model Component-Based Systems. In Chapter 4, we introduce the concept of Interface Automata, which we will use later in our approach to describe behavior protocols and verify component compatibility. Finally, in Chapter 5, we present some works that are related to ours in one way or another.

In Part II, we present the contributions of this thesis regrouped in three chapters. Chapter 6 handles the irst identiied issue, which is how to model, by reinement, a CBS that is initially described only by its interfaces, and guarantee that the proposed system reines the initial abstract deinition. Chapter 7 explains our proposition to formally verify SysML requirements on system components by translating the initial requirements into LTL properties that we later verify over a Promela model. This Promela model is obtained from the component behavior protocol described in its sequence diagram. Finally, we use the model-checker SPIN to verify the properties. Chapter 8 deals with the second identiied issue, which is how to build a CBS from a list of functional requirements, represented by a SysML requirement diagram and a library of reusable components.

In Part III, we conclude our work with Chapter 9, where we present the conclusions and perspectives of this thesis.

I S fi C 2 C -B S
I n this chapter, we deine the main concepts of Component-Based Systems. In Section 2.1 we deine software components, later in Section 2.2 we describe the diference between objects and components. We continue then describing the properties of abstraction and reusability of components in Section 2.3. Section 2.5 introduces behavior protocols, which are used to describe the order of arrival for events accepted or invoked by a component.

. / S C D fi

Over the years, software developing ield has evolved through diferent paradigms. Structured programming changed over time to class paradigm and the revolutionary object oriented programming. Objects of nowadays have grown, and are identiied as software components. In this section, we deine and describe properties of the later to better understand the diferences between objects and components that we will expose in Section 2.2.

Several deinitions have been proposed to deine software components and one of the more complete was proposed in [START_REF] Szyperski | Workshop on Component-Oriented Programming, summary[END_REF] during the European Conference of Object-Oriented Computing (ECOOP 1996). This deinition is: component must encapsulate its implementation and interact with its environment on account of only well deined interfaces. Speciically, these interfaces must give information about what the component requires from other components and what it can ofer as services. Nevertheless, to use a component correctly, we must fulill a contract. This contract lists a series of constraints about the way of use to make the component execute its functionalities [START_REF] Szyperski | Component Software: beyond Object-Oriented Programming[END_REF]. It is also required to deine what the environment of composition and deployment must provide to make the components interact properly. This environment is composed of a component model with composition rules and a framework that deines deployment, installation, and activation rules of components. Therefore, software systems designed to be an assembly of components with a predeined architecture are called Component Bases Systems (CBS).

"A software component
Components can be reined and improved by subsequent versions. A company that sells third party components can propose diferent improved versions of the same component. Traditional version management would assume that the version of a component evolves at a single source. Nevertheless, in a free market, version evolution is more complex and version management can become a problem in its own right, mostly because versions can also change at interface level.

. / C . O

In this section, we discuss the key points that diferentiate a component from an object.

From [START_REF] Szyperski | Component Software: beyond Object-Oriented Programming[END_REF], we can deine an object as a symbolic container, which integrates information and mechanisms that represents a physic or moral identity from the real world. The concept of object leads to the concept of instance, encapsulation, and identity.

Objects and components are frequently considered as synonyms, or very similar. A component can be seen as a collection of objects that communicate between them. The borderline between a component and other components or objects is very clear. The interaction with a component and therefore with its objects must pass through its borderline, which for components is at interface level. In this way, granularity in a component remains hidden, and one cannot use its objects directly. A component cannot be used to identify its composing objects. Moreover, objects inside a component have access to their implementations, but accessing an object implementation from outside the component must be avoided [START_REF] Szyperski | Workshop on Component-Oriented Programming, summary[END_REF].

A component may contain one or several classes, but one class should not be part of several components. Although, a component may depend on other components by import relations like the inheritance relationships between classes and objects. Therefore, the parent class and its subclass do not have to be on the same component. If the parent class resides in another component, the inheritance relationship between the two classes traverse the component limits and demands an import relationship between them [START_REF] Szyperski | Component Software: beyond Object-Oriented Programming[END_REF]. More over, instead of classes or objects, a component may contain traditional procedures to manage global variables or it can be completely developed in a functional programming language.

The following properties list other diferences between objects and components [START_REF] Desmond | Objects, Components, and Frameworks with UML: The Catalysis Approach[END_REF]:

• Components lead to other means of intercommunication more extensive than objects, i.e. distributed SmallTalk components support the interaction of several re-mote users over several machines [START_REF] Bennett | The design and implementation of distributed Smalltalk[END_REF].

• Granularity level of components is more extensive than the one of objects and their communication means through interfaces is widely more complex.

• Components are deployed in diferent conigurations with no need of reconiguration for each host infrastructure.

In summary, components are very close to objects and therefore Component-Based Development (CBD) is greatly linked to Object-Oriented Design (OOD). However, many factors like granularity, the concept of composition and deployment, or even the process of development, distinguish components from objects.

. / A R

In the following section, we present the concept of abstraction and reuse of components, which represent the two main features in the CBD approaches.

Component abstraction is the level of visibility of its implementation through its interfaces. In an ideal component abstraction, the environment should not know any detail of the interface speciication, hence the idea of Blackboxes. To understand the working of a component, it is only a matter of interpretation of its outputs as a function of its inputs. Tests on a component are performed following this principle. Generated outputs, after the component execution, are veriied to decide whether the component works as expected.

Nevertheless, blackbox components, in which implementation information are strictly hidden, are not the best suitable for a more interactive communication with their software environments. Outputs in a component may not depend only from their inputs, but also from the responses of a set of services provided by their neighbors (see Figure 2.1). The external services, activated by the component, must also be speciied. Such services often depend on the calling component state. For example, the design pattern observer [GHJV94] needs to ask information about the state of the observed object. If the observed object is a bank account and the observer is a balance check component, we need to know if the observer component is called before or after a balance change. Operation speciications, like withdraws or deposits, in a blackbox component do not specify when the observer component is called and the calling component state during the operation. This intermediate state in the blackbox component may be described informally but in more complex cases this approach may often fail.

The question now is how to design more interactive components keeping their implementations hidden? The answer is to use greybox components, these are components that reveal some internal operations. The component may give more details if needed, i.e., information about the conditions under which external services are called. For instance, in port interfaces to the environment and can import interfaces from other components. An ofered interface describes one or more services ofered by the component to its clients, whereas a required interface describes a required service by the component from its environment.

Speciically, an interface is a set of operations that may be called by clients (mostly other components). An operation may have zero or more input and output parameters. Generally, an operation has at least one output parameter (return value). These concepts are exposed in the UML metamodel shown in Figure 2.2.

A component may provide an interface directly through procedural interfaces from traditional libraries, or indirectly, through objects. Most of component-based approaches use object interfaces, rather that procedural interfaces, being components an evolution of object-based development.

.

/ B P

In this section, we deine the concepts about behavior protocols for components and some languages used to describe these protocols.

. . / D fi

A component behavior protocol deines the way in which a component must be used, establishing a timing order for calling and/or receiving a response from exposed services. Yellin and Storm described behavior protocols for the irst time in [START_REF] Daniel | Protocol Speciications and Component Adaptors[END_REF].

A protocol describes the interactions between a component and its environment (clients). An interaction can be an event for answering a call to one of the exposed services or an event for asking an ofered service provided by the environment. A beavior protocol aims to establish an order for the use of services of the component and reduce the number of possible combinations while using these services. Another goal of behavior protocols is to give a more detailed description than the services one, and to facilitate the abstraction, reusability and modularity of components.

Behavior protocols allow also to verify composability and compatibility properties in a component assembly. Therefore, it is not enough to call a component service properly, but we must also ensure that the assembly is well composed and that there will not be a blocking state or indesirable situations during the events timeline [START_REF] André | Protocoles d'Utilisation de Composants: Spéciication et Analyse en Kmelia[END_REF].

For instance, in a printer component, a user should not send a document to print before asking to reserve the resources and validate his identity, otherwise the component will respond unexpectedly. In this same case, if the user does not release the printer, then the component will stay in a blocked state waiting for the user to send an event to unlock it.

. . / D P L

There are several languages to describe component protocols as exposed in [START_REF] Mouelhi | Contributions à la Vériication de la Sûreté de l'Assemblage et à l'Adaptation de Composants Réutilisables[END_REF].

There is no language that will it all behavior speciications, as there are languages for diferent contexts. In the following, we present some of them according to the formalism used to express the protocol.

• Formal semantics: in this category we found protocols that provide an explicit semantic to describe the interactions with a component. Here we meet approaches like [START_REF] Allen | A Formal Basis for Architectural Connection[END_REF] where the authors propose a formal protocol to describe the connections between components using Communicating Sequential Processes (CSP) [START_REF] Hoare | Communicating sequential processes[END_REF]. They propose to formally describe the semantic deinitions of connectors independently of component interfaces. The use of CSP allows for consistency and compatibility checking of architectural descriptions.

• Process algebra: in this category we found the proposal of Carlos Canal et al. [START_REF] Canal | Extending CORBA Interfaces with Pi-Calculus for Protocol Compatibility[END_REF]. They propose to extend the descriptions of CORBA Interface Description Language (IDL) [START_REF] Mchale | Corba Explained Simply[END_REF] to specify component protocols using polyadic Π-calculus, a process algebra specially well suited for the speciication of dynamic and evolving systems [START_REF] Milner | Communicating and Mobile Systems: the -Calculus[END_REF]. This language aims to enrich CORBA IDL with information about the way components expect their services to be called, how they use other component services, and even some semantic aspects of user interest.

• Statechart: Some approaches like [START_REF] Moisan | A Behavioral Model of Component Frameworks[END_REF][START_REF] Moisan | Behavioral substitutability in component frameworks: A formal approach[END_REF], propose to model component behavior using statecharts. The use of inite state machines relies on mathematical models and it allows simulation of resulting applications and even generation of code. Another interest of using inite state machines is that we can enhance UML component descriptions by adding statechart diagrams that later we can verify for compatibility and safety properties.

• Automata: In this category we group languages that use automata to describe component behavior. We found here approaches like [ZVB + 08] that uses componentinteraction automata, [START_REF] De Alfaro | Interface automata[END_REF][START_REF] De Alfaro | Interface-Based Design[END_REF] that proposes interface automata, or [START_REF] Kim | Modal I/O Automata for Interface and Product Line Theories[END_REF] who proposes an extension of interface automata named modal automata. In these languages, component behaviors are described through labeled transition systems. The labels have semantics of input, output, or internal actions that represent the internal functions, and required and ofered services of a component. In this category, we place the description language that we will use in this thesis to deine component behavior. A detailed description of interface automata is presented in Chapter 4.

We decided to present some of these languages by their formalism. Nevertheless, we could have also classiied them by their content (i.e., services, messages, channels, etc.), the unit hosting the protocol (i.e., the component itself, its interfaces, etc.), or even their formal veriication capabilities.

. / S A

Software architecture can be seen as the art of designing systems. In the same manner that a building architect proposes new designs to his customers by means of a number of diferent views. A software architect will present several views in which some particular aspect of the system is emphasized to expose his understanding of the system to a client [START_REF] Perry | Foundations for the study of software architecture[END_REF].

Bass et al. [START_REF] Bass | Software Architecture in Practice[END_REF] give the following deinition for software architecture:

The software architecture of a program or computing system is the structure or structures of the system, which comprise software elements, the externally visible properties of those elements, and the relationships among them. Architecture is concerned with the public side of interfaces; private details of elements-details having to do solely with internal implementation-are not architectural.

We can deine a software architecture as an abstract description of the system, of its reinement in components, the interfaces of its components and their interactions. Components provide a way to isolate speciic sets of functionality within units that we can distribute and install separately from other functionality [MHH + 09].

. / A P Software architectures can be categorized according to the pattern used to assemble its components. Patterns like [START_REF] Wirth | Program development by stepwise reinement[END_REF] started to propose to gradually reine a system from upper levels to small functionalities following a desired degree of granularity. Years later, approaches like [START_REF] Tanner | Some Issues in Future User Interface Management System (UIMS) Development[END_REF] wanted to formalise a separate layer for user interfaces and make applications more interactive. Nowadays, most of the systems have an architecture composed of several layers like the one in Figure 2.3 [MHH + 09]. Components of the same layer share the same concern and they do not know much about the internal operation of one another. The main layers that we can identify are:

• Presentation layer: Components in this layer implement the functionalities that allow users to interact with the system. There are UI components that present the information to users and get input from them, and UI Process components that present the information in a logical representation that is independent of any speciic user interface implementation.

• Service layer: Besides, user interfaces, the system can interact with its clients or other systems through services. This layer is charged of presenting to clients the interface for getting information from the business layer in a structured manner and wrap information to be exchanged in structured messages.

• Business layer: Components in this layer implement the core functionalities of the system, and encapsulate the relevant business logic. In this layer, there will be an application façade that will provide a simpliied interface to business components, so the clients will not need to know any details about the internal business components and their relations.

• Data layer: Components in this layer provide access to data that is hosted within the boundaries of the system or network resources. They will hide all the logical deinitions needed to connect to this data sources and will ease the treatement and maintenance of data sources. Another class of components in this layer are service agents that will provide information obtained from other component services in a format understandable by the system.

• Crosscutting layer: In this layer we ind components that will perform their functionalities for more that one layer. For instance, security components are required in other layers to perform authentication, authorization, and validation.

S ML L

T he Systems Modeling Language (SysML) [START_REF] Omg | Systems Modeling Language (SysML) Version 1.3[END_REF] is a modeling language deinition designed in response to the need for unifying the wide range of modeling languages, tools, and techniques used in the systems engineering ield. For this goal, the Object Management Group (OMG) [START_REF] Omg | OMG Organization[END_REF] The basis of SysML are in UML version 2.0 [START_REF] Omg | Uniied Modeling Language Speciication, UML 2.0[END_REF], which allows deining new proiles by modifying, adding and excluding diagrams from its standard set. SysML reuses a subset of its diagrams and adds new features to better it the needs in the RFP, so that it allows the speciication, analysis, design, veriication, and validation of a wide range of complex systems. These systems may include software, hardware, data, processes, people, and facilities.

SysML is deined by nine diagrams, classiied in three subgroups: Structural, Behavioral CHAPTER 3. SYSML LANGUAGE and Cross-Cutting diagrams. Figure 3.1 shows this categorization and the modiication degree of the diagrams with respect to their UML counterparts. Diagrams in orange color are taken from UML without modiications, those in orange/yellow are modiied versions, and yellow ones are the new additions. We will describe these diagrams in the rest of this chapter, with an emphasis on those used in our work. This chapter is organized as follows: Sections 3.1, 3.2, and 3.3 will be consecrated to describe each SysML group and their diagrams, Section 3.4 presents some of the tools widely used in the SysML community to edit the diagrams and we end in Section 3.5 with the conclusion.

.

/ S D

Structural diagrams are intended to describe the system architecture showing its constitutive parts, communication links, internal composition, and initial values. The basic elements in structural diagrams are blocks. A block is a modular unit that represents the structure of a system or one of its elements. It may list structural or behavioral features by properties and actions respectively. Some of the properties may hold other parts of the system (that may be also described by blocks) and be linked through connectors to indicate how they relate to one another.

This set of SysML diagrams are meant to organize blocks and allow us to represent a system hierarchy, in which a system at one level is composed of systems at a more basic level. In the following we present the diagrams grouped in this category:

. . / T B D fi D Block Deinition Diagrams (BDDs) are based on the UML class diagram with some capabilities excluded, such as more specialized forms of associations. They describe the architectural structure of the system as components with their properties, operations, and relationships. Every component is represented by a block, no matter whether they are

. / C -C D

In this category comes the diagrams that do not it in structural neither behavioral diagrams since they describe the system needs in a wide view as for example the functional and non-functional requirements.

.

. / T R D

The The requirement diagram that speciies the system needs for our case study is shown on Figure 3.5. In this diagram, the initial requirement 1 asks for ensuring passengers lives and it is decomposed by a containment relationship into two requirements 1.1 and 1.2 that ask for two safety devices: an airbag system which must be deployed whenever the car is in a collision, and the seat-belts that must be locked when the sensors detect strong movements. On the left side, requirement 1.1 is further decomposed into requirements 1.1.1 , 1.1.2 , and 1.1.3 . Requirement 1.1.1 asks for the capture and sending of sensor values to an Airbag Control Unit (ACU). Requirement 1.1.2 requests an ACU to decide whether to deploy the airbag and lock the seat-belts as soon as the sensors report new values. Finally, requirement 1.1.3 demands to deploy an airbag device, once the signal from the ACU is received.

. / S ML T

The OMG is responsible for releasing SysML and each version comes with a documentation describing the speciication and a machine readable ile in Extensible Markup Language (XML) format with the metadata for building SysML diagrams. From this metadata, developers can create tools to assist the designing of standards-compliant models. So, actually there are several tools available to assist the system designers in their projects, and is up to them to choose the one that its better their needs. Here we list some of the most known tools classiied in commercial and free software:

• Commercial Tools -MagicDraw: Since its release, this tool, produced by the NoMagic society ¹, is intended for designing UML models, nevertheless as SysML is a UML stereotype then one can add a plugin named Paramagic (also a commercial plugin) that includes the SysML speciication. This tool is the most used in the modeling community since it is the one used by the authors of the standards in their books and it integrates the new speciication as soon as they are published.

-Cameo Systems Modeler: This tool, developed also by NoMagic and based in Mag-icDraw is exclusively intended for designing systems and we can say that is the most complete SysML tool as it integrates the new updates as soon as they are proposed by the OMG. It includes the SysML 1.4 version, which at this moment has not been released by the OMG though.

-Artisan Studio: Developed by the Atego society ², this tool provides modeling capabilities to design UML and therefore SysML diagrams. One interesting option with this tool is the posibility to use a free version, which is intended for single users.

-Enterprise Architect: Developed by the Sparx Systems society ³, this tool can be extended to model SysML diagrams, by adding the MDG Technology plugin.

• Free Tools: Most of the free SysML tools are based on the EMF and we can add them as plugins from their respective update sites.

-Papyrus : This plugin is intended to model any kind of EMF model, especially UML and related modeling languages as SysML.

-TopCased : This plugin is intended to model critical embedded systems including hardware and/or software, and its main modeling language is SysML. We have to note that until now they were releasing a dedicated plugin to integrate in eclipse but actually they are migrating their tools to the PolarSys organization which is an open source environment intended for embedded systems.

.

/ C

As seen in this section, SysML is a language intended for the systems engineering community based in UML and allows designers to model not only structural and behavioral properties but also to organize the requirements. For the purpose of this dissertation we will particularly focus in four of the nine diagrams: Block Deinition, Internal Block, Sequences, and Requirements. Requirement diagrams will be used to present the requirements to verify over the other ones. We also presented a vehicle safety system as a case study to show the use of these diagrams. Finally, we presented some of the main commercial and free tools used to model SysML diagrams.

I A

O ne of the several options to describe component behavior is the interface automata approach. In this chapter, we present an overview of the main concepts of this kind of automata proposed by Luca d'Alfaro and Thomas Henzinger en 2001. We will later used them in Part II to verify component compatibility in our proposed approaches. This chapter is organized as follows: in Section 4.1 we present a formal deinition of interface automata and its properties, Section 4.2 presents the application of interface automata to verify component compatibility, Section 4.3 presents some tools that we can use to verify if two components are compatible and we conclude this chapter in Section 4.4 with a conclusion.

. / D fi

Luca d'Alfaro and Thomas Henzinger introduced interface automata in [START_REF] De Alfaro | Interface automata[END_REF]. They used this automata to specify component interfaces and also to verify component assembly. For the matter of this dissertation, we exploit interface automata to model interfaces of SysML blocks (components).

The interface automata approach aims to describe the behavior of a component as an interface automaton, this automaton consists of a set of states and actions allowing the change of state. Actions are decomposed into three groups: input actions, output actions and internal actions. Input actions represent the methods than can be requested to the component, in which case they are the ofered services. These actions are labeled by the character "?". Output actions model the method calls or messages sent to another component. Therefore, they represent the services required by the component. These actions are labeled by the character "!". Internal actions are operations that can be activated locally and are labeled by the character ";".

Formally we describe an interface automaton as follows: • ⊆ is a subset of initial states;

• Σ , Σ , and Σ , respectively denote the sets of input, output, and internal actions. The set of actions of A is denoted by Σ ;

• ⊆ Σ is the set of transitions between states.

We deine by Σ (s), Σ (s), Σ (s), respectively the set of input, output, and internal actions at the state s. Σ (s) represents the set of actions at the state s.

0 1 _ _ ? _ ! _ _ _ Figure .
-Interface automaton for the sensor block

As an example, we present in Figure 4.1 an interface automaton representing the behavior of the sensor block presented in the BDD of Figure 3.2. The process to obtain this automaton will be described later on Part II. Besides this graphical representation, we can describe it formally as follows:

• = {0, 1} ; • = {0}; • Σ = { _ _ }; • Σ = { _ }; • Σ = ; • Σ = { _ _ , _ }; • = {(0, _ _ , 1), (1, _ , 0)}. . / A C V fi
The veriication of the assembly of two components (blocks) is obtained by verifying the compatibility of their interface automata. Before doing this veriication, it is necessary to ensure that the interface automata are composable.

Two interface automata 1 and 2 are composable if

Σ 1 Σ 2 = Σ 1 Σ 2 = Σ 1 Σ 2 = Σ 1 Σ 2 = .
This means that they can not share the same set of input, output or internal actions. In Figure 4.2 we present an automaton representing the behavior of the ACU block in the BDD on Figure 3.2, which we compose with the automaton in Figure 4.1.

0 1 2 _ ? _ ! ; _ ! _ ! _ _ _ Figure . -Interface automaton for the ACU block We deine by Shared( 1 , 2 ) = (Σ 1 Σ 2 ) (Σ 1 Σ 2
) the set of actions shared between 1 and 2 . The veriication of the compatibility of two interface automata is based on their synchronized product, 1 ⊗ 2 , obtained by synchronizing the interface automata on their shared actions (see Deinition 3.4 in [START_REF] De Alfaro | Interface automata[END_REF]).

Deinition 2: Synchronized Product

Let 1 and 2 be two composable interface automata. The synchronized product 1 ⊗ 2 of 1 and 2 is deined by:

• 1 ⊗ 2 = 1 2 and 1 ⊗ 2 = 1 2 ; • Σ 1 ⊗ 2 = (Σ 1 Σ 2 ) ⧵ ℎ ( 1 , 2 ); • Σ 1 ⊗ 2 = (Σ 1 Σ 2 ) ⧵ ℎ ( 1 , 2 ); • Σ 1 ⊗ 2 = Σ 1 Σ 2 ℎ ( 1 , 2 ); • (( 1 , 2 ), , ( ′ 1 , ′ 2 )) ∈ 1 ⊗ 2 if -∉ ℎ ( 1 , 2 ) ( 1 , , ′ 1 ) ∈ 1 2 = ′ 2 -∉ ℎ ( 1 , 2 ) ( 2 , , ′ 2 ) ∈ 2 1 = ′ 1 -∈ ℎ ( 1 , 2 ) ( 1 , , ′ 1 ) ∈ 1 ( 2 , , ′ 2 ) ∈ 2 .
Two interface automata may be incompatible due to the existence of illegal states in their synchronized product. Illegal states are states from which a shared output action from an automaton can not be synchronized with the same enabled action as input on the other component.

Deinition 3: Illegal States

Let 1 and 2 be two composable interface automata, the set of illegal states

( 1 , 2 ) ⊆ 1 2 is deined by {( 1 , 2 ) ∈ 1 2 | ∈ ℎ ( 1 , 2 ).(( ∈ Σ 1 ( 1 ) ∉ Σ 2 ( 2 )) ( ∈ Σ 2 ( 2 ) ∉ Σ 1 ( 1 )))}.
The interface automata approach is considered an optimistic approach. In this approach, the reachability of states in Illegal ( 1 , 2 ) does not guarantee the incompatibility of 1 and 2 . Indeed, in this approach one veriies the existence of an environment that provides appropriate actions to the product 1 ⊗ 2 to avoid illegal states. The states in which the environment can avoid the reachability of illegal states are called compatible states, ( 1 , 2 ). This set is calculated in 1 ⊗ 2 by eliminating illegal states, unreachable states, and states that lead to illegal states through internal actions or output actions, called also incompatible states. These states are eliminated by providing a legal environment which steers away from the illegal states by generating appropriate inputs. By eliminating these states in 1 ⊗ 2 , we obtain the composition 1 ∥ 2 . As a consequence, the interface automata 1 and 2 are compatible if 1 ∥ 2 ≠ [START_REF] De Alfaro | Interface automata[END_REF].

Deinition 4: Composition

The composition 1 ∥ 2 of two automata 1 and 2 is deined by: i.

1 ∥ 2 = ( 1 , 2 ), ii. 1 ∥ 2 = 1 ⊗ 2 ( 1 , 2 ), iii. Σ 1 ∥ 2 = Σ 1 ⊗ 2 , iv. 1 ∥ 2 = 1 ⊗ 2 ( ( 1 , 2 ) Σ 1 ∥ 2 ( 1 , 2 ))
We call the automaton = 1 ∥ 2 , the composite automaton.

The veriication of the compatibility between a component 1 and a component 2 is obtained by verifying the compatibility between their interface automata 1 and 2 . The main steps of the veriication algorithm of the compatibility between 1 and 2 (the complete algorithm in [START_REF] De Alfaro | Interface automata[END_REF]) are listed as follows:

Compatibility veriication algorithm:

1. verify that 1 and 2 are composable.

2. compute the product 1 ⊗ 2 .

3. compute the set of illegal states in 1 ⊗ 2 .

4. compute the set of incompatible states in 1 ⊗ 2 : the states from which the illegal states are reachable by enabling only internal and output actions (one supposes the existence of a helpful environment).

5. compute the composition 1 ∥ 2 by eliminating from the automaton 1 ⊗ 2 , the illegal states, the incompatible states, and the unreachable states from the initial states.

6. if 1 ∥ 2 is empty then 1 and 2 are not compatible, therefore 1 and 2 can not be assembled correctly in any environment. Otherwise, 1 and 2 are compatible and their corresponding component can be assembled properly.

The complexity of this approach is in time linear on

| 1 | and | 2 | [dAH01].
.

/ C V fi U

The veriication steps presented above have already been implemented in mainly two tools, The irst one is Ticc [AdAD + 06, dAFL06] which was developed by Henzinger and de

Alfaro, but is no longer available neither supported. The second one is Ptolemy II [BLL + 05] which is a tool for modeling, simulation and design of concurrent, real-time and embedded systems. Ptolemy II integrates a module to work with interface automata [START_REF] Lee | A behavioral type system and its application in Ptolemy II[END_REF], it represents the interaction between components that are represented as actors and evaluate their compatibility by various means, and one of those is the compatibility veriication by interface automata.

.

/ C

In this chapter we presented the interface automata approach introduced by d'Alfaro and Henzinger in which components are represented as automata. In this approach, component services are implemented as actions to change the component state. The goal of using interface automata is to verify the compatibility between components by synchronizing them in their shared actions and verify if there are states that are still accessible after the composition. In order to automatize the process of veriication we presented also the tool Ptolemy which allows to verify if two interface automata are compatible.

R W

T his chapter presents some ongoing research subjects in the scientiic community related to our matter in this thesis. The chapter is organized as follows: in Section 5.1 we present some relevant approaches about the generation of software architectures for CBS, in Section 5.2 we list some interesting approaches exploring component compatibility veriication, in Section 5.3 we list some proposals for describing component behavior. Section 5.4 introduce some approaches that propose how could we list and describe system requirements, particularly in SysML. We end the chapter with a conclusion in Section 5.5.

. / G CBS A

In [START_REF] Li | Formal and Use-Case Driven Requirement Analysis in UML[END_REF], the authors propose to specify formally system requirements from UML use case diagram and to exploit this formal model to construct the class diagram of the system. The diferences with our proposition are the use of SysML requirement diagram to specify requirements, and the situation of our work in the context of CBS, where we deal with the problem of component compatibility with the interface automata approach.

In [START_REF] Pétin | Combining SysML and formal methods for safety requirements veriication[END_REF], the authors propose a system modeling approach that combines SysML safety requirements and block diagrams, and the model checking approach to prove that the local behavior of each component contributes to satisfy system requirements. In this work the problem of component compatibility and the preservation of the requirements are not treated.

To construct systems, other approaches take into account all the requirements at once. For example, [vL03], based on KAOS framework [BDD + 97], and in [START_REF] Barais | A Framework to Specify Incremental Software Architecture Transformations[END_REF] the authors propose an incremental approach by adding structural and behavioral properties into a software architecture. Therefore, we were inspired by their vision concerning the require- ments where a requirement should be further decomposed to meet the atomic requirements which can be then linked to elementary software components.

In [CLR + 09], the authors propose a component-based design method called rCOS, its goal is to guide the process of system development from requirements elicitation through to coding, providing the formal deinitions of the models in a UML-based RUP development process. Although, our approach is similar to theirs, in the way we use sequence diagrams to express component interfaces, it lacks the use of a component library to look for third party components that can be reused and verify their compatibility.

The works proposed in [START_REF] Dromey | From requirements to design: formalizing the key steps[END_REF][START_REF] Dromey | Engineering Large-Scale Software-Intensive Systems[END_REF] are based on a behavior tree approach and translate atomic requirements into behavior trees. An interesting approach which inspired our approach in Chapter 8 was proposed in [START_REF] Lau | Constructing Component-based Systems Directly from Requirements using Incremental Composition[END_REF], the authors construct the system starting from raw requirements described in a natural language. Speciications of requirements are derived from intermediate requirement models, and these models approximate the raw requirements. These requirements are then directly mapped into system architecture, where a requirement is represented by an element in the system, thus, maximizing the match between the inal system and the raw requirements. This approach is based on a component model that supports incremental composition. However, this model is restrictive and does not consider component protocols and compatibility veriication, because their components do not have external dependencies, which ensures that newly added components do not alter the behavior of existing components. Our approach is diferent and proposes to map requirements, speciied and organized with SysML diagrams, directly into system architecture, by exploiting the interface automata formalism and the composition of component interfaces. Using SysML to list the requirements has the main advantage of seeing them graphically modeled and their relationships are explicitly mapped, which allows seeing the decomposition of the system in early stages of the development [START_REF] Soares | Model-driven user requirements speciication using SysML[END_REF]. The construction of system architecture is guided by the requirements, and the preservation of these requirements in the inal system is guaranteed by the compatibility of interface automata and the preservation of the component actions linked to the requirements.

. / C V fi

In the ield of the veriication of component compatibility, Bauer et al. [START_REF] Bordeaux | When are two web services compatible? Technologies for EServices[END_REF] suggested that "two services are compatible if they can interact properly", which is derived into: irstly the components having opposite behaviors, this means that when one component emits a message, the other one must receive that message and vice-versa, secondly there must not be unspeciied receptions, which means that all services requested from one component to the other one must be ofered, and thirdly the system must be free of deadlocks, in other words, during the interaction between the two services, all reachable states must be deadlock free.

In the ield of components, several approaches have been proposed to describe software architectures like those of [START_REF] Szyperski | Component Software: beyond Object-Oriented Programming[END_REF][START_REF] Medvidovic | A Classiication and Comparison Framework for Software Architecture Description Languages[END_REF]. Most models consider the components with their behavior, connectors, and provided/required services. The assembly operation of components may occur at diferent levels of abstraction, from the design of Dynamic Software Architectures (DSA) to the implementation in platforms such as CORBA [START_REF] Mchale | Corba Explained Simply[END_REF] or .NET [START_REF] Platt | Introducing Microsoft[END_REF].

In our case, we are interested in SysML blocks speciied by their interfaces and their behaviors modeled using Sequence Diagram (SD). We can cite as examples the model of Allen 1997 [AG97] where the protocols are associated with component connectors. Attie in 2006 [START_REF] Pc Attie | Behavioral Compatibility Without State Explosion: Design and Veriication of a Component-Based Elevator Control System[END_REF] combines protocols to interfaces connecting two components. Others, like Becker in 2004 [START_REF] Becker | Classifying Software Component Interoperability Errors to Support Component Adaption[END_REF] propose a framework for comparing models with three levels of interoperability using the signatures, the protocols associated to the components and quality of service. The protocols of Magee et al. 1999 [START_REF] Magee | Behaviour Analysis of Software Architectures[END_REF] are based on works on automata and competition using the formalism of transition systems, including the analysis of reachability. The composition operation is essential to deine the assembly and verify the safety and liveliness properties.

The crucial question that arises to the developer is whether the proposed assembly is valid or not.

The approach of Moizan et al. 2003 [START_REF] Moisan | Behavioral substitutability in component frameworks: A formal approach[END_REF] aims to provide UML components with the speciication of their protocols. The behavior description language is based on hierarchical automata inspired by StateCharts. It can support mechanisms for composition and reinement of behaviors. Properties are speciied in temporal logic.

Attiogbé et al. [AAA05, AAA06

] deine a component model based on services named Kmelia. In this approach they associate components through communication channels following a syntax inspired from Hoare's CSP [START_REF] Hoare | Communicating sequential processes[END_REF]. The behaviors are described by automata and associated to services. To verify component compatibility, they encode the Kmelia components into L processes [START_REF] Iso Lotos | A formal description technique based on the temporal ordering of observational behaviour[END_REF] which are the input of the toolbox for protocol validation and veriication CADP [FGK + 96].

Teixeira in 2011 [START_REF] Sueina | Compatibility Evaluation of Components Speciied in UML[END_REF] proposed an approach to evaluate the compatibility of components speciied in UML, they use the state machine diagram to describe component behaviors which are then translated to a Petri net to identify compatibility problems Although a system architecture is composed by several components, and there are approaches like [START_REF] Carmona | Compatibility in a multi-component environment[END_REF] which propose to verify compatibility in a multicomponent environment by using team automata [START_REF] Ellis | Team Automata for groupware systems[END_REF], we are constrain to verify components by pairs who must not share the same input (resp. output) actions, which allows us to use interface automata obtained from SD.

Other works deal with the inclusion of real-time constraints as in Etienne and Bouzefrane in 2006 [START_REF] Etienne | Vers une approche par composants pour la modélisation d'applications temps réel[END_REF]. It aims to determine the characteristics of components and to deine some criteria to verify compatibility of their speciications during the assembly phase using the tool Kronos.

Our approach allows analyzing the consistency, composability and compatibility between blocks. It combines semi-formal models based on SysML and formal models based on interface automata for correct assembly between blocks.

. / C B D

In this thesis we explore the substitutability and compatibility of software components. Substitutability is the ability of the component to replace another one without been noticed by the clients. Compatibility is the ability of a component to interact properly with other one when connected.

[VVR06] proposes the use of session types, [START_REF] Honda | Language Primitives and Type Discipline for Structured Communication-Based Programming[END_REF] to describe the dynamic behavior of components additionally to the simple descriptions usually provided by software component interfaces, other like [JMO10] use timed automata.

The ability of SD to express the behavior of a system has been exploited before, like in [HL07, HK07, VT04, RF06, GMP11] where they are translated into state machines, Petri nets or even Java code skeleton, nevertheless they are not formally veriied as it is proposed in [LTM + 09]. This later proposes to translate SD into a Promela-based model to simulate its execution and therefore verify properties written in Linear Temporal Logic (LTL) [START_REF] Clarke | Model Checking[END_REF] that can be checked with the model-checker SPIM [START_REF] Holzmann | Design and validation of computer protocols[END_REF].

. / R S fi S ML

Soares [START_REF] Soares | Model-driven user requirements speciication using SysML[END_REF][START_REF] Dos | A proposed extension to the SysML requirements diagram[END_REF] proposed a methodology for Model-based Requirements Engineering using the SysML Requirements and Use Case diagrams. They chose SysML because it allows to have a structured graphic model of the requirements and also a tabular format which may facilitate the traceability of requirements during the system life cycle. In this approach, irst, all the atomic requirements are classiied by type:

• Functional: describes what the users expect the system should do to be useful (functionalities), this type of requirements includes information about logical databases like frequency of use, data entities, and integrity constraints.

• Non-functional:are related to emergent system properties such as reliability, safety or response times. They do not depend from a single element in the system, they are evaluated on the emerging system by assembling the system components.

• External: describes all the inputs and outputs of the system, it can include other systems, users, hardware, software, or communication interfaces.

Then, they represent all the requirements in a SysML Requirement diagram which helps to deine their relationships, which can be useful for discovering subsystems and limit system architectures. At this stage, requirements are also listed in a tabular form to allow their traceability during the system life cycle, this is important to trace when a requirement has been changed, satisied or deleted. Finally, SysML Use Case diagrams are used to represent the actors involved in the system and the use cases which helps to delimit the system. I n this chapter, we propose to exploit SysML language and the relation of reinement between components, to deine the architecture of CBS from an abstract component. As seen above in Chapter 3, a SysML speciication of a system is described by structural diagrams and behavior diagrams. Our approach is based on processing an incremental reinement from an abstract level toward more detailed levels. In our case it is a question of replacing an abstract block in a speciication by a composition of blocks preserving its structural properties and its behavioral properties.

Structural diagrams of SysML describe the system in static mode and behavioral diagrams describe the dynamic operation of the system. We note that the term used in SysML for components is blocks, and they are modeled by two diagrams, the BDD, which deines the architecture of the blocks and their performed operations, and the Internal Block Diagram (IBD), which is used to deine the ports of each block and transactions exchanged between them through their ports. During the reinement process, these two diagrams can be checked to decide whether the proposed architecture of components satisies or not the requirements deined by an abstract component. Let be an abstract block described by a , and an , these both diagrams specify the system architecture. Let 1 , ..., be the set of blocks composing according to the , so 1 , ..., reine by decomposition if:

• 1 , ..., reine structurally ,

• 1 , ..., reine behaviorally , Therefore, to verify the reinement between a block and its sub-blocks, we verify the conditions of consistency and compatibility for structural reinement and alternating simulation for behavioral reinement (see Figure 6.3). To achieve this veriication, we need to specify by Sequence Diagrams (SD) the behavior description of the abstract block and its composing sub-blocks, and then, by exploiting the approach proposed in [START_REF] Chouali | Formal veriication of components assembly based on SysML and interface automata[END_REF], we associate an interface automaton to each SD. These automata are exploited to verify the compatibility between sub-blocks by means of Ptolemy tool [START_REF] Lee | A behavioral type system and its application in Ptolemy II[END_REF], which generates the composition automaton from two interface automata as input. Then we verify the behavioral reinement by means of the MIO Workbench [START_REF] Bauer | On Weak Modal Compatibility, Reinement, and the MIO Workbench[END_REF], which veriies if a behavioral speciication is reined by an implementation using Modal Input/Output (MIO) automata as data input. According to the speciications of SysML 1.3 in [START_REF] Omg | Systems Modeling Language (SysML) Version 1.3[END_REF], each port associated to a block is typed by an interface block which exhibits the provided or the required services related to the port. These latter deine the set of input and output actions of a block. is the set of parts, where each part represents an instance of a block,

• and are respectively the sets of internal input and output ports.

These ports are related to the parts in the .

• and are respectively the external input and output ports. These ports are related to the composite block described by the .

• the function

∶ →

associates input and output ports to other input and output ports, it deines the links between blocks. and are respectively the sets of input and output ports.

For example, the internal block diagram for the block SensorsControl shown in Figure 6.7 will be formally speciied as:

• Φ = { , }, • = { ⟨ _ ⟩, ⟨ _ ⟩}, = { ⟨ _ ⟩, ⟨ _ ⟩} . • = ⟨ _ ⟩, = ⟨ _ ⟩. • ( ⟨ _ ⟩) = ⟨ _ ⟩, ( ⟨ _ ⟩) = ⟨ _ ⟩, ( ⟨ _ ⟩) = ⟨ _ ⟩, ( ⟨ _ ⟩) = ⟨ _ ⟩.
. / S R fi S ML B

In this section we describe our structural reinement process by deining the reinement relation that we exploit to validate SysML architecture of systems. An initial version of this structural reinement approach was published in [START_REF] Carrillo | Formalizing and verifying compatibility and consistency of SysML blocks[END_REF].

We deine a reinement relation between composite blocks (abstract) and their sub-blocks in order to validate SysML system architecture, and to guarantee the decomposition between blocks and sub-blocks. Thus, we analyze the case where an abstract block described with SysML models (BDD and IBD) is reined by a set of sub-blocks, which are described by the internal block diagram of their abstract block. In this case, the sub-blocks reine structurally the abstract block if it is possible to replace the abstract block by its sub-blocks without afecting the set of ofered and required services of the system, and without causing system malfunction. Therefore, to deine the reinement relation, we identify two conditions in which the reinement is based:

• Consistency: the set of sub-blocks are consistent with their abstract block if they ofer at least the same services as the abstract block, and they require at most the same services. This relation ensures that the sub-blocks do not afect the services of their abstract block.

• Compatibility: the set of sub-blocks are compatible if the interoperability holds between them, which means that they interact correctly without causing deadlocks or system malfunction.

Deinition 9: Structural reinement of SysML blocks

Let be an abstract block described with the , and the internal block diagram of . Let 1 , ..., be the set of blocks composing according to the , so 1 , ..., reine structurally if:

• 1 , ..., are consistent with ,

• the interacting blocks 1 , ..., according to are compatible.

In the following section, we deine formally the consistency conditions that must be respected between abstract block and its sub-blocks to verify partly the relation of structural reinement.

. . / C C V fi B

We propose to verify that the sub-blocks are consistent with their parent block by looking if the provided and required services in the abstract block are in accord to those in the composing sub-blocks. Indeed, the consistency condition proposed here allows us to determine if the ofered services of the abstract block are provided by the sub-blocks that compose it. Similarly, it is veriied whether the required services by the composed sub-blocks are required by the abstract block. In addition, composability ensures that the blocks in question do not share the same inputs and/or the same outputs. These conditions are described in the following:

We consider an abstract block , and and two linked sub-blocks, by a connector, in the set 1 , ..., of composing sub-blocks described in an internal block diagram , Φ , Φ , Φ are respectively the ofered services (input actions) of the blocks , , , Φ , Φ , Φ

are respectively the required services (output actions) of the blocks , , , and Φ , Φ , Φ are respectively the internal actions of the blocks , , . We deine the set of shared actions between and by the set ℎ ( ,

) = (Φ Φ ) (Φ Φ ).
The composition of the blocks 1 , ..., is consistent with if :

• Condition 1 (Composability):

For every pair of connected sub-blocks { , }, it holds that:

Φ Φ = Φ Φ = Φ (Φ Φ Φ ) = Φ (Φ Φ Φ ) =
This condition ensures to compose and and to apply later the interface automata theory to verify their compatibility.

• Condition 2 (At least the same inputs):

For a sub-block connected to the external input port it holds that: Φ ⊆ Φ This condition ensures that the sub-block ofers at least the same services (inputs) as the abstract block .

• Condition 3 (At most the same outputs):

For a sub-block connected to the external port it holds that: Φ ⊆ Φ .

This condition ensures that the sub-block requires at most the same services (outputs) as the abstract block .

Remark: Note that according to formal deinitions of conditions 1,2, and 3, their veriication is possible on to the formal speciications of the used SysML model: blocks, BDD, IBD, and block interfaces (see the Algorithm 1 on page 55).

Case Study Consistency Verification

To verify the consistency between the composite block and its composing sub-blocks (see Figures 6.5 and 6.7), we irst identify the connected sub-blocks in its BDI. From the BDI in Figure 6.7 we obtain:

The list of parts in the block will be instances of its composing sub-blocks:

Φ = { , },
we then identify the ports of its composing sub-blocks from the list of internal ports in block:

= { ⟨ _ ⟩, ⟨ _ ⟩}, = { ⟨ _ ⟩, ⟨ _ ⟩},
for each of the identiied ports we use the function to determine its associated counterpart:

( ⟨ _ ⟩) = ⟨ _ ⟩, ( ⟨ _ ⟩) = ⟨ _ ⟩, ( ⟨ _ ⟩) = ⟨ _ ⟩, ( ⟨ _ ⟩) = ⟨ _ ⟩.
We identify the counterparts that are other sub-blocks to determine the connected subblocks, that in this case are and .

Then, as exposed in Condition 1 we check the sub-blocks composability by considering the input, output, and internal actions of each sub-block. These actions are described in the interface blocks of the proposed BDD of Figure 6.6, we formally list them as follows:

Φ = { }, Φ = { }, Φ = Φ = { }, Φ = { _ , _ , _ , _ }, Φ = { _ , } ℎ ( , ) = { }
Notice that we do not ind inputs or outputs that are present simultaneously in both subblocks, ie.

Φ Φ = Φ Φ = Φ (Φ Φ Φ ) = Φ (Φ Φ Φ ) = ;
Then we check the condition 2, and we ind that the input Φ = { } of the abstract block SensorsControl is present in the connected sub-block Sensors, ie.

Φ ⊆ Φ

.

Finally for Condition 3, we check that the outputs

Φ = { _ , _ , _ , _ }
of the abstract block are the same required outputs of the connected sub-block ACU, ie.

Φ ⊆ Φ

.

We can therefore conclude that the blocks and are consistent with .

. . / I A G

The aim of this section is to show the process of generating the interface automata that describe the behavior of the analyzed sub-blocks. We can generate an interface automaton from a sequence diagram that represents the behavior of each block. In the following we present an overview of the approach described in [START_REF] Chouali | Formal veriication of components assembly based on SysML and interface automata[END_REF], which we exploit to generate interface automata. This approach is based on an algorithm that accepts as entry the formal deinition of a sequence diagram (see Deinition 11), which is also based on the formal definition of messages (see Deinition 10) between blocks and environment, and generates as output the components of the corresponding interface automata.

Deinition 10: Message

A message is a tuple:

⟨ , , , ⟩ where :

• is the source block of the message,

• is the target block of the message,

• is the called method

We consider that in a set of messages and an block, the following condition is valid :

∀ = ⟨ , , , ⟩ ∈ we have = or =
. This condition allows us to translate sequence diagrams into interface automata. In the following deinition we consider only the combined fragments , , and which are suicient to the translation to interface automata. In this section, we describe our behavioral reinement process by deining a relation between SysML Sequence Diagrams (SD). In our approach, behaviors are described with SysML SD and when an abstract block is replaced by two or more concrete blocks, we reine its behavior with the actions of the composing blocks. To verify if the abstract block behavior is well reined by the actions of the composing blocks, we verify if the alternating simulation [START_REF] Alur | Alternating reinement relations[END_REF] holds between the IA of the composition and the IA obtained from the SD of the abstract block.

.

. / A S

In order to verify if the composition of a set of blocks reines the behavior of an abstract block, we use the concept of Alternating Simulation for interface automata [START_REF] Alur | Alternating reinement relations[END_REF].

To deine alternating simulation formally, we use the notation ⟶ * ′ for interface automata to mean that there exists a sequence of internal transitions leading from to ′ . Then, we deine alternating simulation for interface automata as commonly used in software speciication [START_REF] De Alfaro | Interface-Based Design[END_REF]. Usually interface automata reinement is veriied by alternating simulation and instead of building a new tool we propose to use the MIO Workbench module to verify modal reinement. Larsen et al. proposed Theorem 1 (a proof can be found in [START_REF] Kim | Modal I/O Automata for Interface and Product Line Theories[END_REF]) to show that we can use observational modal reinement as it coincides with alternating simulation.

Theorem 1: Alternating simulation and observational modal reinement

Alternating simulation and observational modal reinement coincide for interface automata in the following sense:

for any two interface automata , : ≤ if ( ) ≤ * ( ) Indeed, interface automata can be translated into modal automata to use observational modal reinement. This can be achieved by applying the translation function.

Let be a fresh state that allows all behavior but does not require any behavior. If denotes the universe of all inputs, such that for all interface automata , Σ ∈ , then we deine the translation function as follows: .

Deinition 15: Translation function ( , , Σ , Σ , Σ , ) = ( , , Σ , Σ , ⟶ ♢ , ⟶ □ ) where = { }, = , Σ = Σ , Σ = Σ
As an example, we apply the function over the interface automaton 2 associated to the

0 1 2 3 ? ; _ ! _ ! _ ! _ ! _ _ _ _ Figure .
-IA associated to the SensorsControl abstract block .

/ C

We have shown in this chapter, how to specify formally systems described by SysML models with BDD, IBD and SD diagrams. Then, we deined a reinement relation between SysML system blocks, described by structural and behavioral diagrams. The reinement in SysML is an essential concept and it is based on the development of a process from an abstract level towards more detailed levels, which can end in its implementation. Our reinement ensures an incremental substitutability of an abstract block in a speciication by a composition of blocks preserving its structural and behavioral properties.

To verify structural reinement speciied in BDD and IBD diagrams, we veriied irst if the sub-blocks were consistent with the abstract block speciication and then we veriied if they were compatible by applying the model of interface automata. Interface automata were obtained from the SysML SD of each composing sub-block.

To verify behavioral reinement, we applied the approach of alternating simulation for interface automata to verify if the composition of the set of sub-blocks simulated the expected behavior in the abstract block. To ease the task of verifying alternating simulation we proposed to use the module Observational Modal Reinement of the tool MIO Workbench.

To use this tool, we translated interface automata into modal automata.

F V fi S ML R

T his chapter presents a formal veriication technique based on the approach proposed by V. Lima et al. in [LTM + 09]. This technique proposes to create a Promela-based model from UML interactions expressed in Sequence Diagrams (SD), and uses SPIN model checker [START_REF] Holzmann | Design and validation of computer protocols[END_REF] to simulate the execution and to verify properties written in Linear Temporal Logic (LTL) [START_REF] Clarke | Model Checking[END_REF]. In Figure 7.1, we show the position of the contribution presented in this chapter, regarding the contributions of this thesis.

. / A O

To verify if a component satisies a given requirement, we propose to use the tuple Promela/SPIN. We choose them because it provides important concepts for implementing SD: sending and receiving primitives, parallel and asynchronous composition of concurrent processes, and communication channels. Our adaptation of the approach proposed by V. Lima et al. concerns a particular type of sequence diagrams that we exploit to specify the block behaviors.

We propose to use a particular type of SD with only two lifelines, one for the block and one for the environment. Thus, SD can be further translated into interface automata as exposed in [START_REF] Chouali | Formal veriication of components assembly based on SysML and interface automata[END_REF]. In this diagram the exchanged messages will be the ofered services as calls from the environment and the required services as calls to the environment. The main advantage of using SD for veriication is that we can verify temporal properties over it. Messages follow a sequence order that we can trace to detect deadlocks or execution of paths. Figures 7.2 and 7.4 show the interfaces, by SD, for two blocks: sensors and ACU. These are blocks from our block library. In these diagrams we notice that there are only two lifelines and messages are sent to/received from the environment.

Before presenting the veriication approach, we show in the following section a short presentation of LTL.

. / L T L (LTL)

Linear temporal logic is a modal temporal logic with operators referring to time and used for reasoning about ininite behaviors of reactive systems. LTL is mostly used as the logic to specify the properties to verify in model checking environments, such as SPIN.

.

. / S

The set of well-formed LTL formulas Φ is constructed from a set of atomic propositions = { 0 , 1 , ...}, the standard boolean operators: ¬ (not), (or), (and), and the temporal operators: ○, to be read as "next", and , to be real as until. The formula s ○ , means that is true at the next step. And the formula means that is true at some point, and is true until that time. The until operator allows deriving the temporal operators • Eventually ⋄ ∶= , means will become true at some point in the future.

• Always □ ∶= ¬ ⋄ ¬ , means is always true.

The set of LTL formulas over is inductively deined as follows:

• every atomic proposition in belong to Φ.

• if and are formulas in Φ, then ¬ , , ○ , and are formulas in Φ.

.

. / S

Let be an LTL formula, can be satisied by an ininite word that can be viewed asword on an execution path of a Kripke structure. Let = 0 , 1 , 2 , ... over 2 (the set of propositions), be such an -word, where at some time point ∈ ℕ, a proposition is true if ∈ . We note by the suix of starting at . The satisfaction relation ⊧ between a word and an LTL formula is deined as follows:

• In this work we exploit LTL to express properties, specifying SysML requirements, to be veriied on components by means of the model-checker SPIN. These properties are expressed as LTL formulas, and SPIN requires, as input, their corresponding negative formulas, which are converted into Büchi automata to be exploited in the model-checking algorithm.

⊧ if ∈ 0 . • ⊧ ¬ if not ⊧ . • ⊧ if ⊧ or ⊧ . • ⊧ if ∈ ℕ such that ⊧ ∀ ∈ ℕ, 0 ≤ < , ⊧ .

. / V fi SPIN M C

As exposed above in the overview, we exploit and adapt the approach proposed in [LTM + 09] to translate SD to Promela-based models to verify properties with the modelchecker SPIN. Table 7.1 shows the Promela representation of the main elements in SD. Alternative and loop combined fragments are represented as if condition and do operator in Promela respectively, guard condition is declared globally and the non-deterministic behavior is implemented at init time by assigning diferent values to the guards.

Figures 7.3 and 7.5 show partially the Promela representation for the sensors SD and ACU SD respectively (the complete code is presented at the end of this chapter in Listings 7.1 and 7.2). In both diagrams, we notice that their two lifelines are translated as processes in the Promela code, one process for the block and one other for the environment. Both processes are started at the same time thanks to an atomic call at the main process init. We also notice that loop combined fragments are translated as do statements. The alternative combined fragment, alt, in ACU SD is translated as if statement. There, the three possible range values for deceleration are assigned at init time by using an if clause, this way, SPIN will choose non-deterministically, which of the three values will be used to simulate the system.

Once the sequence diagram is translated, the component can be simulated as a SPIN system. However, in order to verify whether the component satisies an LTL property, the authors propose to use a series of lags to keep track of who is sending/receiving what message to/from whom at any time of the execution. In our approach we verify properties over independent components with only two lifelines in their SD, one line for the selected component and the other for the environment. So, we do not use a lag related to to/from whom is sent a message as it will always be the other lifeline. These lags are updated together at each send/receive event using a d_step statement. The lags for our example in . / R fi LTL

After deining the lags to track the execution state of the system, LTL properties can be written as boolean expressions over the lags. In our approach, we propose to translate SysML requirements to LTL properties by respecting this formalism with lags. Hence, for example requirement 1.1.1 in Figure 8.3 can be expressed as: always after receiving a call to get_sensor_values, the sensor block will send a message with the sensor_values. The boolean expression, using the lags described before, will be:

□((sensors && receive && msg_get_sensor_values) → ♢ (sensors && send && msg_sensor_values))
Similarly, requirement 1.1.2 can be expressed as: always after receiving a message with the sensor_values, the ACU will send a message deciding to lock the seat-belt, activate the airbag or wait for another call, and the boolean expression with lags will be:

□((acu && receive && msg_sensor_values) → ♢ (acu && send && (msg_reset || msg_act_sb || msg_act_ab)))
These properties are further veriied over their corresponding Promela model by using SPIN model-checker, which indicates if blocks satisfy the properties. Once a corresponding block is found for a requirement, we continue with another requirement to start building the system architecture.

.

/ C S P

In the following, we present the complete Promela descriptions for the blocks sensors and ACU. To obtain these listings, we used a tool developed by us under the Eclipse framework, by means of an ADL and Acceleo transformation.

Listing

. / C

We have presented in this chapter our proposal to verify SysML functional requirements over SysML blocks. To solve this issue, we have translated requirements into formal properties using linear temporal logic. LTL properties were then veriied over a formal model of a SysML block. Formal models of SysML blocks were obtained by applying the approach of V. Lima et al. to translate SysML sequence diagrams into Promela descriptions. Finally we used the model-checker SPIN to verify LTL properties over the Promela descriptions.

I S fi CBS A G V fi S ML R
T he CBS are widely used in the industrial ield, and they are built by assembling various reusable components (third party components), allowing reducing their development cost. The success of the CBS development is related to the process of building complex systems by assembling smaller and simpler components. Generally these systems are made larger because they are developed with software frameworks. However, this development is a hard task due to two reasons. The irst is the diiculty to decide what to build and how to build it, by considering only system requirements and reusable components. Therefore, the question that arises is: how to specify a CBS architecture satisfying all system requirements? The second reason concerns the compatibility between the set of reusable components that compose the system, which must be guaranteed. Indeed, generally, one exploits reusable components from a component library to construct CBS, thus we need to guarantee component compatibility.

In this chapter, we discuss the relationship between system requirements and CBS architecture speciication. Our goal is to propose a methodology, to the CBS speciier, to build a consistent system architecture that formally fulills all the system requirements. To achieve this goal, we exploit the SysML requirement diagram to specify and organize system requirements, SD to describe components behavior, and BDD and IBD to specify

. / O

We propose an approach to construct a CBS system and to specify its architecture directly from SysML requirements. Our goal is to obtain a consistent architecture respecting all the speciied requirements. To specify this architecture, the software architect exploits a library of reusable components (or blocks). These components are considered as black boxes and described only by their interfaces, speciied with SD. So, we propose to specify CBS requirements with SysML requirement diagram, then analyze this diagram in order to associate one by one its atomic requirements (can not be decomposed) to software components that satisfy them. The satisiability is evaluated by performing a formal veriication step with a model-checker. Each veriied component is tested for compatibility with the other components in the composition and then added to the partial architecture that must preserve the atomic requirements.

In our approach, a CBS is speciied with a SysML requirement diagram that shows the functional requirements, and component interfaces describe component protocols by sequence diagrams. The main steps of our approach, presented in Figure 8.2, can be described as follows:

1. Start by analyzing the SysML requirement diagram to obtain the atomic requirements because they are more precise, and it is easier to ind components that satisfy them (see Section 8.3).

2. Let be the irst atomic requirement, let be a component from the component library, described by the sequence diagram . Specify with the LTL formula and translate to the Promela code , then verify that satisies by verifying that satisies with the model checker SPIN (see Section 7.3). The selection of the component in the library is done by the software architect. However, it is possible to guide this selection (or to automate it) because is a functional requirement, and describes constraints on ofered and required services (Input/output actions). These services are also described in component interfaces. So it is easy to extract these services from and to match them with those described in the interfaces. If this step returns false, then does not satisfy , therefore one has to obtain the appropriate component in other libraries, or to develop it from scratch.

Let be the interface automaton describing the component protocol and obtained

from the sequence diagram (see Section 8.4).

4. Identify the input and output actions in related to (Section 8.4 ).

5. Repeat until all the requirements are treated .

(a) Let +1 be the next atomic requirement, connected to (see Deinition 19), let +1 be a component satisfying +1 , thanks to the LTL formula +1 and the Promela code +1 . Let +1 be the interface automaton describing the component protocol.

End repeat

According to the main steps of our approach, we validate the inal architecture of our CBS when all the atomic requirements are analyzed without problems of component compatibility and/or requirement preservation.

.

/ C S

To illustrate our approach, we use the case study of the vehicle safety system presented in Section 1.4. The associated requirement diagram that speciies the system needs is shown on Figure 8.3.

In this diagram, the initial requirement 1 asks for ensuring passengers lives and it is decomposed into two requirements 1.1 and 1.2 that ask for two safety devices: an airbag system, which must be deployed whenever the car is in a collision, and the seatbelts that must be locked when the sensors detect strong movements, therefore, this last is an atomic requirement as it is not decomposed. On the left side, requirement 1.1 is further decomposed into requirements 1.1.1, 1.1.2, and 1.1.3 which are atomic ones. Requirement 1.1.1 asks for the capture and sending of sensor values to an Airbag Control .

/ S ML R D A

In this section, we specify formally the SysML requirement diagram in order to analyze it and to extract formally the atomic requirements. Then, we show that it is suicient to a CBS to satisfy only the atomic requirements in order to satisfy all the requirements speciied in the requirement diagram. In the following deinition we consider two relations of SysML requirement diagram.

• Containment: exploited to decompose a requirement into other ones more precise.

• Derivation: exploited to connect a requirement with other ones that derive from it. Proof. Due to the semantic of the relation derive in SysML requirement diagram (and also the semantic of requirement diagram), it's obvious to state that a system satisies all requirements that are speciied by a requirement diagram if it satisies the initial requirements and all the ones that are derived (linked by the relation derive) directly or indirectly from them. Indeed, the satisfaction of the derived requirements does not guarantee the satisfaction of the initial ones. Since the atomic requirements are either derived (directly or indirectly) from initial requirements, or related by the relation of containment (directly or not) to initial requirements. And due to the semantic of the containment and the derive relations, the satisfaction of atomic requirements leads to the satisfaction of the requirement which are linked to them. Therefore it is suicient to satisfy atomic requirements to satisfy all requirements. For example in Figure 8.4, the requirements to satisfy (initial and derived) are { 0, 1, 2}. The derived requirements are 1 and 2, and the initial requirement is 0. However, to satisfy a requirement composed of other ones, it is suicient to satisfy the requirements that compose it. This process is repeated until all the atomic requirements are satisied. So, to satisfy 0, it is suicient to satisfy 01 and 02. And to satisfy 01 it is enough to satisfy 011 and 012. Therefore, to fulill all requirements, it is necessary to satisfy { 1, 2, 02, 011, 012}, which deines the set of atomic requirements in our requirement diagram. □

. / C A P S ML R

In this section, we specify interface automata from sequence diagrams thanks to the approach proposed in [START_REF] Chouali | Formal veriication of components assembly based on SysML and interface automata[END_REF], then we propose to compose components and to verify compatibility between them, using their interface automata, by applying the algorithm presented in Chapter 4. We propose also to verify, at the same time as the compatibility veriication is done, whether the atomic SysML requirements are preserved over the composition. Indeed, this veriication allows avoiding the requirement veriication over the obtained composite component, thus, we avoid the state explosion problem for the model checker. Before presenting the algorithm to verify the preservation, we show in the following sections that SysML requirements are related to Input/Output actions of interface automata, and their preservation is related to the preservation of their related actions by the composition.

. . / F R I /O A

The atomic requirements considered in this work concern the functional properties of a CBS. They are related directly to input and output actions of components. Therefore, for each atomic requirement we associate the sets of input and output actions provided by a component.

Let be the set of atomic requirements in the speciication of a requirement diagram. Let be an atomic requirement satisied by the component . Let be the interface automaton describing the protocol of . So, is associated to input actions = { 1 , ..., }, and output ones = { 1 , ..., }.

For example the irst atomic requirement in our case study is 1. The actions related to atomic requirements are formalized by transitions in the interface automata, labeled with these input/output actions.

Deinition 19: Connected requirements

Let and ′ be two atomic requirements speciied in a SysML requirement diagram. and ′ are related respectively to the set of input actions , and ′ , and output ones , and ′ . and

′ are connected if ′ ≠ or ′ ≠ .
According to Deinition 19 and to the condition of composability of interface automata (see Chapter 4), it is obvious to state that two components satisfying two connected atomic requirements are composable. We exploit this deinition in our approach: at each iteration of our approach, we choose an atomic requirement which is connected with the requirement in the iteration -1, in order to compose their components, otherwise the composition is not allowed.

. . / P I /O A A C

In this section, we show that the composition of two interface automata does not guarantee the preservation of their non shared input/output actions in the obtained composite automaton, despite their compatibility.

In fact, in the item (iii) of Deinition 4, the authors in [START_REF] De Alfaro | Interface automata[END_REF] indicate that the set of actions in the composite automaton = 1 ∥ 2 is the same as the set of actions in the synchronized product 1 ⊗ 2 , however, the set of transitions in is not the same as the one in 1 ⊗ 2 (according to Deinition 4). Indeed, the set of transitions in is included in the one of 1 ⊗ 2 . Thus, there may be input/output actions in Σ which are not associated to transitions in . In fact according to the optimistic approach of interface automata, despite that 1 and 2 are compatible, and ≠ , there may be shared input/output actions between 1 and 2 which do not synchronize, but certainly, there are also shared actions which synchronize (because ≠ ). Therefore, the transitions labeled with the shared input/output actions, which do not synchronize, will be eliminated from = 1 ∥ 2 because they lead to illegal states. But the related input/output actions (which label the eliminated transitions) remain in the set of actions in , because the composite component described by the composite automaton could provide these actions, and with the optimistic approach, one decides that it is compatible, because one supposes the existence of the helpful environment which never enables these actions (for more illustration see the example in [START_REF] De Alfaro | Interface automata[END_REF]).

. . / V fi P A R C .

In this section, we show the conditions that the composition of components should respect to preserve the requirements of the composed components. And we show also how to verify these conditions by adapting the compatibility veriication algorithm of interface automata (see Chapter 4).

The preservation of the atomic requirements by the composition of components is necessarily related to the preservation of the input/output actions, associated to these requirements, by the composition of their interface automata. Furthermore, in Section 8.4.2, we indicate that some input/output actions may belong to the set of actions of a composite automaton, but they do not label transitions in this automaton. Hence, in this case we state that these actions are not preserved.

Condition of Input/Output action preservation: An action (input or output) is preserved by the composition of two interface automata, 1 and 2 , if there is at least one transition in the composite automaton, = 1 ∥ 2 , which is labeled with . Which means that the action belongs to the set of Input/Output actions in , when is not shared between Verification algorithm overview: To verify the preservation of atomic requirements by the composition, we propose to adapt the compatibility veriication algorithm [START_REF] De Alfaro | Interface automata[END_REF] (Chapter 4). We verify whether the transitions labeled with input/output actions, related to atomic requirements, are preserved in the transition set of the obtained composite automaton ∥ +1 . This adaptation consists on: to calculate in the step (2) of the compatibility veriication algorithm, the set of transitions in ⊗ +1 , noted , related to the requirements. When we eliminate transitions in the step (5) of the compatibility veriication algorithm, we eliminate also these transitions in . Finally, we verify that all the actions related to the requirements, are associated to at least one transition in , after step (6).

We notice that this adaptation does not increase the complexity of the compatibility veriication algorithm (this can be easily veriiable). So the complexity of the presented algorithm is | ⊗ +1 |. However, in order to calculate the time complexity of one step in our approach, we have to consider a component associated to the current requirement to analyze, . This component is selected from the components library speciied by the set = { 1 , 2 , ..., }. We consider also the sequence diagrams that speciies the protocol of . In each step we have to verify that the current component satisies the current requirement thanks to the Promela code of and to the model checker SPIN. And we verify also the compatibility between the current component and the composite component, , obtained in a precedent step. So the time complexity of one step in our approach is analyzed as follows:

• to select a component from the set that should satisfy an atomic requirement, the complexity is: (| |)

• to verify that satisies , the complexity is :

(| | 2 | | )
, where is the automaton calculated by SPIN from the Promela code associated to (this is the complexity of the LTL model checking), and the LTL formula that speciies the requirement .

• After verifying the atomic current requirement on the component, we verify the compatibility between and and the preservation of the requirements by the composition. The complexity of this step is : (| ⊗ |), where and are the interface automata associated respectively to and .

Therefore, to calculate the complexity of the whole approach, we have to consider the complexity of one step and the number of the atomic requirements which deines the number of steps.

To demonstrate the correctness of our approach, we should prove that the composition of two components preserves the atomic requirements if the composed components are compatible and the input and output actions related to these requirements are preserved according to the condition of preservation of input/output actions. Indeed, each step in the incremental approach is based on the compatibility and the preservation of the atomic requirements by the composition. Thus, it is suicient to show the correctness of a step in our approach.

Theorem 3: Preservation of requirements

Let be a component satisfying the atomic requirement and the interface automaton of , let be the set of input actions related to and the output ones. Let +1 be a component satisfying +1 and +1 the interface automaton of +1 , let +1 be the set of input actions related to +1 and +1 the output ones.

The composite component = ∥ +1 preserves the requirements { , +1 } if the interface automata , and +1 , are compatible, and the input and output actions, , +1 , , and +1 are preserved in .

Proof. The component satisies means that the program Promela describing the component behaviors satisies the LTL property specifying the requirement . In our approach, component behaviors are also described with an interface automaton , and these behaviors are execution paths in the interface automaton. The functional requirement is related to the sets of input/output actions, , , and they express constraints and the order of executing these actions. For example could express: always when enables an input action ∈ then it will inevitably enable the output actions ∈ . So satisies this requirement if in all the execution paths in where a transition labeled by belongs, it will be followed by a transition labeled with . Since our composition approach preserves at least one of these paths, when the compatibility and the preservation of Input/Output actions hold, then the requirements are preserved. Indeed, the composite = ∥ +1 preserves the input/output actions related to the requirements means that for each input/output actions related to and +1 , the transitions labeled with these actions are preserved, therefore at least one execution path, in ∥ +1 containing these transitions is preserved in . Indeed, we have the following possibilities when and +1 are compatible and the actions related to and +1 are preserved (illustration concerning only one action related to or +1 ):

+1 ∥ +1 ′ 1 ′ 1 ′ , ′ 1 , 1 a⁵ a? a; +1 ∥ +1 ′ 1 ′ 1 ′ , 1 , 1 , ′ 1 a⁵ b? a⁵ b? +1 ∥ +1 ′ 1 ′ 1 , 1 a⁵ b?
Figure . -Interface automata composition alternatives

• if there are no illegal states the preservation is guaranteed, because all the paths are preserved. This case (we have two possibilities) is illustrated in the Figure 8.5(a) and (b). In the case (a), we suppose that there is a synchronization between the two automata on the shared action (related to a requirement), so in the composition we obtain a transition labeled with the internal action . Therefore, the action is preserved and becomes internal. And in the second case (b), we suppose that is not shared and there is interleaving in the composite automaton, and is preserved.

• if there are illegal states (and the automata are compatible due the optimistic approach): in this case (see Figure 8.5(c)), we suppose that the irst automaton provides a shared output action , in the state , and the second automaton does not provide the input action , in 1. So we obtain an illegal state and the action is not enabled in the illegal state ( , 1). In this case we have to verify that is preserved in other paths of the composite automaton ∥ +1 , with our approach. So, if we ind a transition labeled with , in ∥ +1 , so it is preserved (according to the condition of preservation), and the associated requirement also, otherwise the related requirement is not preserved. So when the preservation of the Input/Output action is veriied, then the related requirements are preserved.

□ . / S fi S A

The construction of a CBS with our approach is based on constructing, at each incremental step, one SysML composite component, which deines a partial architecture of a CBS. This architecture is based on the interface automata of the assembled components and particularly on their shared actions. So, in the following deinition, we describe the SysML composite by specifying the relation between SysML BDD and IBD diagrams, and the interface automata describing the behaviors of the composed components.

Deinition 20: SysML Composite component

Let 1 and 2 be two components, let 1 and 2 be their respective interface automata. When 1 and 2 are compatible, 1 || 2 ≠ , the composite component composed of 1 and 2 , is well formed and it is written = 1 ∥ 2 . This composite is described with the SysML BDD diagram, , composed of the composite block , and the blocks 1 and 2 . The interactions between the components 1 and 2 are described with the SysML IBD diagram, such that, is composed of the parts 1 and 2 which communicate through internal ports, labeled with the names of the synchronized input and output actions, which are shared between 1 and 2 . The external ports of are labeled with the names of actions which are not shared. This deinition is illustrated in Section 8.6 in Figures 8.9 and 8.10 (BDD and IBD).

. / I C S

In this section we apply our approach on the case study shown in Section 8.2. As exposed in the approach, we start by analyzing the SysML requirement diagram to obtain the atomic requirements. These requirements are 1.1.1, 1.1.2, 1.1.3, and 1.2. Then, we link LTL properties for each of these atomic requirements. These properties are used to verify whether a block in a component library satisies the requirement in order to match them.

For the irst requirement 1.1.1 we take a sensor block with its associated SD shown in Fig- ure 7.2 respectively. This sensor block gets information from several sensors (accelerometers, impact sensors,...) all around the car at each call of the service get_sensor_values, and sends them through a service sensor_values. These services are respectively the input {get_sensor_values} and output actions {sensor_values} related to requirement 1.1.1. To validate if the block sensors satisies requirement 1.1.1, we irst describe the requirement as a LTL property like "always, after the sensors block receives a call for get_-sensor_values, it sends a message sensor_values to the environment". Then we translate the associated SD to a Promela description as exposed in Chapter 7, the generated code is not shown here for lack of space. Following the approach of lags from [LTM + 09], the LTL property in Promela language is:

□((sensors && receive && msg_get_sensor_values) → ♢(sensors && send && msg_sensor_values))
The next requirement to be analyzed is 1.1.2 which is connected to 1.1.1. For this requirement, we ind the ACU block and its associated SD in Figure 7.4, this block ofers an input action {sensor_values} and requires the output actions {act_sb,act_ab} to lock the seat-belts and deploy an airbag respectively, this block analyzes each arrival of sensor values and decides whether the seat-belts must be locked, an airbag must be deployed or wait for another sensor values arrival (reset action). To verify if this block satisies requirement 1.1.2, we express it as a Promela description (the generated code was shown in Listing 7.2 ) and the requirement is expressed as a LTL property: "always after receiving a message with the sensor_values, the ACU will send a message deciding to lock the seat-belt (act_sb), activate the airbag (act_ab) or wait for another call (reset)", which expressed in Promela code using lags will be: These properties are veriied using SPIN model-checker which outputs no errors for both models, therefore, the models satisfy the properties.

Then, to link the blocks that satisfy requirements 1.1.1 and 1.1.2, we verify that they are compatible thanks to their interface automata. These interface automata are generated from SD following the approach in [START_REF] Chouali | Formal veriication of components assembly based on SysML and interface automata[END_REF], and they are shown in Figures 8.6 and 8.7. To verify compatibility we compute the composition; we use Ptolemy Interface Automata tool [START_REF] Lee | A behavioral type system and its application in Ptolemy II[END_REF] which computes the composition of two given interface automata as input. The output composite automaton is shown in Figure 8.8, this automaton is not empty, so the blocks Sensors and ACU are compatible. This composition had illegal states that were eliminated automatically by Ptolemy tool, so we have to validate that the actions related to the requirements are still present on the transitions of the composite automaton to guarantee preservation of the requirements over the composition.

Looking at the transitions in the composite automaton, we ind that the set of input/output actions, related to the requirements, are still present, so the requirements are still preserved over the composition and we can proceed to deine a partial architecture of the system, by presenting a BDD with the reinement of an abstract block into the blocks Sensors and ACU, this diagram is presented in Figure 8.9.

The interactions between the composed blocks are then described by an IBD (see Figure 8.10) where the ports representing the synchronized input and output actions are linked with connectors and the unshared actions are exposed as ofered and demanded services of the composition. Subsequently, we continue adding requirements 1.1.3, with related input action {act_-ab}, and 1.2, with related input action {act_sb}, to our architecture in the same manner, until all atomic requirements are treated. III C Therefore, there are three challenges that a designer must confront:

1. The irst one is how to specify an architecture that satisies all system requirements? 2. The second one concerns the compatibility between the set of reusable components that compose the system, which must be guaranteed. Indeed, generally, one exploits reusable components from a component library to construct CBS, thus, we need to guarantee component compatibility.

3. And inally, we ask for how to integrate formal veriication in the assembly process to build reliable systems.

The philosophy of this thesis is inspired from the concept of CBS, to build, step by step, SysML speciications of a system, by exploiting the notion of SysML reinement. Structural diagrams of SysML describe the system in static mode, and behavioural diagrams describe the dynamic operation of the system. In SysML, blocks are modeled by two diagrams. The BDD, which deines the architecture of the blocks and their performed operations, and the IBD, which is used to deine the ports of each block and transactions exchanged between them through their ports. During the reinement process, these two diagrams can be checked to decide whether the proposed architecture satisies or it is inappropriate to the requirements diagram.

.

/ M C

In this thesis we presented three contributions based on an incremental approach.

1. The irst contribution aimed to formalize the decomposition process, by deining a reinement relation between an abstract block and its sub-blocks. It consisted on exploiting the architecture description in SysML language when a system is described by structural diagrams and behavioral diagrams. The reinement in SysML is an essential concept and it is based on the development of a process from an abstract level towards more detailed levels, which can end in its implementation. Our reinement ensured an incremental substitutability of an abstract block in a speciication by a composition of blocks preserving its structural and behavioral properties.

To verify structural reinement speciied in BDD and IBD diagrams, we veriied irst if the sub-blocks were consistent with the abstract block speciication and then we veriied if they were compatible by applying the model of interface automata of d'Alfaro et al. Interface automata were obtained from the SysML SD of each composing subblock and then veriied for compatibility by means of the Ptolemy tool .

To verify behavioral reinement, we applied the approach of alternating simulation for interface automata to verify if the composition of the set of sub-blocks simulated the expected behavior in the abstract block. To ease the task of verifying alternating simulation we proposed to use the module Observational Modal Reinement of the MIO Workbench tool. To use this tool, we translated interface automata into modal automata.

2. The second contribution focused on properties veriication in our system. We were inspired from works proposed by V. Lima et al. The technique proposes to generate Promela-based models from UML interactions expressed in Sequence Diagrams (SD), and uses conjointly the SPIN model checker in order to simulate and verify properties written in Linear Temporal Logic(LTL). Our minor adaptation of this approach concerned a particular type of sequence diagrams that we exploited to specify the block behaviors. We chose Promela to describe SD speciications and LTL properties to describe functional requirements. We then used SPIN tool to verify these properties. We chose this environment implementation because it is a popular tool in veriication activity and it is easy to specify and implement SD concepts like sending and receiving primitives, parallel and asynchronous composition.

3. The third contribution discussed an interesting approach to describe the relationship between system requirements and a CBS architecture speciication in SysML.

The goal was to propose a methodology to build incrementally a consistent system architecture that formally fulills all the system requirements. We used SD to describe component behavior and BDD and IBD to specify system architecture. In details, the proposed construction extracted the atomic requirements from a requirement diagram and treated them one by one in order to construct the inal system. We obtained then a partial architecture of the system, composed with elementary blocks (components) and composite blocks (components). At each step, we selected an atomic requirement from a SysML requirement diagram, and we chose a block from a library that should satisfy the selected requirement. Then we veriied whether the block satisied the requirement thanks to the LTL properties which speciied the requirement and the Promela speciication which described the component behavior from SD. We then veriied the compatibility between the selected block, and the selected ones in the precedent steps, and we veriied also the preservation of requirements treated in precedent steps. The process ended when all atomic requirements were treated, or when we detected incompatibility between components, or the non preservation of the requirements by the component composition.

In this way we guaranteed the architecture consistency of the inal system which therefore fulilled all the system requirements.

.

/ P W

The works of this thesis targeted the main question: how to introduce formal veriication on informal SyML speciications in the process of the development of CBS?

Our contributions addressed some solutions in order to build consistent CBS, thus we established relations between reinement, concepts of SysML blocks, and CBS characteristics. In the following, we present some perspectives and future works related to our contributions.

Toolchain for verification Develop and provide for the designer a toolchain to support the automatic veriication of the reinement relation between abstract blocks and sub-blocks, and also the veriication of SysML requirements on blocks to decide or not the validation of CBS SysML architecture. This toolchain will be composed of tools that allow (1) verifying conditions of consistency between blocks and exploit Ptolemy tool to verify compatibility (2) translating directly diagrams into Promela language (3) and verifying LTL properties with the model-checker Spin. Some signiicant examples can be experimented to evaluate the proposed approach.

Combining verification and simulation for non functional properties In reliable applications, it is important to specify a system architecture in accord with functional and non functional requirement speciications. To achieve this goal, we have proposed an approach to specify system architecture directly from SysML functional requirements. So, as a future work, it is interesting to address the validation problem with non functional requirements and use simulation techniques.

Adapting and Generating adapters for incompatible blocks The problem of adapting blocks is crucial in the development of CBS by reusing blocks. The adaptation consists to generate automatically, when it is possible, an adaptor block between incompatibles blocks in order to ensure a reliable interaction. The idea of a future work, is to generate an entity capable of ensuring the interaction between two incompatible blocks when the conditions of consistency and compatibility are failed, allowing thus achieving our approach of reinement of abstract blocks, and the generation of CBS architecture based on SysML requirements. SysML comprend donc 9 diagrammes et selon [START_REF] Omg | Systems Modeling Language (SysML) Version 1.3[END_REF] on peut les déinir comme suit:

IV

• Activités: décrit le comportement du système comme lux de contrôle et de données.

• Déinition de blocs (DDB): décrit la structure architecturale du système comme composants avec leur propriétés, opérations et relations.

• Bloc interne (DBI): décrit les structures internes des composants, en ajoutant leurs parties et connecteurs.

• Paquets: décrit comment un modèle est organisé en paquets, vues et points de vue.

• Paramétrique: décrit les contraintes paramétriques entre les éléments structurels.

• Exigences: décrit les exigences du système et leurs relations avec d'autres éléments.

• Séquences (DS): décrit le comportement du système comme interactions entre les composants du système.

• Machines d'état: décrit le comportement du système comme états qu'un composant a en réponse à des événements. , ces deux diagrammes spéciient l'architecture du système. Soit 1 , ..., l'ensemble de blocs composant selon son , alors 1 , ..., rainent par décomposition si:

Σ 2 = Σ 1 Σ 2 = Σ 1 Σ 2 = Σ 2 Σ 1 = . Shared( 1 , 2 ) = (Σ 1 Σ 2 ) (Σ 2 Σ 1 )
• 1 , ..., raine structurellement ,

• 1 , ..., raine comportementalement , Donc, pour vériier le rainement entre un bloc et ses sous-blocs, nous vériions les conditions de consistance et compatibilité pour le rainement structurel, et de simulation alternée pour le rainement comportemental (voir Figure 6.3). Pour réussir cette vériication, nous avons besoin de spéciier par diagramme de séquences la description du comportement du bloc abstrait et ses sous-blocs composants, et puis, en exploitant l'approche proposé dans [START_REF] Chouali | Formal veriication of components assembly based on SysML and interface automata[END_REF], nous associons un automate d'interface à chaque DS. Ces automates sont exploités pour vériier la compatibilité entre les sous-blocs en utilisant l'outil Ptolemy [START_REF] Lee | A behavioral type system and its application in Ptolemy II[END_REF], qui génère l'automate de la composition de deux automate d'interface en entrée. Ensuite nous vériions le rainement comportementale à travers l'outil MIO Workbench [START_REF] Bauer | On Weak Modal Compatibility, Reinement, and the MIO Workbench[END_REF], qui vériie si une spéciication de comportement est rainée par une implémentation en utilisant un automate Modal Input/Output (MIO) comme donnée d'entrée.

Une fois que nous avons vériié le rainement structurel et comportemental par deux ou plus blocs qui décompose un bloc abstrait de niveau supérieur, nous avons aussi vériié que ce bloc parent peut efectivement être substitué par ses entités composants.

Ce processus de vériication peut être appliqué incrémentalement depuis les blocs abstraits de plus haut niveau jusqu'aux blocs de plus bas niveau pour valider l'architecture inale du SBC obtenu à partir du bloc abstrait initial.

Fin Répéter

Selon les étapes principales de notre approche, nous validons l'architecture inale pour notre SBC, une fois que tous les exigences atomiques ont été analysées sans problèmes de compatibilité des composants et/ou préservation des exigences.

A

  BDD Block Deinition Diagram. CBD Component-Based Development. CBS Component-Based Systems. CSP Communicating Sequential Processes. EMF Eclipse Modeling Framework. IBD Internal Block Diagram. IDL Interface Description Language. INCOSE International Council on Systems Engineering. OMG Object Management Group. OOD Object-Oriented Design. RFP Request for Proposals. SD Sequence Diagram. SysML Systems Modeling Language. UML Uniied Modeling Language.

Figure

  Figure . -A safety vehicle system¹

Figure . -A blackbox component

  Figure . -A blackbox component

Contents 3 . 1

 31 Structural Diagrams . . . . . . . . . . . . . . . . . . . . . . . . . . 18 3.1.1 The Block Deinition Diagram . . . . . . . . . . . . . . . . . . . 18 3.1.2 The Internal Block Diagram . . . . . . . . . . . . . . . . . . . . 19 3.1.3 The Parametric Diagram . . . . . . . . . . . . . . . . . . . . . . 19 3.1.4 Package Diagram . . . . . . . . . . . . . . . . . . . . . . . . . . 20 3.2 Behavioral Diagrams . . . . . . . . . . . . . . . . . . . . . . . . . 20 3.2.1 The Activity Diagram . . . . . . . . . . . . . . . . . . . . . . . . 20 3.2.2 The Use Case Diagram . . . . . . . . . . . . . . . . . . . . . . . 20 3.2.3 The Sequence Diagram . . . . . . . . . . . . . . . . . . . . . . . 21 3.2.4 The State Machine Diagram . . . . . . . . . . . . . . . . . . . . 21 3.3 Cross-Cutting Diagrams . . . . . . . . . . . . . . . . . . . . . . . . 22 3.3.1 The Requirements Diagram . . . . . . . . . . . . . . . . . . . . 22 3.4 SysML Tools . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 3.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24

Figure . -A requirement diagram

  Figure . -A requirement diagram

Contents 4 . 1

 41 Deinition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 4.2 Automata Compatibility Veriication . . . . . . . . . . . . . . . . . 26 4.3 Compatibility Veriication Utilities . . . . . . . . . . . . . . . . . . 28 4.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Deinition 1: Interface Automata An interface automaton is represented by the tuple ⟨ S , I , Σ , Σ , Σ , ⟩ such that: • is a inite set of states;

  CHAPTER 4. INTERFACE AUTOMATA and are deined by the set

Contents 5 . 1

 51 Generation of CBS Architecture . . . . . . . . . . . . . . . . . . . 31 5.2 Compatibility Veriication . . . . . . . . . . . . . . . . . . . . . . 32 5.3 Component Behavior Description . . . . . . . . . . . . . . . . . . . 33 5.4 Requirements Speciication in SysML . . . . . . . . . . . . . . . . 34 5.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 CHAPTER 5. RELATED WORKS

Contents 6 . 1

 61 Approach Overview . . . . . . . . . . . . . . . . . . . . . . . . . . 41 6.2 CBS Architecture Speciication with SysML . . . . . . . . . . . . . 44 6.3 Formal Speciication of SysML models . . . . . . . . . . . . . . . . 46 6.4 Structural Reinement of SysML Blocks . . . . . . . . . . . . . . . 48 6.4.1 Consistency and Composability Veriication between Blocks . . . 48 6.4.2 Interface Automata Generation . . . . . . . . . . . . . . . . . . 50 6.4.3 Compatibility Veriication . . . . . . . . . . . . . . . . . . . . . 52 6.4.4 Veriication Algorithm for Structural Reinement . . . . . . . . . 53 6.5 Behavioral Reinement Veriication of SysML Blocks . . . . . . . . 56 6.5.1 Alternating Simulation . . . . . . . . . . . . . . . . . . . . . . 56 6.5.2 Modal I/O Automata . . . . . . . . . . . . . . . . . . . . . . . . 56 6.5.3 Case Study Application . . . . . . . . . . . . . . . . . . . . . . . 58 6.6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 CHAPTER 6. INCREMENTAL REFINEMENT OF A CBS ARCHITECTURE Deinition 5: Reinement by decomposition of SysML blocks

Figure . -

 . Figure . -Structural and behavioral refinement verification in a SysML Block Decomposition

Figure . -Figure . -

 .. Figure . -Product 1 ⊗ 2 between the automata Sensors and ACU

Deinition 12 ::

 12 Alternating SimulationFor a pair of interface automata = ⟨ , , Σ , Σ , Σ , ⟩ and = ⟨ , , Σ , Σ , Σ , ⟩ with the same signature, a binary relation ≤ ⊆ is an alternating simulation if whenever ≤ and ∈ Σ it holds that: if ? ⟶ ′ and ∈ Σ then ′ . ? ⟶ ′ and ( ′ , ′ ) ∈≤ if ! ⟶ ′ and ∈ Σ then ′ . ⟶ * ′ . ″ . ′ ! ⟶ * ″ and ( ′ , ″ ) ∈≤ if ; ⟶ ′ and ∈ Σ then ′ . ⟶ * ′ and ( ′ , ′ ) ∈≤ Deinition 13: Interface Automata Reinement An interface automaton reines an interface automaton , writen ≤ , if 1. Σ ⊆ Σ and Σ ⊇ Σ 2. there is an alternating simulation ≤ by of such that ≤ Actually, we can not verify behavioral reinement through Ptolemy tool but we can do that thanks to the MIO Workbench [BMSH10], an Eclipse-based editor and veriication tool for modal I/O automata. . . / M I/O A Modal automata are an extension of interface automata with modality and control information proposed by Larsen et al. [LNW07]. Deinition 14: Modal automaton A modal automaton S is a six tuple: = ( , , Σ , Σ , ⟶ ♢ , ⟶ □ ) where : is a inite set of states, ∈ : is the initial state, Σ and Σ : are disjoint sets of external and internal actions, is the may transition relation describing allowed behavior, ⟶ □ ⊆ Σ : is the must transition relation describing required behavior.

Figure . -

 . Figure . -Refinement in MIO Workbench

  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 7.2.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 7.3 Veriication with SPIN Model Checker . . . . . . . . . . . . . . . . 65 7.4 Requirement speciication with LTL . . . . . . . . . . . . . . . . . 66 7.5 Case Study Promela descriptions . . . . . . . . . . . . . . . . . . . 69 7.6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71

  Figure 7.2 will be send and receive to indicate the performed action, msg_get_sensor_values and msg_sensor_values to indicate the message exchanged, and sensors and environment to indicate who performed the action.

Contents 8 . 1

 81 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75 8.2 Case Study . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76 8.3 SysML Requirement Diagram Analysis . . . . . . . . . . . . . . . . 77 8.4 Component Assembly Preserving SysML Requirements . . . . . . 79 8.4.1 Functional Requirements and Input/Output Actions . . . . . . . 80 8.4.2 Preservation of Input/Output Actions in Automata Composition . 80 8.4.3 Veriication of Atomic Requirements Preservation . . . . . . . . 81 8.5 Speciication of System Architecture . . . . . . . . . . . . . . . . . 83 8.6 Illustration on the Case Study . . . . . . . . . . . . . . . . . . . . . 84 8.7 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86

Figure . -

 . Figure . -Proposed approach to generate CBS architecture from SysML requirements

  (b) Identify the set of input and output actions in +1 related to +1 . (c) Verify that and +1 are compatible thanks to their interface automata, so verify that ∥ +1 ≠ (see Section 4.2). (d) Verify that the requirements and +1 are preserved by the composition, so they are satisied by the composite = ∥ +1 (see Section 8.4). (e) Deine the consistent partial architecture of the system by the composite = ∥ +1 , according to Deinition 20. (f) Let = ∥ +1 , = ∥ +1 , and = { , +1 }.

Figure . -

 . Figure . -SysML requirements diagram for a safety car system

  Figure . -A SysML requirement diagram

  1.1: always get the sensor values and send them to the ACU. It is satisied by the component Sensor. The interface automaton of this component is described in Figure 8.6. The set of input actions related to 1.1.1 is { _ _ }, and the set of output actions is { _ }.

Figure . -

 . Figure . -IA for the Sensors block

  dans cette thèse est une contribution à la spéciication et à la vériication des Systèmes à Base de Composants (SBC) modélisé avec le langage SysML. Les SBC sont largement utilisés dans le domaine industriel et ils sont construits en assemblant diférents composants réutilisables, permettant ainsi le développement de systèmes complexes en réduisant leur coet de développement. Malgré le succès de l'utilisation des SBC, leur conception est une étape de plus en plus complexe qui nécessite la mise en oeuvre d'approches plus rigoureuses.Pour faciliter la communication entre les diférentes parties impliquées dans le développement d'un SBC, un des langages largement utilisé est SysML, qui permet de modéliser, en plus de la structure et le comportement du système, aussi ses exigences. Il ofre un standard de modélisation, spéciication et documentation de systèmes, dans lequel il est possible de développer un système, partant d'un niveau abstrait, vers des niveaux plus détaillés pouvant aboutir à une implémentation. Généralement ces systèmes sont faits plus grands parce qu'ils sont développés avec des cadres logiciels. Dans ce contexte nous avons traité principalement deux problématiques : La première est liée au développement par rainement d'un SBC modélisé uniquement Contents 10.1 Contexte Scientiique . . . . . . . . . . . . . . . . . . . . . . . . . 96 10.1.1 Systèmes à Base de Composants . . . . . . . . . . . . . . . . . . 96 10.1.2 Le Langage SysML . . . . . . . . . . . . . . . . . . . . . . . . . 97 10.1.3 Les Automates d'Interface . . . . . . . . . . . . . . . . . . . . . 98 10.2 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100 10.2.1 Rainement Incrémental d'une Architecture SBC . . . . . . . . . 101 10.2.2 Vériication Formelle d'Exigences SysML . . . . . . . . . . . . . 103 10.2.3 Spéciication Incrémentale d'une Architecture SBC . . . . . . . . 104 10.3 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107 10.4 Perspectives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108 par ses interfaces SysML. Notre contribution permet au concepteur des SBC de garantir formellement qu'une composition d'un ensemble de composants élémentaires et réutilisables raine une spéciication abstraite d'un SBC. Dans cette contribution, nous exploitons les outils: Ptolemy pour la vériication de la compatibilité des composants assemblés, et l'outil MIO Workbench pour la vériication du rainement La deuxième problématique traitée concerne la diiculté de déterminer quoi construire et comment le construire, en considérant seulement les exigences du système et des composants réutilisables, donc la question qui en découle

  (b) Identiier l'ensemble des actions d'entrée et sortie en +1 liées à +1 . (c) Vériier que et +1 sont compatibles grâce à leurs automates d'interface, en vériiant que ∥ +1 ≠ (voir Section 4.2). (d) Vériier que les exigences et +1 sont préservées par la composition, c'està-dire qu'elle sont satisfaites par le composant composite = ∥ +1 (voir Section 8.4). (e) Déinir l'architecture consistante partielle du système pour le composant composite = ∥ +1 , en accord avec la Déinition 20. (f) Soit = ∥ +1 , = ∥ +1 , et = { , +1 }.

Figure . -

 . Figure . -Approche proposé pour la génération d'une architecture SBC à partir d'exigences SysML

  Oscar Carrillo, Samir Chouali, and Hassan Mountassir. Modélisation Incrémentale d'une Architecture de Système Satisfaisant des Exigences Fonctionnelles SysML. In Conférence en Architectures Logicielles (CAL 2014), Paris, France, 2014 • Oscar Carrillo, Samir Chouali, and Hassan Mountassir. Veriication of a SysML Block Decomposition in a Reinement Process. In Under consideration for publication in Software & Systems Modeling (SOSYM). Springer Berlin Heidelberg, 2015

	Architectures Logicielles
	(CAL 2012), Montpellier, France, 2012
	• Samir Chouali, Oscar Carrillo, and Hassan Mountassir. Specifying System Architec-
	ture from SysML Requirements and Component Interfaces. In Software Architecture
	(ECSA 2013), pages 348-352, Montpellier, France, 2013
	• Oscar Carrillo, Samir Chouali, and Hassan Mountassir. Incremental Modeling of Sys-
	tem Architecture Satisfying SysML Functional Requirements. In José Luiz Fiadeiro,

• Oscar Carrillo, Samir Chouali, and Hassan Mountassir. Formalizing and verifying compatibility and consistency of SysML blocks. In ACM SIGSOFT Software Engineering Notes (UML-FM 2012), volume 37, pages 1-8, Paris, France, 2012. ACM • Oscar Carrillo, Samir Chouali, and Hassan Mountassir. Vériication de la consistence et de la compatibilité entre blocs SysML. In Conférence en Zhiming Liu, and Jinyun Xue, editors, Formal Aspects of Component Software (FACS 2013), Lecture Notes in Computer Science, pages 79-99. Springer International Publishing, Nanchang, China, 2014 •

  and the International Council on Systems Engineering (INCOSE) made in March 2003 a Request for Proposals (RFP) [OMG03] for using the Uniied Modeling Language (UML) in Systems Engineering. Then, in May 2006, they proposed a SysML standard and released the version 1.0 in September 2007. Since then, they have been integrating suggestions from the systems engineering community and nowadays we are in version 1.3 presented in April 2012.

  Matoussi et al. [Mat11, BMC+ 12, LSM + 10] propose a methodology that allows generating a reinement architecture in EventB from SysML requirements speciications. They are based in the KAOS approach[vL03] and extend the SysML requirement diagram in the stereotype SysML/KAOS for functional goals. Once the goals diagram is described, they reine the requirements into atomic goals from which they generate Event-B functions that can be later veriied. requirements aims to facilitate the traceability of requirements validation.Similarly, Linhares et al.[START_REF] Linhares | Introducing the modeling and veriication process in SysML[END_REF] propose to formalize SysML requirements with LTL properties that they verify over Petri nets representing system behavior, for this end, they use the TINA toolbox[START_REF] Bernard | The tool TINA -Construction of abstract state spaces for Petri nets and Time Petri nets[END_REF].In this chapter, we presented some related works of the proposals in this thesis, we cited notably the works of [CLR + 09] who propose the design method rCOS, to develop a CBS architecture following a UML-Based development from requirements, other authors like Matoussi et al.[START_REF] Matoussi | Construction de spéciications formelles abstraites dirigée par les buts[END_REF] and Petin et al.[START_REF] Petin | Méthodes et modèles pour un processus sûr d'automatisation[END_REF] base their work in SysML requirements like we do in this thesis, the former using Event-B to verify requirements and the latter using UPPAL model-checker.

				6
	. / C C	I	R fi D fi CBS A	A
			II
		C

In the ield of requirements validation, Petin et al.

[START_REF] Petin | Méthodes et modèles pour un processus sûr d'automatisation[END_REF][START_REF] Pétin | Combining SysML and formal methods for safety requirements veriication[END_REF]

propose to model requirements through SysML diagrams which they extend in a prototype that allows to link formal properties to the requirements. The requirements can be then linked to the blocks in a BDD to indicate that that block satisies that requirement, to verify the requirement, the linked property is veriied with UPPAL model-checker. This model of linking blocks, properties and

Deinition 7: Block interfaces

	Let	and	be respectively the output and input ports of a SysML Block
	. The required and provided interfaces of are deined by the blocks which type respectively and . The required interface of , noted = ⟨Φ , , ⟩, where Φ deines the set of required services of , i.e. the output actions, and , are both empty (the interfaces have no ports). And the provided interface of , noted = ⟨Φ , , ⟩ Deinition 8: SysML IBD
	A SysML internal block diagram ⟨Φ , , , , ,	, of a composite block, is a tuple ⟩, where:
	• Φ

where Φ deine the set of provided services of , i.e. the input actions, and , are both empty.

For example, the required interface of the block SensorsControl in Figure

6

.5 is deined by IoutSensorsControl where = { _ (), _ (), _ (), _ ()}.

Deinition 11: Sequence diagram formal model A

  sequence diagram representing the protocol of a block is deined by :

			00 ′			04 ′
			03 ′			02 ′	01 ′
			13 ′			12 ′	11 ′
		= ⟨, , ,	,	⟩, where
	• : the initial message,
	• : the set of messages,
	•	= ⟨ ments, = ⟨ 1 , ..., 1 , ..., ( ) >= 1	, ..., , ...,	⟩,	⟩, is the list of the loop combined frag-is a message or a fragment, and
	•	= ⟨ 1 , ..., = ⟨ 1 , ..., , ..., ( ) >= 2	⟩, is the list of alternative combined fragments, , ..., ⟩, is a message or a fragment, and
	•	= ⟨ 1 , ..., = ⟨ 1 , ..., ( ) >= 2	, ..., , ...,	⟩, is the list of sequence combined fragments, ⟩, is a message or a fragment, and
	The formal model corresponding to the sequence diagram specifying the protocol of the block sensors (see Figure 6.8) is = ⟨, , , , ⟩, where:
	• : the message designed by the action
	⟨		,	(),		⟩;
	• : {⟨ ⟨	,	,	(),	(),	⟩, ⟩};
	•	= ⟨	⟩,

  and 1 ⟶ ♢ 2 if ( 1 , , 2 ) ∈ and ∈ Σ Σ and 3 ⟶ □ 4 and 3 ⟶ ♢ 4 if ( 3 , , 4 ) ∈ and ∈ Σ

	and 3 ⟶ ♢	if ∀ ′ ∈	.( 3 , , ′ ) ∉ and ∈

and is a fresh state such that ∀ ∈ Σ .

⟶ ♢

Table . -

 . Mapping of basic concepts from sequence diagrams to Promela

	SD element Lifeline Message Connector Send and receive events	Promela Element Process Message Communication channel for each message arrow Send and receive operations	Promela Statement proctype{...} mtype{m1,...,mn} chan chanName = [1] of {mtype} Send ⇒ ab!m, Receive ⇒ ab?m
	Alt fragment combined Loop combined fragment	if condition do operator	if ::(guard)->ab_p?p; :: else -> ab_q?q; fi; do ::ab_p?p; od

  . -"Promela Description for Sensors Block"

	/*Messages declaration*/ mtype={get_sensor_values ,sensor_values}; /*Channels declaration*/ chan sensors_environment_get_sensor_values=[1] of {mtype}; chan sensors_environment_sensor_values=[1] of {mtype}; /***FLAGS***/ /*Last performed action*/ bit send=0; bit receive=0; /*Message used in the last action*/ bit msg_get_sensor_values=0; bit msg_sensor_values=0; /*Lifeline that performed last action*/ bit sensors=0; bit environment=0; ltl p0 {[]((sensors && receive && msg_get_sensor_values) -> <>(sensors && send && msg_sensor_values))}; /*Lifelines specification */ proctype proc_sensors(){ do ::atomic{sensors_environment_get_sensor_values?get_sensor_values; d_step{send=0; receive=1; msg_get_sensor_values=1; msg_sensor_values=0; sensors=1; environment=0;};}; atomic{sensors_environment_sensor_values!sensor_values; d_step{send=1; receive=0; msg_get_sensor_values=0; msg_sensor_values=1; sensors=1; environment=0;};}; od} proctype proc_environment(){ do ::atomic{sensors_environment_get_sensor_values!get_sensor_values; d_step{send=1; receive=0; msg_get_sensor_values=1; msg_sensor_values=0; sensors=0; environment=1;};}; atomic{sensors_environment_sensor_values?sensor_values; d_step{send=0; receive=1; msg_get_sensor_values=0; msg_sensor_values=1; sensors=0; environment=1;};}; od} /*System Instantiation*/ init{ atomic{run proc_sensors();run proc_environment();} } /*Variable global*/ byte val_acc=0; /***FLAGS***/ /*Last performed action*/ bit send=0; bit receive=0; /*Message used in the last action*/ bit msg_sensor_values=0; bit msg_act_sb=0; bit msg_act_ab=0; bit msg_reset=0; /*Lifeline that performed last action*/ bit acu=0; bit environment=0; ltl p0 {[]((acu && receive && msg_sensor_values) -> d_step{send=0; receive=1; msg_sensor_values=0; msg_act_sb=1; msg_act_ab=0; msg_reset=0; acu=0; environment=1;};}; ::(val_acc >=60)->{ atomic{acu_environment_act_sb?act_sb; d_step{send=0; receive=1; msg_sensor_values=0; msg_act_sb=1; msg_act_ab=0; msg_reset=0; acu=0; environment=1;};}; atomic{acu_environment_act_ab?act_ab; d_step{send=0; receive=1; msg_sensor_values=0; msg_act_sb=0; msg_act_ab=1; msg_reset=0; acu=0; environment=1;};}; } fi; od} <>(acu && send && (msg_reset || msg_act_sb || msg_act_ab)))} /*Lifelines specification */ proctype proc_acu(){ do ::atomic{acu_environment_sensor_values?sensor_values; d_step{send=0; receive=1; msg_sensor_values=1; msg_act_sb=0; msg_act_ab=0; msg_reset=0; acu=1; environment=0;};}; if od} fi; acu=1; environment=0;};};} msg_act_ab=0; msg_reset=1; msg_sensor_values=0; msg_act_sb=0; d_step{send=0; receive=1; atomic{acu_reset?reset; acu=1; environment=0;};}; msg_act_ab=0; msg_reset=1; msg_sensor_values=0; msg_act_sb=0; d_step{send=1; receive=0; atomic{acu_reset!reset; ::else{ acu=1; environment=0;};}; msg_act_ab=0; msg_reset=0; msg_sensor_values=0; msg_act_sb=1; d_step{send=1; receive=0; atomic{acu_environment_act_sb!act_sb; ::((val_acc <60) && (val_acc >=3))-> } acu=1; environment=0;};}; msg_act_ab=1; msg_reset=0; msg_sensor_values=0; msg_act_sb=0; d_step{send=1; receive=0; atomic{acu_environment_act_ab!act_ab; acu=1; environment=0;};}; msg_act_ab=0; msg_reset=0; msg_sensor_values=0; msg_act_sb=1; d_step{send=1; receive=0; atomic{acu_environment_act_sb!act_sb; ::(val_acc >=60)->{ /*System Instantiation*/ init{ if ::(true) ->val_acc=0; ::(true) ->val_acc=10; ::(true) ->val_acc=60; fi; atomic{run proc_acu();run proc_environment();} }
	Listing . -"Promela Description for ACU Block" mtype={sensor_values ,act_sb ,reset,act_ab}; /*Messages declaration*/ /*Channels declaration*/ chan acu_environment_sensor_values=[1] of {mtype}; chan acu_environment_act_sb=[1] of {mtype}; chan acu_environment_act_ab=[1] of {mtype}; chan acu_reset=[1] of {mtype}; proctype proc_environment(){ do ::atomic{acu_environment_sensor_values!sensor_values; d_step{send=1; receive=0; msg_sensor_values=1; msg_act_sb=0; msg_act_ab=0; msg_reset=0; acu=0; environment=1;};}; if ::((val_acc <60) && (val_acc >=3))-> atomic{acu_environment_act_sb?act_sb;

  est la suivante: comment spéciier une architecture SBC qui satisfait toutes les exigences du système? Nous proposons une approche de vériication formelle incrémentale basée sur des modèles SysML et des automates d'interface pour guider, par les exigences, le concepteur SBC ain de déinir une architecture de système cohérente, qui satisfait toutes les exigences SysML proposées. Dans cette approche nous exploitons le model-checker SPIN et la LTL pour spéciier et vériier les exigences. Dans ce chapitre nous présentons un résumé de ces contributions structuré ainsi : d'abord nous présentons un contexte scientiique qui liste les concepts sur lesquels nous nous sommes basés (SBC, SysML, Automates d'Interface), ensuite nous présentons nos contributions et enin nous listons nos conclusions et perspectives de ces travaux. Au ils des années, le domaine du développement logiciel a evolué à travers de diférents paradigmes. La programmation structurée a changé dans le temps vers le paradigme des classes et puis vers la révolution de la programmation orientée objets. Les objets des nos jours ont grandit et ils sont identiiés comme des composants logiciels. Dans cette section, nous allons déinir et décrire les propriétés de ces derniers pour mieux comprendre les diferences entre objets et composants. Ce contrat liste une série de contraintes sur la manière d'exécuter le composant pour que celui-là exécute ses fonctionnalités [Szy02]. Il est aussi requis de déinir ce que l'environnement de composition et déploiement doit fournir pour faire interagir les composants proprement.Cet environnement est composé d'un modèle à composants avec des règles de composition et un cadre qui établi déploiement, installation et activation des règles des composants. Ainsi, les systèmes logiciels conçus pour être un assemblage de composants avec une architecture prédéinit sont appelés Systèmes à Base de Composants (SBC). Les composants peuvent être rainés et améliorés par des versions ultérieurs. Une entreprise qui vend des composants tiers peut proposer diférentes versions améliorées du même composant. Une gestion traditionnelle des versions supposerait que la version d'un composant évolue d'une seule source. Cependant, dans le marché ouvert, l'évolution des versions est plus complexe et la gestion des versions peut devenir un problème en soi, surtout parce que les versions peuvent aussi changer au niveau de son interface.

	. . / L L	S ML
	. / C	S	fi
	Dans cette section nous présentons les concepts de base utilisés dans cette thèse. D'abord,
	nous introduisons les SBC, puis SysML qui est le langage choisi pour modéliser les SBC et
	enin les automates d'interface que nous utilisons pour la vériication de la consistance et
	compatibilité des blocs.
	. . / S è	à B	C
	Plusieurs déinitions ont été proposés pour déinir les composants logiciels et une des plus
	complètes a été proposé dans [SP97]. Cette déinition est :
	"Un composant logiciel est une unité de composition avec des interfaces spéciiés contractuelle-
	ment et seulement dépendances de contexte explicites. Un composant logiciel peut être déployé
	indépendamment et est sujet à la composition par un tiers".
	À partir de cette déinition, un composant logiciel est une unité de composition avec
	d'autres paires, un composant doit encapsuler son implémentation et interagir avec son

environnement en tenant compte de seulement ses interfaces bien déinis. Ces interfaces doivent donner l'information sur les exigences du composant de la part d'autres composants et les services qu'il peut ofrir. Cependant, pour utiliser un composant correctement, il est nécessaire de satisfaire un contrat. SysML (Systems Modeling Language) [OMG12] est un langage de modélisation dédié aux applications d'ingénierie système. Il a été conçu comme réponse à l'appel de propositions (RFP) fait en mars 2003 par l'Object Management Group (OMG) [OMG15] pour l'utilisation d'UML en Ingénierie Système [OMG03], il a été proposé par l'OMG et l'International Council on Systems Engineering (INCOSE) et il a été adopté en tant que standard en Mai 2006.

SysML est un proil d'UML 2.0 [OMG05] qui réutilise un sous-ensemble de ses diagrammes et ajoute de nouvelles fonctionnalités pour mieux s'adapter aux besoins de l'ingénierie système de sorte qu'il permet la spéciication,l'analyse, la conception, la vériication et la validation d'un large éventail de systèmes complexes. Ces systèmes peuvent inclure le logiciel, le matériel, les données, les processus, les personnes et les installations.

  Les automates d'interface ont été introduits par Alfaro et Henzinger[START_REF] De Alfaro | Interface automata[END_REF] pour modéliser les interfaces dans une approche à composants. Ces automates sont issus des automates Input/Output oc il n'est pas nécessaire d'avoir des actions d'entrée activables dans tous les états. Chaque composant est décrit par un seul automate d'interface. L'ensemble des actions est décomposé en trois ensembles : les actions d'entrée, les actions de sortie, et les actions internes. Les actions d'entrée permettent la modélisation des méthodes qui vont être appelées dans un composant, dans ce cas elles représentent les services oferts pour un composant. Elles peuvent aussi modéliser une réception de messages dans un canal de communication. Ces actions sont étiquetées par le caractère "?". Les actions de sortie modélisent les appels des méthodes d'un autre composant. Donc, elles représentent les services requis par un composant. Elles peuvent aussi modéliser la transmission de messages dans un canal de communication. Ces actions sont étiquetées par le caractère "⁵". Les actions internes sont des opérations activables localement et elles sont étiquetées par le caractère ";".Les actions d'entrée et de sortie d'un automate d'interfaceA sont notées actions externes (Σ = Σ Σ ). L'ensemble des actions internes Σ peut contenir l'action, epsilon , qui symbolise un événement non opérationnel. Nous déinissons par Σ (s), Σ (s), Σ (s), respectivement les ensembles des actions d'entrée, de sortie et internes activables à l'état s. et 2 , on vériie s'il existe un environnement pour lequel il est possible d'assembler correctement 1 et 2 . Cela se traduit par la composition de leurs automates d'interface et la vériication si cette dernière n'est pas vide. Deux automates d'interface 1 et 2 sont composables si Σ

	. . / L A	'I
	que :
	•	est ensemble ini d'états;
	• ⊆	est un sous ensemble des états initiaux;
	La vériication de l'assemblage de deux composants (blocs) s'obtient en vériiant la com-
	patibilité de leurs automates d'interface. Pour vériier l'assemblage de deux composants
			1

• Cas d'utilisation: décrit les fonctions du système et leurs acteurs en train de les utiliser. Deinition 21: Automate d'Interface Un automate d'interface A est représenté par le tuple ⟨ S , I , Σ , Σ , Σ , ⟩ tels • Σ , Σ et Σ , représentent, respectivement, les ensembles des actions d'entrée, de sortie et internes. L'ensemble des actions de A est noté par Σ ; • ⊆ Σ est l'ensemble des transitions entre les états.

Σ (s) représente l'ensemble des actions activables de l'état s.

1

  est l'ensemble des actions partagées entre 1 et 2 .En deuxième lieu, en nous basant sur des diagrammes d'exigences et interfaces des composants spéciiés par SD, nous proposons une approche formelle et méthodologique pour spéciier incrémentalement l'architecture de système qui préserve tous les exigences du système (voir Contribution 3 à la Figure10.1). De cette manière, nous proposons de traiter, une à une, les exigences atomiques, extraites du diagramme d'exigences (fourni par le concepteur), pour construire une architecture partielle du système, composée de composants atomiques et composites. À chaque étape, nous proposons de sélectionner une exigence atomique du diagramme d'exigences SysML, et choisir un composant d'une bibliothèque de composants qui devrait satisfaire l'exigence choisie. Après nous vériions si le composant satisfait l'exigence en vériiant le programme Promela qui spéciie le DS du composant (voir Contribution 2 à la Figure10.1). Puis, nous vériions la compatibilité entre les composants choisis dans les étapes précédentes et le nouveau composant et nous vériions aussi la préservation des exigences traitées aux étapes précédentes. Ce processus init quand tous les exigences atomiques ont été traitées, ou si les exigences ne sont pas préservées par la composition des composants. Quand le processus init correctement, nous garantissons la consistance de l'architecture du CBS inal qui satisfait tous les exigences du système.Notre approche s'oriente à proposer une méthode formelle pour construire un bloc composite SysML à partir d'un ensemble des blocs élémentaires réutilisables. Ainsi, à partir d'un bloc composite abstrait, tel que son structure est modélisé par DDB et DBI, et son comportement par DS, nous proposons une approche qui décide si une composition d'un ensemble de blocs élémentaires réutilisables satisfont les exigences structurelles et comportementales, par rapport au bloc composite. Ainsi, nous proposons de vériier la décomposition correcte du bloc composite en un ensemble de composants élémentaires sélectionnés. Nous accomplissons cette décomposition en déinissant une relation de rafinement par décomposition entre le bloc abstrait et ses sous-blocs. À diférents niveaux, en commençant à partir du premier bloc abstrait jusqu'à obtenir les blocs élémentaires. Notre relation de rainement dépende de la vériication de deux relations entre le bloc composite et ses sous-blocs :• relation de rainement structurel : selon l'illustration de la Figure6.2, cette relation se maintient entre le bloc composite et les sous-blocs 1 et 2 si 1 et 2 sont compatibles et les service requis et demandés de 1 et 2 sont consistants avec ceux de .

	Dans ce context, cette thèse propose de nouvelles contributions :
	• L'exploitation du diagramme d'exigences SysML pour spéciier des exigences de CBS
	[CCM13, CCM14a].
	• La vériication de la compatibilité des composants en exploitant le formalisme des
	automates d'interface [dAH01], obtenus à partir des DS des composants, grâce à
	l'approche proposée dans [CH11]. Dans ce travail nous avons adapté l'algorithme de
	vériication de la compatibilité pour gérer des exigences SysML et pour vériier aussi
	sa préservation dans la composition [CCM12a, CCM12b, CCM15].
	• La vériication du rainement du comportement en appliquant la simulation al-
	ternée dans les automates d'interface [CCM15].
	• La proposition d'une approche incrémentale pour construire des SBC et pour véri-
	ier leurs exigences pour éviter le problème de l'explosion combinatoire du nombre
	d'états des composants vériiés. En fait, la vériication des exigences est réalisée sur
	des composants élémentaires que généralement son petits, de tel sorte que nous
	évitons la vériication sur des composants composites grâce à la préservation des
	exigences dans la composition. Cette contribution permet d'obtenir l'architecture
	SBC qui satisfait tous les exigences. En efet, cette architecture est construite incré-
	mentalement et aussi validée incrémentalement par rapport aux exigences SysML
	à chaque étape [CCM13, CCM14a].
	. . / R ffi	I	é	'	A	SBC

• La spéciication d'exigences SysML avec des formules en Logique Temporelle Linéaire (LTL) pour les vériier sur les composants

[START_REF] Carrillo | Incremental Modeling of System Architecture Satisfying SysML Functional Requirements[END_REF]

, grâce à leur DS qui est traduit vers Promela en adoptant l'approche proposée dans [LTM + 09].

L'approche présenté dans cette section cherche proposer une méthode pour formaliser et vériier la décomposition d'un bloc SysML dans un processus de rainement. Nous avons présenté la procédure générale à la Figure

6

.2.

• relation de rainement comportemental : cette relation se maintient si le comportement de la composition de 1 et 2 est un rainement du comportement de .

Deinition 25: Rainement par une décomposition de blocs SysML

Soit un bloc abstrait décrit par un et un

Table . -

 . Règles de correspondance des concepts basiques entre DS et PromelaPour vériier si un composant satisfait une exigence donnée, nous proposons d'utiliser l'ensemble Promela/SPIN. Nous les choisissons car ils fournissent d'importants concepts pour implémenter des DS : primitives d'envoi et réception des messages, composition parallèle et asynchrone de processus concurrents, et chaînes de communication. Notre adaptation de cette approche proposé par V. Lima et al. [LTM + 09] concerne un type particulier de diagramme de séquence que nous exploitons pour spéciier le comportement de blocs.Nous proposons d'utiliser un type particulier de DS avec seulement deux lignes de vie, une pour le bloc et une pour son environnement Ainsi, un DS peut par la suite être traduit en automate d'interface comme montré dans[START_REF] Chouali | Formal veriication of components assembly based on SysML and interface automata[END_REF]. Dans ce diagramme de séquence les messages échangés seront les services oferts comme appels de l'environnement et les services requis comme appels à l'environnement La principale avantage d'utiliser les DS pour la vériication est que l'on peut vériier des propriétés temporelles sur eux. Les messages suivent un ordre séquentiel que nous pouvons tracer pour détecter blocages ou exécution de chemins. Les Figures 7.2 et 7.4 montrent les interfaces, à travers des DS, pour deux blocs : sensors et ACU. Ils sont des blocs pris d'une à partir d'une bibliothèque de blocs. Dans ces diagrammes nous voyons qu'il y a seulement deux lignes de vie et que des messages sont envoyés par/reçus de l'environnement. Ensuite, dans les Figures 7.3 et 7.5 nous montrons partiellement la représentation Promela pour ces deux blocs respectivement (le code complet est présenté dans les Listings 7.1 et 7.2). Ce code est obtenu en appliquant les règles de transformation listées dans la Table 10.1.Dans les deux diagrammes nous pouvons voir qu'il y a deux lignes de vie traduites en tant que processus dans le code Promela, un processus pour le bloc et un autre pour son environnement. Les deux processus commence au même moment grâce à un appel atomique dans le processus main : init. Nous pouvons aussi voir que les fragments combinés de boucle loop sont traduits en tant que déclarations do, et le fragment combiné d'alternative alt est traduit comme une déclaration if. Pour pouvoir parcourir tous les chemins d'exécution, il est nécessaire de déinir les valeurs possibles pour les variables afectées, comme c'est le cas des valeurs deceleration qui est assignée au moment init dedans une déclaration if, de cette manière SPIN va choisir de façon non-déterministe quelle valeur sera utilisée pour simuler le système.Une fois que le DS est traduit, le composant peut être simulé comme un système SPIN. Pour pouvoir vériier si le composant satisfait une propriété LTL, V. Lima propose d'utiliser une série de drapeaux pour garder une trace de qui est en train d'envoyer/recevoir quel message à/de qui à tout moment de l'exécution. Néanmoins, dans notre approche nous vériions des propriétés sur des composants indépendants avec seulement deux lignes de vie dans son DS, une ligne pour le composant sélectionné et l'autre pour son environnement. Donc, nous n'utilisons pas le drapeau lié à à/de qui un message est envoyé car il sera toujours l'autre ligne de vie. Ces drapeaux sont mis à jour au même temps à chaque événement envoi/réception en utilisant une déclaration d_step.Après la déinition des drapeaux pour garder la trace de l'exécution du système, des propriétés LTL peuvent être écrites comme expressions booléennes sur les drapeaux. Dans notre approche, nous proposons de traduire des exigences SysML à propriétés LTL en respectant le formalisme des drapeaux (pour plus des détailles, voir Chapitre 7). Ces propriétés sont par la suite vériiées sur leur modèle Promela correspondant en utilisant le model-checker SPIN, qui indiquera si les blocs satisfont les propriétés. Une fois qu'un bloc correspondant est trouvé pour une exigence, nous continuons avec l'exigence suivante pour commencer à construire l'architecture du système.Nous proposons une approche pour construire un SBC et spéciier son architecture directement à partir de ses exigences SysML. Notre objectif est d'obtenir une architecture consistante en respectant toutes les exigences spéciiées. Pour spéciier cette architecture, l'architecte logiciel exploite une bibliothèque de composants réutilisables (ou blocs). Ces composants sont considérés comme boîtes noires et ils sont décrits seulement par ses interfaces, spéciiés par DS. Ainsi, nous proposons de spéciier des exigences de SBC avec un diagramme d'exigences SysML, puis analyser ce diagramme pour associer une à une ses exigences atomiques (celles qui ne peuvent pas être décomposées) à des composants logiciels qui les satisfont. La satisiabilité est évalué en efectuant une étape de vériication formelle avec un model-checker. Chaque composant vériié est évalué pour compatibilité par rapport aux autres composants dans la composition et par la suite ajouté à l'architecture partielle qui doit préserver les exigences atomiques.Dans notre approche, un SBC est spéciié avec un diagramme d'exigences SysML qui présente les exigences fonctionnelles, et des interfaces des composants qui décrivent leurs comportements à travers de DS.Les étapes principales de notre approche sont présentées dans la Figure10.2, elles peuvent être décrites comme suit : 1. Commencer par analyser le diagramme d'exigences SysML pour obtenir les exigences atomiques car elles sont plus précises et il sera plus facile de trouver des composants qui vont les satisfaire (voir Section 8.3). 2. Soit la première exigence atomique, soit un composant dans une bibliothèque de composants, décrit par le DS . Spéciier avec la formule LTL et traduire au code Promela , puis vériier que satisfait en vériiant que satisfait avec le model-checker SPIN (voir Section 7.3). La sélection du composant dans la bibliothèque est faite par l'architecte logiciel. Néanmoins, il est possible de guider cette sélection (ou l'automatiser) car est une exigence fonctionnelle et décrit des contraintes dans les services ofert et requis (actions d'entrée/sortie). Ces services sont aussi décrits dans les interfaces des composants. Alors, il est facile d'extraire ces services de et de faire une correspondance avec ceux décrit dans les interfaces. Si cette étape retourne false, alors ne satisfait pas et donc l'on doit obtenir le composant approprié dans une autre bibliothèque, ou le développer dès zéro. 3. Soit l'automate d'interface qui décrit le protocol du composant obtenu à partir du DS (voir Section 8.4). 4. Identiier les actions d'entrée et sortie en liées à (voir Section 8.4 ). 5. Répéter jusqu'à avoir traité tous les exigences : (a) Soit +1 l'exigence atomique suivante, connectée à (voir Déinition 19), soit +1 un composant satisfaisant +1 , grâce à la formule LTL +1 et le code Promela +1 . Soit +1 l'automate d'interface décrivant le protocole du composant.

	Élément DS Ligne de vie Message Connecteur		Élément Promela Processus Message Chaîne de communication pour chaque lèche de mes-	Déclaration Promela proctype{...} mtype{m1,...,mn} chan chanName = [1] of {mtype}
	Envoi et réception d'événements	sage Envoi d'opérations et	réception	Send ⇒ ab!m, Receive ⇒ ab?m
	Fragment biné Alt Fragment biné Loop	com-com-	condition if opérateur do		if ::(guard)->ab_p?p; :: else -> ab_q?q; fi; do ::ab_p?p; od
	. . / Vé fi		F	'E	S ML
	. . / S é fi	I	é	'	A	SBC

vérification et simulation pour la validation de propriétés non fonctionnelles Dans

  l'ensemble de sous-blocs simulait le comportement attendu dans le bloc abstrait. Pour faciliter la tâche de vériication de la simulation alternée nous avons proposé d'utiliser le module Observational Modal Reinement de l'outil MIO Workbench.2. La deuxième contribution a été orientée sur la vériication des propriétés de notre système. Nous nous avons inspiré des travaux proposés par V.Lima et al. Cette technique propose de générer des modèles basés en Promela à partir des interactions UML décrites en Diagrammes des Séquences (DS) et utilise l'outil de model-checking SPIN pour simuler et vériier des propriétés écrites en Logique Temporelle Linéaire (LTL). Notre adaptation de cette approche s'est orientée à un type particulière de DS que nous exploitons pour spéciier le comportement d'un bloc. Nous avons choisi Promela pour décrire des spéciications de DS et des propriétés LTL pour décrire des exigences fonctionnelles. Pour la suite, nous avons utilisé le modelchecker SPIN pour vériier ces propriétés. Nous avons choisi cet environnement d'implémentation car c'est un outil de vériication très répandu et permet d'une manière relativement facile de spéciier et implémenter des concepts des DS comme l'envoi et réception de primitives et la composition parallèle et asynchrone. 3. La troisième contribution propose une approche pour décrire la relation entre les exigences du système et la spéciication d'une architecture CBS en SysML. L'objectif était de proposer une méthodologie pour construire incrémentalement une architecture de système consistante que formellement satisfait toutes les exigences du système. Nous avons utilisés des SD pour décrire les comportements des blocs et DDB et DBI pour spéciier l'architecture du système. La construction proposé extrait les exigences atomiques d'un diagramme d'exigences et les traite un par un pour construire le système inal. Nous obtenons donc une architecture partielle du système, composé de blocs élémentaires et blocs composites. À chaque étape, nous sélectionnons une exigence atomique à partir d'un diagramme d'exigences SysML, et nous choisissons un bloc d'une bibliothèque des blocs qui devrait satisfaire l'exigence choisie. Puis, nous vériions si le bloc satisfait l'exigences grâce aux propriétés LTL spéciiés par l'exigence et la spéciication Promela qui décrit le comportement du bloc à partir du DS. Ensuite, nous vériions la compatibilité entre le bloc sélectionné et ceux sélectionnés aux étapes précédentes. Le processus init quand toutes les exigences atomiques ont été traitées ou quand on détecte des incompatibilités entre les blocs, ou si les exigences ne sont pas conservées par le bloc composite formé. De cette manière nous garantissons la consistance de l'architecture du système inal qui satisfait toutes les exigences du système. Les travaux de cette thèse répond à une question principale : comment introduire la vériication formelle dans des spéciications informelles SysML pendant le processus de développement des SBC ? Dans ce but, nos contributions ont introduit quelques solutions pour construire de SBC consistants, ainsi nous avons établi des relations entre le rainement, concepts de blocs SysML et caractéristiques des SBC. Ce travail peut continuer à être enrichi et dans ce contexte nous envisageons d'autres perspectives de travail comme : Chaîne d'outils pour la vérification Développer une chaîne d'outils pour aider le concepteur dans la vériication automatique de la relation de rainement entre les blocs abstraits et ses sous-blocs et aussi la vériication des exigences SysML dans les blocs pour décider la validité de l'architecture CBS en SysML. Cette chaîne d'outils serait composé d'outils qui permettrait (1) vériier les conditions de consistance entre les blocs et utiliser l'outil Ptolemy pour la vériication de la compatibilité, (2) traduire directement des DS en programmes Promela et (3) vériier des propriétés LTL avec le model-checker SPIN. Quelques exemples signiicatifs pourrait être expérimentés pour évaluer l'approche proposée. les applications iables, il es important de spéciier une architecture de système en accord avec des spéciications d'exigences fonctionnelles et non-fonctionnelles. Dans ce but, nous proposons une approche pour spéciier l'architecture du système directement en SysML à partir des exigences fonctionnelles SysML. Ainsi, pour des travaux futurs, il serait intéressant d'adresser le problème de validation pour les exigences non-fonctionnelles et utiliser des techniques de simulation. Le problème d'adapter des blocs est crucial dans le développement de SBC en réutilisant des blocs. L'adaptation consiste à générer automatiquement, quand c'est possible, un bloc adaptateur entre blocs incompatibles pou assurer une interaction iable. L'idée d'un travail futur est de générer une entité capable d'assurer l'interaction entre deux blocs incompatibles quand les conditions de consistance et compatibilité ne sont pas validées.

	Combiner
	. / P

Adapter et générer des adaptateurs pour les blocs incompatibles

¹Image taken from[START_REF] Davis | Mercedes-Benz celebrates 30 years of using airbag technology[END_REF]

¹http://www.nomagic.com

²http://www.atego.com ³http://www.sparxsystems.com http://www.eclipse.org/emf/ http://www.eclipse.org/papyrus/

http://www.topcased.org/ http://www.polarsys.org

and

, and belongs to the internal actions in otherwise.

. En efet, dans cette approche on vériie l'existence d'un environnement qui fournit les services appropriés au produit 1 ⊗ 2 ain d'éviter les états illégaux. Les états dans lesquels l'environnement peut éviter l'atteignabilité des états illégaux sont appelés états compatibles, et sont déinis par l'ensemble Comp( 1 , 2 ). Cet ensemble est calculé dans 1 ⊗ 2 en éliminant les états illégaux, les états inatteignables et les états qui conduisant vers des états illégaux en passant par des actions internes ou des actions de sortie.

Algorithme 1 : Veriication of the consistency and the compatibility between blocks Input : An abstract block described with a = ⟨Φ , , , ⟩ and a = ⟨Φ , , , , , ⟩, and a sequence diagram =1.. = ⟨, , , , ⟩ for each sub-block =1.. described in the .

Output :

The results on the veriication of the structural reinement between the abstract block and its sub-blocks Consistency veriication:

1. Analyze the by exploring the set Φ and the block interfaces from the sets ( , ) (obtained using the function) to identify the ofered, required and internal operations of , =1.. .

Analyze the by exploring the set Φ

(which are instances of blocks in Φ ) and identify the connected sub-blocks using the function on each of the internal ports in and .

3. For each pair of connected sub-blocks and verify the condition 1 (composability), by considering their sets of private operations (Φ , Φ ) and the sets of ofered and required services (Φ , Φ , Φ , and Φ ).

4. Analyze the and identify which internal input port in is connected to the external input port and select the sub-block that owns it.

5. Verify the condition 2 (at least the same inputs)

6. Analyze the and identify which internal output port in is connected to the external input port and select the sub-block that owns it.

7. Verify the condition 3 (at most the same outputs) Let be the automaton representing the behavior of the block ACU, such that:

The result automaton from the translation ( ) is a modal automaton such that:

We say that a modal automaton observationally reines a modal automaton , writen ≤ * , if there exists an observational modal reinement containing ( , ).

. . / C S A

To verify the behavior reinement for the SensorsControl block we need the sequence diagram shown in Figure 6.14, it shows the messages and replies that must be implemented

Deinition 17: Requirement diagram speciication

We specify a SysML requirement diagram by = ⟨ , , , ⟩ such that:

• : deine the set of initial requirements, the irst requirements that the speciier deines in the requirement diagram. Generally, they are not precise, and it is necessary to connect them, with the containment relation, to more reined requirements.

• : the set of all requirements.

• ⊆ ( ) the relation of containment, where ( ) is the set of the subsets of .

• ⊆ ( ) the relation of derivation.

For example in our case study, the speciication of the requirement diagram described in Figure 8.3 is = ⟨ , , , ⟩, where:

. }) ∈ }

An atomic requirement is a requirement that can not be decomposed. It expresses a constraint on input and output actions which are related to one component (see Section 8.4).

The atomic requirements in our case study are (see Figure 8.

Remark: To compute the set of atomic requirements, it is necessary to analyze the set of all requirements and to identify the requirements that are not related by the relation (containment).

Theorem 2: System satisfying all atomic requirements

Let be a CBS, let = ⟨ , , , ⟩ be the speciication of a requirement diagram, and let be the set of atomic requirements of . satisies all the requirements in if it satisies the atomic requirements .

Theorem 2 states that it is suicient for a system to satisfy the atomic requirements, in order to satisfy all requirements represented in a SysML requirement diagram.

To illustrate the proof of this theorem, we propose a simple requirement diagram presented in Figure 8.4. The requirements are connected with a containment relation, with

( 1 , 2 );

Deux automates d'interface pourraient être incompatibles à cause de l'existence des états illégaux dans leur produit synchronisé. Les états illégaux sont des états à partir lesquels une action de sortie partagée d'un automate ne peut pas être synchronisée avec la même action activée en entrée dans l'autre composant.

Deinition 23: Etats Illégaux

Soient deux automates d'interface composables 1 et 2 , l'ensemble des états il-

L'approche des automates d'interface est considérée comme une approche optimiste, car l'atteignabilité des états dans Illégal( 1 , 2 ) ne garantit pas l'incompatibilité des 1 et

Abstract:

The work presented in this thesis is a contribution to the speciication and veriication of Component-Based Systems (CBS) modeled in SysML. CBS are widely used on the industrial ield, and they are built by assembling various reusable components, allowing developing complex systems at lower cost.

To ease the communication between the various stakeholders in a CBS development project, one of the widely used modeling languages is SysML, which besides allowing modeling of structure and behavior, it has capabilities to model requirements. It ofers a standard for modeling, specifying and documenting systems, wherein it is possible to develop a system, starting from an abstract level, to more detailed levels that may lead to an implementation. In this context, we have dealt mainly two issues. The irst one concerns the development by reinement of a CBS, which is described only by its SysML interfaces and behavior protocols. Our contribution allows the designer of CBS to formally ensure that a composition of a set of elementary and reusable components reines an abstract speciication of a CBS. In this contribution, we use the tools: Ptolemy for the veriication of compatibility of the assembled components and MIO Workbench for reinement veriication.

The second one concerns the diiculty to decide what to build and how to build it, considering only system requirements and reusable components. Therefore, the question that arises is: how to specify a CBS architecture, which satisies all system requirements? We propose a formal and incremental veriication approach based on SysML models and interface automata to guide, by the requirements, the CBS designer to deine a coherent system architecture that satisies all proposed SysML requirements. In this approach we use the SPIN model-checker and LTL properties to specify and verify requirements.

Keywords