https://www.mdu.se/

The aging population and the increasing healthcare cost in hospitals are spurring the advent of remote health monitoring systems. Advances in physiological sensing devices and the emergence of reliable low-power wireless network technologies have enabled the design of remote health monitoring systems. The next generation Internet, commonly referred to as Internet of Things (IoT), depicts a world populated by devices that are able to sense, process and react via the Internet. Thus, we envision health monitoring systems that support Internet connection and use this connectivity to enable better and more reliable services. This paper presents an overview on existing health monitoring systems, considering the IoT vision. We focus on recent trends and the development of health monitoring systems in terms of: (1) health parameters, (2) frameworks, (3) wireless communication, and (4) security issues. We also identify the main limitations, requirements and advantages within these systems.

This paper presents application of a fuzzy logic based system to automatically evaluate the

maintainability of code. Code evaluation is accomplished by rating its quality provided with bad smells in

code as inputs. Straightforward bad smells with existing software metrics tools are selected as inputs:

duplicated code, long methods, large classes having a high cyclomatic complexity, or a large number of

parameters and temporary fields. Removing these bad smells can result in significant code improvements

concerning readability and maintainability. However, the precise definition of attributes like small, long, large

or high is not clear, and their identification is rather subjective. Fuzzy logic values are suitable for capturing

partial correspondence to attributes and fuzzy rules model have been used to describe the relation between bad

smells and code quality. Model supporting the experimental evaluation of the fuzzy based code evaluation is

implemented in Java.

Key-Words: - Fuzzy Logic, Reasoning Systems, Refactoring, Bad Smells

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

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 are going to become our reality, with helping to increase the production efficiency and to decrease (potentially completely replace) human effort in harmful environments. In order to make this happen, we need to make sure that critical properties such safety and security are guaranteed. Moreover, it is not sufficient anymore to analyse and guarantee these properties independently in the development process, as it is case now, but we have to be able to address safety and security within a joint effort. Recent research has already pointed to their independencies and ways how they affect each other. In this report we provide insight into the state-of-the-art on safety and security approaches provided in the literature. We overview the most common approaches and methods used to provide reasoning about these properties, as well as we check latest updates in standards related to these properties.

With development of cloud computing new ways for easy, on-demand, Internet-based access to computing resources have emerged. In such context a Service Level Agreement (SLA) enables contractual agreements between service providers and users. Given an SLA, service users are able to establish trust in that the service outcome corresponds to what they have demanded during the service negotiation process. However, an SLA provides a limited support outside of basic Quality of Service (QoS) parameters, especially when it comes to security. We find security as an important factor to be included in adjusting an SLA according to user defined objectives. Incorporating it in an SLA is challenging due to difficulty to provide complete and quantifiable metrics, thus we propose to focus on a systematic way of addressing security using the security process. In this paper we investigate ways in which security might be incorporated already in the service negotiation process and captured in an SLA. We propose a corresponding process to develop and maintain an SLA that considers both design-, and run-time. To demonstrate the approach we built upon the existing SLAC language and extend its syntax to support security. An example of a service being provided with security guarantees illustrates the concept.

