Maria Rita

Pamela Carreño Medrano

Keywords: Type of variable: independent or dependent, Class: product, process, or resource, Entity: instance of class, Type of attribute: internal, external, Scale type: nominal, ordinal, interval, ratio, among others Synthèse d'architectures logicielles pour systèmes-de-systèmes Milena Margarido 2017

result of many years of work. Through the years, many people contributed, directly and indirectly, for achieving this result.

"It's the time you spent on your rose that makes your rose so important" (Antoine de Saint-Exupéry)

Abstract

Systems-of-Systems (SoS) encompass diverse and independent systems that must cooperate with each other for performing a combined action that is greater than their individual capabilities.

In parallel, architecture descriptions, which are the main artifact expressing software architectures, play an important role in fostering interoperability among constituents by facilitating the communication among stakeholders and supporting the inspection and analysis of the SoS from an early stage of its life cycle. The main problem addressed in this thesis is the lack of adequate architectural descriptions for SoS that are often built without an adequate care to their software architecture. Since constituent systems are, in general, not known at design-time due to the evolving nature of SoS, the architecture description must specify at design-time which coalitions among constituent systems are feasible at run-time. Moreover, as many SoS are being developed for safety-critical domains, additional measures must be placed to ensure the correctness and completeness of architecture descriptions. To address this problem, this doctoral project employs SoSADL, a formal language tailored for the description of SoS that enables one to express software architectures as dynamic associations between independent constituent systems whose interactions are mediated for accomplishing a combined action. To synthesize concrete architectures that adhere to one such description, this thesis develops a formal method, named Ark, that systematizes the steps for producing such artifacts. The method creates an intermediate formal model, named TASoS, which expresses the SoS architecture in terms of a constraint satisfaction problem that can be automatically analyzed for an initial set of properties.

The feedback obtained in this analysis can be used for subsequent refinements or revisions of the architecture description. A software tool named SoSy was also developed to support the Ark method as it automates the generation of intermediate models and concrete architectures, thus concealing the use of constraint solvers during SoS design and development. The method and its accompanying tool were applied to model a SoS for urban river monitoring in which the feasibility of candidate abstract architectures is investigated. By formalizing and automating the required steps for SoS architectural synthesis, Ark contributes for adopting formal methods in the design of SoS architectures, which is a necessary step for obtaining higher reliability levels. Keywords: Software architecture, Architectural Description, Systems-of-systems, SoS.

Resumo

Sistemas-de-sistemas (SoS) englobam sistemas diversos e independentes que cooperam entre si para executar uma ação combinada que supera suas competências individuais. Em paralelo, descrições arquiteturais são artefatos que expressam arquiteturas de software, desempenhando no contexto de SoS um importante papel na promoção da interoperabilidade entre constituintes ao facilitar a comunicação entre interessados e apoiar atividades de inspeção e análise desde o início de seu ciclo de vida. O principal problema abordado nessa tese consiste na falta de descrições arquiteturais adequadas para SoS que estão sendo desenvolvidos sem um devido cuidado à sua arquitetura de software. Uma vez que os sistemas constituintes não são necessariamente conhecidos em tempo de projeto devido à natureza evolucionária dos SoS, a descrição arquitetural precisa definir em tempo de projeto quais coalisões entre sistemas constituintes são possíveis em tempo de execução. Como muitos desses sistemas são desenvolvidos para o domínio crítico de segurança, medidas adicionais precisam ser adotadas para garantir a correção e completude da descrição arquitetural. Visando tratar esse problema, esse projeto de doutorado emprega SosADL, uma linguagem formal criada especialmente para o domínio de SoS que permite expressar arquiteturas de software como associações dinâmicas entre sistemas independentes em que as interações devem ser mediadas para desempenhar uma ação conjunta. Em particular, é proposto um novo método formal, denominado Ark, para sistematizar os passos necessários na síntese de arquiteturas concretas aderentes a essa descrição. Para isso, o método cria um modelo formal intermediário, denominado TASoS, que expressa a arquitetura do SoS em termos de um problema de satisfatibilidade de restrições, possibilitando desse modo a verificação automática de um conjunto inicial de propriedades. O resultado obtido por essa análise pode ser utilizado em refinamentos e revisões subsequentes da descrição arquitetural. Uma ferramenta de apoio denominada SoSy também foi desenvolvida para automatizar a geração de modelos intermediários e arquiteturas concretas, ocultando o uso de solucionadores de restrições no projeto e desenvolvimento de SoS. O método e sua ferramenta foram aplicados em um modelo de SoS para monitoramento de rios em áreas urbanas em que a viabilidade de arquiteturas abstratas foi investigada. Ao formalizar e automatizar os passos necessários para a síntese arquitetural de SoS, é possível adotar métodos formais no projeto arquitetural de SoS, que são necessários para alcançar níveis maiores de confiabilidade.

Palavras-chave: Arquitetura de Software, Descrição Arquitetural, Sistemas-de-sistemas, SoS.

Résumé

Les systèmes-de-systèmes (SoS) interconnectent plusieurs systèmes indépendants qui travaillent ensemble pour exécuter une action conjointe dépassant leurs compétences individuelles. Par ailleurs, les descriptions architecturales sont des artefacts qui décrivent des architectures logicielles jouant dans le contexte SoS un rôle important dans la promotion de l'interaction des éléments constituants tout en favorisant la communication parmi les intéressés et en soutenant les activités d'inspection et d'analyse dès le début de leur cycle de vie. Le principal problème traité dans cette thèse est le manque de descriptions architecturales adéquates pour les SoS qui sont développés sans l'attention nécessaire à leur architecture logicielle. Puisque les systèmes constituants ne sont pas forcément connus pendant la conception du projet à cause du développement évolutionnaire des SoS , la description architecturale doit définir à la conception même du projet quelles coalitions entre les systèmes constituants seront possibles pendant son exécution. En outre, comme plusieurs de ces systèmes sont développés pour le domaine critique de sécurité, des mesures supplémentaires doivent être mises en place pour garantir l'exactitude et la complétude de la description architecturale. Afin de résoudre ce problème, nous nous servons du SosADL, un langage formel créé spécialement pour le domaine SoS et qui permet de décrire les architectures logicielles comme des associations dynamiques entre systèmes indépendants où les interactions doivent être coordonnées pour réaliser une action combinée. Notamment, une nouvelle méthode formelle, nommée Ark, est proposée pour systématiser les étapes nécessaires dans la synthèse d'architectures concrètes obéissant à cette description. Dans ce dessein, cette méthode crée un modèle formel intermédiaire, nommé TASoS, qui décrit l'architecture du SoS en tant que problème de satisfaisabilité de restrictions, rendant ainsi possible la vérification automatique d'un ensemble initial de propriétés. Le résultat obtenu par cette analyse peut s'utiliser en raffinements et révisions ultérieurs de la description architecturale. Un outil logiciel nommé SoSy a été aussi développé pour automatiser la génération de modèles intermédiaires et d'architectures concrètes, en cachant l'utilisation de solveurs de contraintes dans le projet de SoS. Particulièrement, cet outil intègre un environnement de développement plus important et complet pour le projet de SoS . Cette méthode et son outil ont été appliqués dans un modèle de SoS de surveillance de rivières urbaines où la faisabilité d'architectures abstraites a été étudiée. En formalisant et en automatisant les étapes requises pour la synthèse architecturale de SoS , Ark contribue à l'adoption de méthodes formelles dans le projet d'architectures SoS , ce qui est nécessaire pour atteindre des niveaux plus élevés de fiabilité.

Mots-clés: Architecture logicielle, Description architecturale, Systèmes de systèmes, SoS. Table 1 -

List of Figures

List of Tables

List of abbreviations and acronyms

Introduction

Software architecture is acknowledged as a particular discipline of software engineering since the late 1990s when it became central to realize managed approaches for the development of increasingly complex software systems [START_REF] Kruchten | Documentation of Software Architecture from a Knowledge Management Perspective -Design Representation[END_REF]OBBINK;[START_REF] Kruchten | The past, present, and future for software architecture[END_REF]. The ISO/IEC/IEEE 42010 (2011) standard defines a software architecture as the "fundamental organization of a system, embodied in its components, their relationships to each other and to the environment, and the principles governing its design and evolution over time." Hence, software architectures must be able to capture the structure of a software system, such as the hierarchical relationship between its elements, as well as its behavior, encompassing interactions that are exchanged at run-time among its elements and environment. To offer a comprehensive view about software systems, software architectures omit implementation details and focus on the architectural decisions, i.e., choices taken during the design of software systems that can largely impact their perception [START_REF] Allen | A Formal Approach to Software Architecture[END_REF]. As a result, different designs for software architectures can be investigated aiming to promote specific quality attributes, e.g., performance, safety, maintainability, and longevity [START_REF] Clements | A survey of architecture description languages[END_REF][START_REF] Buschmann | Patternoriented Software Architecture: A System of Patterns[END_REF]BASS;[START_REF] Clements | A survey of architecture description languages[END_REF][START_REF] Bass | Software Architecture in Practice[END_REF]AVGERIOU;STAL;[START_REF] Avgeriou | Architecture Sustainability[END_REF].

As the set of tangible artifacts that describe a software architecture, the architecture description (or architectural representation) provides the means for assessing software architecture properties, sharing architectural knowledge, and preventing software systems decay (GARLAN;[START_REF] Garlan | An Introduction to Software Architecture[END_REF][START_REF] Kruchten | Documentation of Software Architecture from a Knowledge Management Perspective -Design Representation[END_REF][START_REF] Clements | A survey of architecture description languages[END_REF][START_REF] Kruchten | Documentation of Software Architecture from a Knowledge Management Perspective -Design Representation[END_REF]. In particular, architecture descriptions can be used as input for automated simulation, generation, and analysis tools, and as basis for evaluating software architectures (ISO/IEC/IEEE 42010, 2011; MENS; MAGEE; RUMPE, 2010;[START_REF] Krüger | From scenarios to hierarchical broadcasting software architectures using uml-rt[END_REF]OBBINK et al., 2002;[START_REF] Ledeczi | Synthesis of self-adaptive software[END_REF]KARSAI;[START_REF] Ledeczi | Synthesis of self-adaptive software[END_REF][START_REF] Oquendo | π-ADL: An Architecture Description Language based on the Higher Order Typed π-Calculus for Specifying Dynamic and Mobile Software Architectures[END_REF][START_REF] Allen | Using an architecture description language for quantitative analysis of real-time systems[END_REF][START_REF] Iacobucci | A method for the generation and evaluation of architecture alternatives on the cloud[END_REF][START_REF] Iacobucci | A method for the generation and evaluation of architecture alternatives on the cloud[END_REF]. Since architecture descriptions contribute for a clearer understanding of software architectures, they can also support choosing among different design alternatives (GARLAN;[START_REF] Garlan | An Introduction to Software Architecture[END_REF]. Aiming to disseminate best practices for creating architectural descriptions, the ISO/IEC/IEEE 42010 (2011) standard establishes the main elements of such an artifact, which includes concerns, architecture views, viewpoints, and rationale. Indeed, architecture descriptions address concerns of a specific group of stakeholders [START_REF] Kruchten | Documentation of Software Architecture from a Knowledge Management Perspective -Design Representation[END_REF][START_REF] Clements | A survey of architecture description languages[END_REF]; ISO/IEC/ IEEE-42010, 2011). These concerns or interests can be related to desired properties or requirements for the software system, such as functionality, security, cost, performance, or interoperability (ISO/IEC/IEEE 42010, 2011). Adhering to the separation of concerns principle, the standard recommends creating multiple views, each of which framing one or more distinct concerns about the software architecture. An architecture view conforms to a particular architectural viewpoint, which defines conventions, such as languages, notations, methods, or techniques, for the creation of corresponding views (ISO/IEC/IEEE 42010, 2011). Several studies investigate architecture viewpoints in the description of software architectures (BASS; CLEMENTS; [START_REF] Bass | Software Architecture in Practice[END_REF][START_REF] Clements | Documenting Software Architectures: Views and Beyond[END_REF][START_REF] Rozanski | Software Systems Architecture: Working with stakeholders using viewpoints and perspectives[END_REF][START_REF] Rozanski | Software Systems Architecture: Working with stakeholders using viewpoints and perspectives[END_REF]; ISO/IEC/IEEE 42010, 2011). The ISO/IEC/IEEE 42010 (2011) standard does not constrain which views have to be selected for describing software architectures, thus specific architecture frameworks 1 have been established, such as The Open Group Architecture Framework (TOGAF) (Open Group, 2009), Zachman's framework [START_REF] Zachman | A framework for information system architecture[END_REF], "4+1" Views [START_REF] Kruchten | Documentation of Software Architecture from a Knowledge Management Perspective -Design Representation[END_REF], and "Views and Beyond" [START_REF] Clements | Documenting Software Architectures: Views and Beyond[END_REF]. Finally, the documentation of architecture decisions is also acknowledged as an important part of architecture descriptions [START_REF] Clements | Documenting Software Architectures: Views and Beyond[END_REF][START_REF] Babar | Supporting the Software Architecture Process with Knowledge Management[END_REF]ISO/IEC/IEEE 42010, 2011;[START_REF] Farenhorst | Knowledge Magament in Software Architecture: State of the Art[END_REF][START_REF] Farenhorst | Knowledge Magament in Software Architecture: State of the Art[END_REF][START_REF] Kruchten | Documentation of Software Architecture from a Knowledge Management Perspective -Design Representation[END_REF]. By reporting justifications for architectural decisions (e.g., reasoning that led to a particular decision, or trade-offs between design choices), the documentation of software architectures also contributes for disseminating architectural knowledge.

An Architectural Description Language (ADL), which is any form of expression used in architecture descriptions, provides one or more model kinds 2 for framing a particular set of concerns [START_REF] Clements | Documenting Software Architectures: Views and Beyond[END_REF]ISO/IEC/IEEE 42010, 2011). Differently from implementation languages, ADLs provide tailored abstractions for the main elements which are part of a software architecture, namely: components, which are units of computation representing functional elements of the system, such as packages, classes, systems, and sub-systems; connectors, representing interconnections that enable the communication among components; and architectural configurations, representing the way in which components and connectors can be arranged together, e.g., showing which components are communicating with each other by means of connectors or the hierarchical relationship that exists among elements of the software architecture [START_REF] Medvidovic | A classification and comparison framework for software architecture description languages[END_REF][START_REF] Medvidovic | A classification and comparison framework for software architecture description languages[END_REF]. To further characterize components and connectors, ADLs support the description of interfaces, which define interaction points exposed by these elements to the environment, as well as high-level behavior models and constraints. Desired features that should be supported by ADLs encompass description of functional and non-functional properties, formal semantics for precision and automated analysis, and both graphical and textual representations for easing the communication between stakeholders of architecture descriptions [START_REF] Lago | The road ahead for architectural languages[END_REF].

As a particular class of software systems, Systems-of-Systems (SoS) refer to systems formed by independent systems (also referred to as constituent systems) [START_REF] Maier | Architecting principles for systems-of-systems[END_REF][START_REF] Nielsen | Systems of Systems Engineering: Basic Concepts, Model-Based Techniques, and Research Directions[END_REF]. The term software-intensive SoS 3 has also been used to distinguish SoS that use software for tailoring constituent systems to their particular environments or needs [START_REF] Boehm | Some Future Software Engineering Opportunities and Challenges[END_REF]. One of such needs concerns the formation of temporary alliances among constituent systems, also referred to as coalitions, which enables their combined action (OQUENDO, 2016c). There are five key characteristics that distinguish SoS from traditionally complex, monolithic systems [START_REF] Boehm | Spiral Acquisition of Software-Intensive Systems-of-Systems[END_REF]): (i) coalitions produce an emergent behavior that cannot be provided by any constituent alone; (ii) constituents retain their operational independence since they can still operate even when detached from the SoS; (iii) constituents also retain their managerial independence since they can be developed, maintained, and evolved independently from the SoS; (iv) coalitions are evolutionarily developed by continuously changing in response to different environments and needs; and (v) constituents can be geographically distributed as they can only exchange information with each other.

