Systems of systems (SoS) have been introduced in early 1990s in air traffic control domain, defense and information technologies. Systems like this contain a set of components, being systems itself, with constituent components retaining operational independence. The definition and configuration of SoS have evolutionary nature and emergent behavior is one of the many important characteristics to be mentioned. Over the past ten years fast technological and industrial advances in the domain of autonomous and cooperating systems started to occur, which created new opportunities to use the benefits of SoS. In the near future, fully autonomous and cooperating systems are expected to become our reality and increase the production efficiency, while decreasing the human effort in harmful environments. There exist the need to make sure that critical properties of SoS, such as safety and security are guaranteed as a joint effort, since it is not sufficient anymore to address these properties independently in the development process. In this paper an overview of the most common approaches and methods used to provide reasoning about joint safety and security is provided, as well as a check of the latest updates in standards related to these properties.

Over the past decade, fast technological and industrial advances have been happening in the area of autonomous Systems of Systems (SoS). A SoS is built upon integration of several systems, where the complexity of such a structure is exponentially higher which brings challenges to its analysis. However, it also has provided a large set of new opportunities in domains such as air traffic control, defense, construction industry, etc. It is expected that fully autonomous and cooperating systems will increase the production efficiency, while decreasing (potentially completely replacing) the human effort in harmful environments. In order to enable this, we need to make sure that critical properties of SoS, such as safety and security are guaranteed. We believe that it is not sufficient anymore to analyze and guarantee these properties independently, but we have to be able to address safety and security in a joint effort. Communications in systems with any type of real-time requirements, where data validity is based on its freshness, rely on clock synchronization (CSyn) allowing its subsystems to cooperate and work coherently. Considering reliable and predictable communication as one of the main assets contributing to correct functionality of such systems, protecting CSyn from malicious adversaries should be one of the highest priority efforts in SoS. In this paper we show how CSyn breaches can influence security, and ultimately safety of complex and autonomous SoS, further we identify a missing piece to consider in safety assurance, namely assurance with respect to reliable communications between systems within the SoS. We demonstrate how an outcome of a security analysis can be used as input for the overall safety analysis and we use an autonomous quarry as an example application to illustrate our findings.

The fast development of sensing devices and radios enables more powerful and flexible remote health monitoring systems. Considering the future vision of the Internet of Things (IoT), many requirements and challenges rise to the design and implementation of such systems. Bridging the gap between sensor nodes on the human body and the Internet becomes a challenging task in terms of reliable communications. Additionally, the systems will not only have to provide functionality, but also be highly secure. In this paper, we provide a survey on existing communication protocols and security issues related to pervasive health monitoring, describing their limitations, challenges, and possible solutions. We propose a generic protocol stack design as a first step toward handling interoperability in heterogeneous low-power wireless body area networks.

Ensuring interoperability in the future Internet of Things applications can be a challenging task, especially in mission-critical applications such as Health Monitoring Systems. Existing low-power wireless network architectures are designed in isolated networks, and ensure a satisfying level of performance in homogeneous networks. However, with co-existence of different low-power networks, the interoperability related problems arise. To bridge this gap in this paper, we study various protocol stacks (i.e., Bluetooth, Bluetooth Low Energy, IEEE 802.15.4, ZigBee, 6LoWPAN and IEEE 802.15.6), and explain their specific features. Furthermore, we provide a generic protocol stack design that facilitates multiple radios with different protocol stacks, regardless of being IP-based or non-IP-based networks. We see this approach as a possibility to enhance network performance in terms of reliability, timeliness, and security, while providing higher levels of scalability and connectivity.

We are witnessing a fast technological and industrial advances in the domain of autonomous and cooperating systems. It is believed that in the near future, fully autonomous and cooperating systems ...