An early prediction of resource utilization and its impacton system performance and reliability can reduce theoverall system cost, by allowing early correction of detectedproblems, or changes in development plans with minimizedoverhead. Nowadays, researchers are using both academicand commercial models to predict such attributes, by measuringthem at earliest stages of system development. Inthis paper, we give a short overview of existing predictionmodels for performance and reliability, targeting popularcomponent-based frameworks. Next, we describe our ownapproach for tackling such predictions, through an illustrationon a small example that deals with estimations of energyconsumption.

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 increased opportunities to compose existing units, called services, into various configurations. Developing applications in such a setup, by reusing existing services, brings some concerns regarding the assurance of the expected Quality-of-Service (QoS), and correctness of the employed services. In this paper, we provide a formal mechanism of computing service guarantees, automatically. We assume service models annotated with pre- and postconditions, their semantics given as Priced Timed Automata (PTA), and the forward analysis method for checking the service correctness w.r.t. given requirements. Under these assumptions, we show how to compute the strongest postcondition of the corresponding automata algorithmically, with respect to the specified precondition. The approach is illustrated on a small example of a service modeled as Priced Timed Automaton (PTAn).

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 increased opportunities to compose existing units, called services, into various configurations. Developing applications in such a setup, by reusing existing services, brings some concerns regarding the assurance of the expected Quality-of-Service (QoS), and correctness of the employed services. In this paper, we describe a formal mechanism of computing service guarantees, automatically. We assume service models annotated with pre- and postconditions, with their semantics given as Priced Timed Automata (PTA), and the forward analysis method for checking the service correctness w.r.t. given requirements. Under these assumptions, we show how to compute the strongest postcondition of the corresponding automata algorithmically, with respect to the specified precondition. The approach is illustrated on a small example of a service modeled as Priced Timed Automaton (PTAn).

The service-oriented paradigm has been established to enable quicker development of new applications from already existing services. Service negotiation is a key technique to provide a way of deciding and choosing the most suitable service, out of possibly many services delivering similar functionality but having different response times, resource usages, prices, etc. In this paper, we present a formal approach to the clients-providers negotiation of distributed energy management. The models are described in our recently introduced REMES HDCL language, with timed automata semantics that allows us to apply UPPAAL-based tools for model-checking various scenarios of service negotiation. Our target is to compute ways of reaching the price- and reliability-optimal values of the utility function, at the end of the service negotiation.

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 should have a way of advertising their capabilities to the entities that will use them, and service-oriented 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, for which we also compute resource-efficient behaviors, and energy-time trade-offs, by model-checking the system’s underlying Priced Timed Automata semantic representation.

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.

There is no clear distinction between service-orientedsystems (SOS) and component-based systems (CBS). However,there are several characteristics that could let one considerSOS as a step further from CBS. In this paper, we discussthe general features of CBS and SOS, while accountingfor behavioral modeling in the language called REMES.First, we present REMES in the context of CBS modeling,and then we show how it can become suitable for SOS. Wealso discuss the relation between our model and the currentstate of the art.

Enabling System-of-Systems (SoS) security is an important activity when engineering SoS solutions like autonomous vehicles, provided that they are also highly safety-critical. An early analysis of such solutions caters for proper security architecture decisions, preventing potential high impact attacks and ensuring people's safety. However, SoS characteristics such as emergent behavior, makes security decision-making at the architectural level a challenging task. To tackle this challenge, it is essential to first address known vulnerabilities related to each CS, that an adversary may exploit to realize his attacks within the unknown SoS environment. In this paper we investigate how to use Game Theory (GT) approaches to guide the architect in choosing an appropriate security solution. We formulate a game with three players and their corresponding strategies and payoffs. The proposal is illustrated on an autonomous quarry example showing its usefulness in supporting a security architect to choose the the most suitable security strategy. 

System of Systems (SoS) represent a set of independent Constituent Systems (CS) that collaborate in order to provide functionalities that they are unable to achieve independently. We consider SoS as a set of connected services that needs to be adequately protected. The integration of these independent, evolutionary and distributed systems, intensifies SoS complexity and emphasizes the behavior uncertainty, which makes an SoS security analysis a critical challenge. One of the major priorities when designing SoS, is to analyze the unknown dependencies among CS services and vulnerabilities leading to potential cyberattacks. The aim of this work is to investigate how Software Engineering approaches could be leveraged to analyze the cyberattack propagation problem within an SoS. Such analysis is essential for an efficient SoS risk assessment performed early at the SoS design phase and required to protect the SoS from possibly high impact attacks affecting its safety and security. In order to achieve our objective, we present a model-driven analysis approach, based on Bayesian Networks, a sensitivity analysis and Common Vulnerability Scoring System (CVSS) with aim to discover potential cyberattacks propagation and estimate the probability of a security failure and its impact on SoS services. W