There are several examples of SoS in practice. The Global Earth Observation Systems-of-Systems (GEOSS) (SHIBASAKI; [START_REF] Shibasaki | Systems of Systems Engineering of GEOSS[END_REF] combines several independent systems collecting wind, water, and land observations for creating a comprehensive panorama that can ultimately support disaster reduction, weather monitor and forecasting, efficient use of the land, among others. Other examples of SoS are the US ballistic missile defense system, which encompasses sea-based, land-based, and space-based legacy and new missile defense programs for performing battle management functions (e.g., monitoring missile trajectories since launch until termination) (HOLLON; [START_REF] Hollon | The US Ballistic Missile Defense System: A case study in architecting systems-of-systems[END_REF], medical systems encompassing diagnosis, treatment, and patient management systems (HATA et al., 2007), and air traffic control systems encompassing aircraft, satellites, and control tower systems [START_REF] Wilber | A system of systems approach to e-enabling the commercial airline applications from an airframer's perspective[END_REF]. In this scenario, embedded systems 4 can also be acknowledged as SoS once they evolve and become complex software systems that are geographically distributed and can change their structure and functionality (HAVERKORT, 2013). The term Cyber-Physical System (CPS) can also be used to designate a communication network among embedded systems that may exchange energy as well as information with each other [START_REF] Broy | Seamless Method-and Model-based Software and Systems Engineering[END_REF][START_REF] Broy | Cyber-Physical Systems: Imminent Challenges[END_REF][START_REF] Broy | Cyber-Physical Systems: Imminent Challenges[END_REF]. In this scenario, software is increasingly used as the means for tailoring complex software systems to new scenarios, such as part of a larger SoS. For instance, the automotive industry uses 3 For the sake of simplicity, SiSoS and SoS are used interchangeably throughout the text. [START_REF] Valerdi | A Framework for Evolving System of Systems Engineering[END_REF] In contrast to general-purpose computing systems, embedded systems are dedicated to the execution of a particular set of tasks [START_REF] Wohlin | Formal Modelling Language for Systems of Systems[END_REF], such as software systems deployed in aircraft, vehicles, smart-phones, among others. Moreover, embedded systems can interact with the physical environment by means of sensors that collect information about their surroundings and actuators that enable to perform a physical action [START_REF] Marwedel | Embedded System Design[END_REF].

software for processing complex sensory data, improving reliability, safety, and efficiency, as well as decreasing pollution (HAVERKORT, 2013). Besides the ability for adaptation, learning, communication, and reconfiguration, these systems must satisfy strict quality attributes, such as safety, security, and efficiency, to succeed. Thereby, there is an increasing necessity of software development approaches that can guarantee the quality of such systems (LIGGESMEYER; TRAPP, 2009).

Problem statement

The design, development, and maintenance of SoS faces several challenges due to their intrinsic characteristics (BOEHM; BROWN;[START_REF] Boehm | Spiral Development of Software-intensive systems of systems[END_REF]. For instance, the formation of new configurations at run-time is a challenge that arises from the evolutionary development of SoS. To accomplish their missions in face of acquisition or loss of constituent systems, SoS software architectures must be able to form different coalitions. In this sense, SoS software architectures represent a shift from software architectures of single software systems, which can be determined early in their life cycle and remain relatively stable [START_REF] Rhodes | Evolving Systems Engineering for Innovative Product and Systems Development[END_REF]OQUENDO, 2016c). As a consequence, traditional perspectives on system design and control that assume architectures to be determined early in systems life cycle are not suitable for SoS (ULIERU; [START_REF] Ulieru | Emergent engineering: a radical paradigm shift[END_REF]. Aiming to support SoS evolution, dynamic software architectures can be investigated for promoting SoS resilience in face of uncertainty (DAGLI; [START_REF] Dagli | System of systems architecting[END_REF][START_REF] Nakagawa | The state of the art and future perspectives in systems of systems software architectures[END_REF][START_REF] Nielsen | Systems of Systems Engineering: Basic Concepts, Model-Based Techniques, and Research Directions[END_REF]. Since SoS architecture evolution can have deeper repercussions in regards to structure and behavior, tailored support is needed for rearchitecting, a process in which old elements of the architecture are modified, replaced, or rebuilt and/or new elements are included (AVGERIOU; STAL; [START_REF] Avgeriou | Architecture Sustainability[END_REF]. In particular for safety-critical applications in which there is an eminent risk of harming people and/or the environment, or causing financial loss [START_REF] Knight | Safety critical systems: challenges and directions[END_REF], a rigorous rearchitecting approach must be in place to guarantee that any formed coalition complies with the original design of the SoS. To use architecture descriptions as a guide to such an approach, this thesis addresses three problems, which are further elaborated in the following sections.

Describe Systems-of-Systems Software Architectures

The five intrinsic characteristics of SoS make their architectural design more complex. For instance, due to constituents operational and managerial independence, constituent systems are not controlled by the SoS, implying that they have their own missions and operational life cycles and their management and evolution is carried out independently from the SoS itself. Moreover, as SoS evolve, constituents that were not necessarily known at design time can join and leave the coalition, thus imposing a new requirement to the design of SoS that must be able to identify and incorporate new constituents at run-time (OQUENDO, 2016c). In this scenario, the creation of coalitions among constituent systems should be addressed from an architectural perspective. Abstracting from implementation details, the software architecture expresses the fundamental organization of systems. Thereby, architecture descriptions of SoS must enable to express guarantees for constituents expected behavior and/or architectural properties (FITZGER-ALD; BRYANS; PAYNE, 2012). The connectors that support the communication among these constituent systems can be complex architectural entities on their own, e.g., acting as mediators between independent parts and enabling the realization of combined actions [START_REF] Nakagawa | The state of the art and future perspectives in systems of systems software architectures[END_REF][START_REF] Issarny | Composing Distributed Systems: Overcoming the Interoperability Challenge[END_REF][START_REF] Issarny | Composing Distributed Systems: Overcoming the Interoperability Challenge[END_REF]. Unlike constituents, mediators operate under the explicit control of SoS to fulfill global missions (OQUENDO, 2016c). The description of SoS configurations must capture their structure and emergent behaviors for better understanding such systems [START_REF] Dogan | Economic and Societal Significance of the Systems of Systems Research Agenda[END_REF]. Thereby, the architectural configuration of an SoS must describe how constituents and mediators are arranged together, what interactions are exchanged among them, and what behaviors emerge from the coalition. As configurations are continuously changing, an static description of the software architecture can quickly become obsolete (SELBERG; [START_REF] Selberg | Toward an Evolutionary System of Systems Architecture[END_REF]. Therefore, the description of SoS requires new abstractions supporting dynamic modification of architectures and interfaces [START_REF] Nielsen | Systems of Systems Engineering: Basic Concepts, Model-Based Techniques, and Research Directions[END_REF].

While several ADLs can be used for the description of software systems, expressiveness is still an issue (HILLIARD; [START_REF] Hilliard | Expressiveness in Architecture Description Languages[END_REF]OZKAYA;[START_REF] Ozkaya | Are We There Yet? Analyzing Architecture Description Languages for Formal Analysis, Usability, and Realizability[END_REF], in particular in the context of SoS [START_REF] Batista | Challenges for SoS architecture description[END_REF]OQUENDO, 2016c). These languages can be classified in three broad categories (BASS; CLEMENTS; KAZMAN, 2012): (i) formal languages that present mathematically defined syntax and semantics; (ii) semi-formal languages that present well-defined syntax but lack of complete semantics; and (iii) informal languages that represent ad-hoc, graphical notations with neither defined syntax or semantics. Languages in each category can offer different mechanisms for the communication of architectural design to stakeholders, who in turn may need a specific set of skills for effectively applying and/or understanding models expressed in those languages. Formal languages, such as Wright [START_REF] Allen | A Formal Approach to Software Architecture[END_REF] and π-ADL [START_REF] Oquendo | π-ADL: An Architecture Description Language based on the Higher Order Typed π-Calculus for Specifying Dynamic and Mobile Software Architectures[END_REF], enable the creation of formal models that can be verified and validated against quality attributes using tailored tools. Thus, such languages are particularly interesting for ensuring architectural properties and supporting automated analysis and evolution of software systems (ZHANG; MUCCINI; LI, 2010). In turn, semi-formal languages, such as Unified Modeling Language (UML) (OMG, 2011) and Systems Modeling Language (SysML) (OMG, 2012) that have a well-known syntax, facilitate the communication among stakeholders but offer limited support for automated analysis.

The precision and rigor that can be achieved with formal models becomes essential for obtaining higher reliability in software systems [START_REF] Jackson | Towards a Theory of Conceptual Design for Software[END_REF][START_REF] Mandrioli | On the heroism of really pursuing formal methods[END_REF]. In the context of SoS, precise architecture descriptions are needed for understanding emergent behaviors, evolutionary development, and independence of constituent systems [START_REF] Dogan | Economic and Societal Significance of the Systems of Systems Research Agenda[END_REF][START_REF] Nielsen | Systems of Systems Engineering: Basic Concepts, Model-Based Techniques, and Research Directions[END_REF]. Nonetheless, the design of software architectures for SoS and, in particular, their architecture description are still open topics of research in the Software Engineering field [START_REF] Nakagawa | The state of the art and future perspectives in systems of systems software architectures[END_REF][START_REF] Batista | Challenges for SoS architecture description[END_REF][START_REF] Klein | A systematic review of system-of-systems architecture research[END_REF][START_REF] Klein | A systematic review of system-of-systems architecture research[END_REF]GUESSI et al., 2015). While previous works focus on adaptation and evolution of the dynamic changes in software architectures [START_REF] Lemos | Software Engineering for Self-Adaptive Systems: A Second Research Roadmap[END_REF], traditional practices for architectural description from a run-time viewpoint lack expressiveness to describe SoS architectures [START_REF] Nielsen | Systems of Systems Engineering: Basic Concepts, Model-Based Techniques, and Research Directions[END_REF]GUESSI;CAVALCANTE;OLIVEIRA, 2015). Hence, the first problem addressed in this thesis is summarized as follows:

Problem I

Traditional practices for the description of software architectures of single, complex systems lack tailored abstractions for the main elements of SoS.

Ensure Feasibility of Systems-of-Systems Software Architectures

SoS adaptation can be triggered by changes in constituent systems, emergent behaviors, or missions, which makes dynamic reconfiguration and evolution two capabilities that must be supported for guaranteeing SoS resilience. Dynamic reconfiguration is the result of unplanned changes to the architecture and/or constituents whereas evolution is the result of slow-paced, planned changes to the architecture, hence requiring intervention [START_REF] Nielsen | Systems of Systems Engineering: Basic Concepts, Model-Based Techniques, and Research Directions[END_REF]. In either case, the impact of modifications to the configuration of a SoS can be extensive since, in general, it is not possible to act on the constituents themselves due to their operational and managerial independence. Thus, new means that can mediate the collaboration among heterogeneous constituents and tailor these constituents to the SoS specific context are required [START_REF] Boehm | Some Future Software Engineering Opportunities and Challenges[END_REF]. For instance, [START_REF] Boardman | System of Systems -the meaning of of[END_REF] discuss the need for a dynamic determination of connectivity which is accomplished by establishing and dissolving communication links among constituents accordingly.

A key challenge faced during SoS design and deployment concerns the validation of their architectural feasibility (BOEHM, 2011) to achieve their specified missions (SILVA; BATISTA; OQUENDO, 2015). To avoid quality degradation after reconfiguring or evolving SoS, it is important to check their architectural feasibility, making sure that resulting architectures are still able to form new coalitions that preserve desired architectural properties. Also, this verification can prevent reaching an erroneous state of the SoS architecture for which there will be no feasible coalition. Hence, the second problem addressed in this thesis is summarized as follows:

Problem II Lack of automated support for analyzing the feasibility of SoS software architectures, which is required to prevent the formation of ill-formed coalitions throughout the entire SoS life cycle.

Support Synthesis of Systems-and-Systems Concrete Architectures

The continuous evolution of SoS hinders an early definition of their software architecture (SELBERG; [START_REF] Selberg | Toward an Evolutionary System of Systems Architecture[END_REF]. The need of adhering to best practices for developing SoS is pointed out by [START_REF] Valerdi | A Framework for Evolving System of Systems Engineering[END_REF], who identify three complementary SoS models: (i) normative models, describing norms and standards for how SoS should be; (ii) descriptive models, describing how SoS are by showing deviations from the normative model; and (iii) prescriptive models, describing how one can achieve the normative model given the descriptive model. The creation of normative SoS models, which support the dissemination of best practices about SoS engineering, are needed for evaluating descriptive models and refining predictive models that will enable to improve SoS quality. As normative models, abstract architectures define at design time the baseline from which coalitions will be formed at run-time. In turn, concrete architectures can be regarded as descriptive models of such coalitions, thus detailing how their individual actions are combined. As a consequence, a number of concrete architectures can be realized from a single abstract architecture depending on which and how many constituents participate in the coalition.

Candidate concrete architectures can be verified and validated against each other before choosing the one that better suits stakeholders' interests. Nonetheless, synthesis and comparison of alternative designs can be challenging and time consuming, specially due to the different ways in which constituents can be assembled together [START_REF] Chattopadhyay | A Framework for Tradespace Exploration of Systems of Systems[END_REF]ROSS;[START_REF] Chattopadhyay | A Framework for Tradespace Exploration of Systems of Systems[END_REF]. Moreover, it is not possible to assume that all concrete architectures complying with an abstract description are appropriate, i.e., they preserve all architectural properties, such as performance or safety, and external conditions, such as geographical distribution of constituents. Therefore, tailored support is needed for the synthesis of concrete architectures for a particular SoS abstract architecture. Given that abstract architectures are continuously changing, it is also important to support SoS evolution. In this scenario, a systematic approach that supports evolution of SoS can use formal models of abstract architectures as input for tools that create, analyze, and maintain concrete architectures for these systems prior, during, and after changes have taken place. Formal languages can be used for describing target architectures and then modeling change requests as refinement relations among them so that consistent models of the system can be guaranteed throughout their entire life cycle [START_REF] Broy | Seamless Method-and Model-based Software and Systems Engineering[END_REF]. Hence, the third and last problem addressed in this thesis is summarized as follows:

Problem III Lack of a systematic approach supporting synthesis of SoS concrete architectures in conformance to normative architectural models.

Research Questions

Architectural descriptions play a central role in the three problems that were previously discussed. To adequately support the creation of architecture descriptions for SoS, three research questions should be answered: RQ1. Which abstractions must be supported by ADLs for expressing the software architecture of SoS? A common understanding of what exactly are the requirements of SoS architecture descriptions is needed, mainly for facilitating organizations and partners that will develop or adapt their systems as part of a SoS [START_REF] Nakagawa | The state of the art and future perspectives in systems of systems software architectures[END_REF]). To answer this question, tailored abstractions that can enable architects to reason about the structure and behavior of the SoS as a whole are investigated. In particular, formal languages are desirable aiming to support the creation of traceable, consistent models that can be automatically analyzed.

RQ2

. How is it possible to guarantee the feasibility of SoS software architectures?

The lack of formal foundations can introduce critical gaps in SoS design, specially if an abstract architecture reaches a state from which no possible coalition can be realized. To answer this question, a formal model, which represents SoS software architectures in terms of constraints, is investigated aiming to prevent the design of incorrect coalitions. By resolving these constraints, this model can be used to confirm the feasibility of an abstract architecture by presenting a concrete architecture that satisfies its specification. This approach is in line with the research on autonomous systems architecture (KRAMER; MAGEE, 2009) where mechanisms are provided to either automatically realize a solution for which purposes, properties, and constraints of the description are satisfied, or report that such a solution does not exist.

RQ3

. How is it possible to support architectural synthesis of SoS given an abstract architecture? Since the applicability of formal descriptions can be hampered by the lack of tool support [START_REF] Lago | The road ahead for architectural languages[END_REF], this question investigates a mechanism that automates the synthesis of abstract architectures for SoS. In particular, this question investigates the effectiveness of a method that adopts constraint solving techniques for the automated synthesis of concrete architectures given a normative design of the coalition.

Contributions

This thesis makes the following contributions:

• A conceptual model that expresses SoS abstract architectures in terms of constraints, which can be automatically analyzed using off-the-shelf constraint satisfaction tools;

• A method that combines formal models and constraint solving in the synthesis of concrete architectures in conformance to such a normative design; and

• A software tool that implements model transformations required by the method, hence providing automated support for the synthesis of SoS.

Synthèse d'architectures logicielles pour systèmes-de-systèmes Milena Margarido 2017 1.4. Outline Tool support for SoS architectural synthesis is needed to ensure correctness of coalitions run-time reconfiguration. In particular, it contributes for mitigating the architectural feasibility risk that incurs from continuously changing the SoS architecture throughout their life cycle. In this sense, this tool will facilitate the creation, analysis, and evolution of formal models that are needed to automatically analyze architectural descriptions.

Outline

This chapter presented an overview of the context and problems that motivated the development of this doctoral research. The remaining chapters of this thesis are organized as follows. Chapter 2 presents the main concepts related to the design and description of software architectures for systems and SoS. Chapter 3 presents a method for architectural synthesis of SoS based on formal descriptions, which are detailed in Chapter 4. Chapter 5 details the implementation of a tool that supports this method and enables to employ model finding for confirming the feasibility of SoS architectures and identifying concrete architectures that comply with the abstract architecture design. The evaluation of this method on the case of a SoS for monitoring floods in urban areas is presented in Chapter 6. Finally, Chapter 7 revisits the thesis contributions and discusses perspectives for future research.

The accompanying materials of this thesis encompass: Appendix A details how to use the tool presented in Chapter 5 and provides instructions for uploading and analyzing architectural models; Appendix B presents materials that are referred to in the evaluation of the method in Chapter 6; and Appendix C lists accomplished publications throughout this doctoral research. Finally, Annex A details the ADL that is employed in this thesis for the description of abstract and concrete architectures of SoS.

Chapter 2

State of the Art on Architecture Description of Systems-of-Systems

Software architectures increase the abstraction level with which one can reason about software systems [START_REF] Allen | A Formal Approach to Software Architecture[END_REF]. Among design issues dealt within the software architecture level are the "gross organization and global control structure; protocols for communication, synchronization, and data access; assignment of functionality to design elements; physical distribution; composition of design elements; scaling and performance; and selection among design alternatives" (GARLAN; [START_REF] Garlan | An Introduction to Software Architecture[END_REF]. As tangible artifacts expressing software architectures, architecture descriptions provide concrete ways for accessing systems qualities, sharing architectural knowledge, and preventing software systems decay (GARLAN; [START_REF] Garlan | An Introduction to Software Architecture[END_REF][START_REF] Clements | A survey of architecture description languages[END_REF][START_REF] Clements | Documenting Software Architectures: Views and Beyond[END_REF][START_REF] Kruchten | Documentation of Software Architecture from a Knowledge Management Perspective -Design Representation[END_REF]ISO/IEC/IEEE 42010, 2011). To disseminate best practices regarding the content of such artifacts, the ISO/IEC/IEEE-42010 (2011) standard establishes the main elements framed in architecture descriptions and the relationships that exist among them. Still, the content of architecture descriptions can be tailored for each project, thus requiring specific guidelines for a particular domain or stakeholder community.

This chapter discusses software architectures in light of challenges that are faced when architecting Systems-of-Systems (SoS). First, Section 2.1 presents definitions for the main concepts of software architectures and, in particular, architecture descriptions. This section also details the use of formal methods and model-based practices for the design and analysis of software systems. Then, Section 2.2 introduces a generic process for the architectural design of software systems and discusses new requirements for architecting SoS. Section 2.3 introduces notations for expressing software architectures. Section 2.4 addresses a number of viewpoints that have been adopted in architectural descriptions. Section 2.5 introduces architecture decisions as a means to document architectural knowledge and discusses the main challenges for maintaining SoS. Finally, Section 2.6 summarizes the main gaps regarding architectural descriptions for SoS and how this thesis is expected to advance the state of the art.

Basic Concepts

Throughout software systems life cycle, software architectures can play different roles, such as (BABAR, 2009): (i) a communication vehicle among stakeholders during analysis and development of software systems; (ii) a repository of architecture decisions which impact subsequent development stages; and (iii) an abstraction of software systems which can be read and examined by people and constitutes the basis for supporting reuse. Accordingly, several definitions can be found for software architectures in the literature based on these different roles. For instance, [START_REF] Jansen | Software Architecture as a Set of Architectural Design Decisions[END_REF] define software architectures as the set of architecture decisions that shape software systems and that have greater influence to the quality of software systems. To facilitate the understanding of the following chapters, definitions for the main concepts related to software architectures are presented in this section.

Concrete software architecture: is a descriptive model that identifies the main elements or properties of a system which are embodied in its systems, relationships, and in the principles governing its design and evolution over time (GARLAN;[START_REF] Garlan | An Introduction to Software Architecture[END_REF][START_REF] Kruchten | Documentation of Software Architecture from a Knowledge Management Perspective -Design Representation[END_REF]OBBINK;[START_REF] Kruchten | The past, present, and future for software architecture[END_REF]; ISO/IEC/IEEE 42010, 2011; BASS; CLEMENTS; KAZ-MAN, 2012). It can also be referred to as run-time architecture. This artifact is further explained in Section 3.3.

Abstract software architecture: is a normative model of the main types of elements, relationships, and principles governing the design and evolution of a software system over time. It can also be referred to as design-time architecture, intentional architecture (OQUENDO, 2016e), or conceptual architecture [START_REF] Nielsen | Systems of Systems Engineering: Basic Concepts, Model-Based Techniques, and Research Directions[END_REF]. This artifact is further explained in Section 3.3.

Stakeholder: refers to any individual, team, or organization playing a relevant role in the software architecture process (ISO/IEC/IEEE 42010, 2011;[START_REF] Rozanski | Software Systems Architecture: Working with stakeholders using viewpoints and perspectives[END_REF][START_REF] Rozanski | Software Systems Architecture: Working with stakeholders using viewpoints and perspectives[END_REF]. Examples of stakeholders are clients, users, project managers, developers, and suppliers.

Concern: is any interest or need of one or more stakeholders about the software system (ISO/-IEC/ IEEE 42010, 2011;[START_REF] Rozanski | Software Systems Architecture: Working with stakeholders using viewpoints and perspectives[END_REF][START_REF] Rozanski | Software Systems Architecture: Working with stakeholders using viewpoints and perspectives[END_REF]. For example, concerns can be features, requirements, functionality, or qualities of the software system.

Architecturally Significant Requirement (ASR): is a quality attribute, also referred to as nonfunctional requirement. For instance, an ASR can specify a core feature of the system, a constraint to elements of the system, or a detail of the application environment [START_REF] Chen | Characterizing Architecturally Significant Requirements[END_REF][START_REF] Babar | Supporting the Software Architecture Process with Knowledge Management[END_REF][START_REF] Chen | Characterizing Architecturally Significant Requirements[END_REF]. In particular, an ASR is related to one or more components or to the system as a whole whereas requirements that are not architecturally significant are restricted to single components (OBBINK et al., 2002). The significance of a requirement can be determined in terms of time, resources, reputation, or cost, so that an [START_REF] Chen | Characterizing Architecturally Significant Requirements[END_REF][START_REF] Babar | Supporting the Software Architecture Process with Knowledge Management[END_REF][START_REF] Chen | Characterizing Architecturally Significant Requirements[END_REF]. Thereby, a requirement is architecturally significant if its impact to the architecture can be measured [START_REF] Chen | Characterizing Architecturally Significant Requirements[END_REF][START_REF] Babar | Supporting the Software Architecture Process with Knowledge Management[END_REF][START_REF] Chen | Characterizing Architecturally Significant Requirements[END_REF].

Architecture pattern: addresses a particular recurring design problem that arises in specific design situations, and presents a well-proven generic scheme for its solution [START_REF] Buschmann | Patternoriented Software Architecture: A System of Patterns[END_REF]. This solution scheme encompasses a set of predefined subsystems, their responsibilities and relationships, and the rules and guidelines for organizing these relationships between them. Moreover, architectural patterns can be used as templates for concrete software architectures.

Architecture style: is a set of common restrictions to the form and structure of software architectures (GARLAN; [START_REF] Garlan | Introduction to the special issue on software architecture[END_REF]BASS;[START_REF] Clements | A survey of architecture description languages[END_REF][START_REF] Bass | Software Architecture in Practice[END_REF].

Architecture decision: refers to a design decision that affects the software architecture as a whole (GARLAN;[START_REF] Garlan | An Introduction to Software Architecture[END_REF]. For example, a design decision may require the addition or modification of architecture description elements.

System and System-of-Systems

Systems, as defined by the ISO/IEC/IEEE 15288 (2015) standard, are man-made systems encompassing hardware, software, data, humans, processes, materials, and others. A softwareintensive systems can be distinguished as a system in which software plays a central role in its design, development, deployment, and evolution (ISO/IEC/IEEE 42010, 2011). In this sense, the term system can be used to designate individual applications, subsystems, systems-of-systems, product lines, product families, whole enterprises, among others. Nonetheless, [START_REF] Boardman | System of Systems -the meaning of of[END_REF] discuss five particular dimensions that make SoS intrinsically different from systems, namely: autonomy, belonging, connectivity, diversity, and emergence. First, constituent systems, and the SoS itself, are not merely parts in that they retain their autonomy for pursuing their own purposes. Indeed, by exercising their autonomy, constituents can voluntarily decide whether to belong to the SoS, which is out of the control of the SoS architect. Since constituents are geographically distributed, they can only exchange information with each other. To effectively belong to an SoS, new means are needed for dynamically determining constituents connectivity, i.e., deploying custom communication links on demand. Finally, diversity of constituents provides SoS with rich, dynamic capabilities obtained from independent constituent systems, which have limited functionality by design. Finally, the combination of autonomy, belonging, dynamic connectivity, and diversity allows the emergence of behaviors which enable to fulfill the SoS mission. These dimensions are also discussed by [START_REF] Gonçalves | Towards a Conceptual Model for Software-Intensive System-of-Systems[END_REF], who adds software dominance of constituents as a particular characteristic of software-intensive SoS.

The design of SoS must address the complexity that is added by combining several independent constituent systems, thus requiring tailored processes and techniques, such as for acquisition of constituent systems [START_REF] Boehm | Spiral Acquisition of Software-Intensive Systems-of-Systems[END_REF][START_REF] Gagliardi | System of Systems (SoS) Architecture Centric Acquisition[END_REF][START_REF] Gagliardi | System of Systems (SoS) Architecture Centric Acquisition[END_REF][START_REF] Gagliardi | System of Systems (SoS) Architecture Centric Acquisition[END_REF] and evolution of software architectures (SELBERG; [START_REF] Selberg | Toward an Evolutionary System of Systems Architecture[END_REF]. The evolution must be addressed by SoS software architectures, which must frequently change in unpredictable ways at run-time due to autonomy and diversity of constituent systems (VALERDI; ROSS; [START_REF] Valerdi | A Framework for Evolving System of Systems Engineering[END_REF][START_REF] Selberg | Toward an Evolutionary System of Systems Architecture[END_REF][START_REF] Selberg | Toward an Evolutionary System of Systems Architecture[END_REF]OQUENDO, 2016e). Thus, SoS architectures must address possible changes to constituents' functionality, performance, or interfaces by defining a persistent technical framework that describes how constituents collaborate with each other (DAHMANN et al., 2011a). Since constituents are often out of the control of SoS architects, software architectures can solely focus on those key constituent systems and connectors that are needed for achieving its desired capability, fostering interoperability among them by documenting protocols used for data communication and/or synchronization across constituents (DAHMANN et al., 2011a). In this scenario, the key research challenges raised by SoS are architectural, i.e., they concern how local interactions among constituents can be organized so that global, desired behaviors will emerge (OQUENDO, 2016e).

Architecture Description

As the main artifact expressing software architectures, architecture descriptions offer support to the communication, evaluation, and evolution of software systems (GARLAN; [START_REF] Garlan | An Introduction to Software Architecture[END_REF][START_REF] Clements | A survey of architecture description languages[END_REF][START_REF] Clements | Documenting Software Architectures: Views and Beyond[END_REF][START_REF] Kruchten | Documentation of Software Architecture from a Knowledge Management Perspective -Design Representation[END_REF]MENS;MAGEE;RUMPE, 2010;ISO/IEC/IEEE 42010, 2011). The architecture description of a given software system can present one or more architecture models that depict its main parts and the relationships existing among these parts. By documenting the architecture rationale, the architecture description can support the education of future maintainers of the software architecture, thus providing valuable guidance for evolution of software systems [START_REF] Kruchten | Documentation of Software Architecture from a Knowledge Management Perspective -Design Representation[END_REF]OBBINK;[START_REF] Kruchten | The past, present, and future for software architecture[END_REF]. To effectively use architecture descriptions at different stages of software systems life cycle, the ISO/IEC/IEEE 42010 (2011) standard was introduced. This standard, which replaces the ANSI/IEEE 1471-2000 standard, "addresses the creation, analysis, and sustainment of architectures of software-intensive systems through the use of architecture descriptions" (ISO/IEC/IEEE 42010, 2011). Figure 1 Correspondence Rule: it enforces a particular relationship between architecture description elements. A correspondence rule holds if it is possible to show an associated correspondence satisfying the rule whereas it is violated if it is possible to show an associated correspondence that does not satisfy the rule or if no associated correspondence exists.

Architecture descriptions identify the stakeholders of a software system and build architectural views for framing their concerns. Several architectural models can be created for describing each of these views. Combined, the set of views forms a cohesive, complete description of the software architecture. Then, correspondences can be established among architectural elements for capturing relations (e.g., refinement, constraint, dependency) that are enforced for ensuring the consistency among independent artifacts. Moreover, any known inconsistencies must be recorded so that they can be properly addressed. The architecture rationale is also an important part of the description since it provides the context for understanding views and documents considered alternatives and decisions that shaped the software architecture.

The ISO/IEC/IEEE 42010 (2011) standard also clarifies the requirements of complex elements, such as architecture frameworks, architecture styles, and Architecture Description Languages (ADLs), that can be created on top of these primitive constructs. According to the standard, an architecture framework establishes a common practice for creating, interpreting, analyzing, and using architecture descriptions for a particular domain or stakeholder community and it can be characterized by viewpoints, model kinds, stakeholders, and concerns that it selects for creating architecture descriptions. In turn, an architecture style can be considered as an architecture model in terms of this standard as it selects model kinds and concerns that are characteristic of a particular class of software architectures. Finally, an ADL, which is defined as any form of expression used in architecture descriptions, can be characterized in terms of selected model kinds, concerns, stakeholders, and correspondence rules.

Formal Methods

A formal method is traditionally defined as a mathematical technique employed in the development of software and hardware systems, including methods for specification, execution, proof, model checking, refinement, and test generation (WOODCOCK et al., 2009). Any method based on discrete symbolic systems that enables precise specification and analysis can be perceived as a formal method, encompassing formal notations (such as UML state diagram or xUML (Executable UML) (MELLOR; [START_REF] Mellor | Executable UML[END_REF] and Domain Specific Modeling Languages (DSL) besides formal logics [START_REF] Jaspan | Software Mythbusters Explore Formal Methods[END_REF]. While the impact of formal methods on time and cost is undetermined 1 , the impact of these methods on quality is widely acknowledged (WOODCOCK et al., 2009). In particular for safety and security critical systems, precision and rigor achieved with formal methods seem to be unavoidable for obtaining higher 1 Practitioners interviewed in a survey by Woodcock et al. (2009) regarded formal methods as more beneficial than harmful to time and cost although no quantitative evidence was available to confirm their perception.

reliability 2 (MANDRIOLI, 2015). The use of formal methods has also been linked to increased productivity (by supporting automated generation of source code) and decreased maintenance (by correcting subtle errors early in the development and improving designers understanding) (WOODCOCK et al., 2009).

Aiming to counter-balance costs associated with the introduction of new technologies in the development of software systems, formal methods can be employed with different levels of intensity, focusing on a limited part of the system or step of the design process (WOODCOCK et al., 2009;[START_REF] Jaspan | Software Mythbusters Explore Formal Methods[END_REF]. One can use formal methods for pointing out generic errors, e.g. using statistical analysis to detect trends in code that could be related to anomalies. Formal methods can also be used for checking assertions at run-time (CLARKE; [START_REF] Clarke | A historical perspective on runtime assertion checking in software development[END_REF]. In this scenario, lightweight formal methods emerge as a way to partially employ formal methods in the design of software systems (WOODCOCK et al., 2009). Jones (BOWEN et al., 1996, p. 20-21) advocates in favor of the use of formal methods early on a project's life cycle for producing formal documents that can later be inspected and, if needed, performing formal proofs for steps of (portions of) a system. In turn, Jackson and Wing (BOWEN et al., 1996, p. 21-22) suggest partial application of formal methods for reducing costs. For instance, Alloy (JACKSON, 2012) is a lightweight formal method supporting the adoption of model checking to a limited analysis scope. Advances in SAT solvers have enabled to apply the method for solving partial instances (TORLAK; DENNIS, 2006) and higher-order problems (which contain ∃and∀ quantifiers) [START_REF] Milicevic | A semantic mediation framework for architecting federated ubiquitous systems[END_REF].

Constraint Programming (CP) aims at solving problems, e.g. as graph colouring, nqueens, and time scheduling, that can be expressed in terms of constraints [START_REF] Petke | Bridging Constraint Satisfaction and Boolean Satisfiability[END_REF]. In parallel, constraint satisfaction is a branch of artificial intelligence concerned with finding an assignment of variables that satisfy a Boolean formula [START_REF] Petke | Bridging Constraint Satisfaction and Boolean Satisfiability[END_REF]. Let ϕ(x 1 , . . . , x n ) be a Boolean formula. Variables x 1 , . . ., x n are arranged within several clauses using the logical operators depicted in Table 1 and each of these variables can be assigned a value of 0 (False) or 1 (True). The formula is satisfied if all clauses are satisfied and unsatisfied if at least one clause is unsatisfied after all variables have been assigned. Optionally, it is also possible to express all Boolean formulas in their equivalent Conjunctive Normal Form (CNF), i.e., as a conjunction of clauses that are a disjunction of variables, such as

ϕ(x 1 , x 2 , x 3 ) = ( x1 ∨ x 3 ) ∧ (x 2 ∨ x 3 ) ∧ ( x2 ∨ x 3 )
for variables x 1 , x 2 , and x 3 . In this form, a clause is satisfied if at least one variable is True and unsatisfied if all variables are False. Thereby, only one clause needs to be unsatisfied to render the entire formula unsatisfied. The ISO/IEC 25010:2011 (2011) standard defines reliability as "the degree to which the software product can maintain a specified level of performance when used under specified conditions." Sub-characteristics of reliability are availability, fault tolerance, recoverability, and reliability compliance. The problem of determining if there is any assignment to the Boolean variables that satisfies the formula or proving that such an assignment does not exist is also referred to as Satisfiability Problem (SAT), which is the first known NP-complete problem [START_REF] Cook | The Complexity of Theorem Proving Procedures[END_REF]. Thereby, all known algorithms for this problem face state space explosion issue as the number of variables exponentially increases in the worst-case scenario. Nonetheless, improvements on algorithms and technologies have increased the efficiency of SAT-solvers. These algorithms can be distinguished between: (i) incomplete algorithms (e.g., local search, genetic algorithms) which either prove a formula unsatisfiable or satisfiable, or (ii) complete algorithms (e.g., resolution, recursive learning, conflict-driven clause learning) which prove a formula to be both unsatisfiable and satisfiable.

In this scenario, advances in tools and algorithms have contributed for better understanding and employing formal methods in practice, such as model checking, software verification, and artificial intelligence (WOODCOCK et al., 2009;[START_REF] Jaspan | Software Mythbusters Explore Formal Methods[END_REF]. Constraint solving has been applied in Search-Based Software Engineering (SBSE) for the definition of a search problem that investigates optimal or near optimal solutions by using a fitness function that distinguishes between better and worse solutions (HARMAN; MANSOURI; ZHANG, 2012). Model checking has also been applied to software architectures in the execution of an exhaustive and automatic verification that confirms the presence of desired properties, such as safety 3 , liveness 4 , and compatibility 5 (ZHANG; MUCCINI; LI, 2010). In this scenario, formal languages supporting the specification of software systems, including ADLs, enable to create executable and unambiguous models that play an important role in guaranteeing the correctness and soundness of software systems, often supporting code generation. In turn, support for code generation from formal specifications can have a positive impact in productivity provided that sufficient tools are available (WOODCOCK et al., 2009).

Architecting Software Systems

The ISO/IEC/IEEE 42010 (2011) standard defines architecting as the "process of conceiving, defining, expressing, documenting, communicating, certifying proper implementation of, maintaining and improving an architecture throughout systems' life cycle". There are many ways 3 Safety properties verify whether a specific event never occurs (ZHANG; MUCCINI; LI, 2010). Liveness properties verify whether a specific event eventually occurs (ZHANG; MUCCINI; LI, 2010). in which software architectures can be created. For instance, traditional software development processes, such as the Rational Unified Process (RUP) [START_REF] Kruchten | Documentation of Software Architecture from a Knowledge Management Perspective -Design Representation[END_REF] that encompasses inception, elaboration, construction, and transition phases, the architecture is built iteratively during the elaboration phase, resulting in executable architectural prototypes that can be used for validating the architectural design. Even agile methods, such as Scrum (SCHWABER; BEEDLE, 2001), that favor speed at the expense of having a consolidated design upfront, software architectures support scaling up agile practices to larger system scope, team size, and projects length, as well as minimizing the risk of unpredictable issues by employing smaller incremental steps and engaging stakeholders in the development process (NORD;OZKAYA;[START_REF] Nord | Agile in Distress: Architecture to the Rescue[END_REF]. Indeed, the combination of architecture and agile practices, such as incremental development, design patterns, frequent architecture analysis and improvement, and prototyping, results in a development process that guarantees agility and sustainability for continuous software delivery (KOONTZ; NORD, 2012). [START_REF] Hofmeister | A general model of software architecture design from five industrial approaches[END_REF] propose a general model of architectural design activities depicted in Figure 2. In this model, the process of realizing a suitable software architecture encompasses analyzing the problem that it must solve, synthesizing potential solutions for that problem, and evaluating alternative solutions until reaching a satisfiable design. The architectural analysis uses the context (i.e., environment) and architectural concerns to formulate the set of Architecturally Significant Requirements (ASRs) in terms of desired systems properties that must be fulfilled by the architecture. As distinguishing characteristic, an ASR is related to one or more components or the system as a whole whereas requirements that are not architecturally significant are restricted to single components (OBBINK et al., 2002). The architectural synthesis builds upon these ASRs to outline potential solutions satisfying these requirements. Then, the architectural evaluation validates or invalidates these candidate solutions against ASRs until one of them is chosen as the validated architecture. Each of these activities can be repeated until a validated architecture is obtained.

Architecting Systems-of-Systems

The software architecture of an SoS encompasses the structure of constituent systems, the relationships that exist among them, and the principles and guidelines governing its design and evolution over time [START_REF] Gagliardi | System of Systems (SoS) Architecture Centric Acquisition[END_REF][START_REF] Gagliardi | System of Systems (SoS) Architecture Centric Acquisition[END_REF][START_REF] Gagliardi | System of Systems (SoS) Architecture Centric Acquisition[END_REF]. Descriptions of SoS architectures detail functionality performed by key constituent systems, data and control flow, externally visible properties and interfaces of constituents (e.g., behaviors, dependencies, and use of shared resources), relationships among organizational entities and constituents as well as rationale and governance policies that apply to the SoS, including for instance guidelines for acquisition, termination, and replacement of constituents (GAGLIARDI; BERGEY; WOOD, 2010).

As SoS architectures establish a baseline for developing constituents and shared infrastructure and distributing work, they are key artifacts of SoS engineering processes (DAHMANN et al., 2011a). The process defined by the Office of the Deputy Under Secretary of Defense for Acquisition and Technology, Systems and Software Engineering (2008) identifies seven key activities for engineering SoS: (i) translating capability objectives; (ii) understanding systems; (iii) assessing requirements and solution options; (iv) monitoring change; (v) developing and evolving SoS architectures; (vi) assessing performance; and (vii) orchestrating upgrades. By rearranging these activities in a timeline, Dahmann et al. (2011b) show that this process can be viewed as a wave model (shown in Figure 3), where "Initiate SoS" encompasses activities (i) and (ii), "Conduct SoS Analysis" encompasses activities (i) to (iv), "Develop SoS Architecture" corresponds to activity (v), "Plan SoS Update" corresponds to activity (vi), and "Implement SoS Update" corresponds to activity (vii). In this timeline, normal process flows are depicted by arrows, which optionally have embedded circles indicating that back-and-forth iterations between activities are possible. This workflow highlights some inherent characteristics of SoS, such as: SoS are incrementally developed by evolution iterations; SoS are continuously analyzed against changing contexts and requirements; the development of SoS is constantly receiving inputs from the external environment; the SoS architecture is incrementally developed and can evolve between iterations; external events determine the speed with which new iterations are needed but every iteration delivers a working SoS.

Aiming to support the development of SoS, [START_REF] Maier | Architecting principles for systems-of-systems[END_REF] defines four main architecting principles: (i) stable intermediate forms: "complex systems will develop and evolve within an overall architecture much more rapidly if there are stable intermediate forms than if there are not"; (ii) policy triage: "the triage: Let the dying die. Ignore those who will recover on their own. And treat only those who would die without help"; (iii) interface design: "the greatest leverage in system architecting is at the interfaces. The greatest dangers are also at the interfaces"; (iv) ensuring cooperation: "if a system requires voluntary collaboration, the mechanism and incentives for that collaboration must be designed in. [START_REF] Hollon | The US Ballistic Missile Defense System: A case study in architecting systems-of-systems[END_REF] apply these principles for developing the ballistic missile defense system, which combines several legacy systems, focusing in particular to the interface design that enabled the collaboration among constituents.

According to this fourth principle, SoS architects must design efficient ways for constituents to collaborate with each other [START_REF] Boardman | System of Systems -the meaning of of[END_REF][START_REF] Boardman | System of Systems -the meaning of of[END_REF]. Thus, on top of challenges related to scope, complexity, and distribution, the design of SoS is complicated by enabling connectivity among autonomous constituent systems. For instance, mature constituent systems can resist to make changes for interacting with the SoS (Office of the Deputy Under Secretary of Defense for Acquisition and Technology, Systems and Software Engineering, 2008). In this case, SoS architects can use a gateway or encapsulate the constituent system so that required changes to the actual constituents are minimized. Moreover, architecture styles can be used to foster connectivity among constituent systems, such as net-centric architectures, layered architectures, and agent-based architectures (DAGLI; [START_REF] Dagli | System of systems architecting[END_REF]KOONTZ;NORD, 2012). In particular, Loiret et al. (2011) establish a reference model for developing Component-Based Systems of Systems (CBSoS) in which a front-end component is responsible for loading and checking heterogeneous descriptors used for specifying the CBSoS and instantiating the appropriate models. This approach is particularly interesting for SoS since it is not bound to a specific ADL or implementation language.

Model-driven Development

Models increase the abstraction level with which one can reason about complex systems. Different kinds of abstraction levels can be employed for creating such models, thus determining their purpose and the types of supported analysis [START_REF] Kramer | Is abstraction the key to computing[END_REF]. Models can be useful when designing, maintaining, and evolving software systems since each one of these models focus on a particular aspect of the software system, e.g., structure, behavior, workflow, platform, among others. These models can be either static, in which time does not play a role in the model (e.g., data, topology, or logic), or dynamic, in which time plays a key role (e.g., interactions, events, or state) (BRAMBILLA; CABOT; WIMMER, 2012). In this scenario, source code is the ultimate model of a software system, which can be expressed in programming languages such as C, Java, or Python, and depicts the systems' behavior when executed (FRANCE;[START_REF] France | Model-driven Development of Complex Software: A Research Roadmap[END_REF]. Modern software engineering practices are increasingly relying on different types of models to gain confidence on the design and quality of software systems. These models can be classified between (FRANCE; RUMPE, 2007): (i) development models that represent the software system at a higher abstraction level than source code (e.g., requirements, architectural, implementation, and deployment models), and (ii) run-time models that represent the executing software system.

In Model-Driven Development (MDD) processes, models are first class entities that represent software systems at different abstraction levels. Models can be expressed in Domain Specific Modeling Languages (DSML), which are either graphic or textual notations providing tailored abstractions for concepts of the problem domain (ROYER; ARBOLEDA, 2012). The definition of a DSML encompasses: a concrete syntax, which defines the notation for creating models; an abstract syntax, which defines the vocabulary of domain concepts, e.g., elements supported by the language, relationships between them, and constraints for creating valid models; mappings between abstract and concrete syntax, e.g., stereotypes in classes of a UML Class Diagram that refer to concepts defined by the abstract syntax; and a semantic domain, which specifies how to create well-formed models using domain concepts (ROYER; [START_REF] Royer | Model-Driven Engineering[END_REF]. A model can also be used to define the abstract syntax, thus defining a metamodel for this DSML.

Model transformations are software artifacts that specify an algorithm for obtaining one model from another (ROYER; ARBOLEDA, 2012). Transformations are a key activity of MDD processes as they successively create models for representing software systems at different abstraction layers, thus helping to bridge the gap between problem and solution domains (FRANCE;[START_REF] France | Model-driven Development of Complex Software: A Research Roadmap[END_REF]. Figure 4 illustrates a generic model transformation scenario between one source model and one target model. The model transformation, which is defined at the metamodel level of the source and target models, is composed of several transformation rules, which are functions or procedures implementing a transformation step (ROYER; ARBOLEDA, 2012). An engine can automatically execute these steps for obtaining the target model from the source model. Operational transformations, such as model refinement, abstraction, refactoring, composition, decomposition, and translation, receive the source set of models and produce the target set of models, e.g., a transformation of UML models into Alloy (FRANCE;[START_REF] France | Model-driven Development of Complex Software: A Research Roadmap[END_REF]. Alternatively, synchronization transformations are used for updating the target set of models with changes made to the source set of models (FRANCE;[START_REF] France | Model-driven Development of Complex Software: A Research Roadmap[END_REF].

According to [START_REF] Czarnecki | Feature-based survey of model transformation approaches[END_REF], model transformations can be classified as Model-to-Model (M2M), which transform source models into target models, or as Model-to-Text (M2T), which transform models into source code. [START_REF] Royer | Model-Driven Engineering[END_REF] also classify transformations as Text-to-Model (T2M), which can extract models from source code, thus enabling reverse engineering processes. Alternatively, [START_REF] France | Multi-view software evolution: a UML-based framework for evolving object-oriented software[END_REF] transformations as vertical, which are defined between models at different abstraction levels, or horizontal, which are defined between models at the same abstraction level. Vertical transformations can be further distinguished by direction as refinement (i.e., by decreasing the abstraction level) or abstraction (i.e., by increasing the abstraction level) whereas horizontal transformations can be further classified by purpose as migration (i.e., transforming models conforming to one metamodel into another), merge (i.e., unifying separate models), or identification (i.e., selecting specific elements of the source model).

classify model

The development of software systems based on models gains popularity with the maturity of modeling tools and languages. For instance, modern generation tools can use models to automatically generate executable source code, thus reducing development time and effort. The semantic consistency between models at different abstraction layers is enforced in MDD processes by the correct-by-construction philosophy [START_REF] Balasubramanian | Developing applications using model-driven design environments[END_REF]. By employing formal languages in the description of source and target models, it is possible to implement change requests as model refinements, thus enabling consistent updates and modifications to the model [START_REF] Broy | Seamless Method-and Model-based Software and Systems Engineering[END_REF].

Several variations exist for MDD, with some particularities to each of them (BRAM-BILLA; CABOT; WIMMER, 2012): Model-Driven Architecture (MDA) is a branch of MDD based on Object Management Group (OMG) standards. Among other OMG standards, it relies on the Meta Object Facility (MOF) 6 to define the abstract syntax of modeling languages and UML to represent models; Model-Driven Engineering (MDE) applies MDD to the whole spectrum of activities encompassed in software engineering processes, such as evolution, maintenance, and retirement. In this sense, MDE defines approaches that create and systematically transform abstract models of software systems into concrete implementations, i.e., executable source code (FRANCE;[START_REF] France | Model-driven Development of Complex Software: A Research Roadmap[END_REF].

In the context of SoS, model-driven processes can take advantage of executable models, which provide valuable information for the analysis and construction of SoS architectures (DAGLI; [START_REF] Dagli | System of systems architecting[END_REF]. [START_REF] Graciano | Investigating the Model-Driven Development for Systems-of-Systems[END_REF] 7 investigate MDD practices in the context of SoS and report on a range of approaches that have been using models for documenting the software architecture, generating source code, testing, and representing requirements. Models that have been created in this domain use semi-formal notations, such as UML and SysML, as well as formal notations, such as Object-Constraint Language (OCL), Discrete Event System Specification (DEVS), and Architecture Analysis and Design Language (AADL). Among tools supporting these approaches, the authors identified open-source initiatives, e.g., extensions to the Eclipse Modeling Framework (EMF) 8 that automate model transformations and code generation, as well as proprietary tools, e.g., MATLab 9 . Nonetheless, the authors identified few approaches exploring MDD for modeling and generating source code for SoS.

Architecture Description Languages

The definition of a language encompasses three core elements (BRAMBILLA; CABOT; WIMMER, 2012): (i) abstract syntax, which can be defined in terms of a grammar (for textual languages) or metamodel (for modeling languages), for creating syntactically correct structures; (ii) concrete syntax, which defines the representation (encoding) of structures in terms of textual and graphical notations; and (iii) semantics, which convey the meaning of created structures. Originally, ADLs were mainly regarded as formal notations that were similar to programming languages but offered higher level constructs (such as platforms, systems, components, and connectors) for expressing software architectures (SHAW; [START_REF] Shaw | Characteristics of Higher-Level Languages for Software Architecture[END_REF][START_REF] Clements | A survey of architecture description languages[END_REF][START_REF] Medvidovic | A classification and comparison framework for software architecture description languages[END_REF][START_REF] Medvidovic | A classification and comparison framework for software architecture description languages[END_REF]. By using these constructs, an ADL would facilitate expressing the creation, refinement, and validation of software systems' elements at the software architecture abstraction level [START_REF] Clements | A survey of architecture description languages[END_REF]. Nonetheless, the ISO/IEC/IEEE 42010 (2011) standard broadened this definition by classifying "any form of expression used in architecture descriptions" as an ADL. [START_REF] Shaw | Characteristics of Higher-Level Languages for Software Architecture[END_REF] describe several desired features of notations for expressing software systems at their software architecture abstraction level. For instance, an ADL must support software systems description in terms of compositions of independent architectural components, which can be packaged as styles, patterns, and correspondences and thus can be reused in different contexts. As several models can be created for describing software architectures at different abstraction levels, an ADL must support a consistent translation among them. Moreover, an ADL must support different kinds of analysis over architecture descriptions, thus enabling its use at different stages of development (e.g., design, validation, or evolution). Since then, additional features have been elicited. For instance, while deemed not mandatory, tool support is increasingly desired for an automated analysis of architecture descriptions [START_REF] Clements | A survey of architecture description languages[END_REF][START_REF] Medvidovic | A classification and comparison framework for software architecture description languages[END_REF][START_REF] Medvidovic | A classification and comparison framework for software architecture description languages[END_REF][START_REF] Lago | The road ahead for architectural languages[END_REF]. An ADL must also support expressing different structures (or topologies) in which a particular concern is framed, such as understandability, compositionality, refinement, heterogeneity, scalability, and dynamism (MEDVIDOVIC;[START_REF] Medvidovic | A classification and comparison framework for software architecture description languages[END_REF]. Another desired feature concerns the description 8 EMF, <http://www.eclipse.org/modeling/emf/> 9 MATLab, <https://www.mathworks.com/> of multiple viewpoints (HILLIARD;[START_REF] Hilliard | Expressiveness in Architecture Description Languages[END_REF]. Besides describing software architectures from a run-time viewpoint, i.e., in terms of how components and connectors are arranged together, modern ADLs are also required to describe software architectures from a dynamic viewpoint, i.e., in terms of how the architecture can evolve by means of adding, deleting, reconfiguring, or modifying elements at run-time based on data input, or mobile viewpoint, i.e., in terms of how the architecture can logically move during the execution of the system [START_REF] Oquendo | π-ADL: An Architecture Description Language based on the Higher Order Typed π-Calculus for Specifying Dynamic and Mobile Software Architectures[END_REF]. The description of complex systems can also be facilitated by providing assorted mechanisms for expressing quantification. For instance, first-order logic quantifiers ∀ (for all) and ∃ (exists/some) can be used for describing global properties, thus increasing the ADL expressiveness, whereas constraints can be added for quantifying relations or attributes in architectural models (HILLIARD;[START_REF] Hilliard | Expressiveness in Architecture Description Languages[END_REF].

While more than 100 10 languages can be regarded as ADLs, only a fraction of these are widely employed. Aiming to classify and compare different ADLs, [START_REF] Medvidovic | A classification and comparison framework for software architecture description languages[END_REF] define a framework of required and desired features for describing software architectures, such as support for expressing constraints and non-functional properties. In particular, they define components, connectors, and architecture configurations (i.e., topologies) as the high level building blocks that can be used for describing a software architecture: (i) components are units of computation that represent functional elements of a system; (ii) connectors represent the interconnections enabling the communication among components; and (iii) configurations specify the pattern and/or structure in which components and connectors are assembled. In light of the ISO/IEC/IEEE 42010 (2011) standard, ADLs can also be distinguished by underlying formalism, i.e., formal, semi-formal, and informal notations (BASS; CLEMENTS; [START_REF] Bass | Software Architecture in Practice[END_REF].

Formal notations have well-defined syntax and semantics, such as Rapide [START_REF] Luckham | A Language and Toolset for Simulation of Distributed Systems by Partial Orderings of Events[END_REF], Wright (ALLEN, 1997), and π-ADL [START_REF] Oquendo | π-ADL: An Architecture Description Language based on the Higher Order Typed π-Calculus for Specifying Dynamic and Mobile Software Architectures[END_REF]. For instance, π-ADL was created to support the dynamic nature of software architectures by focusing on the description of architectures from both structural and behavioral viewpoints and evolving these viewpoints together over time. Since π-ADL is based on the higher-order typed π-calculus [START_REF] Sangiorgi | Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms[END_REF], it is also Turing-complete. Solely, π-calculus is not suitable as an ADL since it does not provide architecture-centric constructs which would support the description of architectural structures [START_REF] Oquendo | π-ADL: An Architecture Description Language based on the Higher Order Typed π-Calculus for Specifying Dynamic and Mobile Software Architectures[END_REF]. The main advantage of using formal ADLs is the possibility of formally representing the software architecture. Moreover, formal architecture descriptions are also more likely to be maintained and followed than an informal one as it can be more readily consulted and treated as authoritative and it can be more easily transferred to other projects as a core asset [START_REF] Clements | A survey of architecture description languages[END_REF]. As formal models provide a rigorous, accurate, and unambiguous description of the software architecture (MEDVIDOVIC; [START_REF] Medvidovic | A classification and comparison framework for software architecture description languages[END_REF], they can also be used for verifying and validating the architecture against selected properties and 10 Index of current ADLs, <http://www.di.univaq.it/malavolta/al/> quality characteristics. As a result, formal descriptions offer an important resource in the making of architecture decisions [START_REF] Clements | A survey of architecture description languages[END_REF]. On the other hand, since formal languages can be difficult for non-technical stakeholders to understand, they require specialized tools and training.

Semi-formal notations have well-defined syntax but lack complete semantics, such as UML (Unified Modeling Language) (OMG, 2011), SysML (Systems Modeling Language) (OMG, 2012), and AADL (Architecture Analysis and Design Language) (SAE International, 2011). Firstly, UML is an Object Management Group (OMG) standard for specifying, visualizing, and documenting software systems. Improvements made since its version 2.0 have encouraged its use in architectural descriptions (IVERS et al., 2004;[START_REF] Lago | The road ahead for architectural languages[END_REF]. However, UML still lacks a first-order construct for connectors (OZKAYA; KLOUKINAS, 2013). Second, SysML was developed to fill in the semantic gap between systems, software, and other engineering disciplines. Also an OMG standard, SysML has been introduced as an evolution to UML and it reuses a subset of UML 2.0. For example, SysML introduces a Requirements Diagram that can express hierarchy among requirements, which guarantees traceability among them, and a Parametric Diagram that can describe constraints for system property values (e.g., performance, confidence, or weight), which can be useful for integrating specifications and models of the system into engineering analysis models. Finally, AADL describes architectures in terms of distinct components and their interactions aiming to support model-based analysis and specification of complex real-time embedded systems (FEILER; GLUCH; HUDAK, 2006).

Informal notations presented neither defined syntax or semantics for describing software architectures. Therefore, informal models are solely created to provide a high abstraction picture of the software architecture [START_REF] Clements | Documenting Software Architectures: Views and Beyond[END_REF]. For instance, several informal models can be drafted and later discarded during the design of software architectures. To be part of the architecture documentation, informal models must be accompanied by textual explanations that help to convey architects' intentions, thus hindering reuse and automated analysis of such descriptions [START_REF] Clements | Documenting Software Architectures: Views and Beyond[END_REF]. Another disadvantage of using informal notations concerns the lack of tool support, which makes models difficult to be kept up-to-date and prone to ambiguous interpretations [START_REF] Clements | A survey of architecture description languages[END_REF].

In this scenario, the selection of a semi-formal notation can be seen as a compromise between formal and informal notations as they combine the rigor of formal languages to the understandability of natural languages. However, semi-formal languages often favor higher understandability at the cost of lowered accuracy. For instance, semi-formal languages may conceal mismatches among architectural models that could be propagated to subsequent stages of the development life cycle (MENS; MAGEE; RUMPE, 2010). Thus, semi-formal languages are not adequate for describing software architectures of critical domains since they cannot enforce correctness and consistency of an architecture description (PERSEIL; PAUTET, 2010). Aiming to fill this gap, formal notations are being used in conjunction to semi-formal ones. For example, π-ADL provides an UML Profile for supporting UML as a concrete modeling notation. Thus, an Synthèse d'architectures logicielles pour systèmes-de-systèmes Milena Margarido 2017 UML modelling tool can be used for creating semi-formal models while still taking advantage of π-ADL formal foundations for verifying and modeling transformations [START_REF] Oquendo | π-ADL: An Architecture Description Language based on the Higher Order Typed π-Calculus for Specifying Dynamic and Mobile Software Architectures[END_REF]. On the other hand, semi-formal ADLs have also been enhanced with formal foundations. For example, DesyreML [START_REF] Ferrari | A SysML Profile for Heterogeneous Embedded System[END_REF] is a SySML profile for the formal description of heterogeneous embedded systems. [START_REF] Ozkaya | Are We There Yet? Analyzing Architecture Description Languages for Formal Analysis, Usability, and Realizability[END_REF] add to discussion on the evaluation of formal and semiformal notations by evaluating ADLs in respect to their formal semantics, usability (which is subdivided into easy-to-use formal behavioural specifications and support for user-defined, complex connectors), and realizability. In particular, their evaluation uses as criteria the availability of support for performing formal analysis on architecture models, level of usability of the notations for creating large and complex architectures, and level of protection against the creation of models that cannot be realized. In their study, realizability is a major issue in several formal notations, such as Wright and Rapide, as they allow the creation of invalid models.

To avoid the downside of selecting a single formalism, the research on ontology gains relevance in the Software Engineering area as a possible integrator for different notations and technologies (W3C, 2006). An ontology captures knowledge about some domain of interest for promoting a homogeneous understanding. Different notations can be used for expressing an ontology, ranging from precise, descriptive statements (i.e., informal ontology) to formal models (i.e., formal ontology) (W3C, 2012). A formal ontology, expressed in OWL, represents the domain of interest in terms of classes (which establish the requirements for membership to a class), individuals (which are instances of a class), and properties (which depict relationships among classes, individuals, or literals) [START_REF] Horridge | A Practical Guide To Building OWL Ontologies Using Protégé 4 and CO-ODE Tools[END_REF]. Then, such formal ontology can be automatically processed by computer programs that automatically verify its consistency (i.e., validate the ontology semantics) and infer implicit knowledge (e.g., compute implicit membership of individuals to classes).

Notations in Systems-of-Systems Description

The literature on SoS architecture description has been using varied notations for describing software architectures, including formal, semi-formal, and informal notations as well as combinations among these (GUESSI et al., 2015). Formal notations used or suggested for describing SoS software architecture comprise: COMPASS Modeling Language (CML) (WOODCOCK et al., 2012), Capability Focused Modeling Language (CFML) (IACOBUCCI; MAVRIS, 2011), Finite State Machine (FSM), Message Sequence Charts (MSC) assertions (COOK; DRUSINKSY; SHING, 2007), Petri-nets/colored Petri-nets, fuzzy models, Web Ontology Language (OWL) (W3C, 2012), Web Service Modeling Ontology (WSMO), Vienna Development Method (VDM) specification language [START_REF] Fitzgerald | Validated Designs For Object-oriented Systems[END_REF], and description logic. CML is specifically designed for SoS modeling and analysis. CFML is a declarative notation for describing and evaluating SoS architecture alternatives based on mission dependent metrics, such as probability of mission success and time to completion. MSC assertions is a formal language which extends the UML message sequence diagram by superimposing UML state-charts in which it is possible to distinguish among mandatory and optional events. Petri-nets and colored Petri-nets have been employed for generating executable SoS models. VDM is a formal specification language for defining interfaces and concrete system specifications.

There is an increasing concern for providing SoS stakeholders with a shared vocabulary, encoded as formal and informal ontology, that can promote interoperability and understandability. For example, Henrie and Delaney ( 2005) extend the definition of common terms used in traditional systems engineering to the SoS domain for establishing a terminology framework that could assist engineers in understanding, discussing, and designing complex systems. In turn, [START_REF] Nikolic | Framework for Understanding and Shaping Systems of Systems The case of industry and infrastructure development in seaport regions[END_REF] use OWL for creating a language that specifies the communication among the agents of an agent-based architecture. By requiring all agents to conform to this ontology, a high level modularity can be achieved. In the same perspective, Moschoglou et al. (2012) use WSMO, which provides a richer conceptual model and a formal language for semantically describing aspects of web services, publishing constituents' system capabilities, and enabling the automatic discovery, selection, and composition of web services at run-time.

Semi-formal notations have also been applied for describing SoS architectures, in particular: UML, SysML, and the Unified Profile for DoDAF and MoDAF (UPDM) [START_REF] Hause | The Unified Profile for DoDAF/MODAF (UPDM) enabling systems of systems on many levels[END_REF]. The first two languages are well-known OMG standards for the description of software systems. The latter is an UML profile supporting consistent, standardized descriptions of DoDAF (version 1.5) and MoDAF (version 1.2) architectures using UML-based tools as well as a standard for interchanging between these two frameworks. In spite of its popularity, there are concerns related to UML and SysML expressiveness for SoS architectures, as they may not be sufficient for unambiguously and precisely specifying interfaces. Moreover, semi-formal ADLs offer limited support for automatic analysis, which hampers their applicability in subsequent activities of SoS design.

The combination of formal and semi-formal notations has also been suggested for SoS architectural description. For example, [START_REF] Dagli | System of systems architecting[END_REF] suggest using of UML or SysML for modeling the SoS' static structure, such as user requirements and complex relationships between constituents, whereas Petri-nets or colored Petri-nets are used for building executable models of the SoS. [START_REF] Payne | Interface specification for system-ofsystems architectures[END_REF] combine SysML and VDM for specifying interfaces of constituent systems. Similarly, [START_REF] Bryans | Semi-formal and formal interface specification for system of systems architecture[END_REF] use SysML and CML for specifying interfaces of constituent systems. The model expressed in CML is a collection of process definitions, which encapsulates states and operations expressed in VDM and interact with the environment via synchronous communications. Thereby, formal interface descriptions enable event ordering specifications by means of pre-and post-conditions for operations.

Features of Architecture Description Languages for Systemsof-Systems

The particular nature of SoS, e.g., the independence of constituent systems, their evolutionary development, and emergent behavior, raises additional requirements for their adequate description. For instance, the ways in which constituents interact with each other determine the behaviors of the SoS. Thereby, SoS architecture descriptions should enable reasoning about how these interactions can be organized to enable SoS-wide behaviors to emerge (OQUENDO, 2016c). In this sense, architecture descriptions can help detecting and analyzing emergent behaviors so that undesired behaviors and risks can be mitigated as early as possible. However, there is no consensus on which notations can be adopted or which features are required for expressing SoS software architectures. As a consequence, in spite of the many ADLs that could be employed for expressing SoS software architectures, existing languages often lack the proper set of features for framing the particular concerns of SoS [START_REF] Batista | Challenges for SoS architecture description[END_REF]GUESSI;CAVALCANTE;OLIVEIRA, 2015;OQUENDO, 2016c). [START_REF] Nielsen | Systems of Systems Engineering: Basic Concepts, Model-Based Techniques, and Research Directions[END_REF] discuss some of the main concerns that must be framed by notations expressing SoS, including: (i) description of well-founded interfaces; (ii) description of autonomous behavior and capabilities and responsibilities of systems; (iii) description of rely/guarantee policies for independently modeling constituents; and (iv) description of desired or undesired behaviors that can be observed by means of model simulations. As SoS are continually evolving, notations must provide well-defined semantics, which will enable the analysis as well as extension of core elements of these notations for representing concerns that were not initially known at design time. Considering that the expressiveness of an ADL is improved by having specific constructs for describing the main aspects of the software architecture (HILLIARD; [START_REF] Hilliard | Expressiveness in Architecture Description Languages[END_REF], ADLs for SoS should respectively replace the notions of components, connectors, and configurations by the ones of constituents, mediators, and coalitions (GUESSI; CAVALCANTE; OLIVEIRA, 2015). Figure 5 illustrates features that have been included, tailored, or reused from [START_REF] Medvidovic | A classification and comparison framework for software architecture description languages[END_REF] framework of ADLs characteristics for expressing architectures of SoS.

Constituent is the abstraction for a complex entity, e.g., a system or another SoS, that may participate in the SoS. It can be partially specified at design time in terms of an abstract type, which characterizes the main aspects of a constituent system that it makes visible to other constituents and the SoS, so that at run-time concrete constituents complying with this specification can be attached to the SoS. As an independent entity, a constituent can have its own mission, which it may continue to fulfill in spite of its participation in the SoS. The semantics of a constituent is specified by a behavioral model, such as specific sequences over exchanged messages, that are visible at the SoS level.

Mediator is the abstraction for a complex communication channel that enables to exchange information among constituents. In particular, this abstraction is more complex than the one of connector since mediators accumulate different roles in the architecture (e.g., translating, storing, processing, and coordinating constituents actions). It can be partially specified at design time in terms of an abstract type, which details its tasks and commitments, so that it can be dynamically deployed at run-time as needed. In this sense, the existence of mediators is subjected to the control of the SoS. The semantics of this element clarifies the sequence in which messages will be exchanged and processed.

Coalition is the abstraction representing the configuration of constituents and mediators.

The coalition has a global mission, which can be fulfilled solely by the collaboration among its independent constituents. Because the coalition is continuously changing, it is difficult to explicitly determine at design time how constituents can be arranged together. Therefore, this new framework updates the feature of configuration type with the notion of an intentional description, which defines a normative model of coalitions that can be formed at run-time. To achieve this goal, it is essential that an ADL also supports expressing formal constraints, which can be automatically evaluated. As in traditional ADLs, the compositionality feature is related to the ability of representing coalitions at different abstraction levels (MEDVIDOVIC; [START_REF] Medvidovic | A classification and comparison framework for software architecture description languages[END_REF]. For instance, an entire SoS can be simultaneously viewed at a higher abstraction level as a black-box that only shows its main interfaces and external behavior and at a lower level as a network of constituents and mediators.

Tool support is also added to this set of features as it contributes for the usability and dissemination of ADLs. Thereby, this feature encompasses several mechanisms, such as syntax validators, customizable templates, and code generators that can make creating, debugging, and executing models a straightforward task. In regards to SoS software architectures, tailored tools should be able to support (GUESSI; CAVALCANTE; OLIVEIRA, 2015): (i) architecture-centric design, which ultimately obtain source code from consecutive model refinements; (ii) automated analysis for verifying, validating, and simulating SoS architecture descriptions; (iii) multi-view management for visualizing SoS architectures according to different viewpoints or abstraction levels; (iv) collaborative environment for sharing with geographically distributed teams; and (v) knowledge management for recording and tracking important design decisions.

Comparison between UML, SysML, and X-UNITY

Three ADLs that have been used for describing SoS architectures, namely UML, SysML, and X-UNITY, are evaluated in light of the features discussed in the previous section (GUESSI; CAVALCANTE; OLIVEIRA, 2015). The first two are well-known semi-formal notations whereas the latter is a formal language. SysML is evaluated in conjunction with CML, a formal language that complements the former with the ability to specify contracts. X-UNITY is a formal notation focused on the description of the interface of constituents and SoS. Despite the existence of several profiles to both UML and SysML, this evaluation is limited to the core concepts of these languages. Moreover, since none of these notations provide run-time support, this evaluation is restricted to the expressiveness of these ADLs at design time.

UML provides 14 diagram types in its 2.4.1 version. These diagrams are grouped under structural diagrams (e.g., class diagram, composite structure diagram, deployment diagram) and behavioral diagrams (e.g., timing diagram, sequence diagram, state machine diagram). From a static viewpoint, several UML constructs could be employed for realizing constituents, mediators, and coalitions, such as classes, packages, components, association classes, and composite structures. Table 2, for instance, lists some diagram types that can be employed for each of the features elicited for the description of SoS architectures. For the sake of simplicity, the class diagram can be used for expressing both constituents and mediators. Abstract types of constituents and mediators can be distinguished using stereotypes. In turn, a state machine diagram or sequence diagram can be attached to the specification of both constituents and mediators for detailing their semantics. Constraints on attributes, associations, and operations of constituents and mediators can be expressed in the Object Constraint Language (OCL) 11 . Evolution is currently not supported in UML because structural diagrams are static.

A coalition expressed in a composite structure diagram can explicitly specify constituents and mediators as parts. Ports and interfaces of the coalition can be internally relayed to any of its parts by means of associations. Moreover, bindings between constituents and mediators 11 Object Constraint Language (OCL), <http://www.omg.org/spec/OCL/2.4>. can be expressed as association links. The use of the same name for ports and interfaces is one way of implicitly defining bindings that may occur in a coalition but this feature requires compatible tools. Another downside of using this approach is that it does not support the definition of constraints, such as the ones that express valid bindings between constituents and mediators. A state machine diagram or sequence diagram can also be used to express the emergent behavior of the coalition in terms of the collaborations that take place among its constituents. Regarding compositionality, the class diagram and the composite structure diagram can support the description of SoS from different abstraction levels. The dynamism of a coalition is related to the capability of an SoS to rearrange its own structure. Since this is mainly a run-time feature, it is currently not possible to express it in UML. The description of missions and different levels of coercion is currently not supported. Extensions to core elements of the UML can be investigated to describe non-functional properties.

As UML is a well established standard for modeling software systems, several tools currently support it. For instance, Papyrus Modeling Tool 12 is an open-source graphical editing tool provided as an extension of Eclipse 13 . Papyrus does not support automated analysis, 12 Papyrus Modeling Tool, <http://www.eclipse.org/modeling/mdt/papyrus>. 13 Eclipse IDE, <http://www.eclipse.org>.

Synthèse d'architectures logicielles pour systèmes-de-systèmes Milena Margarido 2017 collaboration, and knowledge management. Even though this tool does not completely support architecture-centric design, it is important to mention that UML does. Therefore, despite the limitations observed in this tool, new features such as for syntax validation and code generation can be integrated due to facilities supported by the development environment. SysML defines nine diagram types which are grouped under behavior diagrams, structure diagrams, and a requirements diagram [START_REF] Friedenthal | A practical guide to SysML: The Systems Modeling Language[END_REF][START_REF] Friedenthal | A practical guide to SysML: The Systems Modeling Language[END_REF][START_REF] Friedenthal | A practical guide to SysML: The Systems Modeling Language[END_REF]. As a UML profile, SysML extends UML with: (i) a requirements diagram specifying textual requirements and their relationships to each other and to other models; (ii) a block construct defining system's structure and properties; (iii) an activity diagram that modifies the one available in UML to support continuous behavior; (iv) a constraint block construct defining constraints in terms of equations and their parameters; and (v) ports and information flows extending the UML structural model. Constituents and mediators can be individually represented in block definition diagrams and coalitions in internal block diagrams, which are a modification to UML's composite structure diagram. Therefore, a coalition can be expressed in terms of parts 14 and interconnections among them. The support for expressing constraints is improved in this notation since they can be captured in a separate parametric model, which promotes the separation of concerns in the architecture description, and then evaluated by custom analysis tools. The requirements diagram can be adapted represent missions and different levels of coercion. There are several tools supporting SysML, such as Papyrus.

CML is a textual language supporting SoS design. A CML model can be derived from SysML block definition or state machine diagrams, thus enabling to describe the combined semantics of constituent systems as synchronous events. This notation supports the definition of interface contracts for determining the collaboration among constituents. A contract expresses behavioral properties as well as specific policies and constraints that are necessary for coordinating constituents in an SoS. As a formal language, CML supports different types of analysis, such as model checking, testing, and simulation [START_REF] Coleman | COMPASS tool vision for a system of systems collaborative development environment[END_REF]. In particular, it enables to observe behaviors that emerge from constituents' interaction. Mediators can be described by channels that bind constituents together, which can further characterized by properties, constraints as well as behavioral protocols. There are also explicit mechanisms for expressing mobile channels and mobile processes. However, the intentional description feature is only partially supported since it is not possible to describe abstract mediator types. The level of coercion can be expressed in CML by specifying if an SoS may interfere in the actions performed by any given constituent. It is also possible to frame SoS dynamic behavior by expressing post-conditions (i.e., the SoS state after performing a given operation) for operations. The main tool supporting CML is Symphony 15 , an open-source tool based on Eclipse. Symphony collaborates with external proprietary tools for automatically generating CML models from SysML and automating 14 A part refers to a particular use of a block. It may present unique behaviors, properties, and constraints that only apply to its particular usage (FRIEDENTHAL; MOORE; STEINER, 2015). analysis.

X-UNITY is a textual language that addresses the description of interfaces of constituents and SoS. In particular, constituents in a X-UNITY description present internal variables (called context) and exposed variables that are visible to other constituents. Thereby, this language addresses the visibility and compatibility problems that can emerge among interfaces of constituents and SoS when they are attached to an existing coalition. However, there is no tool supporting this language. [START_REF] Guessi | Characterizing Architecture Description Languages for Software-Intensive Systems-of-Systems[END_REF].

ADL Feature UML SysML SysML + CML X-UNITY Constituent Abstract type • • • • Interface • • • ∘ Semantics • • • - Constraint ∘ • • • Mission - ∘ - - Evolution - - - - Non-functional property ∘ • • - Mediator Abstract type ∘ ∘ - - Interface • • - - Semantics • • • - Constraint ∘ • • - Evolution - - - - Non-functional property ∘ • • - Coalition Intentional description ∘ ∘ ∘ • Constraint - • • • Compositionality • • • • Evolutionary develop- ment - - ∘ - Coercion - - • ∘ Emergent behavior ∘ ∘ • - Mission - ∘ - - Dynamism - - • - Non-functional property ∘ • • - Tool Support Architecture-centric de- sign ∘ ∘ ∘ - Automated analysis - ∘ • - Multi-view management ∘ ∘ • - Collaborative environ- ment - - • - Knowledge management - - - - Source:
Key: • feature is supported, ∘ feature is partially supported, and -feature is not supported Table 3 summarizes features of the framework that are supported (i.e., the notation enables to frame the feature in the description), partially supported (i.e., the notation indirectly supports the feature), or not supported (i.e., it is currently not possible to frame this feature in the description) by these notations. This chart shows, for instance, that all four notations support a limited subset of the features that are required for expressing the software architecture of SoS (GUESSI; CAVALCANTE; OLIVEIRA, 2015). In particular, only X-UNITY supports an intentional description of the coalition even though this description is limited to the interface. With exception of the combined use of SysML and CML, the tool support available for the remaining notations is limited or nonexistent. Thereby, among evaluated alternatives, the combination of SysML and CML seems more adequate for representing the architecture of SoS. However, it still lacks run-time support and explicit abstractions that would enable to describe complex mediator types as well as dynamic connectivity among constituents.

SosADL: a Formal Language for Describing Systems-of-Systems

Aiming to overcome limitations commonly found on traditional ADLs, such as lack of support for dynamically changing structures, the Systems-of-Systems Architectural Description Language (SosADL) has been introduced for formally describing the architecture of softwareintensive SoS (OQUENDO, 2016c). In SosADL, SoS architectures are represented in abstract terms since concrete systems that will participate in the SoS are not necessarily known at designtime. Then, this abstract architecture can represent a number of concrete architectures, which depict run-time coalitions for the actual constituents of the SoS. The abstract description of a SoS architecture in SosADL encompasses abstract specifications of potential constituent systems, mediators, and their architecture configuration. Thereby, the main architectural elements of the language are the one of system to represent constituents, the one of mediator to represent connectors among constituents, and the one of coalition to represent on-the-fly configurations among constituents and mediators (OQUENDO, 2016c).

The abstract architecture of a SoS encompasses (OQUENDO, 2016c): (i) constituent systems, which are architectural elements defined by intention (in terms of abstract systems) and incorporated at run-time; (ii) mediators, which are architectural elements defined by intention (in terms of abstract mediators) and created at run-time by the SoS to achieve a goal 16 , thus fostering emergent behaviors; and (iii) coalitions, which are architectural configurations of mediated constituent systems, partially defined (in terms of abstract systems, abstract mediators, and policies for their on-the-fly configuration) at design time and created at run-time to fulfill a SoS mission. Thereby, SosADL is the first formal language supporting the description of SoS evolutionary behavior. As the internal structure and behavior of constituents can be concealed from the SoS, SosADL enables to express assumptions and guarantees on their internal behavior in terms of expected input or output. The description of mediators, which are controlled by the SoS, can express guarantees about their concrete behavior. Protocols can be attached to ports for 16 A goal is part of an encompassing mission (SILVA; BATISTA; OQUENDO, 2015). enforcing a predefined sequence of interactions exchanged with the environment. Conditions for the synthesis of mediators as well as assumptions and guarantees over expected mediating behaviors can also be expressed. Moreover, an intentional description of the coalition is supported by expressing constraints on the expected form of concrete coalitions. Finally, the language supports run-time features by means of ask and tell actions. The first action allows mediators to check which constraints hold in the environment while the latter allows constituents to update the set of constraints in the environment. Table 4 summarizes the main architectural elements supported by this language. Appendix A presents additional details on SosADL syntax and semantics. Represents a constituent in terms of gates (interfaces) exposed to the environment and an internal behavior to fulfill its mission. Gates can group connections and enforce assume-guarantee assertions between: (i) assumptions, i.e., properties that must be satisfied by the environment for the system to deliver its expected behavior; and (ii) guarantees, i.e., properties enforced by the system itself when the assumptions are satisfied.

Mediator

Represents possible connectors among constituents in terms of duties (interfaces) exposed to the environment and an internal behavior. Duties and gates can establish a commitment when a gate fulfills the obligations defined by the duty and the duty satisfies the assumptions of the gate. Moreover, interactions between the two are governed by a specific protocol.

Coalition

Represents architecture configurations in terms of constraints that identify and unify constituents by means of mediators created by the SoS itself. Coalitions can be assembled or disassembled on-the-fly in different ways or with different systems.

Environment

Represents the individual surroundings on which constituents operate. Systems can perceive their environment and act on them through gates.

Source: Adapted from Oquendo (2016c).

The SosADL language, which shares some of the foundations of the well known π-ADL (OQUENDO, 2004), is based on a novel process calculus of the family of the π-Calculus, named π-Calculus for SoS (OQUENDO, 2016d). This novel formalism was developed to encompass two additional paradigms, namely concurrent constraints for modeling locality of processes and inferred bindings for modeling mediation. Processes are modeled as behavioral constraints that only have partial information about the state of the environment, i.e., they have local knowledge. In turn, interactions are modeled as binding constraints, which have been tailored for the particular needs of SoS, namely: (i) support for exogenous bindings between channels as interactions are externally driven by the SoS and not by constituents themselves; (ii) support for constrained bindings between channels as interactions are limited by the local context of the constituent; (iii) support for intentional bindings between channels as interactions are dynamically decided; and (iv) support for mediated bindings between channels as interactions are deployed on-the-fly by the SoS itself.

Finally, the language is also supported by a development tool suite, named SosADE [START_REF] Oquendo | SoS ADL for Formal Architecture Description and Analysis of Software-intensive Systems-of-Systems[END_REF], which extends the Eclipse Modeling Framework (EMF) with a tailored environment for SoS design based on SosADL. The tool suite itself is implemented in Xtext [START_REF] Bettini | Implementing Domain-Specific Languages with Xtext and Xtend[END_REF], which provides several custom features for the environment, such as syntax coloring, semantic coloring, error checking, formatting, debugging, structure view, quick fix help, among others.

Architectural Viewpoints

Viewpoints (and views) are an approach for structuring the architectural description based on the principle of separation of concerns (ROZANSKI; WOODS, 2005). Thus, each viewpoint focuses on a particular concern or set of concerns for describing the software architecture. The need of several architectural viewpoints for describing a software architecture reflects the several concerns that may exist. Moreover, it is easier to communicate the software architecture to the several stakeholders that may exist by using separate viewpoints. In this context, several architecture frameworks, which guide the construction of architecture descriptions for a specific domain or stakeholder community, have been proposed in the literature [START_REF] Zachman | A framework for information system architecture[END_REF][START_REF] Kruchten | Documentation of Software Architecture from a Knowledge Management Perspective -Design Representation[END_REF][START_REF] Clements | Documenting Software Architectures: Views and Beyond[END_REF][START_REF] Heesch | Security in context: analysis and refinement of software architectures[END_REF]AVGERIOU;[START_REF] Heesch | Security in context: analysis and refinement of software architectures[END_REF]. The 4+1 Views [START_REF] Kruchten | Documentation of Software Architecture from a Knowledge Management Perspective -Design Representation[END_REF] and the Views and Beyond [START_REF] Clements | Documenting Software Architectures: Views and Beyond[END_REF] frameworks are further detailed in this section since they are broadly referenced in the literature. [START_REF] Kruchten | Documentation of Software Architecture from a Knowledge Management Perspective -Design Representation[END_REF] proposes five viewpoints in the 4+1 Views framework for describing software architectures. The logical viewpoint shows a decomposition of the system, considering abstraction, encapsulation, and inheritance for enabling analysis and identification of common elements throughout the architecture. The development viewpoint describes the static organization of the software, e.g., packages, libraries, or subsystems, in the development environment. Moreover, this viewpoint lists the rules governing the development architecture, such as partitioning, grouping, and visibility. The information presented in the development viewpoint assists in several development and management activities, such as allocating work to development teams, monitoring work progress, and reasoning about software reuse. The process viewpoint captures concurrency and synchronization by mapping elements of the logical viewpoint into processes, i.e., groups of tasks that form an executable unit. For example, the replication of processes can enhance processing load distribution and availability. The physical viewpoint describes how the software can be allocated to the hardware. Moreover, different configurations could be used for testing or deployment. Finally, the scenarios viewpoint illustrates how the elements in previous viewpoints relate to each other. As a result, the scenarios viewpoint plays a special role in illustrating sequences of interactions that can be useful for both test planning and construction of the architecture. While the viewpoints can be described at different abstraction levels, with each level potentially framing different concerns, each viewpoint of the 4+1 Views framework is targeted for a particular audience. For instance, the logical viewpoint is intended for end-users as it presents the high-level functions of the system. Conversely, the development viewpoint is intended for developers and managers as concrete details about the system are exposed. Even though the 4+1 Views framework has great relevance, precise guidelines for tailoring the framework are still missing. Moreover, it is not clear how evaluation could be undertaken, such as manual or automated evaluation of the architecture. [START_REF] Clements | Documenting Software Architectures: Views and Beyond[END_REF] propose the Views and Beyond framework. In particular, the authors introduce the term viewtype as a reference to a set of similar viewpoints. The modular viewtype describes the system decomposition as a set of implementation units (e.g., classes, subsystems, systems, and layers). This viewtype can focus on the decomposition of the system into code units, the uses relations that exist among these units, the relationship among these units (such as generalization), or the organization of these units into layers. The components and connectors viewtype expresses runtime behavior whereas a component (e.g., object, process, or collection of components) is one of the principal processing units of the executing system and a connector (e.g., pipes, repositories, and sockets) is an interaction mechanism for the components. The allocation viewtype describes how software can be mapped to elements of the environment (e.g., hardware, file systems, or development teams). This viewtype can focus on the deployment of processes into processing nodes, communication channels, memory stores, and data stores; the implementation of modules in a development infrastructure; and the work assignment of modules to human development teams. It is also possible to find information that transcend a given viewtype. Therefore, architects using this framework can find among each viewtype the information required for their system and then complement this information with documentation that applies to more than one viewtype. Table 5 summarizes the viewpoints, stakeholders, and concerns of the 4+1 Views and Views and Beyond architecture frameworks.

Architectural Viewpoints for Systems-of-Systems

The heterogeneity, dynamism, and large scale which are inherent to modern SoS require architecture frameworks that can cover a larger diversity and number of concerns and create architecture descriptions that can fulfill different tasks throughout software systems life cycle. The Department of Defense Architecture Framework (DoDAF) (DOD, 2010) is one of such frameworks. In its version 2.0, DoDAF provides a common communication language for designing and operating SoS of the military domain. The framework applies net-centric concepts to meet the needs of next generation SoS developed by DoD. In particular, it focuses on promoting the collection, storage, and maintenance of data that will enable to make efficient and effective decisions. Architects can select views from a set of eight viewpoints, namely: (i) all viewpoint describes global aspects of the architecture context that crosscut other views; (ii) capability (vi) services viewpoint describes solutions in which performers, activities, services, and their exchanges are arranged to fulfill operational and capability functions; (vii) standards viewpoint describes policies, standards, guidelines, constraints, and forecasts applied to operational or capability requirements, processes, systems, and services; and (viii) systems viewpoint describes solutions in which legacy or independent systems, their composition, interactions, and context are arranged to fulfill operational and capability functions. Viewpoints (i), (iii), (v), and (vii) are traversal to the other four viewpoints. In particular, the framework enforces the documentation of relationships and design decisions so that its artifacts can be used for explaining the requirements and proposed solutions to stakeholders.

The European Space Architectural Framework (ESA-AF) [START_REF] Gianni | Introducing the european space agency architectural framework for space-based systems of systems engineering[END_REF] is another example of architecture framework for SoS. In particular, ESA-AF provides an architectural methodology for the representation of interface specifications, data policies, security requirements, and financial regulations tailored for the European Space-based SoS. Another example is SoSE (SoS Engineering) [START_REF] Butterfield | Architecture model developing method for system-of-system[END_REF], an architecture framework that develops a functional architecture model for an SoS which results in system specification and capability descriptions. In common, these three architecture frameworks use different abstraction levels and employ formal or a combination of formal and semi-formal notations in the creation of architecture models.

Architecture Rationale

Software architectures abstract from implementation details to focus on the design issues that have greater impact to the quality of software systems. In this scenario, the software architecture can be acknowledged as the work product of subsequent decisions balancing quality and functionality of software systems [START_REF] Jansen | Software Architecture as a Set of Architectural Design Decisions[END_REF][START_REF] Jansen | Software Architecture as a Set of Architectural Design Decisions[END_REF]. The description of architectural decisions also prevents knowledge vaporization [START_REF] Kruchten | Documentation of Software Architecture from a Knowledge Management Perspective -Design Representation[END_REF][START_REF] Farenhorst | Knowledge Magament in Software Architecture: State of the Art[END_REF][START_REF] Farenhorst | Knowledge Magament in Software Architecture: State of the Art[END_REF] and enables to instruct future users and developers of the software architecture, thus ensuring its sustainability [START_REF] Clements | Documenting Software Architectures: Views and Beyond[END_REF]. Since the architecture description is the main artifact for sharing expertise and best practices, documented decisions play a central part of their content [START_REF] Kruchten | Documentation of Software Architecture from a Knowledge Management Perspective -Design Representation[END_REF][START_REF] Kruchten | Documentation of Software Architecture from a Knowledge Management Perspective -Design Representation[END_REF][START_REF] Clements | Documenting Software Architectures: Views and Beyond[END_REF]; ISO/IEC/IEEE-42010, 2011). For instance, documented decisions may describe consequences, justifications, and trade-offs leading to a particular design, e.g., known limitations of a style or pattern, considered standards impacting the operation and/or management of the system, as well as rules and/or constraints for attaching new components to the system. During evolution, documented architecture decisions can help software architects in making new decisions or removing obsolete ones to satisfy changing requirements [START_REF] Jansen | Software Architecture as a Set of Architectural Design Decisions[END_REF][START_REF] Jansen | Software Architecture as a Set of Architectural Design Decisions[END_REF]. [START_REF] Clements | Documenting Software Architectures: Views and Beyond[END_REF] points out some indicators of relevant architecture decisions: (i) it required a significant amount of time to be taken; (ii) it is critical for a particular requirement of the system; (iii) it covers an intricate topic/concern/context for the system; (iv) it has a widespread effect that will be difficult to undo; and, (v) it solves a problem whose solution is not obvious.

To document architecture decisions, implicit and tacit knowledge must be encoded into explicit and documented knowledge. Several approaches have been proposed for encoding architecture decisions. These approaches can be classified among (FARENHORST; BOER, 2009): (i) pattern-centric, which aims at establishing a shared vocabulary of reusable, abstract solutions; (ii) dynamism-centric, which uses ADLs to codify explicit architectural knowledge into models that can be accessed during run-time; (iii) requirements-centric, which intends to bridge the gap between architecture and requirements; and (iv) decision-centric, which prevents knowledge vaporization by capturing the reasoning leading to the software architecture. For instance, [START_REF] Kruchten | The Decision View's Role in Software Architecture Process[END_REF] follow a requirement-centric approach when they propose the use of architecture knowledge as a new crosscutting viewpoint which overlaps the information of the other viewpoints in the 4+1 Views framework. This new viewpoint shows the underlying design rationale and the motivation of selecting a particular concrete design option. This approach encompasses: (i) deciding what information about the design decision will be present and how it will be represented; (ii) relating the design decision to the requirements motivating it; (iii) managing design decisions state and hierarchy; (iv) linking the design decisions to the resulting architecture; and (v) sharing the decisions using communication and documentation mechanisms. Furthermore, different ADLs, models, or tools can be used for realizing this approach.

Final Remarks

This chapter introduced the basic concepts of the Software Architecture area as well as the current state-of-the-art on architecture description of SoS. As an architecture description provides the basis for evaluating and analyzing software architectures (BASS; CLEMENTS; KAZMAN, 2012), the main part of this chapter was dedicated to the elements that compose such an artifact. The completeness of an architecture description must be evaluated to guarantee that it contains all required data (BASS; CLEMENTS; KAZMAN, 2012). In addition, architecture descriptions can be evaluated in regards to their fit for purpose. For example, to verify that an architecture description communicates the architectural design to all stakeholders, an evaluation can check the readability and effectiveness of the description [START_REF] Clements | Documenting Software Architectures: Views and Beyond[END_REF]. Active design reviews (PARNAS; [START_REF] Parnas | Active Design Reviews: Principle and Practices[END_REF]CLEMENTS, 2000) can also be used to scan the architecture description for defects in documentation and engage reviewers to also exercise the software architecture design, e.g. by thinking how portions of the architecture could be implemented. The main goal of these evaluations is to reveal false assumptions, inconsistencies, omissions, and other weaknesses that limit or jeopardize the use of the architecture descriptions in subsequent stages of the development life cycle [START_REF] Clements | Documenting Software Architectures: Views and Beyond[END_REF].

The architecture description of SoS must be correct and complete to support the analysis and evaluation of coalitions. Due to their inherent characteristics, traditional languages used for describing software systems lack expressiveness for the description of SoS. SosADL, which is presented in this chapter, is the first formal language with tailored building blocks for the architectural description of SoS. While this language supports a normative description of coalitions that can be formed at run-time, further support is needed to verify the feasibility of this design and realize descriptive models that represent actual coalitions derived from it. To address this limitation, the next chapter introduces Ark, a method based on constraint solving for the synthesis of concrete architectures that comply with a SosADL description of the SoS. Thereby, the method can automatically verify if key architectural properties are preserved when moving from SoS abstract architectures to concrete architectures.

Chapter 3

Formal Method for Architectural Synthesis of Systems-of-Systems

Software architectures can establish the blueprint from which coalitions can be formed and reconfigured at run-time. In addition to the identification of user needs, SoS requirements must define which functions are required to accomplish a specific mission and how these functions should be performed (DAHMANN et al., 2011a). The software architecture for a SoS should explain how independent constituent systems can collaborate with each other, functions that are supported by each system, as well as relationships, data flow, and communication protocols that govern the interactions between systems (DAHMANN et al., 2011a). In this scenario, SoS architectural synthesis encompasses creating an architecture solution that meets SoS requirements (GONÇALVES; OQUENDO; NAKAGAWA, 2015). Central to this task are architecture descriptions, which express a SoS from two abstraction levels: i) an abstract architecture provides a normative model for types of coalitions that could be formed among constituents and mediators at run-time. In particular, the architectural configuration is specified by constraints, which abstractly represents a family of run-time coalitions, and ii) a concrete architecture provides a descriptive model for a run-time coalition that could exist at run-time, explicitly showing the interactions that take place among constituents to accomplish the SoS mission. Thereby, it represents a singular operational coalition.

An abstract architecture is feasible if it supports the realization of at least one candidate concrete architecture. In turn, a concrete architecture is correct if it represents a valid arrangement among constituents and mediators that preserves desired architectural properties. In this scenario, a rigorous approach must be in place to perform the architectural synthesis of SoS aiming to guarantee both the feasibility of the abstract architecture and the correctness of all coalitions that can be formed from it, enhancing SoS trustworthiness. Formal languages play an important role in this approach as they enable the creation of precise, traceable models for abstract and concrete architectures that can be used as input to specialized tools. This chapter presents Ark, a method supporting SoS architectural synthesis that aims at preventing the creation of ill-formed concrete architectures. To achieve this goal, the method expresses both the abstract architecture of an SoS as well as the rules governing the formation of coalitions in terms of a Constraint Satisfaction Problem (CSP). Thereby, all solutions can be considered as correct candidate concrete architectures. The remaining of this chapter is organized as follows. Before presenting Ark, Section 3.1 reviews the concepts of formal methods and also how this method adheres to best practices for software systems architectural description. Afterwards, Section 3.2 details each step required for this method, including which are artifacts are used and what is the expected outcome. Then, Section 3.3 further describes these artifacts. Finally, Section 3.4 concludes this chapter with final remarks on Ark.

Foundations of Ark

To perform its mission, which is accomplished by emergent behaviors, an SoS requires specific means for fostering constituents' collaboration [START_REF] Maier | Architecting principles for systems-of-systems[END_REF][START_REF] Boardman | System of Systems -the meaning of of[END_REF][START_REF] Boardman | System of Systems -the meaning of of[END_REF]. Whereas an abstract architecture describes types of elements that can take part of an SoS, a concrete architecture shows actual coalitions that are formed among constituents at runtime. Therefore, a single abstract architecture can represent a number of concrete architectures depending on which connectivity mechanisms are available. The architectural synthesis of SoS must check if an abstract architecture provides mechanisms for establishing connections among constituents and, also, if these mechanisms are adequate for arranging constituents into a cohesive whole, i.e., a coalition that preserves the architectural properties defined by an abstract architecture.

This chapter presents Ark, a method that employs model finding and model transformations for bridging the gap between abstract and concrete architectures. This method expands on [START_REF] Hofmeister | A general model of software architecture design from five industrial approaches[END_REF] general architecting process by adding specific activities for the synthesis of SoS. In particular, the method defines coalitions as a set of constraints, i.e., descriptive specifications expressed as formulas or Boolean expressions [START_REF] Jackson | Towards a Theory of Conceptual Design for Software[END_REF]. As formal notations are employed to describe both abstract and concrete SoS architectures, tailored tools can be developed to automatically analyze and confirm the correctness of created architecture models.

In adherence to the ISO/IEC/IEEE 42010 (2011) standard recommendations, this method identifies: (i) main architectural elements of SoS; (ii) viewpoints for describing SoS architectures, namely an abstract viewpoint and a concrete viewpoint; and (iii) model kinds, for expressing the architectural models that compose the SoS architecture description. In particular, the method adopts three model kinds: a conceptual model (TASoS) that provides the basic theory for representing SoS architectures in terms of a constraint satisfaction problem (described in detail in Chapter 4); a formal language (SosADL), which offers the basic elements to describe abstract types of systems, mediators, and coalitions; and a metamodel of the instance generated by the constraint solver (Solution), which represents a concrete architecture as sets of elements (also described in detail in Chapter 4). Figure 6 shows a fragment of the ISO/IEC/IEEE 42010 (2011) standard conceptual model for architecture description that is tailored for SoS description.

Structure of Ark

Different forces play a role in the architectural synthesis of SoS abstract and concrete architectures. Abstract architectures are impacted by SoS evolutionary development, which can add types of constituents, mediators, and behaviours that were not initially envisioned, whereas concrete architectures are also impacted by SoS dynamic reconfiguration. While the abstract architecture evolves, it also changes what type of concrete architecture can be realized at run-time. Moreover, the concrete architecture can be reconfigured due to environmental conditions (e.g., lost of connection) or constituents independent management or operation (e.g., incorporation or loss of constituent systems), resulting in different arrangements among constituents and mediators.

In this scenario, the Ark method adopts constraint satisfaction techniques to support the synthesis of SoS concrete architectures that comply with a given abstract architecture. To accomplish this task, this method consumes and produces three main architecture models: (i) abstract architectures, which are high-level architectural models of a SoS describing its abstract types of constituents, mediators, and coalitions; (ii) conceptual models, which offer an alternative representation for the SoS abstract architecture in terms of constraints; and (iii) concrete architectures, which are detailed models of a SoS architecture describing its actual constituents, mediators, and configurations. These three artifacts are intrinsically related to each other. Conceptual models frame the same architectural elements described in the abstract architecture. Constraint solving tools can be used for automatically analyzing this conceptual model, whose solutions represent alternative concrete architectures in which the purposes, properties, and constraints of the abstract specification are satisfied. Figure 7 illustrates the four steps encompassed in this method, also outlined in Table 6. Following, each step is further explained.

Step 1: Describe System-of-Systems Abstract Architecture

The first step concerns understanding the SoS mission creating an abstract architecture that describes key constituent systems and available communication capabilities embodied in mediators supporting their collaboration. The description of abstract types of constituents defines properties, interfaces, and constraints that must hold in the environment to enable their participation in a coalition. Due to constituents independence, this abstract description is focused on relevant aspects of constituents for the SoS mission. In turn, the description of abstract types of mediators defines properties and interfaces that it exposes to the environment for establishing communication links among constituents. This abstract description also contains abstract types of coalitions, i.e. mediated architectural configurations, defining a normative design for the way in which communication links can be instantiated among constituents. This design may support, for instance, only a layered or client-server architecture configuration among constituents. To create such a description of the SoS, architects consider Architecturally Significant Requirements (ASRs) identified during architectural analysis and elaborate a candidate abstract architecture that satisfies these requirements. As main output, architects obtain a candidate abstract architecture [START_REF] Valerdi | A Framework for Evolving System of Systems Engineering[END_REF] Architects transform solutions into concrete architectures and evaluate whether they correspond to desired instances of the abstract architecture.

Solution of constraint satisfaction problem.

Concrete architectures that preserve desired architectural properties.

that outlines the general structure and behavior of potential coalitions. This step is repeated whenever ASRs change.

Input: As mandatory input, this step receives one or more ASRs, related to constituents, mediators, coalitions, and/or missions.

Output: This step returns a candidate abstract architecture of the SoS, which describes abstract types of constituents, mediators, and coalitions.

Step 2: Describe Abstract Architecture as a Constraint Satisfaction Problem

The second step concerns expressing candidate abstract architectures obtained in the previous step as an instance module of TASoS, a conceptual model that can be automatically analyzed using constraint solving tools. This conceptual model frames abstract types of constituents, mediators, and coalitions as well as relevant relations that exist among them. In particular, this conceptual model is expressed in terms of constraints, describing rules that relate a specific set of concrete architectures to a given type of coalition or enforcing a particular connectivity requirement between constituent systems. Thereby, a SoS conceptual model defines communication links that can be established between constituent systems that can participate in the coalition. To create this conceptual model, architects map architectural elements of the SoS abstract architecture in TASoS by extending abstract definitions of model and creating custom connectivity constraints on their relationship. Moreover, architects can add constraints that rule out families of concrete architectures, hence limiting architectural configurations that can be realized at run-time. If the resulting instance module cannot be recognized as a valid problem by the constraint solver, the architect can decide whether to go back to Step 1 for correcting the abstract architecture or to select another candidate abstract architecture.

Input: As mandatory input, this step receives a candidate abstract architecture of the SoS.

Output: This step returns a conceptual model of the SoS abstract architecture.

Step 3: Find Solution for Constraint Satisfaction Problem

To synthesize concrete architectures for the SoS, the third step of the method initially checks the feasibility of the abstract architecture. The feasibility can be validated if there is any assignment of values to the constraints that evaluates the SoS conceptual model true. In this case, solutions for this conceptual model represent concrete architectures of the SoS that adhere to the abstract coalition type defined by the abstract architecture. Since a conceptual model is already expressed in a format that can be recognized by off-the-shelf constraint solvers, this evaluation can be automatically performed. In particular, model finding technique is used to search for a solution under a predefined scope, that constrain the analysis space and, consequently, the size of the solutions that can be discovered. Alternatively, different scope sizes can be used to evaluate different scenarios. If no solution exists for this conceptual model under this selected scope, the architect can try to run the analysis again for a larger scope or return to Step 1 and select an alternative abstract architecture for the SoS. Optionally, the SoS architect can also instruct the constraint solver to check the validity of assumptions regarding a particular architectural property that the conceptual model is expected to satisfy. If an assumptions fails, the constraint solver produces a counter-example, which represents a concrete architecture of the SoS that violates this assumption. Otherwise, the architect can infer that the assumption holds for that particular scope and repeat the analysis for a larger scope. As a result, the architect gains confidence in the abstract architecture specification and may proceed to the evaluation of concrete architectures that satisfy these assumptions.

Input: As mandatory input, this step receives a conceptual model that expresses SoS abstract architectures in terms of constraints.

Output: Provided that the conceptual model is valid and that it describes a feasible abstract architecture, this step returns a solution that corresponds to a candidate concrete architecture for the abstract coalition type.

Step 4: Evaluate Candidate Concrete Architectures

The fourth step of the method concerns the evaluation of candidate concrete architectures obtained in the previous step against ASRs and its abstract description. First, the solution returned by the constraint solver must be expressed in a notation that SoS architects are more familiar with. Then, architects can review the artifacts related to different coalitions for confirming that the concrete architecture is in-line with what they have originally envisioned. If not successful, SoS architects can decide whether to change abstract coalition types (i.e., return to Step 1) or to add new constraints to the conceptual model (i.e., return to Step 2) for ruling out ill-formed coalitions. Moreover, alternative concrete architectures can be compared with each other aiming to elect one of them as the validated concrete architecture, which is then used as supporting evidence to architecture reviews, e.g. as a coalition prototype for which the presence of desired properties, such as performance, dependability, among others, can be evaluated, or as part of feasibility studies that document ASRs met by the design and elaborate on architectural concepts or technical approaches that can be used for realizing them (OBBINK et al., 2002). Validated concrete architectures can also be used for simulating the emergence of new behaviors that can only be observed when constituents interact with each other. This step can be repeated whenever SoS architects identify a new concrete architecture for the SoS.

Input: As mandatory input, this step receives a solution for the constraint satisfaction problem representing the SoS architecture obtained in the previous step.

Output: This step produces one or more concrete architectures that hold desired architectural properties as well as adheres to the abstract architecture of the SoS.

Artifacts

The architecture description of SoS must employ notations with well defined semantics for effectively using these models in their analysis [START_REF] Nielsen | Systems of Systems Engineering: Basic Concepts, Model-Based Techniques, and Research Directions[END_REF]. In this scenario, two formal notations were selected to express architectural models in Ark: SosADL (OQUENDO, 2016c), an ADL that has been specifically created for describing SoS architectures, and TASoS, a conceptual model implemented in Alloy (JACKSON, 2012) for the representation of SoS architectures in terms of constraints. Table 7 summarizes the main elements of architectural models expressed for each notation. The content and purpose of each of these artifacts is further explained in the following sections.

Abstract Architecture

An abstract architecture defines the main concepts or properties of a SoS embodied in abstract types of elements, relationships, and in the principles governing its design and evolution over time. The abstract architecture can be perceived as an open structure from which several concrete architectures can be synthesized. [START_REF] Nielsen | Systems of Systems Engineering: Basic Concepts, Model-Based Techniques, and Research Directions[END_REF] refer to an abstract architecture as a conceptual description of an envisaged SoS. Since concrete systems that will actually participate in the coalition are not necessarily known at design time, the abstract architecture defines abstract types of constituents, which can be identified and incorporated to the coalition at

SosADL

System is an abstract type of system that can participate in the SoS. It can engage or disengage from the SoS at run-time by their own decision.

Mediator is an abstract type of mediator that realizes the interaction between systems. It can be dynamically created, modified, and destroyed by the SoS.

Sos is an abstract type of coalition that combines constituents and mediators into a cohesive whole. The Sos configuration is defined by intention, i.e., it defines policies for selecting and binding declared constituents using declared mediators that can be created by the SoS itself.

Conceptual Model

Alloy

Signature is a set of objects.

Relation is a function relating objects of different sets. It can also be understood as a field of a signature.

Fact is a constraint that is assumed to hold.

Assertion is a constraint that is intended to hold but whose satisfaction must be checked. Concrete Architecture

SosADL

System is a concrete system that participates in the SoS. It can enter or leave the coalition without the control of the SoS.

Mediator is a concrete mediator that realizes the interaction between systems.

Sos is an alliance between concrete constituents and mediators. The Sos configuration explicitly defines the topology of this alliance which is realized by concrete bindings among its participants.

run-time. Thereby, abstract architectures support a normative model of SoS without having to constrain which will be its actual constituent systems. Architectural descriptions of SoS from an abstract viewpoint frame which are the types of mediators that can be dynamically realized to support constituents' interaction. As such, architects can use the abstract architecture to focus on the policies governing the interactions among constituents that can foster emergent behaviors. Moreover, the architecture description is completed by defining constraints for arranging these elements into cohesive coalitions so that different ones can be realized at run-time with different elements and/or different configurations to fulfill the SoS mission.

The main elements of an abstract architecture expressed in SosADL encompass abstract types of systems, mediators, and coalitions, which can be used (and reused) across several SoS. The system is an abstraction for a complex, independent entity (e.g., system or SoS) that may participate in the SoS, mediator is an abstraction for a complex, dependent connection that supports the communication between constituent systems, and coalition is an abstraction for the intentional, dependent architectural configuration that can be created based on abstract types of constituents and mediators, constraining which sort of configurations can be formed at run-time (GUESSI; CAVALCANTE; OLIVEIRA, 2015). The description of abstract types of constituents, mediators, and coalitions is enriched by the specification of interfaces, which are predefined interaction points exposed by these architectural elements to the environment supporting the definition of a high-level behavior models for the SoS. Source code 1 1 illustrates the abstract coalition type of an SoS composed of clients (system abstraction) and exactly two servers (mediator abstraction), defined in lines 8-10. The coalition type has a gate and a connection which receives an integer value as input (lines 4-6). Constituents of this coalition may be arranged according to the policy described in lines 12-19, which states that all clients in a coalition must be linked to exactly one server.

Source code 1 -Example of abstract coalition type expressed in SosADL

Conceptual Model

The SoS conceptual model expresses the abstract architecture in terms of constraints. In particular, this model formally specifies SoS architectural elements as concepts and intentional bindings as constraints between these concepts. A constraint can for instance define that any concrete architecture must have all constituents connected by mediators, hence preventing disconnected topologies. Thereby, this model enables the specification of global constraints that 1 This source code was elaborated by the Jérémy Buisson and Jean Quilbeuf, members of the ArchWare research group.

will prevent an entire group of ill-formed concrete coalitions and promote the trustworthiness of run-time SoS architectures. Moreover, the description of abstract architectures as a constraint satisfaction problem enables using off-the-shelf constraint solvers in the automated analysis of concrete architectures that adhere to this specification. Source code 2 illustrates an excerpt of the constraint problem expressed in Alloy that corresponds to the abstract coalition type presented in Source code 1. This description imports tasos library (line 1), the conceptual model of SoS architectures. Chapter 4 presents TASoS and details how to express SosADL architectural elements in Alloy. Additional libraries can be imported by this model (line 3), preserving the structure of the original SosADL project in that it is based on. To create an instance module of TASoS, architects must extend existing definitions with new elements that will frame a particular SoS, e.g., ServersXor, unusedGate, and unusedConnection, which are respectively defined in lines 6, 7, and 8. The behavior of the architecture is used for customizing definitions introduced by this SoS, e.g., the signature server1 extends the abstract signature server which is defined in the ClientServerDefinitions library (line 12). Also, architects translate intentional bindings of the abstract architecture into constraints (lines 18-39). Finally, the model can have one or more execution commands, such as the one shown in line 43, that either attempt to find an instance within a predefined analysis scope or produce a counterexample for a property defined as an assertion.

Source code 2 -Excerpt of abstract coalition expressed in terms of constraints

Concrete Architecture

Differently from an abstract architecture, a concrete architecture explicitly defines the architectural configuration of coalitions, identifying concrete constituents and establishing interconnections that will enable information exchange among them. It can also be referred to as a run-time software architecture of a particular SoS since all of its constituent systems are known. [START_REF] Kenley | Synthesizing and Specifying Architectures for System of Systems[END_REF] refer to concrete architectures as allocated architectures, which represent candidate solutions. A candidate solution represents assorted distribution of functionality among constituents, hence potentially showing varying levels of quality. In fact, each concrete architecture is unique in the way that constituent systems interact with each other, depending on which communication links have been instantiated [START_REF] Maier | Architecting principles for systems-of-systems[END_REF]. To be feasible, an abstract architecture must have at least one possible concrete architecture adhering to its specification. A single abstract architecture can designate a number of concrete architectures that comply with its specification. New concrete architectures should be realized when constituents are incorporated to the coalition, which can require changes to current constituent systems and/or associated mediating elements as well as new instances of communication links among them. To be correct, all concrete architectures must comply with the policies defined by an abstract architecture and satisfy the constraints defined by its corresponding conceptual model.

To facilitate the analysis of concrete architectures by architects, Ark also selects SosADL for expressing concrete architectures. The main elements of such description are the same ones of the abstract architecture, i.e., systems, mediators, and coalitions. Nonetheless, the description of a coalition is different in that: it concretely specifies constituents and mediators that participate in the SoS, and it explicitly defines the communication links that exist among systems and mediators within the coalition. Thus, the concrete instance of a coalition specifies the architectural configuration of a SoS in the traditional way that ADLs usually specify configurations instead of defining policies as in abstract architectures. Source code 4 illustrates a candidate concrete coalition expressed in SosADL for the abstract coalition type presented in Source code 1. In this instance, there are exactly two servers and two clients (identified as clients1 and clients2) and each client communicates with only one server.

Source code 3 -Excerpt of constraint solver solution 28 t a s o s / System={ c l i e n t s $ 0 , c l i e n t s $ 1 , c l i e n t s $ 2 , c l i e n t s $ 3 } 29 C l i e n t S e r v e r D e f i n i t i o n s / c l i e n t ={ c l i e n t s $ 0 , c l i e n t s $ 1 , c l i e n t s $ 2 , c l i e n t s $ 3 } 30 t h i s / c l i e n t s ={ c l i e n t s $ 0 , c l i e n t s $ 1 , c l i e n t s $ 2 , c l i e n t s $ 3 } 31 . . . u n i f y one { c l i e n t s 1 : : r r 0 : : r e q 0 } to one { s e r v e r 1 0 : : r r 1 : : r e q 1 } and 22 u n i f y one { c l i e n t s 0 : : r r 1 : : r e q 1 } to one { s e r v e r 2 0 : : r r 0 : : r e q 0 } 23 } } }

1 ---INSTANCE--- 2 . . .

Source code 4 -Example of concrete coalition expressed in SosADL

Final Remarks

The formal representation of SoS architectures plays a central role in the synthesis and analysis of concrete architectures since it enables to verify the presence of key architectural properties, hence validating the architectural design. To confirm the feasibility of SoS architectures, this chapter presented Ark, a method for synthesis of SoS concrete architectures. Ark is intended to support normative models of SoS architectures in which only abstract types of constituents, mediators, and coalitions are specified at design time. This method is composed of four steps: (i) description of SoS abstract architectures; (ii) translation of SoS abstract architecture to constraints; (iii) search of solutions for the resulting constraint satisfaction problem; and (iv) evaluation of solutions obtained by the constraint solver as candidate concrete architectures. In particular, Ark prevents the realization of ill-formed concrete architectures by formalizing SoS architectures in terms of a constraint satisfaction problem, enabling to use constraint solving technologies in the realization of concrete architectures that are correct-by-construction.

Ark is further explained in the following chapters. First, Chapter 4 TASoS, a theory for modeling SoS architectures in terms of a constraint satisfaction problem. Inspired by elements of the SosADL notation, this model is the basis for the verification of abstract architectures, whose feasibility must be confirmed. Chapter 5 details SoSy, a tool developed for assisting architects in tasks comprised by the Ark method. New abstractions are needed for describing and reasoning about SoS dynamic architectures and interfaces [START_REF] Nielsen | Systems of Systems Engineering: Basic Concepts, Model-Based Techniques, and Research Directions[END_REF]. In particular, abstractions should support the description of independent constituent systems whose interactions are mediated towards accomplishing a global mission. The SosADL introduces the concept of intentional bindings as an abstraction for dynamic connectivity, which is the capability associated with the on demand realization of connections enabling the collaboration among concrete constituents (BOARD-MAN; SAUSER, 2006). In particular, bindings are expressed as relations that identify which constituents' connections fulfill the commitments of which mediators. In this scenario, the feasibility of an abstract architecture implies that at least one concrete coalition adhering to its abstract description exists. While synthesizing concrete coalitions from an abstract architecture, a number of different configurations can be obtained as new concrete systems are identified and attached to the coalition. However, it is not possible to assume that all coalitions are correct. While the abstract architecture evolves, it is important to preserve its dynamic connectivity so that it does not reach a state for which there cannot be concrete architectures adhering to the specification.

To check the feasibility of abstract architectures and help to uncover hidden flaws in the design of SoS, this chapter presents a conceptual model for SoS architectures, named TASoS. In particular, this model employs Alloy (JACKSON, 2012), a formal method expressing the fundamental concepts related to software systems behavior [START_REF] Jackson | Towards a Theory of Conceptual Design for Software[END_REF], for modeling the main architectural elements framed by SosADL, namely constituents, mediators, and coalitions, and expressing connectivity as constraints. Thereby, this model is able to characterize SoS concrete architectures in terms of a satisfiability problem so that constraint solvers can be used for automatically determining the feasibility of an intentional description. In this scenario, constraint solvers will play a key role in the synthesis of SoS concrete architectures by producing a valid coalition that satisfies the abstract architecture, if any exists within the analyzed space.

The remaining of this chapter is organized as follows. First, Section 4.1 introduces the main concepts of the Alloy language that are needed for understanding this conceptual model. The TASoS model encompasses two separate modules: (i) a core module, which defines concepts for the main architectural elements supported by the abstract syntax of SosADL (presented in Section 4.2); and (ii) an instance module, which is a customization of the core module for the particular elements described by the SoS under analysis. Thereby, the core module can be reused across SoS models whereas instance modules must be created for each SoS. Section 4.3 describes tailored functions that could facilitate the creation of instances of the core module. The mapping between the SosADL abstract syntax and TASoS is discussed in Section 4.4. Finally, Section 4.5 concludes this chapter with final remarks on the use of formal methods and, in particular, constraint solvers in the context of software architectures.

The Alloy Language

Alloy is a formal language that expresses software systems in terms of constraints, i.e., formal statements about the software system which are also referred to as formulas or Boolean expressions [START_REF] Jackson | Towards a Theory of Conceptual Design for Software[END_REF]. This language combines quantifiers from first-order logic with operators of relational calculus for expressing the behavior of software systems. Instead of defining test cases (as in testing), the analysis performed by Alloy is based on checking the validity of a property (i.e., a constraint). To guarantee efficiency, the analysis performed by the language (i.e., model checking and model-finding) is complete under a predefined execution scope, i.e., the analyzed space (also referred to as solution space) is finite. Therefore, the scope must be carefully selected so that a sufficiently large space is considered for analysis. Nonetheless, a small scope still yields a sizable solution space (in the order of 10 8 clauses) which is sufficiently large for discovering problems in small instances of the model [START_REF] Jackson | Towards a Theory of Conceptual Design for Software[END_REF]. In fact, the analysis performed by the language is grounded on the premise that even small instances of a model can illustrate flaws, which arise from incorrectly handling shapes (JACKSON, 2012). Furthermore, the power of this analysis is greater than one that could be achieved by specifying the problem in Java, which would lack support for generating arbitrary samples, performing exhaustive checking on test cases, and visualizing the results.

Atoms are the primitive entities of an Alloy model presenting three inherent properties: (i) indivisible; (ii) immutable; and (iii) uninterpreted. A signature defines an atom that behaves as a set, i.e., they have a containment relationship to other atoms. It is also possible to define relations among atoms. Relations can also be defined among atoms of different sets and they can be defined as unary, binary, and ternary relations. Constraints that always hold in the model can be declared inside a signature declaration or as part of a fact. Because Alloy is a declarative language, the order in which facts are declared is not relevant since all constraints are analyzed together. The language supports the declaration of predicates and functions which define operations over signatures. A predicate defines one or more constraints that when executed instruct the analyzer to produce an instance of the model satisfying the predicate. A function defines an expression whose evaluation yields a subset of atoms and, thus, can be used for improving modularity and readability of models. Differently from a predicate, it is also possible to declare assertions, i.e., constraints that are intended to be valid in the model. The execution of an assertion instructs the analyzer to produce a counterexample, i.e., an instance of the model that violates the property. Modules can be created for sharing generic declarations and constraints among models, thus facilitating reuse. Table 8 summarizes supported commands for the creation of conceptual models in Alloy. The Alloy Analyzer is an open-source tool supporting Alloy [START_REF] Jackson | Towards a Theory of Conceptual Design for Software[END_REF]. This tool can automatically translate an Alloy formula (relational) into a Boolean formula, thus enabling to invoke an off-the-shelf SAT-solver, such as the SAT4J 1 or KodKod (TORLAK; [START_REF] Torlak | Kodkod for Alloy Users[END_REF], for performing the analysis. However, the tool has two limitations: it lacks an API for the creation, manipulation, and analysis of Alloy formulas, and it lacks support for partial instances, i.e., a part of the problem's solution that is known a priori. An API is needed to enable the use of a constraint solver as a back-end analyzer for modeling tools that accept the Alloy language. Besides addressing these two limitations, KodKod can replace the Alloy Analyzer because it accepts a subset of the Alloy language and, hence, can support the creation, manipulation, and analysis of Alloy models. KodKod is also more efficient than the Alloy Analyzer since it employs a mechanism for sharing sub-formulas and sub-expressions which contributes for the performance of SAT solvers. To execute an Alloy model, a fixed scope (i.e., bound) must be assigned to the analysis. While the Alloy Analyzer requires an integer to be assigned to each 1 SAT4J, <http://www.sat4j.org/>. signature in the model, which bounds the maximum number of atoms that can exist for each set, KodKod requires a formula to be bounded by a relational constant, i.e., a fixed set of tuples drawn from the universe of atoms. In particular, KodKod assigns an upper bound (i.e., tuples that a variable may contain) as well as a lower bound (i.e., tuples that a variable must contain), thus enabling to describe partial solutions, which enhance the efficiency of the solver by further constraining the solution space.

To illustrate the expressiveness of Alloy for describing conceptual models, Figure 8a shows an example of a complete Alloy model about the view and viewpoint concept as defined by the ISO/IEC/IEEE 42010 (2011) standard. The standard specifies that each viewpoint governs exactly one view and frames some stakeholders' concerns. In this example, governs is a binary relation (its atoms can be tuples of type Viewpoint → View) and frames is a ternary relation (its atoms can be tuples of type Viewpoint → Stakeholder → Concern). Quantifiers can be used for qualifying relations, such as the keyword some that in the case of the frames relation of the Stakeholder 2 signature constrains each stakeholder to be related to at least one concern. Then, the fact body adds constraints without which signatures and relations would be allowed to potentially contain all possible tuples. For instance, the constraint in lines 15-17 defines that the set of concerns framed by a particular viewpoint is always equal to the set of concerns framed by the view that it governs. The empty body of the predicate show instructs the Alloy Analyzer to return any instances of this model that can be found within the scope of three atoms per signature, with exception of Viewpoint that can have at most two atoms. The execution of this specification by the constraint solver confirms that this is a syntactically correct and sound model since it was able to find at least one solution for the problem within the informed scope. In particular, this solution can be alternatively presented to the user as text or a graphic model. Figure 8b shows one of the model's solutions in which there are two viewpoints, each of them governing their own view and framing one of the two concerns that a given stakeholder has on the described system.

Conceptual Model of Systems-of-Systems Architecture

To capture the main concepts framed by SoS architecture descriptions, the TASoS model takes inspiration on the SosADL abstract syntax. The reasons for the selection of this language are threefold: (i) it has explicit constructs for abstract types of constituents, mediators, and coalitions, including a mathematical foundation that enables to express dynamic connectivity in terms of constraints; (ii) it supports the description of SoS abstract architectures from a dynamic as well as static viewpoint; and (iii) it is supported by a tool that can be extended to work with different modeling and implementation languages, such as UML, Java, and C, as well as used in Architects can describe at design-time abstract types of constituents that will only be realized later on at run-time. Each constituent is described in terms of external gates (interfaces) that are exposed to the SoS environment and an internal behavior to fulfill its own mission. Moreover, the participation of the constituent in the coalition is not controlled by the SoS and it only occurs if there exists a duty that satisfies the assumptions of its gates.

Belonging to voluntarily contribute for the SoS mission

Architects can express assumptions for the participation of constituents in the coalition, which describe conditions for their permanence in the SoS that must be fulfilled by the environment. Moreover, the language supports on-the-fly evolution of the architecture by enabling to identify and incorporate different concrete constituents. Connectivity to dynamically establish connections among constituents Architects can describe obligations of duties that must be fulfilled by gates and assumptions of gates that must be satisfied by duties, thus supporting dynamic creation of commitments between constituents and mediators that participate in the coalition. Moreover, architects can describe physical properties about constituents and mediators, thus enabling to take location as a condition for constituents interaction. Diversity to create new capabilities from constituents inherited limited functionality Architects can describe several abstract types of constituents and mediators, which can then be arranged in different coalitions for taking advantage of SoS diversity.

Emergence of behaviors by exercising the connectivity, autonomy, and belonging of constituents

Connections can be dynamically created from abstract commitments between gates of constituents and duties of mediators if the obligations defined by the duty are fulfilled by the gate and the assumptions of the gate are satisfied by the duty. Thus, coalitions can be composed in different ways or with different systems, thereby providing the necessary conditions for new behaviors to emerge.

Source: Adapted from Oquendo (2016c).

The conceptual model for SoS architectures, which is named TASoS, defines 20 signatures and 14 relations listed in Table 10 and covers the architecture elements supported by SosADL, such as systems, mediators, and coalitions. Signatures may inherit the relations of higher level signatures by extending its prior definition and, optionally, adding more relations. For the sake of simplicity, inherited relations are omitted in this chart. Atoms of an extension are treated as atoms of the higher level signature in that they must also satisfy the constraints that apply to the higher level signature. Atoms of a higher level signature with only one extension must necessarily pertain to that extension. On the other hand, if there are more extensions, atoms can pertain to only one of them. For instance, System, Mediator, and SoS are all extensions to the higher level signature ArchitecturalElement and, therefore, atoms of this higher level signature necessarily pertain to either System, Mediator, or SoS. In the case where the conceptual model should allow atoms of a higher level signature to pertain to more than one of its extensions, the set operator in is used instead of extends in the signature definition instruction. Following, the main signatures of TASoS are detailed. The source code of the conceptual model is presented in its entirety in Appendix A. The signature extends the one marked with *. This implies that the current signature inherits the relations of the extended one and that atoms of sister signatures do not overlap with each other.

ArchitecturalElement is the signature for entity blocks in SosADL. As previously mentioned, this signature is further extended by the ones of System, Mediator, and SoS, which are separated in TASoS because they play a different role in the coalition and, thus, are subjected to different constraints. Source code 5 presents an excerpt of constraints referring to ArchitecturalElement or one of its extensions. Atoms of the higher level signature have a binary relation named hasPort of type ArchitecturalElement → Port that specifies the ownership of ports 3 , which in turn may contain one or more connections (constraint 14). Additional constraints are defined to refine this relation for each extension, i.e., mediators can own duties (constraint 11) and systems and SoS can own gates (constraints 12 and 13, respectively). In particular, the SoS signature extends the one of ArchitecturalElement with a binary relation arch that has atoms of type Architecture → Relay for internally relaying a set of connections to the elements of a particular coalition, which is supported by SosADL. The evolving nature 3

The Port signature is extended by the ones of Gate and Duty.

of systems, mediators, and SoS is also supported by allowing a set of ports owned by a given element to change.

Source code 5 -Excerpt of constraints on architectural elements in TASoS An interaction represents a physical or logical channel that enables to exchange information between architectural elements. In SosADL, interactions take place at the connection level of interfacing architectural elements. In TASoS, two independent signatures can be used for modeling interactions, namely Unification and Relay. Source code 6 presents an excerpt of constraints that apply to interactions. The first signature is used for modeling interactions between systems and mediators within coalitions and has two binary relations for mapping its domain (src, which is of type Uni f ication → Connection) and image (dest, which is of type Uni f ication → Connection). To convey the direction of a unification, atoms of the domain must be of type Uni f ication → Outward (constraint 17.1) and atoms of image must be of type Uni f ication → Inward (constraint 17.2). Moreover, a unification can only exist between connections of systems and mediators (constraint 17.3-5). To prevent two or more unifications over the same pair of connections, which should not be allowed in concrete architectures, there cannot be two unifications to the same pair of domain and image connection (constraint 18). In turn, the latter signature models the interaction that exists between a connection owned by the SoS and a connection of a system or mediator. In particular, the ternary relation named relayCon of type Relay → Connection → Connection can only map connections owned by a SoS to connections of elements that are presently in the coalition (constraint 8). Moreover, connections of a SoS can be relayed only once (constraint 9) to connections of the same type (constraint 10) in any given coalition.

Source code 6 -Excerpt of constraints on interactions in TASoS 1: //#8 R e l a y i n t e r a c t i o n s r e q u i r e some element i n t h e c o a l i t i o n Another core signature of TASoS is Architecture, which combines elements of abstract and concrete architectures for expressing possible run-time coalitions for a SoS. This concept is defined in terms of three relations, namely: (i) contains, a binary relation of type Architecture → (System + Mediator) relating a particular architecture to the set of systems and mediators that are presently engaged in a coalition; (ii) bindings, a binary relation of type Architecture → Uni f ication listing intentional bindings between systems and mediators that have been defined in the abstract architecture; and (iii) unifiedAs, a binary relation of type Architecture → Topology describing different ways (i.e., candidate configurations) in which systems and mediators within the coalition can be arranged given the available types of bindings. The Topology signature, which is introduced in TASoS for representing the explicit configuration of concrete architectures and it is further explained in the next section. Source code 7 shows an excerpt of constraints in which Architecture plays an important role. For instance, any two architectures are considered to be equal if they share the same set of topologies (constraint 28). Systems that participate in any given architecture must engage in at least one unification of candidate concrete architectures (constraint 31). All unifications of a system in the coalition must appear in candidate concrete architectures (constraint 32). Moreover, connections of any given gate only can be unified to connections of a single duty (constraint 34).

Source code 7 -Excerpt of constraints on architectures in TASoS 1: //#28 Two a r c h i t e c t u r e s s h o u l d be e q u a l i f t h e y have t h e same s e t o f t o p o l o g i e s

2: a l l a ,a ': Architecture | 3: ( a . unifiedAs ) . elems = (a ' . unifiedAs ) . elems i m p l i e s a =a ' 4: //#31 A l l s y s t e m s t h a t p a r t i c i p a t e i n an a r c h i t e c t u r e must engage i n a t l e a s t one u n i f i c a t i o n i n a l l c a n d i d a t e t o p o l o g i e s

The Topology Concept

The architectural configuration is abstractly expressed in SosADL in terms of policies. To automatically resolve concrete configurations adhering to such an abstract description, TASoS introduces the Topology signature for representing explicit configurations that comply with the policies described in the abstract architecture. Atoms of this signature have two relations, namely: (i) inTopology, a binary relation of type Topology → Uni f ication which contains the set of intentional bindings that can be realized between abstract types of systems and mediators; and (ii) path, a ternary relation of type Topology → Uni f ication → Uni f ication which connects atoms of Unification in order to compose a network of systems and mediators. Thereby, this signature merges the description of an abstract architecture with the one of a concrete architecture in that the first relation lists abstract types of bindings that can take place among systems and mediators at run-time (which is taken from the abstract description) and the latter lists connected networks that can be created on top of these bindings (which results in the concrete description). Source code 8 shows an excerpt of constraints that apply to Topology. For instance, only unifications listed by the inTopology relation can be used by path (constraint 25). Moreover, the path of all possible topologies for architectures without any systems must be necessarily empty (constraint 29). A mediator that participates in a topology engages in at least one unification in the topology (constraint 30). Finally, the connectivity of the path is guaranteed by constraining related unifications to share at least one system or mediator (constraint 33).

Source code 8 -Excerpt of constraints on topologies in TASoS

Verification of the Architecture

Differently from facts, which denote constraints that always hold, assertions define constraints whose satisfiability must be evaluated. In fact, the execution of an assertion instructs the constraint solver to find a counterexample that violates the property. If no counterexample is found within the predefined analysis scope, the user can infer that the assertion holds and repeat the analysis for larger scope. Thereby, if subsequent analyses still cannot produce a counterexample, the architect gains confidence on the correctness of the model. The main purpose of assertions in TASoS is to verify the soundness of the model by stating constraints that are expected to hold or fail in the context of SoS abstract and concrete architectures. Table 11 describes all assertions included in the model, which cover different aspects of the architecture of SoS. These assertions can be used in the analysis of abstract architectures, e.g., in the verification of completeness of the set of constraints that describe a particular SoS. In particular, assertions can be used to find families of configurations that violate a particular property so that new policies might be added to the abstract architecture for preventing them to occur. As a result, the correctness and completeness of the abstract architecture of a SoS is enhanced.

A7 cantModifyConstituents

Checks the changeability of systems in an architecture. This assertion is expected to fail.

A8 cantModifyBindings

Checks the changeability of set of bindings of an architecture. This assertion is expected to fail.

Source code 9 shows an excerpt of these assertions. The first assertion, named architecture-CantBeEmpty, evaluates the feasibility of architectures without elements. When executed, the command check in line 5 instructs the constraint solver to find a counterexample that shows an architecture without elements. This assertion is expected to fail since the contain relation of Architecture is only defined as a set of systems and mediators. To prevent scenarios in which coalitions have no elements, one could change the definition of the contain relation to some systems and mediators. But, since the feasibility of empty coalitions is needed for validating the outcome of operations (e.g., loss of systems) on the architecture, no constraint was added or changed in the model. The second assertion, named pathCantBeEmpty, evaluates the feasibility of architectures that are not empty but have candidate configurations that are. This assertion is expected to hold due to constraint 31 (shown in Source code 7), which states that all elements of an architecture must participate in at least one unifications in its path relation. Finally, the third assertion, named samePortUnification, evaluates the feasibility of having more than one unification between two ports. Even though there is a constraint that prevents a connection to participate in more than unification in the same path, this assertion is expected to fail since there are not any constraints preventing this scenario. Thus, if this assertion holds, the model of the architecture might be overconstrained. It is also worth mentioning that the execution of this assertion under the small analysis scope of 5 atoms per signature can produce an instance of the architecture that violates the property and is also easier to understand than a large instance of the model would be.

Source code 9 -Excerpt of assertions in TASoS

Predicates for the Customization of TASoS

As mentioned in the beginning of this chapter, the TASoS model encompasses a core module, which has been presented in the previous section, and an instance model, which has to be created for each particular SoS under analysis. To create such an instance model, one needs to extend the abstract signatures in TASoS with elements derived from the SoS abstract architecture. To facilitate the creation of such an instance, the core module defines the predicates listed in Table 12, which encompass one or more constraints that apply to the atoms passed as parameters.

In particular, if the predicate is called within a fact statement, it is also treated as constraints that always hold. Thereby, these predicates can further refine the problem by adding new constraints to the instance module. Source code 10 shows an excerpt of predicates for the customization of TASoS. For instance, the first predicate, named attributeConToPort, customizes which atoms of Connection pertain to the hasConnection relation of Port. The second predicate, named attributeArchToSos, attributes a given atom of Architecture to a particular atom of SoS. Finally, the third predicate, named unify, attributes a pair of atoms of Connection to the relations src and dest of an atom of Unification. Thereby, this predicate can customize the atoms of Unification based on intentional bindings defined by the abstract architecture.

Source code 10 -Excerpt of predicates in TASoS for creating instances of the core module Once an instance module has been created, constraint solvers can be employed for automatically synthesizing configurations that adhere to the description of the SoS abstract architecture. To do so, the architect must instruct the solver to search for concrete architectures within a predefined analysis scope. Source code 11 shows an excerpt of the core module that instructs the solver to search for one or more architectures that comply with the constraints described in the predicate named case. This predicate describes a scenario where there must be two distinct mediators participating in such a concrete architecture. Based on the core set of constraints defined in TASoS, this predicate describes a feasible setting and, hence, should return at least one concrete architecture adhering to this description. Since the investigation is limited to a small analysis space, this scope must be carefully selected so it is sufficiently large that it finds an instance of the model (in other words, a solution of the problem) and yet small that it returns such an instance within an acceptable time frame. The abstract architecture is considered to be feasible if at least one concrete architecture is found to satisfy the complete set of constraints, i.e., the core and instance modules of TASoS. But, in the case where the evaluated scenario cannot return a solution for the abstract architecture, the architect can decide between broaden the scope of the analysis or check the correctness of the instance module by using assertions that have been previously described or new ones that can be created for checking a particular SoS instance.

Source code 11 -Excerpt of a predicate checking the feasibility of a scenario in TASoS

Mapping between SosADL and TASoS

As previously discussed, the conceptual model for SoS architectures implemented in Alloy takes inspiration on the abstract syntax of SosADL. Figure 9 on page 72 shows an excerpt of the metamodels for SosADL and TASoS. Despite many similarities between the two metamodels, some of the concepts framed by TASoS play a different role from their namesakes in SosADL. Moreover, not all elements that appear in the SosADL metamodel are explicitly framed by TASoS. For instance, SosADL has a SosADL element as the overarching construct of the architecture description. While there is no explicit concept for this element in TASoS, an instance module may be regarded as such since it encompasses the set of constraints that make up for the corresponding architecture. Also regarding the SosADL element, it can import several Library elements and it can be composed of at most one Unit element, which is either a SoS or Library element. In turn, TASoS supports referencing external libraries as modules, which are not signatures but a mechanism provided by the Alloy language for referencing external files, and SoS elements can be modeled as extensions to the SoS signature. The Unit element is defined in SosADL by at most one Entity Block, which can be composed of an assorted group of System, Mediator, Architecture, Function, or Datatype elements. Apart from Function, all other elements can be modeled as extensions to existing signatures in TASoS. In particular, the Architecture element is framed by two separate signatures, namely: (i) SoS, which models the structure of this element, e.g., its interfaces; and (ii) Architecture, which models its behavior and configuration. Table 13 presents a detailed comparison between the elements of SosADL and their corresponding signatures in TASoS. A System extends the Entity Block element with its own set of formal parameters, datatypes, and gates. It also has an internal behavior and assertions, which must be fulfilled by Mediators. In TASoS, the System signature extends the one of Architectural Element and constrains the hasPort relation to only have atoms of type System → Gate, thus describing which gates are owned by a particular system. Mediator (Entity Block)

Mediator (Architectural Element)

A Mediator extends the Entity Block element with its own set of formal parameters, datatypes, and duties. Differently from systems, a Mediator has only an internal behavior. In TASoS, the Mediator signature extends the one of Architecture Element and constrains the hasPort relation to only have atoms of type Mediator → Duty, thus describing which duties are owned by a particular mediator. Architecture (Entity Block)

SoS (Architectural Element), Architecture

Similarly to the System element, an Architecture extends the Entity Block with its own set of formal parameters, datatypes, and gates. In addition, this element contains an architecture behavior and assertions. In TASoS, the SoS signature can also have its own set of gates. In particular, the arch relation of this signature is used for associating a particular configuration (captured by the Architecture signature) to a particular set of connections that are internally relayed to some of its constituents. Function (Entity Block) -A Function element defines an operation over a Datatype element described by the SosADL model. This element is not mapped to TASoS. A Datatype element is extended by the one of IntegerType, NamedType, TupleType, SequenceType, RangeType, and ConnectionType. The difference between TupleType and SequenceType is that elements of the latter must necessarily be of the same Datatype. The first five elements are mapped in TASoS by namesake signatures. However, TASoS does not have constraints in which the aforementioned signatures play a determinant role, such as one forbidding unifications that do not match a particular datatype. On the other hand, the ConnectionType element must be specified for every Connection in the model as either in, out, or inout. In TASoS, this element is mapped by signatures Inward and Outward, which are extensions of the Connection signature and play a determinant role in several constraints of the model, such as the ones for customizing unifications.

Continued on next page

Gate and Duty

Gate and Duty (Port)

A Gate and Duty are distinct elements representing an interface. Besides the declaration of connections, a duty also declares assertions that once satisfied will guarantee the operation of the mediator. In TASoS, these elements are represented by namesake signatures, which can customize the hasConnection relation for expressing connection ownership.

Expression Unification, Relay

An Expression element describes constraints over the SoS description. Several elements extend Expression, such as Binding, Any, UnobservableValue, CallExpression, among others. The TASoS model is mainly concerned with the description of Binding, which is specialized by elements Relay and Unify, the latter being required for expressing intentional bindings. These elements are captured by namesake signatures, which can be customized for a particular SoS.

Protocol -A Protocol element describes a logical order for the analysis of expressions (such as choose, repeat, for, and if-then-else) or execution of actions (such as receive, send, assert, and done). This element is not mapped to TASoS.

Behavior -A System and Mediator elements can have an internal behavior that describes a logical order for the action of these elements, such as the sequence of interactions exchanged with the environment. This element is not mapped to TASoS.

Connection Inward, Outward (Connection)

A Connection element describes an interaction point that a Gate or Duty element exposes to their environment. An environment connection is similar to a regular connection, hence they are both mapped to the Connection signature in TASoS. Moreover, Inward and Outward signatures extend the one of Connection, thus enabling to distinguish them based on their mode.

Architecture Behavior

Architecture, Topology

An Architecture Behavior element has three main parts: constituents that are allowed to participate at run-time, parameters that it can receive from the environment, and bindings that it can replicate for connecting these constituents. In TASoS, the first relation is mapped to the contain relation of the Architecture signature, the second relation is not mapped, and the third is mapped to the bindings relation, which associates atoms of Unification with a particular Architecture. Moreover, to describe different ways in which concrete architectures can be assembled, the unifiedAs relation is added to associate a given Architecture signature to one or more topologies.

This table shows that the conceptual model for SoS architectures defined by TASoS frames several of the elements defined in the abstract syntax of SosADL. In particular, this conceptual model has explicit signatures supporting the description of abstract and concrete architecture for SoS, such as coalitions, intentional bindings, and configurations. Still, some elements of SosADL are not mapped in the conceptual, such as the behavior of systems and mediators, functions, and protocols. Expressions, on the other hand, are partially supported. TASoS maps Unify and Relay expressions to namesake signatures, thus enabling the description of constraints related to interactions that take place within a coalition. Finally, the model can be refined with additional constraints for the customization of existing signatures, hence resulting in an instance module of TASoS that complements the core module introduced in this chapter.

Final Remarks

This chapter presented TASoS, a theory for the specification of SoS architectures based on formal constraints. To describe SoS, this model takes inspiration on the main architectural elements supported by SosADL, in particular coalitions, configurations, and intentional bindings. By using Alloy as the underlying model-finder tool built on SAT solvers, the feasibility and correctness of abstract architectures can be automatically analyzed. Therefore, if the solver does not find a concrete architecture complying with such an abstract description, architects can refine the set of policies governing the connectivity among constituents and run the solver to check the satisfiability of a new abstract coalition type. Moreover, architects can instruct the constraint solver to analyze the correctness of user-specified properties that are expected to hold in any architectural configuration of the SoS. To create such a model for representing a particular SoS, architects must extend the abstract signatures defined in TASoS with custom elements and add new constraints for the relation among these elements. In the following chapter, an automated mechanism is presented to support the creation of such an instance model for TASoS and automate the steps for the architectural synthesis of SoS based on constraint solving.

Chapter 5

Automated Synthesis of Systems-of-Systems Architectures

This chapter presents a software tool named SoSy that supports the synthesis of concrete architectures given an abstract description of a coalition type expressed in SosADL. This tool is provided as an extension to SosADE (Architectural Framework for Systems-of-Systems Design) [START_REF] Oquendo | SoS ADL for Formal Architecture Description and Analysis of Software-intensive Systems-of-Systems[END_REF], an integrated environment for the design, validation, and simulation of SoS based on SosADL. In particular, SoSy supports the translation of abstract architectures as constraints and, if feasible, the translation of the constraint solver as concrete architectures. These two translations are accomplished by two transformations: (i) a Model-to-Text (M2T) transformation from SosADL to TASoS, in which instance modules can be dynamically created for abstract architectures; and (ii) a Text-to-Model (T2M) transformation from the solution returned by the constraint solver to SosADL, in which concrete instances found by the tool are represented in SosADL. Thereby, SoSy is able to conceal the use of constraint solvers in a process for the architectural synthesis of SoS based in Ark.

The remainder of this chapter is organized as follows. First, Section 5.1 presents an automated model-driven process that supports the activities defined by Ark and how this process was implemented to complement an integrated environment for the design of SoS. Section 5.3 discusses the results of a functional evaluation of this tool. Finally, Section 5.4 concludes with final remarks on the use of an integrated environment for the design of SoS. Appendix A complements this chapter with additional guidance for installing and executing SoSy.

A Model-Driven Process Supporting Ark

To perform the tasks recommended by Ark, architects must create at least three models of the SoS architecture. First, architects manually create an abstract architecture for the SoS under analysis using SosADL. Then, to express the abstract architecture as a set of constraints, architects translate the first artifact as an instance module of TASoS. If the new model corresponds to a correct instance of TASoS, architects can automatically analyze this artifact using constraint solvers. Finally, architects might need to translate the solution found by the constraint solver, which is provided as either text or graphic models, back into a format that is more familiar to them so that they can proceed to the analysis of the concrete architecture. In this scenario, the tasks required by Ark can be time consuming and prone to error. Aiming to mitigate these risks, this chapter presents SoSy, a tool that automates model transformations among SosADL, TASoS, and the constraint solver solution. In particular, this tool implements two model transformations (illustrated in Figure 10): (i) an Xtend 1 class named SosADL2Alloy-Generator, which implements a M2T transformation from SosADL to TASoS; and (ii) a Java method named Solution2SosADLGenerator, which implements a T2M transformation from solutions of the constraint solver to SosADL. This figure also shows that each transformation is defined at different abstraction levels, i.e., the former is defined at the metamodel level between SosADL and TASoS whereas the latter is defined at their instance level. The tool implements a model-driven process illustrated in Figure 11 that takes inspiration on steps of the Ark method. This process is represented in SPEM (OMG, 2008), an OMG standard for the specification of software methods and processes. In particular, this figure describes the sequence in which tasks (i.e., work that has a particular purpose) and activities (i.e., group of related tasks) must be carried out by architects. The creation of an abstract architecture triggers an automatic transformation of this model as an instance of TASoS. In parallel, a Java 2 class that calls the constraint solver over the generated Alloy artifact is also generated. Afterwards, the architect executes the main method of this class for analyzing the generated Alloy artifact. If the analyzed model is a valid architecture, the solver returns one or more instances of this model which can then be automatically translated into concrete architectures expressed in SosADL. Otherwise, architects can decide whether to increase the analysis scope (if the model is correct) or revise the abstract architecture (if the model is incorrect), triggering an update of related artifacts in the project. The process is concluded by an evaluation of candidate concrete architectures that is expected to terminate with a valid concrete architecture of the SoS. In particular, SoSy is developed as an extension to a comprehensive environment supporting the design of SoS named SosADE [START_REF] Oquendo | SoS ADL for Formal Architecture Description and Analysis of Software-intensive Systems-of-Systems[END_REF]. In particular, this environment is itself an extension to Eclipse 3 that supports SosADL as modeling notation. This tool is developed in Xtext, a framework that supports the development of customized run-time and Integrated Development Environment (IDE) features for the use of DSL (Domain-Specific Languages) in the design of software systems. To achieve this purpose, the framework adopts the programming language Xtend, which is similar to Java and offers additional facilities for the implementation of customized tool support for DSLs. Moreover, as an Eclipse modeling environment, SosADE offer several facilities that support the use formal methods in practice, including (WOODCOCK et al., 2009): multi-language support, cross-platform support, version control, and assistance for teams working on shared projects. Thereby, architects can leverage the facilities provided by SosADE in the creation and analysis of SosADL models that are required by the Ark method.

Figure 12 shows an activity detail diagram for the synthesis of concrete architectures as part of SosADE. The architect interacts with the tool in three instances: (i) to create an abstract description for the SoS, (ii) to execute the Java class that calls the constraint solver; and (iii) to evaluate candidate concrete architectures returned by the solver. Hence, intermediary tasks are automatically handled by SoSy, which implements transformations from architectural models to conceptual models and from the solution to this conceptual model back to architectural models. In particular, the analysis of the conceptual model is automatically handled by the constraint solver, which in this figure is represented by the Alloy Analyzer. As intermediary models are automatically managed by SoSy, in particular by two separate transformations, the architect is responsible for managing initial and final work products, namely abstract architecture and validated concrete architecture descriptions. Additional details about the installation and use of this tool are presented in Appendix A. Following, the implementation of the two transformations supported by the tool are further explained.

Transformation from SosADL to TASoS

The first transformation is implemented in SoSy as an Xtend class, which is named SosADL2AlloyGenerator. Table 14 lists the classes that compose this generator and explains their role in the creation of instance modules of TASoS and Java classes. The main class of this generator is SosADL2AlloyGenerator, which extends the SosADE class SosADLPretty-PrinterGenerator by changing the way in which elements of a SosADL model are printed in an instance of TASoS. Since this is the main class of this generator, it is discussed in more detail.

The complete list of methods in the SosADL2AlloyGenerator class is included in Appendix A. The main method of this class is doGenerate, which receives as input an element of type Resource, which is the link for a persistent document. Each resource is identified by a Uniform Resource Identifier (URI), which determines its location so that it can be reached by other methods. This method also receives an element of type fsa, which grants file system access for the creation and exclusion of files in the project, enabling to dynamically update its content as the abstract architecture changes. Two different types of files are created by the execution of this generator: (i) instance module of TASoS that describes a SosADL model in terms of a set of constraints; and (ii) Java class that calls the constraint solver on these instance modules. The remaining methods in this class are responsible for transforming each element of a SosADL model and translating them into elements of an instance of TASoS. To realize this transformation, these methods implement templates, a special type of expression delimited by triple single quotes ("') for string concatenation. The text within quotations is copied "as-is" to an instance module. Within a template, guillemets (« ») indicate a placeholder for values or expressions that can be dynamically evaluated and replaced by their toString representation. The method illustrated in Source code 12 compiles a SosADL object and creates the header of both a library and architecture instance modules of TASoS. Then, compilation of library and architecture are delegated to their corresponding methods.

Throughout the execution of this transformation, three global variables are accessed to customize generated instance modules. The variable runargs of type AlloyBound (shown in Source code 13) defines the quantity of elements for each signature in an architecture instance. This data is needed to specify a custom command that instructs the solver to search for a solution within a predefined scope. As previously mentioned, the analysis scope must be carefully selected so that it comprehends at least one feasible solution but it is still small enough so that the efficiency Class Description SosADL2AlloyGenerator Main class of the generator. It is responsible for calling the methods that transform SosADL models in the project folder into Alloy instance modules of TASoS and Java classes.

AlloyFunction

Defines the content of a function. In particular, defines the datatype name as a signature of TASoS. It stores the function declaration as it appears in the SosADL model so that it can be copied to concrete architectures.

AlloyListOfFunctions

Defines a list of functions declared in SosADL models. AlloyType Defines a superclass for datatypes that are declared in SosADL models. It is extended by the classes AlloyIntType, Alloy-BoolType, AlloyRangeType, AlloyTupleType, AlloySequence-Type, and AlloyNamedType which provide their own implementations for the methods toString and equals.

AlloyBound

Defines the content of a custom analysis scope for an instance module. In particular, it can scale up the number of allowed elements for signatures in an Alloy model based on the number of constituents instances in the coalition.

AlloyConnection

Defines the content of a connection. In particular, connections of mode inout are translated as two separate connections in an instance module.

AlloyPredicate

Defines how TASoS predicates are to be printed in instance modules.

AlloyPort

Defines the content of a port. In particular, it copies the content of guarantees for ports declared in the abstract architecture to related ports in the concrete architecture.

AlloySystem

Defines the content of a system, mediator, or architecture. In particular, it copies the content of the behavior of a system or mediator declared in the abstract architecture to related elements in the concrete architecture.

AlloyLibrary

Defines the content of a SoS or a Library unit.

ConcreteSolution

Defines the location and content of a template Java class that will call the constraint solver on a particular Alloy file in the project folder.

Table 14 -Classes in the SosADL2AlloyGenerator file of the constraint solver is not impacted. In turn, the sigs variable is used to relate the signatures of constituents that participate in the analyzed scenario with their corresponding abstract signatures in the TASoS model. Finally, the elems variable is used to support the compilation of SosADL unifications by documenting extensions of the signature connection.

Source code 12 -Excerpt of method that compiles SosADL objects p r i v a t e LinkedHashMap<S t r i n g , I n t e g e r > a r g s 3 p r i v a t e LinkedHashMap<S t r i n g , L i s t <I n t e g e r >> l i s t A E 4 p r i v a t e I n t e g e r s i z e // D e f a u l t i s 3 e l e m e n t s p e r s i g n a t u r e The customization of instance modules is also facilitated by the implementation of the predicates defined in Table 12. The class AlloyPredicate defines templates that can be dynamically evaluated during the transformation of a SosADL model. As some predicates can be attributed to a set of related signatures (as extensions to the same high level signature) to a particular element, these templates may vary depending on which sets of parameters are passed. Table 15 identifies all uses of predicates in methods of the generator. For instance, the method that compiles ArchitectureDecl creates an object of AlloyPredicate set with predicate attributeArchToSoS, which associates the current architecture with the SoS that is being described. Source code 14 shows an excerpt of the AlloyPredicate class that implements this predicate.

Source code 14 -Excerpt of the AlloyPredicate class 1 c l a s s A l l o y P r e d i c a t e {

Transformation from Solution to SosADL

Once the first transformation is successfully concluded, the architect can execute the generated Java class that will use a constraint solver to automatically analyze its corresponding architecture instance module. Each generated Java class is derived from a template defined by the ConcreteSolution class that is referenced in the previous SosADL2AlloyGenerator class for the description of library and architecture models for a particular abstract architecture. In particular, this class encompasses custom methods derived from the abstract declaration of systems, mediators, and SoS that are responsible for printing the content of these elements in the format of a SosADL model. Thereby, the definition of this class as a template supports transferring data that are not processed by intermediary models between an abstract architecture and its concrete description, such as the declaration of behavior, protocol, and guarantee.

Provided that an analyzed abstract architecture is feasible, i.e., there are concrete architectures satisfying its set of constraints, the execution of this Java class will return a solution to the instance model which represents one or more concrete architectures for the coalition. Since this solution is originally presented to the user in a format other than SosADL, a second transformation is required so that architects can more easily understand the outcome of this analysis. This transformation is implemented by a method named Solution2SosADLGenerator that is provided as part of the generated Java class and defines the main structure of library and architecture models in SosADL based on elements provided by the solution. Because it is defined as a template, the content of this method can be customized for each architecture, thus showing custom names for ports and connections as well as updated behaviors, guarantees, and protocols. An excerpt of this method is shown in Source code 15. The result of this transformation is a set of new SosADL models which correspond to library and SoS concrete models.

Source code 15 -Excerpt of library template in Solution2SosADLGenerator method . . . }

Project Content

As shown in Figure 12, the content of a project in SoSy comprises artifacts related to abstract architectures as well as generated artifacts, which comprise Java classes, conceptual models, and concrete architectures. All artifacts created by SoSy can be accessed by the user from the project folder perspective in Eclipse. Figure 13a illustrates the artifacts of an abstract architecture description in the project folder, namely: (i) one or more abstract system types;

(ii) one or more abstract mediator types; and (iii) at least one coalition type, which identifies potential participants for the SoS and establishes the intentional bindings (i.e., policies) for arranging them into a cohesive whole. Abstract types of systems and mediators are arranged into library files, which can be reuse across different SoS. In Figure 13b, a conceptual model that is generated for an abstract architecture is composed of: (i) one or more library instance modules, which can be reused and/or shared among different instance modules; (ii) a coalition type, which is an architecture instance module of TASoS that represents the architecture behavior defined by the abstract architecture in terms of constraints; and (iii) TASoS, which is the Alloy module that defines the main elements expressed in a SosADL description. This organization promotes reuse and readability of the resulting project since details about a particular architecture are not interwoven with constraints related to SosADL building blocks. The solution for a conceptual model represents one or more concrete instances of the abstract architecture for which all constraints hold. Therefore, the outcome of the constraint solver can be transformed into concrete architectures expressed in SosADL, which contain (Figure 13c): (i) one or more concrete systems; (ii) one or more concrete mediators; and (iii) one or more candidate coalitions, which depict a feasible architectural configuration for these elements. In particular, a validated concrete architecture is selected among concrete architectures realized by this process.

Suitability of Tool Support

The suitability of SoSy is demonstrated using the project of a client-server abstract architecture (previously presented in Section 3.3.1 on page 49) as an illustrative scenario. This project is originally composed of four SosADL models: one library model, which declares the abstract types of client and server, and three SoS models, which declare abstract coalition types. For the sake of completeness, an excerpt of the declaration of clients and servers is shown in Source code 16. According to this description, a client is an abstract type of system that has one public gate named rr. The interactions taking place on this gate follow a specific protocol which is omitted from this excerpt. Moreover, the behavior of this element specifies that for each value that it sends through its req connection, it receives a response through its ack connection. In turn, a server is an abstract type of mediator that has one public duty named rr. This duty follows a specific interaction protocol provided that a particular property holds in the environment. The internal behavior of a server defines that for each request that it receives through its req connection, it shall send as response the processed value of this request through its ack connection. Following, different abstract architectures are outlined, each of which defines their own set of policies for assembling constituents within coalitions.

Source code 16 -Excerpt of library model with client-server abstract types expressed in SosADL The first coalition type, referred to as "Exactly Two Servers" and shown in Source code 1 on page 51, defines a client-server architecture that can have any number of clients but exactly two servers. The configuration of this architecture is constrained by a single policy in which each client necessarily sends and receives messages from either one of these servers. The second coalition type is specified as compositions of any number of clients and servers. The configuration of this coalition is constrained by two policies: each client must necessarily send and receive a message from a server, and also its interactions are constrained to a single server, hence its name "Single Server" architecture. Source code 17 shows an excerpt of its abstract description. Finally, the third coalition type describes an architecture that can has any number of clients and server provided. In particular, its configuration is constrained by a single policy that states that each client is necessarily connected to the same server for both request and acknowledgement interactions. Source code 18 shows an excerpt of this coalition type.

Source code 17 -Excerpt of coalition type for client-server architectures expressed in SosADL The suitability of SoSy is determined by its efficiency in terms of elapsed time for the automated synthesis of concrete architectures for each of the aforementioned abstract coalition types. In particular, the tool is expected to: (i) automatically generate valid instance modules of TASoS from abstract descriptions in SosADL; (ii) automatically generate valid Java classes that delegate the search for a solution to a constraint solver; (iii) automatically find a solution that satisfies the constraint satisfaction problem specified by an instance module within the analyzed scope; and (iv) automatically generate one or more concrete architectures in SosADL from the previous solution. A criteria is satisfied if the tool manages these previous tasks without requiring external changes to automatically generated artifacts, e.g., modifying the analysis scope or manually specifying predicates in Alloy models. Table 16 details the outcome of this evaluation. As shown in this table, the tool is able to successfully generate instance modules and Java classes for the three coalition types. The user can manually execute these Java classes to execute the constraint solver and synthesize candidate concrete architectures adhering to the specification of each coalition, such as the one presented in Source code 4 on page 55 for the abstract coalition type "Exactly Two Servers". The table also shows the total running time of this tool, which discounts user interactions. Moreover, it is possible to notice that both transformations are quickly accomplished by the tool.

Final Remarks

In the previous chapter, a constraint based model was presented to support checking the correctness and feasibility of an abstract architecture by finding concrete architectures that adhere to its specification. Nonetheless, the translation of concrete architectures into a constraint satisfaction problem is not trivial, specially as this technology requires one to be familiar with a declarative programming paradigm. To fully take advantage of formal methods in the design of SoS whilst diminishing the risks incurred by adopting a new technology, specialized tools are needed to support architects in the creation of such artifacts. In this scenario, a new tool was presented in this chapter to support activities that are required by Ark. This tool is provided as part of a larger tool set that allows architects to design software architectures for SoS in SosADL. In particular, the tool automates the transformations between SosADL and TASoS and between the output of constraint solvers and SosADL so that the use of constraint solving tools is concealed from the user who can work directly with artifacts expressed in SosADL. In the next chapter, this tool is demonstrated in a case study where it is used to check the feasibility of an abstract architecture for the case of a urban river monitoring SoS.

Chapter 6

Evaluation on Architectural Synthesis of System-of-Systems

One way of automatically verifying if there is any concrete architecture satisfying the set of properties defined by an abstract architecture is through the description of coalitions in terms of a set of constraints. Thereby, off-the-shelf constraint solvers can be employed to search for instances of a family of architectural configurations. To systematize the steps of this process, a new method named Ark was developed, which employs formal languages and model transformations. A custom tool named SoSy supporting this method is provided to automatically describe abstract descriptions of SoS as a Constraint Satisfaction Problem (CSP) and synthesize concrete architectures adhering to such descriptions. In particular, this chapter reports the results of a quasi-experiment on the effectiveness of Ark for the synthesis of SoS architectures.

The remaining of this chapter is organized as follows. Section 6.1 presents the main characteristics and emergent behaviors of a Urban River Monitoring SoS (URMSoS). Section 6.2 details the context and motivation for this experiment. Section 6.3 presents its planning, describing hypothesis, validity concerns, instrumentation, and analyses procedures. Section 6.4 details the execution of Ark steps supported by SoSy and discusses the outcome of these steps. Section 6.5 evaluates the effectiveness of this method. Moreover, this section discusses related work, including alternative approaches for the synthesis of concrete architectures for SoS. Finally, Section Section 6.7 presents final remarks on the results of this evaluation.

Urban River Monitoring System-of-Systems

Emergency management and response is a relevant application domain for complex SoS [START_REF] Nielsen | Systems of Systems Engineering: Basic Concepts, Model-Based Techniques, and Research Directions[END_REF]. The design of such SoS often requires the coordination among heterogeneous constituent systems (e.g., surveillance, weather forecast, and flood monitoring systems) and protocols (e.g., police, firefighters, traffic management, first aid and rescue teams).

An Urban River Monitoring SoS plays a key role in obtaining precise, real-time data that supports authorities' timely and organized response. By collecting data about current speed and level of rivers crossing urban areas, the existence of such SoS is key for organizing and taking action in case of flash floods. To achieve this goal, information provided by independent, heterogeneous sensors (e.g., water level, current, and pollutant sensors) are combined. This information can be used for determining imminent flooded zones and organizing rescue and defense teams response. Ultimately, the effectiveness of such SoS has also a relevant impact on costs incurred by flood events, which can be greatly diminished by sending out warnings in advance (ROURE, 2005).

The Urban River Monitoring (URM) is one of such systems that have been placed on the Monjolinho River in São Carlos, Brazil [START_REF] Hughes | A middleware platform to support river monitoring using wireless sensor networks[END_REF]DEGROSSI et al., 2014). This system is based on a wireless sensor network (WSN) composed of multiple sensor motes 1 , which are spread in flood-prone areas near the riverbed and monitor the river condition. Sensor motes can provide pressure and/or ultrasound sensors to respectively gauge the depth and the average current speed. These networks have been widely used in river monitoring and warning systems as they support distributed data collection and provide wide area coverage as a result of independent communication capabilities that are embedded in sensor motes, such as WiFi, ZigBee (IEEE 802.15.4), GPRS, or Bluetooth (HUGHES et al., 2009). To determine the water level, data collected from these sensors are forwarded to a gateway station, which has dedicated resources for processing, integrating, and publishing this information. The gateway station can transform raw data collected by the sensor for determining the relative height reached by the water level and feed this information to a web-based tool that supports decision-making processes. In particular, if a gateway station cannot be reached by individual communication capabilities of a sensor, the sensors network transmits these data to their neighboring motes until the gateway station is reached.

Since this system operates in a highly dynamic environment, its architectural configuration must be continuously changed for ensuring: (i) efficiency in the use of the available resources, mainly in terms of power consumption and communication; (ii) resiliency in case of temporary unavailability of motes during operation; (iii) accuracy in flood detection; and (iv) autonomy in adapting to dynamic environmental conditions while minimizing manual intervention. Thereby, the Urban River Monitoring presents the five characteristics of an SoS [START_REF] Maier | Architecting principles for systems-of-systems[END_REF]. Each sensor mote operates in a way that is independent of other sensor motes, as they belong to different city councils and have different missions, e.g. pollution control or water supply. Each one has its own management strategy for transmission vs. energy consumption and acts under the authority of the different city councils. New sensor motes may be installed by the different councils as well as existing ones may be changed or deactivated without any control from the system. Finally, the sensor motes, coordinated by the gateway, make emerge the behavior of flood detection. This behavior is collectively achieved by the distributed, independent sensors 1 Sensor motes are tiny hardware/software platforms equipped with embedded CPU, wireless networking capabilities, and simple sensors working together with the gateway station rather than being provided by any of them working in isolation. In particular, the URM can be considered as collaborative SoS.

Experiment Scoping

The objective of this experiment is to investigate the effectiveness of the Ark method and its tool support for analyzing an abstract architecture that is originally described in SosADL. As previously discussed in Chapter 3, the analysis performed in Alloy is complete within a limited analysis scope. Thus, the Ark method returns concrete architectures for the SoS provided that one of such instances exist within the analyzed scope. Still, an architect may wish to increase the analysis scope to find alternative concrete architectures for the SoS or decrease the scope to improve the efficiency of the solver. As all constraint solvers face the state explosion problem, increasing the analysis scope has a direct impact to the running time of the tool. In this scenario, this experiment is motivated by a need to understand the trade-off that exists between analyzing a broader scope and realizing concrete architectures within feasible amount of time. To ensure the performance of the constraint solver, it is important that architects understand how different scope sizes impact the concrete architectures realized by the method so that it is possible to optimize computational resources and advise them against or in favor of changing the generated analysis scope.

Object of study. The object of study is the Ark method and its support for the transformation of SosADL models into a constraint satisfaction problem expressed in Alloy.

Purpose. The purpose of the experiment is to evaluate the effectiveness of the method based on the analysis scope that is assigned to the constraint solver. In this scenario, the study will help to understand whether an assigned scope is sufficient for discovering any concrete architectures that comply with a given abstract architecture.

Perspective. The perspective is from the point of view of the author, who would like to minimize required computational resources for the synthesis of concrete architectures by means of a constraint solver.

Quality focus. The main effect investigated in this experiment is the tool's performance measured in terms of elapsed time for automatically performing the steps of the Ark method. In particular, the study focuses on productivity (i.e., number of lines of code of generated concrete architecture) and existence of at least one concrete architecture within the analyzed scope.

Context. The experiment is run within the context of a Urban River Monitoring SoS. The analysis is based on a SosADL description for the abstract architecture of this SoS that is composed of one library model and one SoS model. The subject runs this model in the SoSy tool to obtain a representation of the abstract architecture as a set of constraints in Alloy. Using the Alloy Analyzer, several test cases are performed over this description, each of which considers a custom analysis scope for the architecture instance module that is automatically generated by the tool. The evaluation is performed by one subject, who operates the Alloy Analyzer with the purpose of finding one or more concrete architectures that comply with this model. The subject is familiar with both SosADL and Alloy languages, particularly with the TASoS model, as well as the SoSy tool. In this scenario, the experiment can be characterized as a "single object study", which is run on a single subject and a single object. Moreover, the lack of randomization of subjects and objects characterizes this experimental setting as a quasi-experiment [START_REF] Wohlin | Formal Modelling Language for Systems of Systems[END_REF]. The scope of this quasi-experiment can be summarized as follows:

Scope: Analysis of Ark and its tool support, SoSy, for the purpose of evaluation with respect to effectiveness from the point of view of the SoS researcher in the context of a Urban River Monitoring SoS.

Experiment Planning

Context Selection. The quasi-experiment is developed in the context of a Urban River Monitoring SoS. The experiment is run off-line (not in an industrial software development), being conducted by the author, and it is focused on a singular architecture and its corresponding abstract description in SosADL. The quasi-experiment addresses the architectural synthesis of concrete architectures and its relation to the analyzed scope.

Hypothesis Formulation. The quasi-experiment aims at understanding two potential implications of an analysis scope to the architectural synthesis of SoS with the Ark method: (i) a larger scope faces the state explosion problem, hence the method is expected to present lower reliability due to failure of returning a concrete architecture within a feasible time frame; and (ii) a larger scope may hold an architectural instance that is larger than the one that would exist in a smaller scope, hence the method is expected to present a higher productivity. Based on this description, it is possible to formally state these hypothesis and the measures that are needed to evaluate them:

1. There is no difference in the reliability of the method based on the selection of different analysis scope for the synthesis of concrete architectures.

H 0 : The reliability of the method is independent of analysis scope.

H 1 : The reliability of the method changes with analysis scope.

Measures: analysis scope and satisfiability of abstract architecture.

2. There is no difference in the productivity of the method based on the selection of different analysis scope for the synthesis of concrete architectures.

H 0 : The productivity of the method is independent of analysis scope.

H 1 : The productivity of the method changes with analysis scope.

Measures: analysis scope, productivity (LOC/running time), and satisfiability of abstract architecture.

Based on these hypothesis, the following data must be collected: (i) analysis scope: measured by the quantity of elements assigned to each signature in the execution of the conceptual model (ordinal scale); (ii) SoS description: measured as LOC of the abstract architecture (ratio scale); (iii) productivity: measured as LOC of the concrete architecture divided by running time (ratio scale); (iv) running time: measured as combined running time of the constraint solver and the Solution2SosADL generator (ratio scale); and (v) satisfiability of abstract architecture: measured by satisfiable, undetermined, or unsatisfiable (nominal scale). In particular, the measure for LOC is determined by a line counter program.

Variables Selection. The quasi-experiment has control over independent variables, or input variables. In turn, dependent variables, also referred to as response or output variables, have their values observed throughout the quasi-experiment to determine the effect of the independent variable on them. In this scenario, the independent variables in this quasi-experiment are analysis scope and SoS description, which is then transformed into a constraint satisfaction problem. Dependent variables are productivity, running time, and satisfiability of abstract architecture. Table 17 further details these variables. Since the SoS description is an independent variable with fixed level (the experiment is run on a single object case), the analysis scope is the single treatment investigated in this quasi-experiment.

Experiment Design. Neither the object of this experiment or its subject have been selected by chance. The subject of this experiment is a PhD student with experience on architectural descriptions and ADLs (in particular, UML, SysML, and SosADL).

1. The first part of this quasi-experiment evaluates the correlation between the analysis scope and reliability of the method.

2. The second part of this quasi-experiment evaluates the correlation between the analysis scope and productivity of the tool and transforming the model back into a SosADL description.

Instrumentation. The object of this experiment is the abstract architecture description of URM is described in SosADL. This description is uploaded in the SoSy tool, which automatically generates an instance module of TASoS for SosADL model and a Java class for executing the SoS model. Once the Java class is generated, its main method is modified to measure the running time of the constraint solver and the transformation from the solution returned by the solver to a SosADL model. This operation is repeated for each different scope that varies the maximum number of systems, mediators, and relay connections in a coalition (the scope of other signatures is dynamically determined). The Java class is then executed several times and the satisfiability of the instance module representing the abstract architecture and productivity of the tool are recorded. The generated concrete architectures are kept in the project folder and their size is calculated by a line counter tool. The materials used in this experiment are organized into two datasets: Dataset 1 contains the input for the Ark method, which is the source code for the library model and the SoS model of the URM described in SosADL; and Dataset 2 contains the output of the SoSy tool, which includes generated instance modules of TASoS as intermediary models and solutions found by the constraint solver as concrete architectures, and experiment materials, i.e., the instrumented Java class and a set of concrete architectures.

Validity Evaluation. Four levels of validity threats were identified for this quasi-experiment.

Following, each of these threats are discussed in detail.

• Internal validity is an inherent risk of quasi-experiments since treatments are not assigned to subjects and objects by chance. Furthermore, there is only one object and one subject in this experiment due to stage of development of the tool set (SosADE) and lack of subjects with required skills. Still, this risk is ameliorated since the experiment is focused on evaluating the constraint solving activity of the method and, thus, the subject plays a minimal role to start the execution of the test and record its outcome.

• External Validity is also a concern for this experiment since results reflect a single object case and particularly only one abstract coalition type. This risk is mitigated by selecting as object a system that has the fundamental characteristics of an SoS, as previously discussed.

It is also possible to expand this experiment for the comparison of the reliability for different constraint solvers and/or coalition types.

• Construct validity is related to the threat that selected measurements are not appropriate for the entities. To mitigate this threat, the experiment selects objective measurements, such as LOC and analysis scope, which do not depend on the context. To mitigate this risk for subjective variables, such as running time, each test is replicated twice.

• Conclusion Validity is a threat in this experiment since only one abstract architecture for the SoS is investigated. However, for the purposes of this experiment, i.e. investigate the effect of analysis scope to the productivity and reliability of the method, it is important to select a feasible abstract architecture, for which the constraint solver is expected to eventually produce a concrete architecture. This threat is further mitigated by presenting a detailed protocol that can be used for future replications and expansions of this experiment.

Experiment Operation

This section details step-by-step of the synthesis of a concrete architecture for the URM given its abstract description in SosADL. First, the abstract architecture of the SoS is detailed in Step 1. Then, the transformation of this description into instances modules of TASoS is described in Step 2. Step 3 describes how this instance module is run with different analyses scope by instrumenting the generated Java class. Finally, Step 4 discusses solutions that have been found for this model.

Step 1: Describe URM Abstract Architecture

The first step of the method concerns the description of an abstract architecture for the SoS under analysis. To perform this task, the subject uses the SosADE tool to create SosADL models for URM. The SosADL description of this SoS comprises two abstract types of systems, namely sensor and gateway. These systems can collaborate with each other by means of a mediator, named transmitter, which represents wireless connections. Then, an abstract coalition type that describes families of architectural configurations that can be realized from such elements is also specified for URM. Following, the description of these abstract types is further elaborated.

A gateway is an abstract type of system that requests observations to sensors and publishes collected data. The specification of this system, shown in Source code 19, encompasses one gate named alerting that has three connections: (i) request receives queries from other systems about current condition of the river; (ii) measure handles observations returned by other systems; and (iii) alert sends out warning messages when an internal parameter of the gateway is violated by environmental conditions. All connections have an associated direction (inward or outward) and data type, which is limited to an abstract integer type named t for the sake of simplicity. For describing the behavior, the subject specifies a sequence in which the system is expected to interact with the environment. The main behavior of the gateway is depicted in lines 20-28. It begins by receiving an observation from another systems via its measure connection. Then, the gateway evaluates if this observation surpasses the local depth threshold (line 24). If so, it publishes a warning message via its alert connection of the same gate. These actions can be repeated indefinitely.

Source code 19 -Excerpt of abstract gateway type for URM in SosADL A sensor is also an abstract type of system that collects observations from the environment. The specification of this system, shown in Source code 20, encompasses two gates: (i) measuring, that comprises one environment connection named sense that reads observations and one connection named measure that handles these observations over to a neighboring system; and (ii) passing, that has two connections pass and measure for just handling observations over to other systems. The specification of these gates is complemented by a guarantee protocol, which describes assumptions (i.e., properties) that must be fulfilled by the environment. For instance, the measuring gate guarantees that while the sensor is operational (i.e., if all assumptions that a sensor makes about the environment hold), it will continually receive observations from the environment via its connection sense and transmit these data via its connection measure. The main behavior of this system is declared in lines 54-64. The sequence of interactions is formed by a choice, the sensor either makes an observation via its sense connection of the measurement gate and sends it to one of its neighboring systems via the measure connection of the same gate, or it receives an observation via its pass connection of the passing and forwards it to one of its neighboring systems via the measure connection of the same gate.

Source code 20 -Excerpt of abstract sensor type for URM in SosADL A transmitter is an abstract type of mediator that forwards observations from sensors to a gateway, either directly or by means of other sensors. The specification of this mediator, shown in Source code 21, comprehends one duty, named transmitting. This duty has two connections named fromSensors and toGateway that handle the transmission of observations from sensors to a gateway. A duty can also declare assumptions that must be fulfilled by constituents in the environment. In this case, this duty requires that the distance between the source and target of this communication link do not exceed a predefined range threshold. If this property holds, then the abstract description of mediator can guarantee that the protocol declared in transmittingpact is also fulfilled. This protocol defines that all observations received via the fromSensors connection are forwarded via its toGateway connection. Then, transmitting behavior of this mediator states that this behavior is continuously repeated, with no processing in between.

Source code 21 -Excerpt of abstract mediator type for URM in SosADL mediator t r a n s m i t t e r ( ) i s {

Step 2: Describe URM as a Constraint Satisfaction Problem

The second step of Ark requires the transformation of the URM abstract architecture described in SosADL into a constraint satisfaction problem described in Alloy. To accomplish this task, the subject must extend abstract signatures in TASoS with elements of URM that were defined in the abstract architecture. In SosADE, this task can be automatically performed by the SoSy tool, which is running on the background. Therefore, instance modules of TASoS are dynamically created by the environment while the subject is creating SosADL models. Source code 23 shows an excerpt of the generated Alloy model for the simple coalition abstract type. The compose statement of the abstract architecture is mapped by the constraints in lines 30-32. Accordingly, the binding statement is mapped by the constraints in lines 39-50. SoSy also generates a default scope to run the analysis, which is shown in line 65.

Step 3: Find Solution for Constraint Satisfaction Problem

The third step of Ark comprises the automated analysis of the generated instance model by the constraint solver. To perform this task, the subject executes the main method of the generated Java class. For the default analysis scope, the subject is presented with a solution that shows a concrete coalition of this model. Thus, SoSy automatically transforms this solution into its corresponding SosADL model. Source code 24 shows an excerpt of a concrete architecture found in this analysis.

Source code 24 -Excerpt of concrete architecture for URM that is compliant with abstract coalition type Since this model is satisfiable, the generated Java class was instrumented to repeatedly run this analysis with a different scope each time. Appendix B further details which materials were used to automatically run this quasi-experiment. The scope of each test case is a combination of all possible variations withing the interval defined in Table 18, which adds up to 396 test cases. For the sake of simplicity, signature Relay was fixed with value 1. In particular, the scope assigned to signature ArchitecturalElement covers all elements of types System, Sos, and Mediator, including their extensions, if any of such exists in the analyzed model. For each test case, the running time and response of the constraint solver were recorded. Also, if the model was satisfiable, the running time of the Solution2SosADL generator was also recorded. In particular, only the first solution returned by the solver is translated into a SosADL model. Thereby, even if an analysis scope contains more than one solution, only the first solution returned by the solver is considered for the determination of productivity.

Step 4: Evaluate Candidate Concrete Architectures for URM

Finally, in the fourth and final step of Ark, the subject can evaluate generated concrete architectures in order to check the suitability of this concrete architecture in regards to one's original intent when designing the abstract coalition type in the first step. For instance, the subject can use generated concrete architectures as input for simulations of this SoS. Then, based on the outcome of this analysis, the subject may want to modify the bindings described in the abstract architecture to prevent the formation of a particular kind of coalition or accept this abstract architecture, hence proceeding to next stage of development. Despite its relevance, this activity is out of the scope of this quasi-experiment.

Analysis and Interpretation of Results

From all 396 test cases, only one (n. 108) did not terminate correctly due to lack of memory. For all other cases, the constraint solver was able to produce a response under the predefined time limit of five minutes. Moreover, the evaluated coalition type was considered as unsatisfiable in 237 cases (i.e., 60%) and as satisfiable in 158 cases (i.e, 40%). Raw data collected in this quasi-experiment is presented in Appendix B. Following, the results of the analysis performed over these data are discussed. First, Table 19 summarizes the descriptive statistics for dependable variables running time of solver, running time of transformation, and productivity (LOC/min). In particular, productivity is only calculated for satisfiable test cases since unsatisfiable or undetermined test cases generate no solution. The running time of the constraint solver shows great variation among test cases that have been evaluated, although none of them has taken longer than one minute to complete. Analyzing satisfiable and unsatisfiable test cases separately, it is possible to observe that the solver was at least three times faster to evaluate the latter (running time between 754ms minimum and 6861ms maximum) than the former (running time between 2591ms minimum and 42910ms maximum). Overall, the transformation of the solution back into SosADL is efficient once a solution for the architecture is found. Figure 14 shows the distribution of test cases for type of result (satisfiable or unsatisfiable) and maximum quantity of elements per signature. This analysis shows that only the scope of connections has a potential relation with the outcome of the solver, i.e., practically all test cases that assigned 10 or 11 connections to this signature evaluated the model as satisfiable. Indeed, there is only one test case that had 10 or 11 connections but it was evaluated as unsatisfiable. All other signatures, however, seem not to interfere with the outcome of the constraint solver. To evaluate the impact of a particular scope to the reliability of the method, the distribution of test results was analyzed in regards to the maximum number of elements per signature, shown in Figure 15. By selecting a scope that is too small, the constraint solver can fail to return an instance of the analyzed abstract coalition type, which is observed in Figure 15a and Figure 15b for a scope of three elements and a scope of eight or nine elements, respectively. A scope that has less than four elements for ArchitecturalElement is always unfeasible because this top level signature encompasses the ones of Sos, System, and Mediator and the model defines four elements of this type, namely sensor, gateway, transmitter, and FloodMonitoring. Hence, an analysis scope must have at least four elements of ArchitecturalElement. The fact that a particular scope for a signature presents mixed results also indicates that it is not determinant for the outcome. Conversely, by selecting a scope that is too large, the constraint solver can fail to return an instance within a feasible amount time. Nonetheless, it was not possible to further investigate this issue since all test cases finished under the time limit.

The productivity evaluation of SoSy is measured as the ratio between LOC of generated SosADL architectures and combined running time of the constraint solver and the Solution2SosADL transformation. The following analysis is focused on test cases that returned a solution, since the productivity of an unsatisfied test case is always zero (i.e., no architecture is generated). Figure 16 shows how different scopes for the signatures ArchitecturalElement, Port, and Connection, Unification are distributed in respect to productivity. The greatest productivity variation is observed in Figure 16a for the ArchitecturalElement signature, whose values are more scattered. It is important to point out that raw data collected in this experiment (presented in Appendix B on page 151) shows the same LOC for all satisfied test cases. This is due the fact that the solver automatically returns the smallest solution within the analyzed scope. Considering the design of this experiment, it follows that the productivity of a (combined) small scope is greater than the one of a (combined) large scope as it takes less time to perform an exhaustive analysis of the solution space. However, a larger scope might contain more than one solution, which are not taken into account in this measure. Therefore, it is not possible to conclude that the productivity of the tool is always better with a smaller scope, since only the first solution returned by the solver is transformed into SosADL.

Related Work

The method presented in this thesis is related to works that investigate constraint solving in the context of software architectures. [START_REF] Kezniki | Automated resolution of connector architectures using constraint solving (ARCAS method)[END_REF] use Alloy for automatically conceiving a connector instance configuration which determines how available elements can be composed together for realizing the architecture. Their approach takes into account nonfunctional properties, which describe structured/enumerated features, and roles for connectors. Their work, however, does not take into account the concept of coalition, which is covered in the approach developed in this thesis. Heyman, Scandariato and Joosen (2010) propose a metamodel of software architectures in terms of constraints, focusing on security aspect of these software architectures. Their metamodel is derived from the "4+1" Viewpoints (KRUCHTEN, 1995) realized with UML. Despite the relevance of UML for describing software systems, UML lacks important features for describing all relevant aspects of SoS, such as abstract types for mediators, coalitions, and dynamic properties (GUESSI; CAVALCANTE; OLIVEIRA, 2015).

The design and analysis of SoS is also the subject of international projects, such as COM-PASS 2 (Comprehensive Modelling for Advanced Systems of Systems) and DANSE (Designing for Adaptability and evolutioN in System of systems Engineering) 3 . DANSE employs SysML to the description of executable architectures that can be analyzed against interface contracts. The approach is aimed at supporting the generation of new architectures as well as generation of subsequent ones by means of transformation steps from its evolution. COMPASS develops a formal approach and applies CML (discussed in Table 20) for enriching the specification of systems and interfaces with contracts. One disadvantage of this approach is that an automatic transformation of SysML into CML can produce large, unreadable descriptions. [START_REF] Kenley | Synthesizing and Specifying Architectures for System of Systems[END_REF] defines a process for synthesizing SoS architectures. The authors refer to three different models of the SoS: a functional architecture, that establishes a flow for functions execution that facilitates to achieve a mission; a physical architecture, that defines a set of physical capabilities (e.g., sensors, databases, and communication links); and an allocated architecture, which attributes functional capabilities to physical components. According to this description, the purpose of functional and physical architectures is closer to the meaning of abstract architectures whilst an allocated architecture is closer to concrete architectures. The authors use a dynamics mode for the dynamic behavior of allocated architectures as input for an executable model that simulates its behavior. These executable models are implemented using Discrete Agent Framework (DAF) (MOUR et al., 2013), which is based on MATLAB. The task of creating allocated architectures is automated by a model builder developed in DAF that replaces explicit definitions of arrangements and interconnections by a physical network, which defines available point-to-point links, and an agent data path, which selects which constituents are to be connected. Assumptions and the link allocation algorithm are employed to tailor architectures according to architects preferences, e.g., by choosing faster physical links in place of the shortest path. Then, different techniques can be used, including UML activity diagrams for modeling the dynamics model and transforming then in Petri nets to create an executable model. Table 20 summarizes the characteristics of each related approach.

The method is also related to works that investigate the main concepts that are covered by a SoS architecture. [START_REF] Gonçalves | Towards a Conceptual Model for Software-Intensive System-of-Systems[END_REF] present a conceptual model of SoS that extends the ISO/IEC/IEEE 42010 (2011) standard with notions that are derived from the literature on SoS. In particular, their conceptual model defines purposes, stakeholders, and systems (i.e., constituents and the SoS itself) related to SoS. In turn, TASoS is a theory for describing SoS architectures •: supported, ∘: partially supported, -: not available as constraints. Besides covering the architectural elements presented by SosADL language, the model is implemented Alloy, hence enabling its automated analysis with constraint solving tools.

The method is also related to works that investigate formal architectural models for SoS. [START_REF] Baldwin | Modeling the characteristics of system of system[END_REF] use set theory for mathematically representing SoS characteristics by means of systems, goals, and actions. Autonomy is individually defined for each system as the cardinality of the set of actions that it contributes for achieving the SoS goals. Belonging is defined as the ratio between actions that a system contributes for the SoS goal and its autonomy. Still, systems can only participate in the SoS if their belonging is greater than a threshold, which is inversely proportional to their contributed value. Connectivity is enabled if two systems share at least one connector. Moreover, the connection is broken if any system contributes below the belonging threshold.Using agent-based modeling, they simulated if it is possible to dynamically create coalitions given constituents' autonomy, belonging, and connectivity. At the architectural level, however, their model lacks abstractions for describing interfaces, coalitions, and architectural configurations, which would enable to specify particular architectural styles for their interaction. [START_REF] Khlif | A multi-scale modelling perspective for SoS architectures[END_REF] focus on the decomposition and refinement of an SoS architecture expressed in SySML. In particular, their approach does not cover the topology of the architecture, i.e., how constituents and mediators are connected together, and possible modifications to the software architecture. In this scenario, SoSy enables to use Ark to automatically derive formal models that can be analyzed in constraint solving tools and analyze alternatice concrete architectures that can be realized from it.

Final Remarks

This chapter presented the results of a quasi-experiment that evaluates the effectiveness of Ark and its accompanying tool. This experiment showed that the tool can provide architects with a quick feedback on the soundness and correctness of the abstract architecture description. In particular, architects can use the tool to visualize potential instances of this description and, hence, decide in favor of refining or changing the policies that govern the formation of coalitions at run-time. The study also investigated the reliability and productivity of the method considering different scopes for analysis. This evaluation shows that a scope must be sufficiently large to encompass all possible extensions of a given signature. While it was not possible to conclude about the productivity of the tool, the study shows that it can automatically generate SosADL models that adhere with an abstract description. Motivated by these results, further studies can be conducted to investigate different scenarios and case objects.

Chapter 7

Conclusion

SoS are evolutionarily developed to achieve missions through emergent behaviors. In this context, a precise architectural description is important to better understand the particularities of SoS [START_REF] Dogan | Economic and Societal Significance of the Systems of Systems Research Agenda[END_REF], as well as enhance their perceived quality (PARNAS, 2010). However, a complete description of SoS architecture is often not possible since concrete systems that actually participate in a coalition could be not known in advance and, as a consequence, architectural configurations might change in unpredictable ways at run-time. While some studies address the architectural description of SoS (LANE; BOHN, 2012), some challenges still remain. For instance, well known ADLs that have been used in the description of SoS (GUESSI et al., 2015), such as UML and SysML, lack expressiveness for describing structural and behavior changes (GUESSI; CAVALCANTE; OLIVEIRA, 2015;[START_REF] Malavolta | What Industry Needs from Architectural Languages: A Survey[END_REF]. Therefore, this thesis applies a formal ADL to create partial descriptions (referred to as abstract architectures) of the SoS and its constituent systems. To guarantee the correctness and soundness of abstract architectures that are being designed for SoS, additional means must be put in place to verify that all possible concrete configurations that can be realized from it strictly conform to its original intent.

This thesis contributed in this direction, supporting the synthesis of SoS based on partial descriptions. Deliverables of this thesis encompass a method, supported by tailored techniques and tools, for the automated analysis of a normative description of the architecture of a SoS. In particular, this method takes advantage of constraint solving to perform an exhaustive, yet limited search for concrete architectures that adhere to such an abstract description. Thereby, it can be used to automatically analyze a comprehensive set of families of architectural configurations that can be realized at run-time. The remaining of this chapter is organized as follows. First, Section 7.1 revisits the main contributions of the thesis. Then, Section 7.2 discusses limitations of the method and techniques, detailing how these limitations could be overcome in future research. Finally, Section 7.3 presents possible extensions to this thesis that can further the contributions of this research.

Revisiting the Thesis Contributions

This thesis makes the following contributions: Definition of a theory for software architectures of SoS: we elaborated a conceptual model, named TASoS, for the elements framed in an abstract description of the SoS architecture. This conceptual model, presented in Chapter 4, maps most of the architectural elements of SosADL, a formal language presented in Section 2.3.3. In particular, this conceptual model supports the specification of coalitions, intentional bindings, and explicit configurations of SoS architectures in terms of constraints, i.e. Boolean expressions, that can be automatically analyzed by constraint solver tools. As a result, this formal model can be used to verify the correctness and completeness of a partial description of the SoS as well as obtain instances of this model for which all properties have been satisfied.

Definition of a method for the synthesis of concrete architectures: we elaborated a method, named Ark, to support the architectural synthesis of SoS based on abstract descriptions (presented in Chapter 3). This method details activities and artifacts that are required for realizing concrete architectures that comply with an abstract description. In particular, it comprises the specialization of the aforementioned conceptual model for the SoS under analysis. By incorporating constraint solving, this method will perform an exhaustive investigation of the solution space in order to produce a concrete architecture for which all constraints of the abstract architecture are satisfied. The method enables to verify the correctness and completeness of policies that constrain dynamic connectivity in abstract architectures.

Development of tool support: to facilitate the execution of the activities required by Ark, we developed a tool, named SoSy, that automates the main model transformations encompassed in the method (presented in Chapter 5). This tool is provided as part of a larger tool set that is tailored for the design and analysis of SoS in SosADL. In particular, the tool enables to automatically create an instance of the aforementioned conceptual model for the particular SoS under analysis and generate concrete architectures for this SoS based on solutions that were returned by the constraint solver. Thus, the tool supports the creation of intermediary and final artifacts required by Ark for the synthesis of concrete architectures that are correct-by-construction.

Experimental evaluation of the method: we evaluated the effectiveness of Ark and its accompanying tool, reported in Chapter 6. This quasi-experiment investigated the efficiency of Ark for checking the feasibility of concrete architectures for a urban river monitoring SoS described in SosADL considering different analyses scope. Results of this investigation indicate that there is a minimum scope for two of the four signatures analyzed in the scope range. The tool can also improve the productivity of architects by providing a quick feedback for the feasibility of the architecture The main advantage of the method and its accompanying tool is the automation of feasibility checks during the design of SoS abstract architectures. In other words, it allows to determine the existence of any concrete architecture that complies with a partial description without requiring an explicit description of its architectural configuration. Furthermore, the provided tool automates the transformations among abstract architectures, conceptual models, and concrete architectures, which can possibly reduce learning requirements for the adoption of this new technique. Thereby, the achievements of this thesis can contribute to the areas of Software Architecture and SoS, advancing the state of the art on architectural design and analysis of SoS based on formal methods.

Limitations and Future Work

This section describes limitations of this thesis and how these can be addressed in future research.

Expand the experiment: the evaluation of the effectiveness of Ark and its tool was based on one object case and one subject. We plan to expand this evaluation considering more object case. In particular, the experiment can consider several abstract architectures for each object, so as to obtain more data for the productivity of the method. Moreover, the experiment can investigate the impact of a larger analysis scope to memory consumption.

Overcome limitations in the experiment: the evaluation reported in Chapter 6 was unable to explore where the analyzed scope is unable to find a solution within the assigned time frame. We plan to repeat the previous experiment, considering a larger portion of the solution space. This new evaluation can also expand the current measure for productivity, taking into account generated source code of all possible solutions found by the constraint solver within the analyzed scope.

Evaluate Ark in a case study: the experiment reported in this thesis focuses on the perspective of one subject that executes generated Java classes with different analyses scope. In future work, we plan to perform a case study to investigate the perspective of multiple subjects that use Ark as part of their regular activities for architecting SoS in SosADL. This study can compare, for instance, how much time and effort incurs from revising an abstract architecture with and without the support of Ark and its accompanying tool.

Evaluate concrete architectures: although Ark contains a step for the evaluation of generated architecture for SoS, this activity is out of the scope of the experiment reported in Chapter 6.

In future work, we intend to individually assess alternative concrete architectures realized with the support of SoSy.

Possible Extensions

Several opportunities of research emerge to further the achievements of this thesis. Following, three of these opportunities are described.

Improve the description of bindings in SosADL: as SoSy automatically generates an instance of TASoS for a SosADL model, it translates intentional bindings of an abstract architecture as a set of constraints. Nonetheless, the way in which constraints can be nested in SosADL may impact the performance of the constraint solver. Therefore, a first extension to this thesis encompasses the investigation of how bindings can be described in SosADL to improve the efficiency of the constraint solver.

Integrate SoSy with an approach for SoS simulation: the outcome generated by the SoSy tool can be used as input to an approach that simulates the behavior of coalitions formed at run-time. Hence, a second extension to this thesis concerns the integration of SoSy to such an approach. For instance, SoSy can be modified to customize generated concrete architectures, e.g. passing specific values to be evaluated in a simulation.

Define concrete architectures as partial instances: the theory for SoS presented in this thesis is based on abstract architecture descriptions. To check the feasibility of concrete architectures requires a new theory that accepts the description of partial instances, in which part of the solution is provided as input to the constraint solver. Hence, future research focused on resolving partial instances of a concrete architecture can complement the Ark method by enabling to verify the feasibility of concrete architectures as well. compile Import Adds a reference to an imported library in the header of an instance module file.

compile Library Creates the main body of a library instance module, which consists of constraints on abstract types of systems and mediators.

compile SoS Creates the main body of an architecture instance module. Transforms an architecture declaration into an extension to the SoS signature of TASoS. Also, it defines a scenario that must be checked (which lists constituents of the architecture) and the analysis scope for the execution of a constraint solver, which is given by the runargs global variable.

compile EntityBlock Defines the structure of a library instance module, which is composed of the declaration of an entity block as a list of optional datatypes and functions followed by signatures and constraints related to systems and mediators.

compile DatatypeDecl Transforms the declaration of a SosADL datatype as a signature in Alloy.

compile FunctionDecl, AlloyType

Copies the declaration of a function to the description of concrete architectures. However, it is not part of an instance module file.

compile FormalParameter Copies the declaration of parameters passed to an entity block to the description of concrete architectures. However, it is not part of an instance module file.

compile SystemDecl Transforms a system declaration into an extension to the System signature of TASoS and calls the method that compiles gates. The behavior and assertion elements are not part of an instance module but they are copied to the description of concrete architectures. The method also adds a new type of system to the runargs global variable.

compile MediatorDecl Transforms a mediator declaration into an extension to the Mediator signature of TASoS and calls the method that compiles duties. The behavior, assumption, and assertion elements are not part of an instance module but they are copied to the description of concrete architectures. The method also adds a new type of mediator to the runargs global variable. compile

ArchitectureDecl, AlloyLibrary

Transforms an architecture declaration into an extension to the Mediator signature of TASoS and calls the method that compiles duties. The behavior, assumption, and assertion elements are not part of an instance module but they are copied to the description of concrete architectures. The method also adds a new type of architecture to the runargs global variable. compile GateDecl, String, AlloySystem

Transforms a gate declaration into an extension of the Gate signature of TASoS. It also attributes connections to gates and datatypes to these connections. The assertion block is not part of an instance module but it is copied to the description of concrete architectures.

It adds new type of gate to the runargs global variable. Level of contribution: Medium -the PhD candidate contributed to paper planning and writing.

Continued on next page

• Santos, J. F. M., Guessi, M., Galster, M., Feitosa, D., Nakagawa, E. Y. A Checklist for Evaluation of Reference Architectures for Embedded Systems. p. 451-454.

Event: 25th International Conference on Software Engineering and Knowledge Engineering (SEKE). Boston, United States, 2013.

Level of contribution: High -the PhD candidate contributed in the planning, execution, and reporting.

• Soares, D., Oliveira, B., Guessi, M., Oquendo, F., Delamaro, M. E., Nakagawa, E. Y.

Towards the Evaluation of System-of-Systems Software Architectures. p. 53-57.

Event: 8th Workshop de Desenvolvimento Distribuído de Software, Ecossistemas de Software e Sistemas de Sistemas (WDES), Maceió, Brazil, 2015.

Level of contribution: Medium -the PhD candidate contributed to paper planning and writing.

Figure 1 -Figure 2 -Figure 3 -Figure 5 -

 1235 Figure 1 -Architecture description conceptual model . . . . . . . . . . . . . . . . . . Figure 2 -General model of architectural design activities . . . . . . . . . . . . . . . Figure 3 -Wave model for engineering SoS . . . . . . . . . . . . . . . . . . . . . . . Figure 4 -A generic model transformation scenario . . . . . . . . . . . . . . . . . . .Figure 5 -Features of ADLs for SoS software architectures . . . . . . . . . . . . . . . Figure 6 -Instance of ISO/IEC/IEEE 42010 (2011) standard for SoS description . . . . Figure 7 -General model of Ark for SoS architectural synthesis . . . . . . . . . . . .Figure 8 -Example of a complete Alloy specification on the relation among views, viewpoints, concerns, and stakeholders . . . . . . . . . . . . . . . . . . . . Figure 9 -Elements of architecture descriptions for SoS . . . . . . . . . . . . . . . . .Figure 10 -Relationship between abstract and concrete architecture models in SosADL and TASoS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Figure 11 -Workflow of a model-driven process for the synthesis of concrete architectures Figure 12 -Activity detail diagram for the synthesis of concrete architectures in SosADE Figure 13 -Description of SosADL project content . . . . . . . . . . . . . . . . . . . . Figure 14 -Distribution of signature per satisfiability . . . . . . . . . . . . . . . . . . . Figure 15 -Distribution of test result per signature . . . . . . . . . . . . . . . . . . . . Figure 16 -Distribution of test productivity per signature . . . . . . . . . . . . . . . . . Figure 17 -User interface of SoSy . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 10 -

 10 Figure 1 -Architecture description conceptual model . . . . . . . . . . . . . . . . . . Figure 2 -General model of architectural design activities . . . . . . . . . . . . . . . Figure 3 -Wave model for engineering SoS . . . . . . . . . . . . . . . . . . . . . . . Figure 4 -A generic model transformation scenario . . . . . . . . . . . . . . . . . . .Figure 5 -Features of ADLs for SoS software architectures . . . . . . . . . . . . . . . Figure 6 -Instance of ISO/IEC/IEEE 42010 (2011) standard for SoS description . . . . Figure 7 -General model of Ark for SoS architectural synthesis . . . . . . . . . . . .Figure 8 -Example of a complete Alloy specification on the relation among views, viewpoints, concerns, and stakeholders . . . . . . . . . . . . . . . . . . . . Figure 9 -Elements of architecture descriptions for SoS . . . . . . . . . . . . . . . . .Figure 10 -Relationship between abstract and concrete architecture models in SosADL and TASoS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Figure 11 -Workflow of a model-driven process for the synthesis of concrete architectures Figure 12 -Activity detail diagram for the synthesis of concrete architectures in SosADE Figure 13 -Description of SosADL project content . . . . . . . . . . . . . . . . . . . . Figure 14 -Distribution of signature per satisfiability . . . . . . . . . . . . . . . . . . . Figure 15 -Distribution of test result per signature . . . . . . . . . . . . . . . . . . . . Figure 16 -Distribution of test productivity per signature . . . . . . . . . . . . . . . . . Figure 17 -User interface of SoSy . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

  AADL . . . . Architecture Analysis and Design Language ADL . . . . . Architectural Description Language ASR . . . . . Architecturally Significant Requirement CML . . . . . COMPASS Modeling Language CNF . . . . . Conjunctive Normal Form CP . . . . . . . Constraint Programming CPS . . . . . . Cyber-Physical System DEVS . . . . Discrete Event System Specification DSL . . . . . . Domain Specific Modeling Languages DSML . . . Domain Specific Modeling Languages EMF . . . . . Eclipse Modeling Framework FSA . . . . . . File System Access IDE . . . . . . Integrated Development Environment M2M . . . . . Model-to-Model M2T . . . . . Model-to-Text MDD . . . . . Model-Driven Development OCL . . . . . Object-Constraint Language OMG . . . . . Object Management Group OWL . . . . . Web Ontology Language RUP . . . . . Rational Unified Process SAT . . . . . . Satisfiability Problem SoS . . . . . . Systems-of-Systems SPEM . . . . Software and Systems Process Engineering Meta-Model Specification SysML . . . Systems Modeling Language T2M . . . . . Text-to-Model UML . . . . . Unified Modeling Language URI . . . . . . Uniform Resource Identifier URM . . . . . Urban River Monitoring VDM . . . . . Vienna Development Method WSMO . . . Web Service Modeling Ontology

  clarifies the relationship among the main elements of architecture descriptions, namely: Model kind: selects a set of techniques (e.g., metamodels, templates, languages, and operations) for creating architectural models from a particular viewpoint. Examples of model kinds are class diagrams, Petri nets, charts, among others; Architecture model: it uses the modeling conventions defined by a model kind for framing a particular set of concerns; Architecture viewpoint: it establishes the languages, notations, methods, and model kinds for creating, interpreting, and using architectural views; Architecture view: it expresses a particular software architecture from a given architecture viewpoint. Considering this definition, an abstract architecture and a concrete architecture can be regarded as two different views of software architectures; Architecture rationale: it adds explanations, reasoning, and implications of architecture decisions, such as considered alternatives, trade-offs, and consequences; Correspondence: it is a relation among architecture description elements. Examples of meaningful relations among architecture description elements are composition, refinement, consistency, traceability, dependency, constraint, and obligation;

Chapter 2 .Figure 1 -

 21 Figure 1 -Architecture description conceptual model Source: ISO/IEC/IEEE 42010 (2011).

2

 2

4

 4

5

  Compatibility properties verify whether components or connectors can collaborate to achieve the desired interactions (ZHANG; MUCCINI; LI, 2010).

Figure 2 -

 2 Figure 2 -General model of architectural design activities Source: Hofmeister et al. (2007).

Figure 3 -

 3 Figure 3 -Wave model for engineering SoS Source: Dahmann et al. (2011b).

Figure 4 -

 4 Figure 4 -A generic model transformation scenario Source: Royer and Arboleda (2012).

  6 MOF, <http://www.omg.org/mof/> 7 This literature review included 12 studies from 2002 to 2013 reporting on the use of MDD practices in SoS.

Chapter 2 .Figure 5 -

 25 Figure 5 -Features of ADLs for SoS software architectures Source: Guessi, Cavalcante and Oliveira (2015).

Chapter 2 .

 2 State of the Art on Architecture Description of Systems-of-Systems

Figure 6 -

 6 Figure 6 -Instance of ISO/IEC/IEEE 42010 (2011) standard for SoS description

Figure 7 -

 7 Figure 7 -General model of Ark for SoS architectural synthesis

1 7 b

 7 with C l i e n t S e r v e r D e f i n i t i o n s 2 s o s S e r v e r s X o r i s { 3 a r c h i t e c t u r e C o a l i t i o n ( ) i s { 4 gate u n u s e d G a t e i s { 5 connection u n u s e d C o n n e c t i o n i s i n { t } 6 } guarantee { p r o t o c o l a l l o w A l l i s { r e p e a t { a n y a c t i o n }}} f y one { c : : r r : : r e q } to one { s e r v e r 1 : : r r : : r e q } 15 and u n i f y one { s e r v e r 1 : : r r : : ack } to one { c : : r r : : ack } 16 ) xor ( 17 u n i f y one { c : : r r : : r e q } to one { s e r v e r 2 : : r r : : r e q } 18 and u n i f y one { s e r v e r 2 : : r r : : ack } to one { c : : r r : : ack }

1

  open t a s o s 2 open u t i l / o r d e r i n g [ t a s o s / A r c h i t e c t u r e ] as A0 3 open C l i e n t S e r v e r D e f i n i t i o n s 4 5 --A r c h i t e c t u r e ( s ) D e c l a r a t i o n ( s ) 6 s i g S e r v e r s X o r extends Sos {} 7 s i g C o a l i t i o n _ u n u s e d G a t e extends Gate {} 8 s i g C o a l i t i o n _ u n u s e d G a t e _ u n u s e d C o n n e c t i o n extends I n w a r d {} 9 10 . . .11 --c o n s t r a i n t s a b o u t c o n s t i t u e n t s i n s t a n c e s i n t h e c o a l i t i o n12 one s i g s e r v e r 1 extends s e r v e r {} 13 one s i g s e r v e r 2 extends s e r v e r {} 14 s i g c l i e n t s extends c l i e n t {} 15 16 --a b s t r a c t u n i f i c a t i o n s t h a t can e x i s t i n t h e a r c h i t e c t u r e 17 s i g C o a l i t i o n extends A r c h i t e c t u r e {}{ 18 a l l c : c l i e n t s | 19 ( ( ( u n i f y [ c l i e n t _ r r _ r e q&( c . ~owner ) , 20 s e r v e r _ r r _ r e q&( s e r v e r 1 . ~owner ) ] and 22 c l i e n t _ r r _ a c k&( c . ~owner ) ] ) n i f y [ c l i e n t _ r r _ r e q&( c . ~owner ) , 25 s e r v e r _ r r _ r e q&( s e r v e r 2 . ~owner ) ] and 26 u n i f y [ s e r v e r _ r r _ a c k&( s e r v e r 2 . ~owner ) , 27 c l i e n t _ r r _ a c k&( c . ~owner ) ] ) n i f y [ c l i e n t _ r r _ r e q&( c . ~owner ) , 31 s e r v e r _ r r _ r e q&( s e r v e r 1 . ~owner ) ] and 32 u n i f y [ s e r v e r _ r r _ a c k&( s e r v e r 1 . ~owner ) , 33 c l i e n t _ r r _ a c k&( c . ~owner ) ] ) 34 ) and 35 ( ( u n i f y [ c l i e n t _ r r _ r e q&( c . ~owner ) , 36 s e r v e r _ r r _ r e q&( s e r v e r 2 . ~owner ) ] and 37 u n i f y [ s e r v e r _ r r _ a c k&( s e r v e r 2 . ~owner ) , 38 c l i e n t _ r r _ a c k&( c . ~owner ) ] ) i n s t a n c e O f C o a l i t i o n } f o r 3 but 3 A r c h i t e c t u r e , 8 A r c h i t e c t u r a l E l e m e n t , 7 Port , 14 C o n n e c t i o n , 32 U n i f i c a t i o n , 3 R e l a y

3

  t a s o s / C o n n e c t i o n = { . . . } 4 t a s o s / C o n n e c t i o n <: owner = { . . . } 5 t a s o s / C o n n e c t i o n <: h a s D a t a t y p e = { . . . } 6 t a s o s / I n w a r d = { . . . } 7 t h i s / C o a l i t i o n _ u n u s e d G a t e _ u n u s e d C o n n e c t i o n = { . . . } 8 C l i e n t S e r v e r D e f i n i t i o n s / c l i e n t _ r r _ a c k = { . . . } 9 C l i e n t S e r v e r D e f i n i t i o n s / s e r v e r _ r r _ r e q = { . . . } 10 t a s o s / Outward = { . . . } 11 C l i e n t S e r v e r D e f i n i t i o n s / c l i e n t _ r r _ r e q = { . . . } 12 C l i e n t S e r v e r D e f i n i t i o n s / s e r v e r _ r r _ a c k = { . . . } 13 t a s o s / P o r t = { . . . } 14 t a s o s / Gate = { . . . } 15 t h i s / C o a l i t i o n _ u n u s e d G a t e = { . . . } 16 C l i e n t S e r v e r D e f i n i t i o n s / c l i e n t _ r r = { . . . } 17 t a s o s / Duty = { . . . } 18 C l i e n t S e r v e r D e f i n i t i o n s / s e r v e r _ r r = { . . . } 19 t a s o s / A r c h i t e c t u r a l E l e m e n t ={S e r v e r s X o r $ 0 , c l i e n t s $ 0 , c l i e n t s $ 1 , c l i e n t s $ 2 , c l i e n t s $ 3 , s e r v e r 1 $ 0 , s e r v e r 2 $ 0 } 20 t a s o s / A r c h i t e c t u r a l E l e m e n t <: h a s P o r t = { . . . } 21 t a s o s / Sos={ S e r v e r s X o r $ 0 } 22 t a s o s / Sos <: a r c h = { . . . } 23 t h i s / S e r v e r s X o r ={ S e r v e r s X o r $ 0 } 24 t a s o s / M e d i a t o r={ s e r v e r 1 $ 0 , s e r v e r 2 $ 0 } 25 C l i e n t S e r v e r D e f i n i t i o n s / s e r v e r ={ s e r v e r 1 $ 0 , s e r v e r 2 $ 0 } 26 t h i s / s e r v e r 1 = { . . . } 27 t h i s / s e r v e r 2 = { . . . }

1

  with A 1 _ S e r v e r s X o r _ l i b r a r y 2 s o s S e r v e r s X o r 0 i s { 3 a r c h i t e c t u r e C o a l i t i o n 0 ( ) i s { 4 gate u n u s e d G a t e 0 i s { 5 connection u n u s e d C o n n e c t i o n 0 i s i n { RangeType0 } f y one { s e r v e r 2 0 : : r r 0 : : ack0 } to one { c l i e n t s 0 : : r r 1 : : ack1 } and 20 u n i f y one { s e r v e r 1 0 : : r r 1 : : ack1 } to one { c l i e n t s 1 : : r r 0 : : ack0 } and 21

2

  Identifiers and commands are case sensitive in Alloy.Synthèse d'architectures logicielles pour systèmes-de-systèmes Milena Margarido 2017

Figure 8 -

 8 Figure 8 -Example of a complete Alloy specification on the relation among views, viewpoints, concerns, and stakeholders

1 : 2 : 4 :

 124 //#11 A l l P o r t s o f m e d i a t o r s a r e d u t i e s Mediator . hasPort i n Duty 3: //#12 A l l P o r t s o f c o n s t i t u e n t s a r e g a t e s System . hasPort i n Gate 5: //#13 A l l P o r t s o f s o s a r e g a t e s 6: Sos . hasPort i n Gate 7: //#14 A l l P o r t s owned by a g i v e n a r c h i t e c t u r a l element must have a t l e a s t one c o n n e c t i o n 8: a l l p : Port | some p . ~hasPort i m p l i e s 9: some p . hasConnection

2 :

 2 a l l r : Relay , c1 , c2 : Connection | 3: c1->c2 i n r . relayCon i m p l i e s { 4: a l l a : Architecture , s : Sos | a->r i n s . arch i m p l i e s 5: c2 . owner i n a . contain and c1 . owner = s 6: } 7: //#9 A l l c o n n e c t i o n s o f an Sos can be r e l a y e d to a t most c o n n e c t i o n p e r R e l a y s i g 8: a l l d i s j c ,c ': Connection , r : Relay | 9: c->c ' i n r . relayCon i m p l i e s 10: { no c ' ': Connection | c ' !=c ' ' and c '->c ' ' i n r . relayCon } 11: //#10 A c o n n e c t i o n can be r e l a y e d to a n o t h e r o f t h e same t y p e 12: a l l d i s j c1 , c2 : Connection , r : Relay | 13: c1->c2 i n r . relayCon i m p l i e s 14: ( c1+c2 ) i n Inward o r ( c1+c2 ) i n Outward 15: a l l u : Unification { 16: //#17 . 1 The domain o f an u n i f i c a t i o n i s an outward c o n n e c t i o n 17: u . src i n Outward 18: //#17 . 2 The image o f an u n i f i c a t i o n i s an inward c o n n e c t i o n 19: u . dest i n Inward 20: //#17 . 3-5 U n i f i c a t i o n s a r e a l l o w e d between e l e m e n t s o f System and Mediator 21: ( u . src . owner+u . dest . owner ) i n ( System+Mediator ) 22: u . src . owner i n System i m p l i e s u . dest . owner i n Mediator 23: u . src . owner i n Mediator i m p l i e s u . dest . owner i n System 24: } 25: //#18 Two u n i f i c a t i o n s a r e e q u a l i f t h e y r e l a t e t h e same p a i r o f c o n n e c t i o n s 26: a l l x , y : Unification | 27: ( x . src = y . src ) and ( x . dest = y . dest ) i m p l i e s x = y

Figure 9 -

 9 Figure 9 -Elements of architecture descriptions for SoS. While (b) is based on (a), (b) introduces a new element (colored green) to explicitly describe the configuration of concrete architectures.

Figure 10 -

 10 Figure 10 -Relationship between abstract and concrete architecture models in SosADL and TASoS

Figure 11 -

 11 Figure 11 -Workflow of a model-driven process for the synthesis of concrete architectures

3

  Figure 12 -Activity detail diagram for the synthesis of concrete architectures in SosADE

1 5 «

 5 o v e r r i d e def c o m p i l e ( SosADL s ) i l / o r d e r i n g [ t a s o s / A r c h i t e c t u r e ] a s A0 Source code 13 -Excerpt of the AlloyBound class 1 c l a s s A l l o y B o u n d { 2

2 v

 2 a r S t r i n g p r e d i c a t e 3 v a r S t r i n g r e l a t i o n 4 v a r i n t s r c S i z e // 1 i f e l e m e n t , 0 i f s e t 5 v a r i n t d e s t S i z e // 1 i f e l e m e n t , 0 i f s e t Synthèse d'architectures logicielles pour systèmes-de-systèmes Milena Margarido 2017 Chapter 5. Automated Synthesis of Systems-of-Systems Architectures def s e t P r e d i c a t e ( S t r i n g p r e d ) { t h i s . p r e d i c a t e = p r e d s w i t c h p r e d { . . . case ' a t t r i b u t e A r c h T o S o s ' : { t h i s . r e l a t i o n = S t r i n g ( L i s t <S t r i n g > s r c , L i s t <S t r i n g > d e s t ) { v a r S t r i n g o u t p u t = " " . . . // I f b o t h s r c and d e s t have e x a c t l y one e l e m e n t i f ( s r c S i z e == 1 && d e s t S i z e == 1 ) { s r c P a r a m s = ' ' ' «src.get(0)» ' ' ' d e s t P a r a m s = ' ' ' «dest.get(0)» ' ' ' } i f ( s r c . s i z e > 0 && d e s t . s i z e > 0

1 2 S 3 F 4 . . . 5 /6 7 « 8 ««

 234578 p u b l i c s t a t i c v o i d S o l u t i o n 2 S o s A D L G e n e r a t o r ( S t r i n g answer , S t r i n g p a t h ) t h r o w s E x c e p t i o n { t r i n g l i b r a r y = " " ; i l e s o l u t i o n L i b r a r y = new F i l e ( p a t h . c o n c a t ( " _ l i b r a r y . s o s a d l " ) ) ; / D e c l a r a t i o n o f d a t a t y p e s LinkedHashMap<S t r i n g , S t r i n g > f u n c t i o n s = new LinkedHashMap< S t r i n g , S t r i n g >() ; FOR elem: libs.entrySet» FOR t : elem.getValue.types.entrySet» 9 f o r ( S t r i n g d t : e l e m s . g e t ( " D a t a t y p e " FOR elem: abstractions.entrySet» 15 «FOR t : elem.getValue.typesMap.entrySet» 16 f o r ( S t r i n g d t : e l e m s . g e t ( " D a t a t y p e " ) ) { 17 S t r i n g aux = d t . s u b s t r i n g ( d t . l a s t I n d e x O f ( " / " ) +1) ; 18 «IF !t.value.functions.empty» Synthèse d'architectures logicielles pour systèmes-de-systèmes Milena Margarido 2017 r a r y += l e v e l ( 1 , " d a t a t y p e "+aux+" i s «t.value» " ) ; o n c r e t e d e c l a r a t i o n o f s y s t e m s f o r ( S t r i n g s y s : e l e m s . g e t ( " System " ) ) { «FOR elem: abstractions.entrySet» «IF elem.getValue.type==0» i f ( s y s . c o n t a i n s ( " «elem.getKey» " ) ) { l i b r a r y+=«elem.getKey» D e c l ( s y s ) o n c r e t e d e c l a r a t i o n o f m e d i a t o r s f o r ( S t r i n g med : e l e m s . g e t ( " M e d i a t o r " ) ) { «FOR elem: abstractions.entrySet» «IF elem.getValue.type==1» i f ( med . c o n t a i n s ( " «elem.getKey» " ) ) { l i b r a r y+=«elem.getKey» D e c l ( med ) r a r y = u p d a t e D a t a t y p e s ( l i b r a r y , f u n c t i o n s ) ; S t r i n g l i b D e c l = newBlock ( " l i b r a r y «nameClass» _ l i b r a r y i s " , 0 , l i b r a r y ) ;

  Figure 13 -Description of SosADL project content

1

  l i b r a r y C l i e n t S e r v e r D e f i n i t i o n s i s { 2 datatype t i s i n t e g e r { 0 . . 0 } { 3 f u n c t i o n ( s e l f : t ) : : f ( ) : t i s { . . . } r r : : r e q r e c e i v e v 26 v i a r r : : ack send v : : f ( )

1 8 } 17 f 23 )and 25 ( 3 a 5 }

 817232535 with C l i e n t S e r v e r D e f i n i t i o n s 2 s o s C l i e n t T o S i n g l e S e r v e r i s { 3 a r c h i t e c t u r e C o a l i t i o n ( ) i s { 4 gate u n u s e d G a t e i s { . . . } 5 b e h a v i o r main i s compose { 6 s e r v e r s i s s e q u e n c e { s e r v e r } 7 c l i e n t s i s s e q u e n c e { c l i e n t } b i n d i n g { 9 // e v e r y c l i e n t i s c o n n e c t e d t o a t l e a s t one s e r v e r 10 f o r a l l { c i n c l i e n t s suchthat 11 e x i s t s { s i n s e r v e r s suchthat 12u n i f y one { c : : r r : : r e q } to one { s : : r r : : r e q } 13 and u n i f y one { s : : r r : : ack } to one { c : : r r : : ack } v e r y c l i e n t t a l k s t o a t most one s e r v e r one { c : : r r : : r e q } to one { s 1 : : r r : : r e q } 22 or u n i f y one { s 1 : : r r : : ack } to one { c : : r r : : ack } 24 // c t a l k s t o s 2 26 u n i f y one { c : : r r : : r e q } to one { s 2 : : r r : : r e q } 27 or u n i f y one { s 2 : : r r : : ack } to one { c : : r r : Source code 18 -Excerpt of coalition type for well-formed client-server architectures expressed in SosADL 1 with C l i e n t S e r v e r D e f i n i t i o n s 2 s o s C l i e n t T o S i n g l e S e r v e r i s { r c h i t e c t u r e C o a l i t i o n ( ) i s { 4 gate u n u s e d G a t e i s { . . . guarantee { . . . } 6 b e h a v i o r main i s compose { 7 s e r v e r s i s s e q u e n c e { s e r v e r } 8 c l i e n t s i s s e q u e n c e { c l i e n t } 9 } b i n d i n g { 10 f o r a l l { c i n c l i e n t s suchthat 11 f o r a l l { s i n s e r v e r s suchthat 12 // c-s c o n n e c t e d v i a r e q <=> c-s c o n n e c t e d v i a ack 13 u n i f y one { c : : r r : : r e q } to one { s : : r r : : r e q } 14 = u n i f y one { s : : r r : : ack } to one { c : : r r : : ack } 15

  measure r e c e i v e any 14 r e p e a t { a n y a c t i o n } 15 } 16 v i a a l e r t send any Synthèse d'architectures logicielles pour systèmes-de-systèmes Milena Margarido 2017 a l e r t i n g : : measure r e c e i v e v 24 i f ( v > d e p t h t h r e s h o l d ) then { 25 v i a a l e r t i n g : : a l e r t send v

  t o c o l m e a s u r i n g p a c t i s { 36 r e p e a t { 37 v i a s e n s e r e c e i v e o b s e r v a t i o n 38 r e p e a t { a n y a c t i o n } 39 v i a measure send o b s e r v a t i m e a s u r i n g : : s e n s e r e c e i v e o b s e r v a t i o n v i a m e a s u r i n g : : measure send o b s e r v a t i o n } or { v i a p a s s i n g : : p a s s r e c e i v e d a t a v i a p a s s i n g : : measure send d a

Source code 23 -

 23 Architecture instance module of TASoS for URM 1 open t a s o s 2 open u t i l / o r d e r i n g [ t a s o s / A r c h i t e c t u r e ] as A0 3 open u r m L i b r a r y 4 /* * A r c h i t e c t u r e ( s ) D e c l a r a t i o n ( s ) 5 */ 6 s i g F l o o d M o n i t o r i n g extends Sos {} 7 s i g s i m p l e _ s e r v i n g extends Gate {} 8 s i g s i m p l e _ s e r v i n g _ r e q u e s t extends I n w a r d {} 9 s i g s i m p l e _ s e r v i n g _ a l e r t extends Outward {} 10 --c o n s t r a i n t s a b o u t t h e s t r u c t u r e o f t h e a r c h i t e c t u r a l e l e m e n t 11 f a c t { 12 a t t r i b u t e P o r t T o A E [ s i m p l e _ s e r v i n g , F l o o d M o n i t o r i n g ] 13 a l l c : F l o o d M o n i t o r i n g | 14 one p1 : s i m p l e _ s e r v i n g | 15 p1 i n c . h a s P o r t 16 a t t r i b u t e C o n T o P o r t [ s i m p l e _ s e r v i n g _ r e q u e s t+s i m p l e _ s e r v i n g _ a l e r t , s i m p l e _ s e r v i n g ] 17 a l l c : s i m p l e _ s e r v i n g | 18 one p1 : s i m p l e _ s e r v i n g _ r e q u e s t , p2 : s i m p l e _ s e r v i n g _ a l e r t | 19 p1 i n c . h a s C o n n e c t i o n and p2 i n c . h a s C o n n e c t i o n 20 a t t r i b u t e D a t a t y p e T o C o n [ t , s i m p l e _ s e r v i n g _ r e q u e s t ] 21 a l l c : s i m p l e _ s e r v i n g _ r e q u e s t | 22 one p1 : t | 23 p1 i n c . h a s D a t a t y p e 24 a t t r i b u t e D a t a t y p e T o C o n [ t , s i m p l e _ s e r v i n g _ a l e r t ] 25 a l l c : s i m p l e _ s e r v i n g _ a l e r t |

1 3 a 25 }

 325 with u r m _ l i b r a r y 2 s o s F l o o d M o n i t o r i n g 0 i s { r e q u e s t 0 r e c e i v e l o c a t i o n 11 r e p e a t { a n y a c t i o n } L i b r a r y / gateway0 i s u r m L i b r a r y / gateway0 19 t r a n s m i t t e r s 0 i s t r a n s m i t t e r s 0 20 } b i n d i n g { 21u n i f y one { t r a n s m i t t e r s 0 : : t r a n s m i t t i n g 0 : : toGateway0 } to 22 one { u r m L i b r a r y / gateway0 : : a l e r t i n g 0 : : r e q u e s t 0 } and 23 u n i f y one { gateway10 : : a l e r t i n g 1 : : a l e r t 1 } to 24 one { t r a n s m i t t e r s 0 : : t r a n s m i t t i n g 0 : : f r o m S e n s o r s 0 } Synthèse d'architectures logicielles pour systèmes-de-systèmes Milena Margarido 2017 } 27 }

Figure 14 -

 14 Figure 14 -Distribution of signature per satisfiability

Figure 15 -

 15 Figure 15 -Distribution of test result per signature

2 COMPASS

 2 , <www.compass-research.eu> 3 DANSE, <www.danse-ip.eu>

  Synthèse d'architectures logicielles pour systèmes-de-systèmes Milena Margarido 2017 TASoS Source code 25 presents the source code for the conceptual model describing SoS architectures in Alloy that is discussed in more detail in Chapter 4. Source code 25 -TASoS source code 1 module t a s o s 2 open u t i l / o r d e r i n g [ A r c h i t e c t u r e ] as A0 3 a b s t r a c t s i g D a t a t y p e {} 4 a b s t r a c t s i g I n t e g e r T y p e , NamedType , SequenceType , RangeType extends D a t a t y p e {} 5 a b s t r a c t s i g TupleType extends D a t a t y p e { 6 complexType : s e t D a t a t y p e 7 } 8 f a c t D a t a t y p e f a c t { 9 // #1 A l l D a t a t y p e must be r e l a t e d t o one c o n n e c t i o n 10 a l l d : D a t a t y p e | some {d . ~h a s D a t a t y p e } 11 } 12 a b s t r a c t s i g C o n n e c t i o n { 13 owner : one A r c h i t e c t u r a l E l e m e n t , // #2 A l l C o n n e c t i o n s a r e owned by one AE 14 h a s D a t a t y p e : one D a t a t y p e 15 } 16 f a c t C o n n e c t i o n F a c t { 17 // #3 A l l C o n n e c t i o n s have e x a c t l y one D a t a t y p e and a l l D a t a t y p e s a r e r e l a t e d t o some C o n n e c t i o n 18 h a s D a t a t y p e i n C o n n e c t i o n some -> one D a t a t y p e 19 // #4 A l l C o n n e c t i o n s map t o e x a c t l y one AE 20 a l l c : C o n n e c t i o n | c . owner = h a s P o r t . h a s C o n n e c t i o n . c 21 } 22 a b s t r a c t s i g Inward , Outward extends C o n n e c t i o n {} // There i s no o v e r l a p p i n g between i n o r o u t c o n n e c t i o n s C o n n e c t i o n p e r t a i n s t o a t most one P o r t s o t h a t we can add new c o n n e c t i o n s t o a p o r t 28 h a s C o n n e c t i o n i n P o r t l o n e -> s e t C o n n e c t i o n 29 } 30 a b s t r a c t s i g Gate , Duty extends P o r t {} // There i s no o v e r l a p p i n g between g a t e s and d u t i e s h a s P o r t : s e t P o r t } // There i s no o v e r l a p i n g between S y s t e m s and M e d i a t o r s a b s t r a c t s i g System , M e d i a t o r extends A r c h i t e c t u r a l E l e m e n t {} a b s t r a c t s i g Sos extends A r c h i t e c t u r a l E l e m e n t { a r c h : A r c h i t e c t u r e some -> some R e l a y } a b s t r a c t s i g R e l a y { r e l a y C o n : C o n n e c t i o n s e t -> s e t C o n n e c t i o n } f a c t { // E v e r y Sos s i g i s r e l a t e d t o one o r more a r c h i t e c t u r e s and r e l a y c o n n e c t i o n s a l l s : Sos | some a : A r c h i t e c t u r e , r : R e l a y | a -> r i n s . a r c h // E v e r y R e l a y s i g i s r e l a t e d t o one o r more a r c h i t e c t u r e s a l l r : R e l a y | some s : Sos , a : A r c h i t e c t u r e | a -> r i n s . a r c h // Two R e l a y s i g s a r e t h e same i f t h e y s h a r e t h e same r e l a y c o n n e c t i o n s a l l r1 , r 2 : R e l a y | r 1 . r e l a y C o n = r 2 . r e l a y C o n i m p l i e s r 1=r 2 // R e l a y u n i f i c a t i o n s r e q u i r e some c o n s t i t u e n t i n t h e a r c h i t e c t u r e a l l r : R e l a y , c1 , c2 : C o n n e c t i o n | c1->c2 i n r . r e l a y C o n i m p l i e s { a l l a : A r c h i t e c t u r e , s : Sos | a->r i n s . a r c h i m p l i e s c2 . owner i n a . c o n t a i n and c1 . owner=s } // A l l c o n n e c t i o n s o f an Sos e n g a g e i n a t most one r e l a y u n i f i c a t i o n p e r R e l a y s i g a l l c : C o n n e c t i o n , s : Sos , r : R e l a y | c . owner = s and c i n i n R e l a y [ r ] i m p l i e s { a l l a : A r c h i t e c t u r e | a->r i n s . a r c h i m p l i e s {one c ' : C o n n e c t i o n | c ' i n a . c o n t a i n . h a s P o r t . h a s C o n n e c t i o n and c->c ' i n r . r e l a y C o n } } // A c o n n e c t i o n p a r t i c i p a t e s i n a R e l a y u n i f i c a t i o n i f i t i s o f t h e same t y p e a l l c1 , c2 : C o n n e c t i o n , r : R e l a y | c1->c2 i n r . r e l a y C o n i m p l i e s ( c1+c2 ) i n I n w a r d or ( c1+c2 ) i n Outward } f a c t AEFact { // #10 A l l P o r t s o f m e d i a t o r s a r e d u t i e s M e d i a t o r . h a s P o r t i n Duty // #11 A l l P o r t s o f c o n s t i t u e n t s a r e g a t e s System . h a s P o r t i n Gate // #12 A l l P o r t s o f s o s a r e g a t e s Sos . h a s P o r t i n Gate // #12 A l l P o r t s owned by a g i v e n a r c h i t e c t u r a l e l e m e n t must ha ve a t l e a s t one c o n n e c t i o n . a l l p : P o r t | some {p . ~h a s P o r t } i m p l i e s some {p . h a s C o n n e c t i o n } // # 13 A l l S y s t e m s must p a r t i c i p a t e i n some A r c h i t e c t u r e a l l e : System | some c : A r c h i t e c t u r e | e i n c . c o n t a i n // # 14 Any two s o s a r e e q u i v a l e n t i f t h e y p r e s e n t t h e same a r c h -> r e l a y r e l a t i o n s h i p s a l l s1 , s 2 : Sos | g e t A r c h [ s 1 ] = g e t A r c h [ s 2 ] i m p l i e s s 1 = s 2 } a b s t r a c t s i g U n i f i c a t i o n { //An U n i f i c a t i o n b i n d s c o n n e c t i o n s among a r c h i t e c t u r a l e l e m e n t s s r c : one C o n n e c t i o n , // Outward d e s t : one C o n n e c t i o n // I n w a r d } f a c t U n i f i c a t i o n F a c t { // #14 G e n e r a l p r o p e r t i e s o v e r t h e domain and image o f U n i f i c a t i o n s a l l u : U n i f i c a t i o n { u . s r c i n Outward // #14 . 1 The domain o f an u n i f i c a t i o n i s i n t h e s e t o f o u tw a r d c o n n e c t i o n s u . d e s t i n I n w a r d // #14 . 2 The image o f an u n i f i c a t i o n i s i n t h e s e t o f i n w a r d c o n n e c t i o n s u . s r c . owner != u . d e s t . owner // #14 . 3 An u n i f i c a t i o n may o n l y u n i f y c o n n e c t i o n s between d i f f e r e n t AEs // #14 . 4 U n i f i c a t i o n s a r e a l l o w e d between e l e m e n t s o f System and e l e m e n t s o f M e d i a t o r e x c l u s i v e l y u . s r c . owner i n System i m p l i e s u . d e s t . owner i n M e d i a t o r u . s r c . owner i n M e d i a t o r i m p l i e s u . d e s t . owner i n System // #14 . 5 A c o n n e c t i o n can o n l y e n g a g e i n an u n i f i c a t i o n i f i t i s owned by some AE some u . s r c . owner some u . d e s t . owner } // #15 A l l U n i f i c a t i o n s a r e u n i q u e , t h e r e a r e no two u n i f i c a t i o n s t o t h e same i n * and * o u t c o n n e c t i o n s // However , we can hav e u n i f i c a t i o n s t h a t s h a r e one o f t h e c o n n e c t i o n s a l l x , y : U n i f i c a t i o n | ( x . s r c = y . s r c ) and ( x . d e s t = y . d e s t ) i m p l i e s x=y // #16 There i s up t o one u n i f i c a t i o n p e r c o n n e c t i o n i n any g i v e n t o p o l o g y a l l t : Topology , c : C o n n e c t i o n | l e t s P o r t = p o r t s O f U n i f i c a t i o n [ t . i n T o p o l o g y ] | c i n s P o r t . h a s C o n n e c t i o n i m p l i e s { l o n e u : U n i f i c a t i o n | u i n t . i n T o p o l o g y and { c = u . s r c or c h i s s i g n a t u r e r e p r e s e n t s t h e a r c h i t e c t u r a l c o n f i g u r a t i o n o f an SoS , i . e . , t h e way // i n w h i c h i t s c o n s t i t u e n t s and m e d i a t o r s a r e a s s e m b l e d t o g e t h e r i n T o p o l o g y : s e t U n i f i c a t i o n , p a t h : U n i f i c a t i o n s e t -> s e t U n i f i c a t i o n } f a c t T o p o l o g y F a c t { // #17 A p a i r o f u n i f i c a t i o n may p e r t a i n t o a g i v e n t o p o l o g y ' s p a t h i f t h e y a r e d i f f e r e n t . // T h i s p a t h r e l a t i o n i s b i d i r e c t i o n a l . a l l u , v : U n i f i c a t i o n , t : T o po log y | u -> v i n t . p a t h i m p l i e s u != v and v -> u i n t . p a t h // #18 A l l u n i f i c a t i o n s i n t h e r e l a t i o n p a t h e x i s t i n t h e r e l a t i o n i n T o p o l o g y a l l t : T o p o l o g y | { ( t . p a t h ) . U n i f i c a t i o n + U n i f i c a t i o n . ( t . p a t h ) } = t . i n T o p o l o g y // #19 Two t o p o l o g i e s a r e e q u a l i f t h e y s h a r e t h e same p a i r o f u n i f i c a t i o n s . A l s o a p p l i e s t o empty t o p o l o g i e s . a l l t , t ' : T o p o l o g y | t . p a t h = t ' . p a t h i m p l i e s t = t ' } a b s t r a c t s i g A r c h i t e c t u r e { // T h i s s i g n a t u r e c o n t a i n s t h e c o n s t i t u e n t s o f t h e SoS . Each s e t o f c o n s t i t u e n t s can // be a s s e m b l e d i n d i f f e r e n t ways . T h e r e f o r e , e a c h c o a l i t i o n can be r e l a t e d t o d i f f e r e n t t o p o l o g i e s c o n t a i n : s e t System , b i n d i n g s : s e t U n i f i c a t i o n , u n i f i e d A s : seq T o p o l o g y } f a c t A r c h i t e c t u r e F a c t { c o n t a i n i n A r c h i t e c t u r e some -> s e t System // #20 A l l s y s t e m s Synthèse d'architectures logicielles pour systèmes-de-systèmes Milena Margarido 2017 must be r e l a t e d t o a t l e a s t one A r c h i t e c t u r e b i n d i n g s i n A r c h i t e c t u r e some -> s e t U n i f i c a t i o n // #21 A l l U n i f i c a t i o n must be r e l a t e d t o a t l e a s t one A r c h i t e c t u r e // #22 A t o p o l o g y may o n l y u s e t h e u n i f i c a t i o n s t h a t e x i s t i n t h e s e t o f p o s s i b l e b i n d i n g s and c o n n e c t t h e s y s t e m s t h a t p a r t i c i p a t e i n t h e a r c h i t e c t u r e a l l t : Topology , a : A r c h i t e c t u r e | t i n ( a . u n i f i e d A s ) . e l e m s i m p l i e s t . i n T o p o l o g y i n a . b i n d i n g s and ( i s U n i f i e d T o [ t . i n T o p o l o g y ] & System ) = a . c o n t a i n // Obs : T h i s c o n d i t i o n a l o n e d o e s n o t c o n s t r a i n t t h a t c o n s t i t u e n t s form a c o n n e c t e d t o p o l o g y . // #23 A T o p o l o g y i s r e l a t e d t o a t l e a s t one a r c h i t e c t u r e // I f we do n o t add t h i s r u l e , i t i s p o s s i b l e t o hav e a t o p o l o g y t h a t i s r e l a t e d t o no a r c h i t e c t u r e a l l t : T o p o l o g y | some a : A r c h i t e c t u r e | t i n ( a . u n i f i e d A s ) .e l e m s // #24 An A r c h i t e c t u r e i s r e l a t e d t o a t l e a s t one t o p o l o g y a l l a : A r c h i t e c t u r e | {some ( a . u n i f i e d A s ) . e l e m s } // #25 Two c o a l i t i o n s s h o u l d be e q u a l i f t h e y have t h e same s e t o f t o p o l o g i e s a l l a , a ' : A r c h i t e c t u r e | ( a . u n i f i e d A s ) . e l e m s = ( a ' . u n i f i e d A s ) . e l e m s i m p l i e s a=a ' // #26 The r e l a t i o n s i n T o p o l o g y and p a t h a r e empty i f no s y s t e m p a r t i c i p a t e s i n t h e c o a l i t i o n a l l t : Topology , a : A r c h i t e c t u r e | t i n ( a . u n i f i e d A s ) . e l e m s i m p l i e s { {no t . p a t h } and {no t . i n T o p o l o g y } i f f {no a . c o n t a i n } } // #27 For a l l t o p o l o g i e s o f an a r c h i t e c t u r e , a m e d i a t o r e n g a g e s i n a t l e a s t one u n i f i c a t i o n a l l t : Topology , m: M e d i a t o r | l e t S u n i = p a r t i c i p a t e s I n T o p o l o g y [m, t ] | --r e t u r n s t h e s e t o f u n i f i c a t i o n s i n t o f which m p a r t i c i p a t e s {m i n p a r t i c i p a t e s I n T o p o l o g y [ t ] } i m p l i e s m i n owner [ S u n i . s r c ] or m i n owner [ S u n i . d e s t ] // #28 A l l s y s t e m s t h a t p a r t i c i p a t e i n an a r c h i t e c t u r e must be b i n d e d by a t l e a s t one u n i f i c a t i o n i n a l l o f i t s t o p o l o g i e s a l l e : System , a : A r c h i t e c t u r e , t : To pol ogy | e i n a . c o n t a i n and t i n ( a . u n i f i e d A s ) . e l e m s i m p l i e s { some u : U n i f i c a t i o n | e i n i s U n i f i e d T o [ u ] and u i n t . i n T o p o l o g y } // #29 The p a t h o f a t o p o l o g y c o n n e c t s u n i f i c a t i o n s t h a t ha ve // A#4 Checks i f a l l b i n d i n g s o f a c o a l i t i o n a p p e a r i n a t l e a s t one o f i t s t o p o l o g i e s a s s e r t a l l B i n d i n g s A r e U s e d { a l l a : A r c h i t e c t u r e , u : U n i f i c a t i o n | u i n a . b i n d i n g s i m p l i e s { some t : T o p o l o g y | t i n a . u n i f i e d A s . e l e m s and u i n i n T o p o l o g y [ l B i n d i n g s A r e U s e d f o r 8 // A#5 Checks i f a c o a l i t i o n can have more t h a n two m e d i a t o r s a s s e r t moreThanOneMediator { no d i s j m,m' : M e d i a t o r , t : To pol ogy | l e t Smed = p a r t i c i p a t e s I n T o p o l o g y [ t ] | m i n Smed and m' i n Smed } check moreThanOneMediator f o r 7 but 3 Topology , 3 A r c h i t e c t u r e , 8 Port , 12 C o n n e c t i o n --s h o u l d be v a l i d when t h e e x e c u t i o n bound i s s u f f i c i e n t l y b i g . // A#6 Checks i f a c o n s t i t u e n t can be b i n d e d t o more t h a n two m e d i a t o r s a s s e r t moreThanOneMediatorPerSystem { --some t : Topology , d i s j m,m' : M e d i a t o r | l e t Smed = p a r t i c i p a t e s I n T o p o l o g y [ t ] | m i n Smed and m' i n Smed and some { i s M e d i a t e d B y [m, t ]&i s M e d i a t e d B y [m' , t ] } a l l t : T o p o l o g y | l e t Smed = p a r t i c i p a t e s I n T o p o l o g y [ t ] | no d i s j m,m' : M e d i a t o r | m i n Smed and m' i n Smed and { i s M e d i a t e d B y [m, t ]= i s M e d i a t e d B y [m' , t ] } } check moreThanOneMediatorPerSystem f o r 6 but 2 A r c h i t e c t u r e , 2 Topology , 10 Port , 4 System , 10 C o n n e c t i o n , 10 U n i f i c a t i h i s s e t o f a s s e r t i o n s c o v e r s d i f f e r e n t a s p e c t s o f t h e dynamic s u p p o r t r e q u i r e d by SoS , s u c h a s a d d i t i o n , d e l e t i o n , // o r m o d i f i c a t i o n o f a r c h i t e c t u r a l e l e m e n t s // A#7 Checks i f c o n s t i t u e n t s can e n t e r / l e a v e t h e a r c h i t e c t u r e ( w h i c h i s i n d i c a t e d a s a new i n s t a n c e o f t h e a r c h i t e c t u r e ) a s s e r t c a n t M o d i f y S y s t e m s I n A r c h i t e c t u r e { no a , a ' : A r c h i t e c t u r e , s : System | s i n a . c o n t a i n and s not i n a ' . c o n t a i n } check c a n t M o d i f y S y s t e m s I n A r c h i t e c t u r e f o r 8 --T h i s a s s e r t i o n

Table 2 -

 2 Boolean logic operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . Design time features for describing SoS architectures in UML . . . . . . . .

Table 3 -

 3 Design time features for realizing SoS architectural description in UML, SysML, and X-UNITY . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Table 4 -

 4 Architectural elements supported by the SosADL language . . . . . . . . .

Table 5 -

 5 Summary of classic architecture frameworks in the literature . . . . . . . . .

Table 6 -

 6 Outline of activities in the Ark method . . . . . . . . . . . . . . . . . . . .

Table 7 -

 7 Notations for the description of abstract architectures, concrete architectures, and conceptual models . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Table 8 -

 8 Commands of operators and quantifiers supported by Alloy . . . . . . . . . .

Table 9 -

 9 SosADL support for SoS characteristics . . . . . . . . . . . . . . . . . . . . Table 10 -Signatures and relations defined by TASoS . . . . . . . . . . . . . . . . . . Table 11 -Summary of assertions included in TASoS . . . . . . . . . . . . . . . . . . .

Table 12 -

 12 Predicates for customization of TASoS . . . . . . . . . . . . . . . . . . . .

Table 13 -

 13 Mapping between SosADL and TASoS . . . . . . . . . . . . . . . . . . . .

Table 14 -

 14 Classes in the SosADL2AlloyGenerator file . . . . . . . . . . . . . . . . .

Table 15 -

 15 Use of predicates for the customization of instances of TASoS . . . . . . . .

Table 16 -

 16 Overview of SoSy performance . . . . . . . . . . . . . . . . . . . . . . . .

Table 17 -

 17 Description of experiment variables . . . . . . . . . . . . . . . . . . . . . .

Table 18 -

 18 Variation of analyzed scope . . . . . . . . . . . . . . . . . . . . . . . . . .

Table 19 -

 19 Descriptive statistics of dependent variables . . . . . . . . . . . . . . . . . .

Table 20 -

 20 Comparison of model-based approaches for SoS architectural synthesis . . .

Table 21 -

 21 Methods in the SosADL2AlloyGenerator class . . . . . . . . . . . . . . . .

Table 22 -

 22 Raw data collected in quasi-experiment . . . . . . . . . . . . . . . . . . . .

Table 1 -

 1 Boolean logic operators Conjunction (read x n AND x m must be true)x n ∨ x m Disjunction (read either x n OR x m must be true)

	Operator Description
	xn	Negation (read NOT x n )
	x n ∧ x m

Table 2 -

 2 Design time features for describing SoS architectures in UML

	Element	Feature	Diagram
		Abstract type	Class diagram
		Interface	Class diagram
	Constituent	Semantics Constraint	State machine or sequence diagram OCL expressions
		Mission	Not supported
		Evolution	Not supported
		Non-functional property	UML profile
		Abstract type	Class diagram
		Interface	Class diagram
	Mediator	Semantics Constraint	State machine or sequence diagram OCL expressions
		Evolution	Not supported
		Non-functional property	UML profile
		Intentional description	Composite structure diagram
		Constraint	Not supported
		Compositionality	Composite structure diagram
		Evolutionary	Not supported
	Coalition	Coercion	Not supported
		Emergent behavior	State machine or sequence diagram
		Mission	Not supported
		Dynamism	Not supported
		Non-functional property	UML profile

Source:

[START_REF] Guessi | Characterizing Architecture Description Languages for Software-Intensive Systems-of-Systems[END_REF]

.

Table 3 -

 3 Design time features for realizing SoS architectural description in UML, SysML, and X-UNITY

Table 4 -

 4 Architectural elements supported by the SosADL language

	Architecture	Description
	Element
	System

Table 5 -

 5 Summary of classic architecture frameworks in the literature

	Framework Viewpoint	Stakeholder	Concern
		Logical Viewpoint	End-user	Functionality
	4+1 Views (KRUCHTEN,	Development Viewpoint Process Viewpoint	Developer, Manager System integrator	Organization, product-line Performance, availability, software reuse, portability, fault-tolerance, integrity, scalability
	1995)	Physical Viewpoint	System designer	Scalability, performance, availability
		Scenarios Viewpoint	End-user, Developer	Understandability
		Modular	End-user, Developer,	Functionality, responsability, reuse, and
	Views and	Viewtype	Manager	portability
	Beyond (CLEMENTS et al., 2011)	Component and Connector Viewtype Allocation Viewtype	Developer Manager	Performance, reliability, availability, in-tegrity, fault-tolerance Performance, security, reliability

viewpoint frames capability requirements, delivery timing, and deployed capability; (iii) data and information viewpoint frames data relationships and alignment structures that are consumed by requirements, processes, systems, and services; (iv) operational viewpoint describes the operational scenarios, activities, and requirements supporting capabilities; (v) project viewpoint describes the relation between operational and capability requirements and current projects;

Table 6 -

 6 Outline of activities in the Ark method

	Step Description	Input	Output
	1	Architects describe the SoS in terms of	ASRs for con-	Description of an
		an abstract description, which comprises	stituents, medi-	abstract architec-
		types of systems and mediators that can	ators, coalitions,	ture.
		participate in the architecture, and types of	and/or missions.
		coalitions that can be formed at run-time.
	2	Architects translate an abstract architec-	Description of an	Conceptual model
		ture in terms of a constraint satisfaction	abstract architec-	of the abstract ar-
		problem that is recognized as a valid	ture.	chitecture.
		model by the constraint solver
	3	Architects find solution for the constraint	Conceptual model	Solution	of
		satisfaction problem that represent a con-	of the abstract ar-	constraint satis-
		crete architecture that satisfy the proper-	chitecture.	faction problem
		ties of the abstract description.		corresponding to
				a candidate con-
				crete architecture.

Table 7 -

 7 Notations for the description of abstract architectures, concrete architectures, and conceptual models

	Artifact	Notation	Language Elements
	Abstract
	Architecture

Table 8 -

 8 Commands of operators and quantifiers supported by Alloy

	Constants	Set	Operators Relational		Constraints Logical	Quantification
	none empty	+ union		-> product	not	! negation	all universal
	set	& intersection .	join	and	&& conjunction no empty
	univ universal	-difference	[] join	or	|| disjunction lone empty or
	set	in subset		∼ transpose	implies => implication	singleton
	iden identity	= equality		^transitive	if	<=>bi-	one singleton
					closure		implication	some not
				* reflexive-		empty
					transitive
					closure
				<: domain
					restriction
				:> range
					restriction
				++ override

Table 9 -

 9 SosADL support for SoS characteristics

	Characteristic	SosADL features
	Autonomy to operate
	without the control of
	another entity

Table 10 -

 10 Signatures and relations defined by TASoS

	Signature	Relation
	ArchitecturalElement	hasPort
	System (ArchitecturalElement*)
	Mediator (ArchitecturalElement*)
	Sos (ArchitecturalElement*)	arch
	Port	hasConnection
	Gate (Port*)
	Duty (Port*)
	Connection	hasDatatype, owner
	Outward (Connection*)
	Inward (Connection*)
	Unification	src, dest
	Relay	relayCon
	Datatype
	IntegerType (Datatype*)
	NamedType (Datatype*)
	RangeType (Datatype*)
	SequenceType (Datatype*)
	TupleType (Datatype*)	complexType
	Architecture	contain, unifiedAs, bindings
	Topology	inTopology, path

Key:

Table 11 -

 11 Summary of assertions included in TASoS

	Assertion	Description
	A1 architectureCantBeEmpty Checks the feasibility of architectures without elements. This
		assertion is expected to fail.
	A2 pathCantBeEmpty	Checks if a not empty architecture can have no path in topol-
		ogy. This assertion is expected to hold since elements of a
		coalition must necessarily participate in at least one unifica-
		tion.
	A3 samePortUnification	Checks the feasibility of a topology for an architecture in
		which there are more than one unification over two ports.
		This assertion is expected to fail. Otherwise, it might indicate
		that the model is overconstrained.
	A4 allBindingsAreUsed	Checks the feasibility of an architecture for which some of
		its bindings do not appear in at least one of its topologies.
		This assertion is expected to fail.
	A5 oneMediator	Checks the correctness of a description by investigating if it
		allows any topology to have more than one mediator. This
		assertion is expected to fail. Otherwise, it might indicate that
		the model is overconstrained.
	A6 oneMediatorPerSystem	Checks the correctness of a description by investigating if
		it allows a system to interact with more than one mediator.
		The outcome of this assertion varies depending on particular
		binding policies of each SoS. If it is expected to fail and does
		not, it might indicate that the model is underconstrained.

  have no e l e m e n t s 6: // A#2 Checks i f a t o p o l o g y can have no u n i f i c a t i o n s .

	1: //A#1 Checks whether an a r c h i t e c t u r e can have no e l e m e n t s .
	2: a s s e r t a rc h it ec t ur e Ca nt B e E m p t y {
	3:	no a : Architecture | no a . contain
	4: }
	11: // A#3 Checks i f i t i s p o s s i b l e to have more than one u n i f i c a t i o n
		o v e r t h e e x a c t same p a i r o f p o r t s
	15:	u i n inTopology [ t ] and
	16:	v i n inTopology [ t ] and
	17:	#( portsOfUnif ication [ u ] & po rt sO fUni fi ca tion [ v ]) >1
	18: }
	19: check samePortUnif icatio n f o r 5 --I f t h i s a s s e r t i o n h o l d s , t h e model
		might be o v e r c o n s t r a i n e d

5: check a rc h it ec t ur e Ca n tB e E m p t y f o r 4 but 2 Architecture , 3 Topology --I f t h i s a s s e r t i o n f a i l s , an a r c h i t e c t u r e i s a l l o w e d to 7: a s s e r t pathCantBeEmpty { 8: no a : Architecture , t : Topology | t i n ( a . unifiedAs ) . elems and some a . contain and { no path [ t ] . Unification } 9: } 10: check pathCantBeEmpty f o r 4 but 2 Architecture , 3 Topology --I f t h i s a s s e r t i o n f a i l s , t h e model might need c o r r e c t i o n s 12: a s s e r t samePortUnif icatio n { 13: no a : Architecture , t : Topology , d i s j u , v : Unification | 14: t i n a . unifiedAs . elems and

Table 12 -

 12 Predicates for customization of TASoS

	1: p r e d at trib uteConTo Port [ sCon : s e t Connection , p : Port ]{
	2:	p . hasConnection i n sCon
	3: }
	4: p r e d at trib uteArchT oSos [ a : Architecture , s : Sos ]{
	5:	getArch [ s ] i n a
	6: }
	7: p r e d unify [ cFirst , cSecond : Connection ] {
	8:
		Predicate	Parameter
		attributeConToPort	set, element
		attributePortToAE	set, element
		attributeDatatypeToCon element, element
		attributeRelay	element, element
		attributeArchToSoS	element, element
		attributeNary	set, element
		unify	element, element

cFirst i n Outward and cSecond i n Inward i m p l i e s 9: {some u : Unification | u . src i n cFirst and u . dest i n cSecond } e l s e 10: cFirst i n Inward and cSecond i n Outward i m p l i e s 11: {some u : Unification | u . src i n cSecond and u . dest i n cFirst } 12: }

Table 13 -

 13 Mapping between SosADL and TASoS. Extended elements are depicted within parenthesis. Unit element, a SoS has at most one Entity Block element, which defines a collection of assorted System, Mediator, Architecture, Function, and Datatype elements. Moreover, a SoS element can also define its own set of Gate and Connection elements. This element is framed in TASoS by the SoS signature, which extends the Architecture Element signature with an additional ternary relation named arch of type SoS → Architecture → Relay describing connections of the SoS that are internally relayed to participants of the coalition, which is modeled by the Architecture signature.

	SosADL	TASoS	Description
	Element	Signature
	SosADL	-	A SosADL element imports any set of Library and comprises at most one
			Unit, which is either a Library or a SoS element. TASoS does not have a
			signature for this element but an instance module can be regarded as one of
			such since it also describes a SoS or a Library element.
	Library (Unit) -	As a Unit element, a Library has at most one Entity Block element, which
			defines a collection of assorted System, Mediator, Architecture, Function,
			and Datatype elements. TASoS does not have a signature for this element
			but references to external libraries are possible as a module, which is an
			importing mechanism provided by the Alloy language.
	SoS (Unit) As a System SoS (Architectural Element) System
	(Entity Block)	(Architectural
		Element)

Table 13 -

 13 Continued from previous page

	SosADL	TASoS	Description
	Datatype	Datatype,
	(Entity Block)	Inward,
		Outward
		(Connection)

Table 15 -

 15 Use of predicates for the customization of instances of TASoS

	Predicate	Parameter	Used By (Method)
	attributeConToPort	set, element	Gate, Duty
	attributePortToAE	set, element	Gate, Duty
	attributeDatatypeToCon element, element Gate, Duty
	attributeRelay	element, element Relay
	attributeArchToSoS	element, element ArchitectureDecl
	attributeNary	set, element	DatatypeDecl
	unify	element, element Unify

Table 16 -

 16 Overview of SoSy performance

	Artifact

Table 17 -

 17 Description of experiment variables

	Name		Type	of	Class	Entity	Type of	Scale	Unit	Range or scale	Counting rule
			variable				attribute	type		points
	Analysis scope	independent Process	Constraint	Internal Interval	Quantity	0 < n < 10	Quantity of elements in sys-
	(treatment)				solving			of ele-		tem, mediator, and relay signa-
									ments in		tures (quantity of unifications,
									category		ports and connections are de-
											rived from the previous ones)
	SoS description independent Product Abstract	Internal Ratio	LOC	t >= 0	LOC of abstract architecture
						architecture					expressed in SosADL
	Productivity	dependent	Resource	Concrete architecture	External Ratio	LOC per ms	t >= 0	LOC of generated concrete architecture expressed in
											SosADL per running time
	Running time	dependent	Process	Transformation External Ratio	ms	0 < t < 3 ×	Combined elapsed time for
										10 5 ms(5min)	the execution of the constraint
											solver execution and the Solu-
											tion2SosADL generator
	Satisfiability	dependent	Process	Constraint	Internal Nominal Category Satisfiable,	Satisfiable if the solver finds a
	of	abstract				solving				undetermined,	solution within the scope. Un-
	architecture								unsatisfiable	satisfiable if it terminates exe-
											cution within 5 minutes with-
											out finding a solution. Unde-
											termined if it does not termi-
											nates execution within 5 min-
											utes.

Table 18 -

 18 Variation of analyzed scope

			Signature
	Variation Architectural Element Port Connection Unification
	Min	3	4	8	8
	Max	7	8	11	11

Table 19 -

 19 Descriptive statistics of dependent variables

		Solver (ms) Transformation (ms) Productivity (LOC/min)
	Quantity 395	158	158
	Min	754	30	37
	Max	42910	5706	680
	Mean	3954	109	322
	Median 3578	43	309

Table 20 -

 20 Comparison of model-based approaches for SoS architectural synthesis

	Citation	Abstract	Concrete	Technique	Tool Support
		Architecture	Architecture
	Ark	•	•	SosADL, Alloy	SoSy (Eclipse)
	COMPASS	•	•	SysML, CML	Symphony (Eclipse)
	DANSE	∘	•	SysML	Tool-Net
	Kenley et al.	∘	•	UML, Petri net	DAF (MATLAB)
	(2014)

Table 21 -

 21 Methods in the SosADL2AlloyGenerator class

	Method	Parameter	Description
	doGenerate	Resource, fsa	Main method that is responsible for generating all files in the project folder.
	compile	SosADL	Creates the header of an instance module file.

Table 22 -

 22 Continued from previous page

	Test	AE Port Connection Unification Solver Result Transf. LOC Productivity
	58	3	7	10	9	1658	0	0	0
	59	3	7	10	10	1618	0	0	0
	60	3	7	10	11	1404	0	0	0
	61	3	7	11	8	1895	0	0	0
	62	3	7	11	9	1557	0	0	0
	63	3	7	11	10	1785	0	0	0
	64	3	7	11	11	1826	0	0	0
	65	3	8	8	8	1091	0	0	0
	66	3	8	8	9	1257	0	0	0
	67	3	8	8	10	1183	0	0	0
	68	3	8	8	11	1387	0	0	0
	69	3	8	9	8	1549	0	0	0
	70	3	8	9	9	1562	0	0	0
	71	3	8	9	10	1290	0	0	0
	72	3	8	9	11	1976	0	0	0
	73	3	8	10	8	1698	0	0	0
	74	3	8	10	9	1787	0	0	0
	75	3	8	10	10	1689	0	0	0
	76	3	8	10	11	1874	0	0	0
	77	3	8	11	8	2083	0	0	0
	78	3	8	11	9	1723	0	0	0
	79	3	8	11	10	1946	0	0	0
	80	3	8	11	11	1980	0	0	0
	81	4	4	8	8	1244	0	0	0
	82	4	4	8	9	1353	0	0	0
	83	4	4	8	10	1529	0	0	0
	84	4	4	8	11	2053	0	0	0
	85	4	4	9	8	1780	0	0	0
	86	4	4	9	9	1959	0	0	0
	87	4	4	9	10	2476	0	0	0
	88	4	4	9	11	2990	0	0	0
	89	4	4	10	8	2591	1	57	30
	90	4	4	10	9	3068	1	46	30
	91	4	4	10	10	3581	1	103	30
	92	4	4	10	11	5109	1	932	30
	93	4	4	11	8	3567	1	54	30
	94	4	4	11	9	3593	1	43	30
	95	4	4	11	10	42910 1	5706	30
	96	4	4	11	11	4992	1	47	30
	97	4	5	8	8	1682	0	0	0
	98	4	5	8	9	2039	0	0	0
	99	4	5	8	10	2356	0	0	0
	100	4	5	8	11	2579	0	0	0
	101	4	5	9	8	2272	0	0	0
	102	4	5	9	9	2089	0	0	0
									Continued on next page

Table 22 -

 22 Continued from previous page

	Test	AE Port Connection Unification Solver Result Transf. LOC Productivity
	103	4	5	9	10	2526	0	0	0
	104	4	5	9	11	2816	0	0	0
	105	4	5	10	8	3143	1	50	30
	106	4	5	10	9	3658	1	62	30
	107	4	5	10	10	4012	1	46	30
	109	4	5	11	8	4151	1	43	30
	110	4	5	11	9	4771	1	110	30
	111	4	5	11	10	5429	1	175	30
	112	4	5	11	11	5172	1	43	30
	113	4	6	8	8	1750	0	0	0
	114	4	6	8	9	1821	0	0	0
	115	4	6	8	10	2134	0	0	0
	116	4	6	8	11	2608	0	0	0
	117	4	6	9	8	2239	0	0	0
	118	4	6	9	9	2397	0	0	0
	119	4	6	9	10	2833	0	0	0
	120	4	6	9	11	3000	0	0	0
	121	4	6	10	8	3774	1	44	30
	122	4	6	10	9	3734	1	47	30
	123	4	6	10	10	4619	1	47	30
	124	4	6	10	11	10562 1	584	30
	125	4	6	11	8	4217	1	43	30
	126	4	6	11	9	5136	1	41	30
	127	4	6	11	10	5276	1	48	30
	128	4	6	11	11	6015	1	43	30
	129	4	7	8	8	2191	0	0	0
	130	4	7	8	9	2446	0	0	0
	131	4	7	8	10	3102	0	0	0
	132	4	7	8	11	3270	0	0	0
	133	4	7	9	8	2758	0	0	0
	134	4	7	9	9	2852	0	0	0
	135	4	7	9	11	6861	0	0	0
	136	4	7	10	8	9338	1	2970	30
	137	4	7	10	10	4584	1	47	30
	138	4	7	10	11	5028	1	39	30
	139	4	7	11	8	4590	1	45	30
	140	4	7	11	9	5198	1	42	30
	141	4	7	11	10	5606	1	38	30
	142	4	7	11	11	6426	1	45	30
	143	4	8	8	8	1971	0	0	0
	144	4	8	8	9	2151	0	0	0
	145	4	8	8	10	2591	0	0	0
	146	4	8	8	11	2976	0	0	0
	147	4	8	9	8	2742	0	0	0
	148	4	8	9	9	3090	0	0	0
									Continued on next page

Table 22 -

 22 Continued from previous page

	Test	AE Port Connection Unification Solver Result Transf. LOC Productivity
	149	4	8	10	8	4185	1	41	30
	150	4	8	10	9	4638	1	40	30
	151	4	8	10	10	4670	1	39	30
	152	4	8	10	11	5228	1	40	30
	153	4	8	11	8	5471	1	42	30
	154	4	8	11	9	5531	1	40	30
	155	4	8	11	10	6450	1	38	30
	156	4	8	11	11	6902	1	40	30
	157	5	4	8	8	1149	0	0	0
	158	5	4	8	9	1869	0	0	0
	159	5	4	8	10	1994	0	0	0
	160	5	4	8	11	1774	0	0	0
	161	5	4	9	8	1914	0	0	0
	162	5	4	9	9	2499	0	0	0
	163	5	4	9	10	2520	0	0	0
	164	5	4	9	11	2971	0	0	0
	165	5	4	10	8	2889	1	41	30
	166	5	4	10	9	3180	1	39	30
	167	5	4	10	10	3738	1	44	30
	168	5	4	10	11	4092	1	39	30
	169	5	4	11	8	3826	1	41	30
	170	5	4	11	9	4156	1	35	30
	171	5	4	11	10	4632	1	44	30
	172	5	4	11	11	4873	1	41	30
	173	5	5	8	8	1746	0	0	0
	174	5	5	8	9	2117	0	0	0
	175	5	5	8	10	2287	0	0	0
	176	5	5	8	11	2656	0	0	0
	177	5	5	9	8	2291	0	0	0
	178	5	5	9	9	2370	0	0	0
	179	5	5	9	10	2688	0	0	0
	180	5	5	9	11	3325	0	0	0
	181	5	5	10	8	4010	1	45	30
	182	5	5	10	9	4341	1	37	30
	183	5	5	10	10	4910	1	52	30
	184	5	5	10	11	5753	1	38	30
	185	5	5	11	8	4702	1	47	30
	186	5	5	11	9	5096	1	42	30
	187	5	5	11	10	5529	1	39	30
	188	5	5	11	11	6187	1	43	30
	189	5	6	8	8	2306	0	0	0
	190	5	6	8	9	3429	0	0	0
	191	5	6	8	10	3192	0	0	0
	192	5	6	8	11	3613	0	0	0
	193	5	6	9	8	3560	0	0	0
									Continued on next page

Table 22 -

 22 Continued from previous pageContinued on next page • Graciano Neto, V. V.,Guessi, M., Oliveira, L., Oquendo, F., and Nakagawa, E. Y. Investigating the Model-Driven Development for Systems-of-Systems. p. 1-8. DOI: <http: //dx.doi.org/10.1145/2642803.2642825> Event: 8th European Conference on Software Architecture Workshop(ECSAW), Vienna, Austria, 2014. Level of contribution: Medium -the PhD candidate contributed to paper planning and writing. • Guessi, M., Oquendo, F., and Nakagawa, E. Y. Variability Viewpoint to Describe Reference Architectures. p. 1-6. DOI: <http://dx.doi.org/10.1145/2578128.2578238> Event: 3rd International Workshop on Variability in Software Architecture (VARSA) at 11th Working IEEE/IFIP Conference on Software Architecture (WICSA). Sydney, Australia, 2014.Level of contribution: High -the PhD candidate is the main investigator.• Nakagawa, E. Y., Gonçalves, M., Guessi, M., Oliveira, L., and Oquendo, F. The State-ofthe-Art and Future Perspectives in Systems-of-Systems Software Architectures. p. 13-20.Plataforma de Recursos Educacionais Abertos: Uma Arquitetura de Referência com Elementos de Gamificação. URL: <http://seer.ufrgs.br/index.php/renote/article/view/70650> Journal:RENOTE. 2016. v. 14, n. 2, p.1-10. ISSN: 1679-1916. h-index: 20 (Publish or Perish).

	Test	AE Port Connection Unification Solver Result Transf. LOC Productivity
	194	5	6	9	9	3113	0	0	0
	195	5	6	9	10	3474	0	0	0
	196	5	6	9	11	3629	0	0	0
	197	5	6	10	8	4276	1	46	30
	198	5	6	10	9	4841	1	51	30
	199	5	6	10	10	4984	1	56	30
	200	5	6	10	11	5510	1	39	30
	201	5	6	11	8	5130	1	46	30
	202	5	6	11	9	6103	1	42	30
	203	5	6	11	10	7932	1	51	30
	204	5	6	11	11	8250	1	53	30
	205	5	7	8	8	2904	0	0	0
	206	5	7	8	9	2946	0	0	0
	207	5	7	8	10	3991	0	0	0
	208	5	7	8	11	3573	0	0	0
	209	5	7	9	8	3083	0	0	0
	210	5	7	9	9	3600	0	0	0
	211	5	7	9	10	3741	0	0	0
	212	5	7	9	11	4452	0	0	0
	213	5	7	10	8	5234	1	45	30
	214	5	7	10	9	4956	1	53	30
	215	5	7	10	10	5753	1	47	30
	216	5	7	10	11	6741	1	64	30
	217	5	7	11	8	6269	1	56	30
	218	5	7	11	9	6941	1	46	30
	219	5	7	11	10	7259	1	54	30
	220	5	7	11	11	9312	1	54	30
	221	5	8	8	8	2896	0	0	0
	222	5	8	8	9	3624	0	0	0
	223	5	8	8	10	3786	0	0	0
	224	5	8	8	11	3744	0	0	0
	225	5	8	9	8	3556	0	0	0
	226	5	8	9	9	3868	0	0	0
	227	5	8	9	10	3578	0	0	0
	228	5	8	9	11	3648	0	0	0
	229	5	8	10	8	4595	1	35	30
	230	5	8	10	9	5125	1	41	30
	231	5	8	10	10	5568	1	44	30
	232	5	8	10	11	6609	1	39	30
	233	5	8	11	8	6204	1	41	30
	234	5	8	11	9	6725	1	43	30
	235	5	8	11	10	7177	1	43	30
	236	5	8	11	11	7432	1	40	30
	237	6	4	8	8	1473	0	0	0
	238	6	4	8	9	1776	0	0	0

DOI: <http://dx.doi.org/10.1145/2489850.2489853> Event: 1st International Workshop on Software Engineering for Systems-of-Systems (SESoS) at the 7th European Conference on Software Architecture (ECSA), Montpellier, France, 2013.

Level of contribution: Medium -the PhD candidate contributed to paper planning and writing.

• Toda, A. M., Valle, P. H. D., Guessi, M., Rocha, R. V.; Maldonado, J.C.; Isotani, S.

Synthèse d'architectures logicielles pour systèmes-de-systèmes Milena Margarido 2017 Synthèse d'architectures logicielles pour systèmes-de-systèmes Milena Margarido 2017

Synthèse d'architectures logicielles pour systèmes-de-systèmes Milena Margarido 2017

Chapter 2. State of the Art on Architecture Description of Systems-of-Systems

Symphony IDE, <http://symphonytool.org> Synthèse d'architectures logicielles pour systèmes-de-systèmes Milena Margarido 2017

u n i f y [ s e r v e r _ r r _ a c k&( s e r v e r 1 . ~owner ) , Synthèse d'architectures logicielles pour systèmes-de-systèmes Milena Margarido 2017

Synthèse d'architectures logicielles pour systèmes-de-systèmes Milena Margarido 2017 4.3. Predicates for the Customization of TASoS

Acknowledgements

List of source codes

Source code 1 -Example of abstract coalition type expressed in SosADL . . . . . . . Source code 2 -Excerpt of abstract coalition expressed in terms of constraints . . . . . Source code 3 -Excerpt of constraint solver solution . . . . . . . . . . . . . . . . . . Source code 4 -Example of concrete coalition expressed in SosADL . . . . . . . . . . Source code 5 -Excerpt of constraints on architectural elements in TASoS . . . . . . . Source code 6 -Excerpt of constraints on interactions in TASoS . . . . . . . . . . . . Source code 7 -Excerpt of constraints on architectures in TASoS . . . . . . . . . . . . Source code 8 -Excerpt of constraints on topologies in TASoS . . . . . . . . . . . . . Source code 9 -Excerpt of assertions in TASoS . . . . . . . . . . . . . . . . . . . . . Source code 10 -Excerpt of predicates in TASoS for creating instances of the core module Source code 11 -Excerpt of a predicate checking the feasibility of a scenario in TASoS Source code 12 -Excerpt of method that compiles SosADL objects . . . . . . . . . . . Source code 13 -Excerpt of the AlloyBound class . . . . . . . . . . . . . . . . . . . . Source code 14 -Excerpt of the AlloyPredicate class . . . . . . . . . . . . . . . . . Source code 15 -Excerpt of library template in Solution2SosADLGenerator method . Source code 16 -Excerpt of library model with client-server abstract types expressed in SosADL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Source code 17 -Excerpt of coalition type for client-server architectures expressed in SosADL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Source code 18 -Excerpt of coalition type for well-formed client-server architectures expressed in SosADL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Source code 19 -Excerpt of abstract gateway type for URM in SosADL . . . . . . . . . Source code 20 -Excerpt of abstract sensor type for URM in SosADL . . . . . . . . . . Source code 21 -Excerpt of abstract mediator type for URM in SosADL . . . . . . . . Source code 22 -Excerpt of abstract coalition type for URM in SosADL . . . . . . . . Source code 23 -Architecture instance module of TASoS for URM . . . . . . . . . . . Source code 24 -Excerpt of concrete architecture for URM that is compliant with abstract coalition type . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Source code 25 -TASoS source code . . . . . . . . . . . . . . . . . . . . . . . . . . . Source code 26 -SosADL abstract syntax . . . . . . . . . . . . . . . . . . . . . . . . .

To the São Paulo Research Foundation (FAPESP), for the financial support to this research (N. 2012/01646-4, 2014/

References APPENDIX A Usage Guidelines of SoSy

The aforementioned types compose a single SosADL library, named urmLibrary. To complement this description, the subject creates an abstract coalition type for URM built on top of these definitions. Source code 22 shows the abstract architecture named simple for URM. The serving gate of this architecture enables the communication of the Flood Monitoring coalition with other systems and SoS. This gate declares two connections named request and alert that handles external queries about the conditions of the river and publish warning messages in case one of the sensors has identified a flood event. The main behavior of this coalition is named main. Differently from the behavior of systems and mediators, the behavior of architectures contains: a compose statement, which establishes that constituents are allowed to participate in the coalition; and, a binding statement, which defines policies for organizing systems and mediators into a cohesive whole (lines 16-39). The simple type of this coalition is composed of any number of sensors and transmitters but has only one gateway, named gateway1. Furthermore, any instance of this abstract coalition type may only exercise the unifications defined in the binding statements. : m e a s u r i n g : : measure } to one { t : : t r a n s m i t t i n g : : f r o m S e n s o r s } or u n i f y one { s 1 : : p a s s i n g : : measure } to one { t : : t r a n s m i t t i n g : : f r o m S e n s o r s } // and s e n d s t o s o r g ) and ( u n i f y one { t : : t r a n s m i t t i n g : : toGateway } to one { gateway1 : : a l e r t i n g : : measure } xor u n i f y one { t : : t r a n s m i t t i n g : : toGateway } to one { s 2 : : p a s s i n g : : p a s s } )

Source code 22 -Excerpt of abstract coalition type for URM in SosADL

Usage Guidelines of SoSy

This appendix details how one can install and use SoSy, a tool that provides automated support for the Ark method within a larger framework for the design of SoS architectures in SosADL. First, Section A.1 explains how to download and install SosADE, an integrated environment for designing and simulating SoS based on SosADL. In particular, it describes how SoSy can be used from within a SosADE instance of the Eclipse environment.

A.1 Installation of SosADE

SosADE requires Java 8 or higher installed and runs on a Windows 7 ou Linux operational systems. The tool is provided as an Eclipse Mars 2 1 plugin. The user can create a new Java project or upload an existing SosADL project in the environment that will recognize the .sosadl extension in files and execute the SosADL2AlloyGenerator on the background, hence automatically starting the transformation of SosADL models into instances of TASoS and related Java classes. The user should follow these steps to start SosADE and obtain instances of concrete coalitions that adhere to a SosADL abstract architecture:

• Download and execute the SosADE plugin for Eclipse at <https://goo.gl/RgqR9K>.

• Upload or create a new project.

• Upload or create one or more .sosadl files in your project. To generate an executable Java class, it is important that the project contains at least one SoS unit to translate into a TASoS instance module.

• Right click the main project folder > Build path > Configure Build Path > Add external JAR > select alloy4.2_2015-02-22.jar (this JAR is automatically added by SoSy in the generated folder of the project, usually named src-gen).

• Right click the generated folder > Build path > Use as source folder.

1 Eclipse Mars, <https://eclipse.org/mars/>.

• Run the generated .java file in the generated folder as a Java application. The console will show "Translation to KodKod and Solution: (ms)" after the constraint solver terminates its execution. The tool will also prompt a new window that shows the graphical representation of the solution automatically generated by the solver.

• Right click the generated folder and select the option Refresh. Any concrete instance that has been found by the constraint solver will appear as a separate file in the generated folder. In particular, generated files are named after the abstract description with which they are related.

The graphical interface of SosADE is illustrated in Figure 17 using the "Simple-ClientServer" project as example. This figure shows that the tool created an Alloy (.als extension) file in the generated folder named "src-gen" for each SosADL (.sosadl extension) file in the main project folder named "src". In addition, SoSy also automatically created a Java class for running each SoS unit in the project folder. Besides these files, the generated folder also contains a copy of the TASoS model (tasos.als) and a custom theme for visualizing the instance found by the solver (minisosrun.thm).

Experiment Materials

Table 22 presents raw data collected in the operation of the quasi-experiment described in Chapter 6. The assigned scope of signature Relay is fixed in the beginning of this experiment as 1. The solver column corresponds to running time of the constraint solver while the transformation column corresponds to running time of the Solution2Alloy generator, both measured in milliseconds. The constraint solver used in this experiment is the SAT4J 1 . Since the transformation is only performed when the model is satisfiable, this data is only available for a subset of test cases. Moreover, the value of productivity is calculated as the ratio between LOC of generated abstract architecture and running time of the transformation (calculated as LOC/min), hence unsatisfiable models present zero productivity. Source code for the instrumented class, test case commands, and script used for automatically operating this experiment are externally available at <https://goo.gl/RgqR9K> (accessed on 08/05/2017). Continued on next page Continued on next page Level of contribution: High -the PhD candidate is the main investigator.

• Guessi, M., Cavalcante, E., Oliveira, L. B. R. Characterizing Architecture Description Languages for Software-Intensive Systems-of-Systems. p. 12-18.

Event: 3rd International Workshop on Software Engineering for Systems-of-Systems (SESoS) at 37th International Conference on Software Enginnering (ICSE), 2015. Florence, Italy.

Level of contribution: High -the PhD candidate is the main investigator.

• Guessi, M., Graciano Neto, V. V., Bianchi, T., Felizardo, K. R., Oquendo, F., and Level of contribution: High -the PhD candidate is the main investigator. Level of contribution: Medium -the PhD candidate contributed to paper planning and writing.

C.2 Other Publications

• Guessi, M., Oliveira, L. B. R., Garcés, L., Oquendo, F. Towards a Formal Description of ANNEX A

The SosADL Language

This annex presents the abstract syntax for SosADL (shown in Source code 26), an ADL tailored for the description of SoS discussed in Section 2.3.3 on page 35. This grammar is implemented in Xtext 1 . Examples, justifications, and foundations of this new are discussed by Oquendo on (OQUENDO, 2016a;OQUENDO, 2016c;OQUENDO, 2016b;OQUENDO, 2016d).

Source code 26 -SosADL abstract syntax 1 grammar o r g . a r c h w a r e . s o s a d l . SosADL w i t h o r g . e c l i p s e . x t e x t . common .

T e r m i n a l s

2 g e n e r a t e sosADL ' h t t p : / /www-a r c h w a r e . i r i s a . f r / s o s a d l /SosADL '