Contains fulltext : 331392.pdf (Publisher’s version ) (Open Access)

In the context of modern day embedded safety-critical systems and low-resource edge devices in particular, Sigma-Delta Neural Networks (SDNNs) offer a promising alternative to traditional Artificial Neural Networks (ANNs) by leveraging event-driven, sparse computations inspired by biological neural processing. This energy-efficient paradigm makes SDNNs well-suited for neuromorphic hardware and real-time applications, particularly in scenarios with temporal redundancy, such as video processing. However, as neural networks become integral to safety-critical systems, ensuring their robustness against adversarial perturbations is an absolute necessity. In this work, we propose an end-to-end framework for formal modeling and verification of SDNNs using Satisfiability Modulo Theory (SMT). Unlike empirical robustness evaluations, SMT-based verification provides formal guarantees by encoding SDNN behavior and adversarial robustness properties as mathematical constraints. We introduce an SMT-based formulation for encoding SDNNs with SMT constraints and define a robustness property motivated by video stream processing. Our approach systematically examines how well SDNNs can handle adversarial attacks, ensuring they work correctly in safety-critical applications. We validate our framework through experiments on temporal version of the MNIST dataset. To the best of our knowledge, this is the first formal verification framework for SDNNs, bridging the gap between neuromorphic computing and rigorous verification.

In this paper, we address the problem of safety verification for Spiking Neural Networks (SNNs) with Spiking Rectified Linear Activation (SRLA). The SNNs are obtained by first training Artificial Neural Networks (ANNs) and then translating to SNN with subsequent hyperparameter tuning. We propose a solution which tunes the temporal window hyperparameter of the translated SNN to ensure both accuracy and compliance with the safe range specification that requires the SNN outputs to remain within a safe range. We demonstrate our approach with experiments on 5 benchmark neural controllers.

5G advanced network slicing use cases have gained momentum with the ability to provide differentiated Quality of Service (QoS) to various services (voice, mobile broadband, gaming, eXtended Reality, enterprise). However, it is essential to implement adaptive and scalable Network Slice Assurance to ensure differentiated service performance with varying traffic and dynamic requirements. The intent-driven network management paradigm aims at building autonomous systems with minimal expert-driven policies, which may be applied to slice assurance. In this paper, we propose Convergence, a cognitive intent driven framework for 5G Radio Access Network (RAN) slice assurance. Via the use of intelligent agents registered during the prediction, assurance, evaluation and actuation phases, emerging issues in slice assurance may be handled autonomously. In particular, Artificial Intelligence (AI) planning agents are exploited to generate partition over-use, partition top-up or partition ramp-down actions dynamically. The slice assurance framework is demonstrated over a real-world operator use case with multiple slices and intent specifications.

With the emergence of Industry 4.0, comes an increasing need for multi-robot coordination and communication to efficiently complete joint tasks. A critical technology is the fifth generation (5G) mobile network, which enables cloud-controlled robots to execute tasks with differentiated quality-of-service (QoS) features. While there has been significant research on multi-robot planning, the integration with the capabilities of realistic network systems has been limited. In this paper, we introduce RoboPlan5G, a framework for 5G-aware robot planning. We propose a joint state-search model that includes task planning coordination in conjunction with 5G physical resource block (PRB) allocation. This process ensures efficient usage of the limited indoor 5G spectrum and effective service performance, while still aiming for the completion of tasks in the shortest possible time frame. Scenarios are generated in an Industry 4.0 environment, where the planner is shown to decrease the required 5G spectrum allocation by 50%, and on average improve the plan quality by 45% while maintaining a small computation time.

With the emergence of Industry 4.0, comes an increasing need for multi-robot coordination and communication to efficiently complete joint tasks. A critical technology is the fifth generation (5G) mobile network, which enables multiple robots to execute control tasks with differentiated quality-of-service (QoS) features. However, there has been limited analysis of the impact of real 5G capabilities on multi-agent robot planning problems. In this paper, we provide a review of robot planning algorithms suitable for industrial use-cases, which consider communication aspects in the planning formulation. The paper is further positioned to identify gaps in existing state of the art within communication-aware planning. This is followed by an analysis of key challenges to be targeted at the intersection of 5G, Industry 4.0 and multi-agent robot planning. This analysis is strategically important and would prove useful to academic researchers and industry experts focusing on deployment of robots in industrial settings.