In this paper we present a modeling and analysis tool for service-oriented systems. The tool enables graphical modeling of service-based systems, within the resource-aware timed behavioral language Remes, as well as a textual system description. We have developed a graphical environment where services can be composed as desired by the user, together with a textual service composition interface in which compositions can also be checked for correctness. We also provide automated traceability between the two design interfaces, which results in a tool that enhances the potential of system design by intuitive service manipulation. The paper presents the design principles, infrastructure, and the user interface of our tool.

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.

In recent years, autonomous systems have become an important research area and application domain, with a significant impact on modern society. Such systems are characterized by different levels of autonomy and complex communication infrastructures that allow for collective decision-making strategies. There exist several publications that tackle ethical aspects in such systems, but mostly from the perspective of a single agent. In this paper we go one step further and discuss these ethical challenges from the perspective of an aggregate of autonomous systems capable of collective decision-making. In particular, in this paper, we propose the Caesar approach through which we model the collective ethical decision-making process of a group of actors—agents and humans, as well as define the building blocks for the agents participating in such a process, namely Caesar agents. Factors such as trust, security, safety, and privacy, which affect the degree to which a collective decision is ethical, are explicitly captured in Caesar. Finally, we argue that modeling the collective decision-making in Caesar provides support for accountability. 

In process automation installations, the I/O system connect the field devices to the process controller over a fieldbus, a reliable, real-time capable communication link with signal values cyclical being exchanged with a 10-100 millisecond rate. If a deviation from intended behaviour occurs, analyzing the potentially vast data recordings from the field can be a time consuming and cumbersome task for an engineer. For the engineer to be able to get a full understanding of the problem, knowledge of the used I/O configuration is required. In the problem report, the configuration description is sometimes missing. In such cases it is difficult to use the recorded data for analysis of the problem.In this paper we present our ongoing work towards using neural network models as assistance in the interpretation of an industrial fieldbus communication recording. To show the potential of such an approach we present an example using an industrial setup where fieldbus data is collected and classified. In this context we present an evaluation of the suitability of different neural net configurations and sizes for the problem at hand.

Industrial control systems control and supervise our most important and critical infrastructures, such as power utilities, clean water plants and nuclear plants, as well as the manufacturing industries at the base of our economy. These systems are currently undergoing a transformation driven by the Industry 4.0 evolution, characterized by increased connectivity and flexibility. Consequently, the cybersecurity threat landscape for industrial control systems is evolving as well. Current strategies used for access control within industrial control systems are relatively rudimentary. It is evident that some of the emerging cybersecurity threats related to Industry 4.0 could be better mitigated using more fine-grained access control policies. In this article we discuss and describe a number of access control strategies that could be used within manufacturing systems. We evaluate the strategies in a simulation experiment, using a number of attack-scenarios. Moreover, a method is outlined for automatic policy-generation based on engineering-data, which is aligned with one of the best performing strategies.

In the emerging trend towards modular automation, a need for adaptive, strict access control between interacting components has been identified as a key challenge. In this article we discuss the need for such a functionality, and propose a workflow-driven method for automatic access control policies generation within a modular automation system. The solution is based on recipes, formulated using Sequential Function Charts (SFC). The generated policies are expressed using Next Generation Access Control (NGAC), an Attribute Based Access Control (ABAC) standard developed by NIST. We provide (1) a definition of required policies for device-to device interactions within a modular automation system, (2) an algorithm for automatic generation of access policies, (3) a formal proof of the correctness of this algorithm, and (4) an illustration of its use.

Today’s industrial automation systems are undergoing a digital transformation that implies a shift towards the Internet of Things (IoT), leading to the Industrial Internet of Things (IIoT) paradigm. Existing Industrial Automated Control Systems (IACS), enriched with a potentially large number of IoT devices are expected to make systems more efficient, flexible, provide intelligence, and ultimately enable autonomous control. In general, the majority of such systems come with high level of criticality that calls for well-established methods and approaches when achieving cybersecurity, preferably prescribed by a standard. IEC 62443 is an industrial standard that provides procedures to manage risks related to cybersecurity threats in IACS. Given the new IIoT paradigm, it is likely that existing standards are not sufficiently aligned with the challenges related to developing and maintaining cybersecurity in such systems. In this paper we review the applicability of the IEC 62443 standard in IIoT contexts and discuss potential challenges the process owners might encounter. Our analysis underlines that some areas within the standard could prove difficult to reach compliance with. In particular, handling of cross zone communication and software updates require additional guidance. 

