Behavior Trees are increasingly used in the design of autonomous systems. They support modularity and hierarchical composition of requirements. Moreover, they explicitly define the external and internal operating conditions that should be monitored by the system. However, Behavior Trees leave aside the problem of reconfiguration and adaption required to achieve fault tolerant behavior that is implicitly assumed. To address this problem, we propose to integrate FMEA – Failure Modes and Effect Analysis with Behavior Trees to explicitly define the failure conditions and fallback actions. Such an approach facilitates identification of conditions to be monitored under both nominal as well as failure scenarios. It supports holistic modeling of the behavior of a system both under nominal and failure conditions.

Multi-agent systems are examples of complex distributed systems enabling dynamic adaptation in providing their services. By establishing on-the-fly collaborations, the agents can execute complex scenarios and adapt to changing operating conditions including agent failures. We investigate how goal-oriented modelling can enhance reliability by providing a structured support for designing fault tolerant service orchestration.

Side-channel attacks impose a serious threat to cryptographic algorithms, including widely employed ones, such as AES and RSA. These attacks take advantage of the algorithm implementation in hardware or software to extract secret information via side channels. Software masking is a mitigation approach against power side-channel attacks aiming at hiding the secret-revealing dependencies from the power footprint of a vulnerable implementation. However, this type of software mitigation often depends on general-purpose compilers, which do not preserve non-functional properties. Moreover, microarchitectural features, such as the memory bus and register reuse, may also leak secret information. These abstractions are not visible at the high-level implementation of the program. Instead, they are decided at compile time. To remedy these problems, security engineers often sacrifice code efficiency by turning off compiler optimization and/or performing local, post-compilation transformations. This paper proposes Secure by Construction Code Generation (SecCG), a constraint-based compiler approach that generates optimized yet protected against power side channels code. SecCG controls the quality of the mitigated program by efficiently searching the best possible low-level implementation according to a processor cost model. In our experiments with twelve masked cryptographic functions up to 100 lines of code on Mips32 and ARM Thumb, SecCG speeds up the generated code from 77% to 6.6 times compared to non-optimized secure code with an overhead of up to 13% compared to non-secure optimized code at the expense of a high compilation cost. For security and compiler researchers, this paper proposes a formal model to generate power side channel free low-level code. For software engineers, SecCG provides a practical approach to optimize performance critical and vulnerable cryptographic implementations that preserve security properties against power side channels.

Embedded devices are increasingly present in our everyday life. They often process critical information, and hence, rely on cryptographic protocols to achieve security. However, embedded devices remain particularly vulnerable to attackers seeking to hijack their operation and extract sensitive information by exploiting side channels and code reuse. Code-Reuse Attack (CRA) can steer the execution of a program to malicious outcomes, altering existing on-board code without direct access to the device memory. Moreover, Side-Channel Attacks (SCAs) may reveal secret information to the attacker based on mere observation of the device. Thwarting Code-Reuse Attacks (CRAs) and Side-Channel Attacks (SCAs) against embedded devices is especially challenging because embedded devices are usually resource constrained. Fine-grained code diversification can hinder CRAs by introducing uncertainty to the binary code; while software mechanisms can thwart timing or power SCAs. The resilience to either attack may come at the price of the overall efficiency. Moreover, a unified approach that preserves these mitigations against both CRAs and SCAs is not available. In this paper, we propose a novel Secure Diversity by Construction (SecDivCon) approach that tackles this challenge. SecDivCon is a combinatorial compiler-based approach that combines software diversification against CRAs with software mitigations against SCAs. SecDivCon restricts the performance overhead introduced by the generated code that thwarts the attacks and hence, offers a secure-by-design approach enabling control over the performance-security trade-off. Our experiments, using 16 benchmark programs, show that SCA-aware diversification is effective against CRAs, while preserving SCA mitigation properties at a low, controllable overhead. Given the combinatorial nature of our approach, SecDivCon is suitable for small, performance-critical functions that are sensitive to SCAs. SecDivCon may be used as a building block to whole-program code diversification or in a re-randomization scheme of cryptographic code.

Multi-robotic systems are typical examples of com-plex multi-agent systems. The robots - autonomous agents - should cooperate with each other while planning and executing tasks required for achieving various missions. While designing multi-robotic systems, especially for such critical applications as surveillance and rescue operations, we should ensure that the missions could be successfully completed despite robot failures. Therefore, guaranteeing system fault tolerance constitutes an important design goal. However, achieving fault tolerance for multi-agent systems is a notoriously difficult task due to highly decentralized control and asynchronous communication between the agents. In this paper, we propose a formalization of fault tolerance behavior of cooperative mission planning for the multi-robotic system. Our model incorporates such essential fault tolerance mechanisms as the cooperative error recovery and dynamic reconfiguration. To demonstrate how to specify and verify essential fault tolerance requirements, we propose several dedicated mechanisms for knowledge sharing between the robots, which enable cooperative planning. We define the mission as a set of goals that should be accomplished by a collaborative functioning of the robots and derive the conditions for enabling fault tolerant planning and coordinated execution.