During the past decade service-orientation has become a popular design paradigm, offering an approach in which services are the functional building blocks. Services are self-contained units of composition, built to be invoked, composed, and destroyed on (user) demand. Service-oriented systems (SOS) are a collection of services that are developed based on several design principles such as: (i) loose coupling between services (e.g., inter-service communication can involve either simple data passing or two or more connected services coordinating some activity) that allows services to be independent, yet highly interoperable when required; (ii) service abstraction, which emphasizes the need to hide as many implementation details as possible, yet still exposing functional and extra-functional capabilities that can be offered to service users; (iii) service reusability provided by the existing services in a rapid and flexible development process; (iv) service composability as one of the main assets of SOS that provide a design platform for services to be composed and decomposed, etc. One of the main concerns in such systems is ensuring service quality per se, but also guaranteeing the quality of newly composed services. To accomplish the above, we consider two system perspectives: the developer's and the user's view, respectively. In the former, one can be assumed to have access to the internal service representation: functionality, enabled actions, resource usage, and interactions with other services. In the second, one has information primarily on the service interface and exposed capabilities (attributes/features). Means of checking that services and service compositions meet the expected requirements, the so-called correctness issue, can enable optimization and possibility to guarantee a satisfactory level of a service composition quality. In order to accomplish exhaustive correctness checks of design-time SOS, we employ model-checking as the main formal verification technique, which eventually provides necessary information about quality-of-service (QoS), already at early stages of system development. ~As opposed to the traditional approach of software system construction, in SOS the same service may be offered at various prices, QoS, and other conditions, depending on the user needs. In such a setting, the interaction between involved parties requires the negotiation of what is possible at request time, aiming at meeting needs on demand. The service negotiation process often proceeds with timing, price, and resource constraints, under which users and providers exchange information on their respective goals, until reaching a consensus. Hence, a mathematically driven technique to analyze a priori various ways to achieve such goals is beneficial for understanding what and how can particular goals be achieved.This thesis presents the research that we have been carrying out over the past few years, which resulted in developing methods and tools for the specification, modeling, and formal analysis of services and service compositions in SOS. The contributions of the thesis consist of: (i)constructs for the formal description of services and service compositions using the resource-aware timed behavioral language called REMES; (ii) deductive and algorithmic approaches for checking correctness of services and service compositions;(iii) a model of service negotiation that includes different negotiation strategies, formally analyzed against timing and resource constraints; (iv) a tool-chain (REMES SOS IDE) that provides an editor and verification support (by integration with the UPPAAL model-checker) to REMES-based service-oriented designs;(v) a relevant case-study by which we exercise the applicability of our framework.The presented work has also been applied on other smaller examples presented in the published papers.

Negotiation is a key aspect of Service-Oriented Systems, which is rarely supported by formal models and tools for analysis. Often, service negotiation proceeds with timing, cost and resource constraints, under which the users and providers exchange information on their respective goals, until reaching a consensus. Consequently, a mathematically driven technique to analyze various ways to achieve such goals is beneficial. In this paper, we propose an analyzable negotiation model between service clients and providers, in our recently introduced language REMES and its corresponding textual service composition language HDCL. The model can be viewed as a negotiation interface for different negotiation strategies and protocols, which iterates until an agreement is reached. We show how to analyze the negotiation model against timing, cost and utility constraints, by transforming it into the Timed Automata formal framework. We illustrate our approach through an insurance scenario assuming a form of the Contract Net Protocol for web services.

Service-Oriented Systems (SOS) have gained importance in different application domains thanks to their ability to enable reusable functionality provided via well-defined interfaces, and the increas ...

Service-oriented systems have recently emerged as context-independent component-based systems. Unlike components, services can be created, invoked, composed, and destroyed at run-time. Consequently, all services need a way of advertising their capabilities to the entities that will use them, and serviceoriented modeling should cater for various kinds of service composition. In this paper, we show how services can be formally described by the resource-aware timed behavioral language REMES, which we extend with service-specific information, such as type, capacity, time-to-serve, etc., as well as boolean constraints on inputs, and output guarantees. Assuming a Hoare-triple model of service correctness, we show how to check it by using the strongest postcondition semantics. To provide means for connecting REMES services, we propose a hierarchical language for service composition, which allows for verifying the latter's correctness. The approach is applied on an abstracted version of an intelligent shuttle system.