To achieve efficient and flexible production at affordable prices, industrial automation is pushed towards a digital transformation. Such a transformation assumes an enhancement of current Industrial Automated Control Systems with a large amount of IoT-devices, forming an Industrial Internet of Things (IIoT). The aim is to enable a shift from automatic towards autonomous control in such systems. This paper discusses some of the main challenges IIoT systems are facing with respect to cybersecurity. We discuss our findings in an example of a flow-control loop, where we apply a simple threat model based on the STRIDE method to deduce cybersecurity requirements in an IIoT context. Moreover, the identified requirements are assessed in the light of current state of the art solutions, and a number of challenges are discussed with respect to a large-scale IIoT system, together with some suggestions for future work.

Abstract. In the ongoing 4th industrial revolution, a new paradigm of modular and flexible manufacturing factories powered by IoT devices, cloud computing, big data analytics and artificial intelligence is emerging. It promises increased cost efficiency, reduced time-to-market and extreme customization. However, there is a risk that technical assets within such systems will be targeted by cybersecurity attacks. A compromised device in a smart manufacturing system could cause a significant damage, not only economically for the factory owner, but also physically on humans, machinery and the environment. Strict and granular Access Control is one of the main protective mechanisms against compromised devices in any system. In this paper we discuss the requirements and implications of Access Control within the context of Smart Manufacturing. The contributions of this paper are twofold: first we derive requirements on an Access Control Model in the context of smart manufacturing, and then asses the Attribute Based Access Control model against these requirements in the context of a use case scenario.

Dynamic access control in industrial systems is becoming a concern of greater importance as a consequence of the increasingly flexible manufacturing systems developed within the Industry 4.0 paradigm. With the shift from control system security design based on implicit trust toward a zero-trust approach, fine grained access control is a fundamental requirement. In this article, we look at an access control enforcement architecture and authorization protocol outlined as part of the Open Process Communication Unified Automation (OPC UA) protocol that can allow sufficiently dynamic and fine-grained access control. We present an implementation, and evaluates a set of important quality metrics related to this implementation, as guidelines and considerations for introduction of this protocol in industrial settings. Two approaches for optimization of the authorization protocol are presented and evaluated, which more than halves the average connection establishment time compared to the initial approach.

Industrial systems have traditionally been kept isolated from external networks. However, business benefits are pushing for a convergence between the industrial systems and new information technology environments such as cloud computing, as well as higher level of connectivity between different systems. This makes cybersecurity a growing concern for industrial systems. In strengthening security, access control is a fundamental mechanisms for providing security in these systems. However, access control is relatively immature in traditional industrial systems, as compared to modern IT systems, and organizations’ adherence to an established cybersecurity standard or guideline can be a deciding factor for choices of access control techniques used. This paper presents the results of a questionnaire study on the usage of access control within industrial system that are being developed, serviced or operated by Swedish organizations, contrasted to their usage of cybersecurity standards and guidelines. To be precise, the article focuses on two fundamental requirements of cybersecurity: identification and authentication control, and presents related findings based on a survey of the Swedish industry.

Industrial control systems are undergoing a trans-formation driven by business requirements as well as technical advances, aiming towards increased connectivity, flexibility and high level of modularity, that implies a need to revise existing cybersecurity measures. Access control, being one of the major security mechanisms in any system, is largely affected by these advances.In this article we investigate access control enforcement architectures, aiming at the principle of least privilege1 in dynamically changing access control scenarios of dynamic manufacturing systems. Several approaches for permission delegation of dynamic access control policy decisions are described. We present an implementation using the most promising combination of architecture and delegation mechanism for which available industrial standards are applicable.