5G Radio Access Network (RAN) slicing concerns strategies to share radio resources while guaranteeing differentiated service requirements. Current state of the art approaches make use of strict isolation or dedicated RAN physical resource block (PRB) partitioning among slices to ensure differentiated services. However, spectrum multiplexing may be rendered suboptimal due to isolation of resources; it further cannot handle variations in traffic patterns or intents in a dynamic way. In this paper, we propose a flexible multi-service partitioning strategy that can balance functional isolation and optimal sharing of resources. This system, called Muesli: Multi-objective Radio Resource Slice Management, makes use of model-based reinforcement learning techniques to dynamically modify PRB partitions. The reinforcement learning reward structure ensures that the system is trained to meet multiple objectives such as network slice Service Level Agreement (SLA) compliance, spectrum usage efficiency and fairness among customer classes. On a real use case from Ericsson, the throughput levels for individual services are shown to be optimized with accurate PRB partitioning.

With the rapid proliferation of strategic alliances between service providers, enterprises cooperate towards service quality improvement and provide lower cost service bundles. This article presents a novel solution to the minimum cost service bundle selection problem for workflows in the presence of singleton subscription costs and service bundle offerings and compatibility requirements. Given a workflow specifying a set of tasks and a set of candidate services for each task, with a set of compatibility constraints between services, the selection problem has the objective of selecting the most suitable service offering(s) for each task. In this article, we analyze the selection problem in the presence of service bundle offerings. We present a novel multi-partite hyper-graph visualization of the selection problem and analyze its hardness. Additionally we present a novel combination of ILP and abstraction refinement as a potential solution, that is shown to expedite a naïve ILP based solution. We present experiments to substantiate this claim.

Realization of industry-scale, goal-driven, autonomous systems with AI planning technology faces several challenges: flexibly specifying planning goal states in varying situations, synthesizing plans in large state spaces, re-planning in dynamic situations, and facilitating humans to supervise, give feedback and intervene. In this paper, we present Intent-driven Strategic Tactical Planning (ISTP) to address these challenges. We demonstrate its efficacy through its application for radio base station inspection across several locations using drones. The inspection task involves capturing images, thermal images or signal measurements - called knowledge-objects - of various components of the base stations for downstream processing. In the ISTP approach, an operator indicates her goals by flying the drone to different components of interest. These goals are generalized to capture the intent of the operator, which are then instantiated in new situations to generate goals dynamically. Towards planning and re-planning in large state spaces to achieve these goals efficiently, we extend the Strategic-Tactical Planning paradigm. All the components of ISTP are integrated in an intuitive UI and demonstrated through a real life use-case built on the UNITY simulator platform.

Well-connected, regulatory compliant flight paths are crucial for UAVs to be adopted in mission-critical applications. In this paper, we present the Connectivity-Aware Path plannEr with Regulatory compliance (CAPER): a solution for planning safe, cellular-connected UAV paths in environments with heterogeneous connectivity regions, such that the planned paths comply with regulatory no-fly zones and height constraints. CAPER builds on the sampling-based planner Rapidly-exploring Random Trees (RRT), and makes a number of algorithmic modifications both in the planner and the collision detector. RRT has seen widespread use in planning paths in robotics, due to its ability to quickly search high dimensional spaces for feasible paths. However, several challenges exist in adopting RRTs for the connectivity-aware path planning problem in realistic spaces, which CAPER seeks to alleviate. In this paper we detail CAPER, and present results of its implementation in two realistic urban environments in Stockholm and Los Angeles. Since CAPER is built on the randomized algorithm RRT, we also present a brief analysis of multiple runs within the same environment.

Service-oriented Architecture (SOA) has been recognized as a key technology for operating IoT-based systems, by abstracting sensing and actuation capabilities of IoT resources via services or microservices. However, such systems being dynamic in nature, must be proactive in responding to changing circumstances, hence they need to be autonomic in nature. Therefore this requires the design and deployment of an autonomic serviceoriented middleware that can mediate interactions, and control sensing & actuation, within the IoT-based system. To that end, in this paper, we present our vision of an autonomic service-oriented middleware AUSOM (pronounced "awesome") for IoT based systems. The key features of AUSOM are: incorporation of the well-known MAPE-K loop (Monitor, Analyze, Plan, Act, using stored Knowledge) from autonomic computing for proactive adaptation, incorporation of a multilayered context model, and using contextual information to facilitate adaptation at the IoT device (sensor and actuator) layer. We present the architecture of AUSOM and also illustrate how it would function via a simple yet realistic example.