Microservices is an increasingly popular architectural style that promotes structuring an application as a collection of loosely coupled fine-grained services. Typically, each microservice accesses different data. Hence, while composing complex applications, a special emphasis should be put on monitoring data access and privacy protection. In this paper, we formalise the main privacy preservation constraints in the applications developed in the microservices architectural style.

Despite the growing popularity of swarm-based applications of drones, there is still a lack of approaches to maximize the safety of swarms of drones by minimizing the risks of drone collisions. In this paper, we present an approach that uses optimization, learning, and automatic immediate responses (reflexes) of drones to ensure safe operations of swarms of drones. The proposed approach integrates a high-performance dynamic evolutionary algorithm and a reinforcement learning algorithm to generate safe and efficient drone routes and then augments the generated routes with dynamically computed drone reflexes to prevent collisions with unforeseen obstacles in the flying zone. We also present a parallel implementation of the proposed approach and evaluate it against two benchmarks. The results show that the proposed approach maximizes safety and generates highly efficient drone routes.

Authorization is an important security concern in cloud computing environments. It aims at regulating an access of the users to system resources. A large number of resources associated with REST APIs typical in cloud makes an implementation of security requirements challenging and error-prone. To alleviate this problem, in this paper we propose an implementation of security cloud monitor. We rely on model-driven approach to represent the functional and security requirements. Models are then used to generate cloud monitors. The cloud monitors contain contracts used to automatically verify the implementation. We use Django web framework to implement cloud monitor and OpenStack to validate our implementation.

REST APIs are being increasingly used in the industry including their application in safety-critical domain and in the IoT world. They offer basic CRUD (create, retrieve, update and delete) interfaces. However, REST APIs can be used to build services with more advanced scenarios. Developing such services with REST constraints requires rigorous approaches that are capable of creating services that can be trusted for their behavior. In this work, we present an approach based on formal verification technique for a development of REST services using Event-B. We focus on deriving a correct system architecture by refinement and consistency verification of service design models. We illustrate our approach on a Hotel Reservation System.

Swarms of drones are increasingly been used in a variety of monitoring and surveillance, search and rescue, and photography and filming tasks. However, despite the growing popularity of swarm-based applications of drones, there is still a lack of approaches to generate efficient drone routes while minimizing the risks of drone collisions. In this paper, we present a novel approach that integrates learning, optimization, and prediction for generating efficient and safe routes for swarms of drones. The proposed approach comprises three main components: (1) a high-performance dynamic evolutionary algorithm for optimizing drone routes, (2) a reinforcement learning algorithm for incorporating the feedback and runtime data about the system state, and (3) a prediction approach to predict the movement of drones and moving obstacles in the flying zone. We also present a parallel implementation of the proposed approach and evaluate it against two benchmarks. The results demonstrate that the proposed approach allows to significantly reduce the route lengths and computation overhead while producing efficient and safe routes.

Swarms of drones are increasingly deployed to perform a variety of monitoring tasks. However, despite a growing popularity of swarm-based monitoring solutions, there is still a lack of approaches that allow the designers to ensure that a swarm configuration maximizes coverage of the monitored area and delivers the desired quality of the monitored data. A drone might fail or run out of energy and hence leave some blind spots in the monitored area. Moreover, an inefficient configuration resulting in the energy-greedy communication can quickly deplete the batteries of the drones and force a premature mission termination. We propose a novel data-driven integrated solution that combines learning and optimization over the streams of monitored data to ensure fault tolerance and efficiency of the swarm navigation. The benchmarking results demonstrate that the proposed approach allows us to significantly improve the coverage and energy efficiency characteristics.

Abstract Dependability is a property of a computer system to deliver services that can be justifiably trusted. Formal modelling and verification techniques are widely used for development of dependable computer-based systems to gain confidence in the correctness of system design. Such techniques include Event-B—a state-based formalism that enables development of systems correct-by-construction. While Event-B offers a scalable approach to ensuring functional correctness of a system, it leaves aside modelling of non-functional critical properties, e.g., reliability and responsiveness, that are essential for ensuring dependability of critical systems. Both reliability, i.e., the probability of the system to function correctly over a given period of time, and responsiveness, i.e., the probability of the system to complete execution of a requested service within a given time bound, are defined as quantitative stochastic measures. In this paper, we propose an extension of the Event-B semantics to enable stochastic reasoning about dependability-related non-functional properties of cyclic systems. We define the requirements that a cyclic system should satisfy and introduce the notions of reliability and responsiveness refinement. Such an extension integrates reasoning about functional correctness and stochastic modelling of non-functional characteristics into the formal system development. It allows the designer to ensure that a developed system does not only correctly implement its functional requirements but also satisfies given non-functional quantitative constraints.