When developing products or performing experimental research studies, the simulation of physical or logical systems is of great importance for evaluation and verification purposes. For research-, and development-related distributed control systems, there is a need to simulate common physical environments with separate interconnected modules independently controlled, and orchestrated using standardized network communication protocols.The simulation environment presented in this paper is a bespoke solution precisely for these conditions, based on the Modular Automation design strategy. It allows easy configuration and combination of simple modules into complex production processes, with support for individual low-level control of modules, as well as recipe-orchestration for high-level coordination. The use of the environment is exemplified in a configuration of a modular ice-cream factory, used for cybersecurity-related research.

For interconnected and complex systems, security is paramount for establishing trust in their correctness and design adequacy. Thus, security needs to be assured and a corresponding security assurance case needs to be presented to system stakeholders, security assessors, as well as to system users. However, security is dynamic by its nature and to maintain its acceptable security level, frequent updates might be required. Traditionally, a security assurance case is built from scratch whenever a change occurs, however given the cost of resources needed for such a task, a more effective and less time consuming way of handling updates is needed. Hence, the challenge of security case run-time adaptation is considered in this work. We survey the state of the art in security assurance and security case development to refine the challenge and identify system decomposition as one the enablers for security case run-time adaptation. We propose to apply system decomposition in terms of services and use service choreographies to facilitate security case run-time adaptation. The proposed approach is illustrated on an E-gas example.

Today's systems are being built to connect to public or semi-public networks, are able to communicate with other systems, e.g., in the context of Internet-of-Things (IoT), involve multiple stakeholders, have dynamic system reconfigurations, and operate in increasingly unpredictable environments. In such complex systems, assuring safety and security in a continuous and joint effort is a major challenge, not the least due to the increasing number of attack surfaces arising from the increased connectivity. In this paper we present an approach that aims to bridge the gap between safety and security engineering. The potential of the approach is illustrated on the example of E-gas system, discussing the cases when unintentional faults as well as malicious attacks are taken into consideration when assuring safety of the described system. 

A term systems of systems (SoS) refers to a setup in which a number of independent systems collaborate to create a value that each of them is unable to achieve independently. Complexity of a SoS structure is higher compared to its constitute systems that brings challenges in analyzing its critical properties such as security. An SoS can be seen as a set of connected systems or services that needs to be adequately protected. Communication between such systems or services can be considered as a service itself, and it is the paramount for establishment of a SoS as it enables connections, dependencies, and a cooperation. Given that reliable and predictable communication contributes directly to a correct functioning of an SoS, communication as a service is one of the main assets to consider. Protecting it from malicious adversaries should be one of the highest priorities within SoS design and operation. This study aims to investigate the attack propagation problem in terms of service-guarantees through the decomposition into sub-services enriched with preconditions and postconditions at the service levels. Such analysis is required as a prerequisite for an efficient SoS risk assessment at the design stage of the SoS development life cycle to protect it from possibly high impact attacks capable of affecting safety of systems and humans using the system.

Latest technological trends lead toward systems connected to public networks even in critical domains. Bringing together safety and security work is becoming imperative, as a connected safety-critical system is not safe if it is not secure. The main objective of this study is to investigate the current status of safety and security co-analysis in system engineering by conducting a systematic literature review. The steps of the review are the following: the research questions identification; agreement upon a search string; applying the search string to chosen databases; a selection criterion formulation for the relevant publications filtering; selected papers categorization and analysis. We focused on the early system development stages and identified 33 relevant publications categorized as follows: combined safety and security approaches that consider the mutual influence of safety and security; safety-informed security approaches that consider influence of safety on security; and security-informed safety approaches that consider influence of security on safety. The results showed that a number of identified approaches are driven by needs in fast developing application areas, e.g., automotive, while works focusing on combined analysis are mostly application area independent. Overall, the study shows that safety and security co-analysis is still a developing domain.