SUMMARY Model‐based test generation techniques based on random input generation and guided simulation do not satisfy the demands of high test coverage and completeness guarantees as required by safety‐critical applications. Recently, test generation techniques based on model checking have been reported to bridge this gap. To evaluate the effectiveness of these techniques, an in‐house tool suite, AutoMOTGen, has been developed for Simulink/Stateflow and applied on real‐life case studies at General Motors. This paper outlines the test generation methodology of AutoMOTGen and gives a comparative study with a commercial, primarily random input‐based, test generation tool on the same set of examples. The results indicate that in terms of coverage, model checking‐based techniques complement the random input‐based techniques. In addition, they provide proofs for unreachability that can aid in debugging the models. Therefore, it is recommended that model checking‐based tools be utilized to complement and enhance the effectiveness of model‐based testing methods in safety‐critical systems engineering. Copyright © 2013 John Wiley & Sons, Ltd.

Correct functioning of automotive embedded controllers requires hard real-time constraints on a number of system parameters. To avoid costly design iterations, these timing constraints should be verified during the design stage itself. In this paper, we describe a formal verification technique for a class of timing constraints called timing synchronization constraints in the recent adaptation of AUTOSAR standard (WPII-1.2 Timing Subgroup, Release 4.0). These constraints require, unlike the well studied end-to-end latency constraint, simultaneous analysis of multiple task/message chains or multiple data items traversing through a task/message chain. We show that they can be analyzed by model-checking with finite-state monitors. We also demonstrate this method on a case-study from the automotive domain.

In a Software Product Line (SPL), the central notion of implementability provides the requisite connection between specifications (feature sets) and their implementations (component sets), leading to the definition of products. While it appears to be a simple extension (to sets) of the trace-ability relation between components and features, it actually involves several subtle issues which are overlooked in the definitions in existing literature. In this paper, we give a precise and formal definition of implementability over a fairly expressive traceability relation to solve these issues. The consequent definition of products in the given SPL naturally entails a set of useful analysis problems that are either refinements of known problems, or are completely novel. We also propose a new approach to solve these analysis problems by encoding them as Quantified Boolean Formula(QBF) and solving them through Quantified Satisfiability (QSAT) solvers. The methodology scales much better than the SAT-based solutions hinted in the literature and is demonstrated through a prototype tool called SPLANE (SPL Analysis Engine), on a couple of fairly large case studies.

Exhaustive state space exploration based verification of embedded system designs remains a challenge despite three decades of active research into Model Checking. On the other hand, simulation based verification of even critical embedded system designs is often subject to financial budget considerations in practice. In this paper, we suggest an algorithm that minimizes the overall cost of producing an embedded system including the cost of testing the embedded system and expected losses from an incompletely tested design. We seek to quantify the trade-off between the budget for testing and the potential financial loss from an incorrect design. We demonstrate that our algorithm needs only a logarithmic number of test samples in the cost of the potential loss from an incorrect validation result. We also show that our approach remains sound when only upper bounds on the potential loss and lower bounds on the cost of simulation are available. We present experimental evidence to corroborate our theoretical results.

Embedded control systems in automobiles are typically implemented by a set of tasks deployed on multiple Electronic Control Units (ECUs) communicating via one or more buses like CAN or FlexRay. In the case of safety-critical systems, there are hard real-time bounds on the (i) response times of tasks/messages, and (ii) end-to-end latencies of certain task/message chains. These depend on various factors like the number of tasks (and messages) involved in the processing (and communication) sequence, parameters of these tasks/messages, scheduling policies, communication protocols, clock drifts, etc. Moreover, since the data transfer among tasks/messages is typically via asynchronous buffers that are overwritable and sticky, multiple semantics are possible for end-to-end latency. Hence, precise estimation of response times and end-to-end latencies in embedded systems is a non-trivial problem.

End-to-end latency of messages is an important design parameter that needs to be within specified bounds for the correct functioning of distributed real-time control systems. In this paper we give a formal definition of end-to-end latency, and use this as the basis for checking whether a stipulated deadline is violated within a bounded time. For unbounded verification, we model the system as a set of communicating Timed Automata, and perform reachability analysis. The proposed method takes into account the drift of clocks which is shown to affect the latency appreciably. The method has been tested on a medium sized automotive example.