editorial Free AccessKaisa Sere: In Memoriam Authors: Luigia Petre Department of Information Technologies, Åbo Akademi University, Joukahaisenkatu 3-5A, 20520, Turku, Finland Department of Information Technologies, Åbo Akademi University, Joukahaisenkatu 3-5A, 20520, Turku, FinlandSearch about this author , Elena Troubitsyna Department of Information Technologies, Åbo Akademi University, Joukahaisenkatu 3-5A, 20520, Turku, Finland Department of Information Technologies, Åbo Akademi University, Joukahaisenkatu 3-5A, 20520, Turku, FinlandSearch about this author , Marina Waldén Department of Information Technologies, Åbo Akademi University, Joukahaisenkatu 3-5A, 20520, Turku, Finland Department of Information Technologies, Åbo Akademi University, Joukahaisenkatu 3-5A, 20520, Turku, FinlandSearch about this author Authors Info & Claims Formal Aspects of ComputingVolume 26Issue 2Mar 2014 pp 197–201https://doi.org/10.1007/s00165-013-0292-5Published:01 March 2014Publication History 0citation11DownloadsMetricsTotal Citations0Total Downloads11Last 12 Months9Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

Modes are widely used to structure the behaviour of control systems. For many such systems, derivation and verification of a mode logic is challenging due to a large number of modes and complex mode transitions. In this paper we propose an approach to deriving, formalising and verifying consistency of a mode logic for fault tolerant control systems. We demonstrate how to use Failure Modes and Effects Analysis (FMEA) to systematically derive the fault tolerance part of the mode logic. To tackle the problem of mode consistency, we propose a formalisation of the mode logic and mode consistency conditions for layered systems with reconfigurable components. We use our formalisation to develop and verify a mode-rich system by refinement in Event-B.

Distributed systems are usually large and complex systems composed of various components. System components are subject to various errors. These failures often require error recovery to be conducted at architectural-level. However, due to complexity of distributed systems, specifying fault tolerance mechanisms at architectural level is complex and error prone. In this paper, we propose a formal approach to specifying components and architectures of fault tolerant distributed and reactive systems. Our approach is based on refinement in the action system formalism - a framework for formal model-driven development of distributed systems. We demonstrate how to specify and refine fault tolerant components and complex distributed systems composed of them. The proposed approach provides designers with a systematic method for developing distributed fault tolerant systems.

Developing fault tolerant ambient systems requires many challenging factors to be considered due to the nature of such systems, which tend to contain a lot of mobile elements that change their behavior depending on the surrounding environment, as well as the possibility of their disconnection and reconnection. It is therefore necessary to construct the critical parts of fault tolerant ambient systems in a rigorous manner. This can be achieved by deploying formal approach at the design stage, coupled with sound framework and support at the implementation stage. In this paper, we briefly describe a middleware that we developed to provide system structuring through the concepts of roles, agents, locations and scopes, making it easier for the developers to achieve fault tolerance. We then outline our experience in developing an ambient lecture system using the combination of formal approach and our middleware

Currently UML2 is widely used for modelling software-intensive systems. Model driven development of complex software typically starts from abstract, high-level UML2 models which specify the system from several different viewpoints. Abstract models are further refined into more detailed design models in successive development stages. While specifying various aspects and abstraction levels of such systems, we create a set of different models, which should be inter- and intra-consistent. In this paper we propose an approach to ensuring consistency in Lyra – a rigorous, service-oriented and model-based method for developing industrial telecommunication systems and communication protocols. We derive informal requirements to ensuring intra- and inter-consistency and then formalize them in the B Method. The formalization in B allows us to structure complex informal requirements and formally ensure intra- and inter-consistency of models created at various stages of the Lyra development.

Transient faults constitute a wide-spread class of faults typical in control systems. These are faults that appear for some time during system operation and might disappear and reappear later. However, even by appearing for a short time, they might cause dangerous system errors. Hence designing mechanisms for tolerating transient faults is an acute issue, especially in the development of safety-critical control systems. In this paper we propose a formal approach to specifying software-based mechanisms for tolerating transient faults in the B method. We focus on deriving a general specification and development pattern which can be applied in the development of various control systems. We illustrate an application of the proposed patterns by an example from avionics software product line.

A probabilistic extension of the refinement calculus has been successfully applied in the design of safety-critical systems. The approach is based on a firm mathematical foundation within which the reasoning about correctness and behavior of the system under construction is carried out. The framework allows us also to obtain a quantitative assessment of the attributes of system dependability. We present an extension of our main design technique-refinement-the so-called parameterized refinement. The purpose of the extension is to create a technique which facilitates refinement of a system in such a way that the dependability of the implementation would be maximal. We mostly focus on the reliability aspect. The parameterized refinement resolves the problem of how to build more reliable systems by incorporating statistical information about a controlled environment and reliabilities of system components in the development process. We illustrate this by a case study-the development of a state monitoring system.