Being used in key features, such as sensing and intelligent path planning, Artificial Intelligence (AI) has become an inevitable part of automated vehicles (AVs). However, their usage in the automotive industry always comes with a 'label' that questions their impact on the overall AV safety. This paper focuses on the safe deployment of AI-based AVs. Among the various ways for ensuring the safety of AI-based AVs is to monitor the safe execution of the system responsible for automated driving (i.e., Automated Driving System (ADS)) at runtime (i.e., runtime monitoring). Most of the research done in the past years focused on verifying whether the path or trajectory generated by the ADS does not immediately collide with objects on the road. However, as we will show in this paper, there are other unsafe situations that do not immediately result in a collision but the monitor should check for them. To build our case, we have looked into the National Highway Traffic Safety Administration (NHTSA) database of 5.9 million police-reported light-vehicle accidents and categorized these accidents into five main categories of unsafe vehicle operations. Furthermore, we have performed a high-level evaluation of the runtime monitoring approach proposed in [1], by estimating what percentage of the total population of 5.9 million of unsafe operations the approach would be able to detect. Lastly, we have performed the same evaluation on other existing runtime monitoring approaches to make a basic comparison of their diagnostic capabilities.

Manufacturers of self-driving cars need to significantly improve the safety of their products before the series of such cars are deployed in everyday use. A large number of architecture proposals for Automated Driving Systems (ADS) are aiming at addressing the challenge of safety. These solutions typically define redundancy schemes and quite commonly include self-checking pair structures, e.g., commander/monitor approaches. In such structures, the problem of detecting false positive failures arises, i.e., the monitor may falsely classify the output of the commander as being faulty. In this report we provide details regarding a formal verification of an approach aiming at false positive mitigation in the domain of automated driving. We formalize our proposal in an abstract model an

There is a growing interest in using the Blockchain for resolving IoT security and trustworthiness issues existing in today's complex systems. Blockchain concerns trust in peer to peer networks by providing a distributed tamper-resistant ledger. However, the combination of these two emerging technologies might create new problems and vulnerabilities that attackers might abuse.In this paper, we aim to investigate the trust mechanism of Lightweight Scalable BlockChain (LSB), that is a Blockchain specifically designed for Internet of Things networks, to show that a malicious participant in a Blockchain architecture have possibility to pursue an On-Off attack and downgrade the integrity of the distributed ledger. We choose a remote software update process as an instance to represent this violation. Finally, using the actor-based language Rebeca, we provide a model of a system under attack and verify the described attack scenario.

Technical advances as well as continuously evolving business demands are reshaping the need for flexible connectivity in industrial control systems. A way to achieve such needs is by using a service-oriented approach, where a connectivity service middleware provides controller as well as protocol-specific interfaces. The Message Queuing Telemetry Transport (MQTT) protocol is a widely used protocol for device-to-device communication in the Internet of Things (IoT). However it is not commonly integrated in industrial control systems. To address this gap, this paper describes the development and implementation of a prototype of a connectivity service middleware for MQTT within an industrial private control network. The prototype implementation is done in the context of an industrial controller, and used in a simulated modular automation system. Furthermore, various deployment scenarios are evaluated with respect to response time and scalability of the connectivity service.

Abstract—Programmable logic controllers (PLCs), as aspecialized type of embedded systems, have been introduced toincrease system flexibility and reliability, but at the same time togive faster response time and lower cost of implementation. Inthe beginning, their use brought a revolutionary change, but withthe constant growth of system complexity, it became harder toguarantee both functional and extra functional properties, asearly as possible in the development process. In this paper, weshow how formal methods can be applied to describe PLC-basedsystems and illustrate it on an example of a car wash system.First, we show how the existing behavioral modeling languageREMES (REsource Model for Embedded Systems) can beextended to model the behavior of such systems. Second, we showhow REMES can be translated into networks of timed automataand priced timed automata in order to support safety andresource-wise reasoning about PLC systems. The formalverification of PLC systems is carried out in the UPPAAL andUPPAAL CORA tools.

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.