Recently, centralized receding horizon online multi-robot coverage path planning algorithms have shown remarkable scalability in thoroughly exploring large, complex, unknown workspaces with many robots. In a horizon, the path planning and the path execution interleave, meaning when the path planning occurs for robots with no paths, the robots with outstanding paths do not execute, and subsequently, when the robots with new or outstanding paths execute to reach respective goals, path planning does not occur for those robots yet to get new paths, leading to wastage of both the robotic and the computation resources. As a remedy, we propose a centralized algorithm that is not horizon-based. It plans paths at any time for a subset of robots with no paths, i.e., who have reached their previously assigned goals, while the rest execute their outstanding paths, thereby enabling concurrent planning and execution. We formally prove that the proposed algorithm ensures complete coverage of an unknown workspace and analyze its time complexity. To demonstrate scalability, we evaluate our algorithm to cover eight large 2D grid benchmark workspaces with up to 512 aerial and ground robots, respectively. A comparison with two state-of-the-art horizon-based algorithms shows its superiority in completing the coverage with up to 1.6× speedup. For validation, we perform ROS + Gazebo simulations in six 2D grid benchmark workspaces with 10 Quadcopters and TurtleBots, respectively. We also successfully conducted one outdoor experiment with three quadcopters and one indoor with two TurtleBots.

Introduction to the Special Issue on Formal Methods and Models for System DesignThe ACM-IEEE International Symposium on Formal Methods and Models for System Design (MEMOCODE) brings together researchers and practitioners interested in formal methods for system design and development to exchange ideas, research results, and lessons learned.The symposium focuses on the foundations and applications of formal methods in the development of hardware, firmware, middleware, and application software for systems, ranging from single embedded devices to highly networked cyber-physical systems and the Internet of Things.MEMOCODE is unique in the way it merges the formal community with the hands-on design community, and it creates a forum where principle meets practice.The 20th edition of MEMOCODE was a part of ESWEEK 2022, which was held as a hybrid event, with the onsite component in Shanghai, China, October 7-14, 2022.This special issue in the ACM Transactions on Embedded Computing Systems considers peer-reviewed journal versions of top papers from this MEMOCODE edition, as well as other papers received from the open call.We thank the involved reviewers, who were selected based on their expertise on the topics of the submissions.Most of the submissions went through two rounds of reviews, including both major and minor revisions, to further enhance their technical quality.For instance, in the first round, on average, we had four reviews per submission.Thorough revisions were made by the authors, and careful revision reviewing and cross-checking were done by the reviewers and the guest editors to ensure that the revisions comprehensively addressed all the comments.This represents a tremendous effort by the authors, reviewers, guest editors, technical and administrative staff of TECS, and the editor-in-chief.Here is the list of the articles included in this special issue:• The article "Real-time Fixed Priority Scheduling Synthesis Using Affine Dataflow Graphs: From Theory to Practice" presents an approach to automatically generate fixed priority schedules from a dataflow specification.To do so, precedence dependencies between actors in the dataflow graphs are abstracted, as well as the task periods, by using affine relations.This abstraction allows one to synthesize schedules efficiently considering two main objectives: the maximization of throughput and the minimization of buffer sizes. • The article "AMULET: A Mutation Language Enabling Automatic Enrichment of SysMLModels" introduces AMULET, the first mutation language for SysML. While model-based design methods often require successive modifications of the models, AMULET encompasses the modifications targeting SysML block and state-machine diagrams.The proposed

We study a variant of the multi-robot goal assignment problem where a unique goal to each robot needs to be assigned while minimizing the largest cost of movement among the robots, called makespan. A significant step in solving this problem is to find the cost associated with the robot-goal pairs, which requires solving a complex path planning problem. We present OM, a scalable optimal algorithm that solves the multi-robot goal assignment problem by computing the paths for a significantly less number of robot-goal pairs compared to the state-of-the-art algorithms, leading to a computationally superior mechanism to solve the problem. We extensively evaluate our algorithm for hundreds of robots on randomly generated and standard workspaces. Our experimental results demonstrate that the proposed algorithm achieves a noticeable speedup over two state-of-the-art baseline algorithms.

We present an online centralized path planning algorithm to cover a large, complex, unknown workspace with multiple homogeneous mobile robots. Our algorithm is horizon-based, synchronous, and on-demand. The recently proposed horizon-based synchronous algorithms compute all the robots’ paths in each horizon, significantly increasing the computation burden in large workspaces with many robots. As a remedy, we propose an algorithm that computes the paths for a subset of robots that have traversed previously computed paths entirely (thus on-demand) and reuses the remaining paths for the other robots. We formally prove that the algorithm guarantees complete coverage of the unknown workspace. Experimental results on several standard benchmark workspaces show that our algorithm scales to hundreds of robots in large complex workspaces and consistently beats a state-of-the-art online centralized multi-robot coverage path planning algorithm in terms of the time needed to achieve complete coverage. For its validation, we perform ROS+Gazebo simulations in five 2D grid benchmark workspaces with 10 Quadcopters and 10 TurtleBots, respectively. Also, to demonstrate its practical feasibility, we conduct one indoor experiment with two real TurtleBot2 robots and one outdoor experiment with three real Quadcopters.

Deep Reinforcement Learning (DRL) has the potential to be used for synthesizing feedback controllers (agents) for various complex systems with unknown dynamics. These systems are expected to satisfy diverse safety and liveness properties best captured using temporal logic. In RL, the reward function plays a crucial role in specifying the desired behaviour of these agents. However, the problem of designing the reward function for an RL agent to satisfy complex temporal logic specifications has received limited attention in the literature. To address this, we provide a systematic way of generating rewards in real-time by using the quantitative semantics of Signal Temporal Logic (STL), a widely used temporal logic to specify the behaviour of cyber-physical systems. We propose a new quantitative semantics for STL having several desirable properties, making it suitable for reward generation. We evaluate our STL-based reinforcement learning mechanism on several complex continuous control benchmarks and compare our STL semantics with those available in the literature in terms of their efficacy in synthesizing the controller agent. Experimental results establish our new semantics to be the most suitable for synthesizing feedback controllers for complex continuous dynamical systems through reinforcement learning.

Self-triggered controllers have the potential to improve the state-of-the-art of Cyber-Physical Systems (CPSs) by enhancing the performance of the underlying closed-loop control systems. However, a major concern in deploying a self-triggered controller in a safety-critical CPS is that the stabilizing self-triggered controller may not always guarantee the satisfaction of the safety constraints. We propose a self-triggered control scheme that deals with the safe scheduling of control tasks for uncertain continuous-time linear systems. We derive a computationally efficient scheduling function that computes an upper bound on the next sampling period as a function of the current state in the presence of additive disturbance. To reduce the computational complexity of online reachability analysis and increase accuracy, we compute a large sequence of reachable sets offline and use these precomputed sets to derive a low-complexity online scheduling function that computes sufficiently large bounds in real time. We evaluate our algorithm on three high-dimensional benchmark control systems, where two of the examples have a twelve-dimensional joint state plus feedback input. Experimental results demonstrate that our self-triggered control algorithm guarantees the safety of the closed-loop control system through negligible online computation, establishing the feasibility of its practical implementation.

Optimal placement of charging stations in a workspace is a crucial problem to address, for efficient operation of battery-driven mobile robots. When the battery charge of a robot reaches a certain threshold, the robot must be able to reach a nearby charging station to recharge its battery. In this paper, we deal with two different versions of the optimization problem related to the optimal placement of charging stations in a robot workspace. The first problem is formulated to find an optimal number of charging stations given a battery threshold deciding the need to move to a charging station, and the second problem finds an optimal battery threshold for a given number of charging stations. Both the problems involve finding the locations of charging stations, such that from any obstacle-free location at least one charging station is reachable with at most threshold amount of battery charge remaining with the robot. In this paper, we prove these optimization problems to be NP-hard, i.e., computationally intractable. To handle intractability of the above minimization problems, we design two polynomial-time approximation algorithms to find near-optimal solutions. Our algorithms achieve significantly high scalability without compromising the quality of the solution beyond a certain factor of the optimal solution. Experimental results show that our algorithms run order-of-magnitude faster than a recently proposed Satisfiability Modulo Theory (SMT)-based approach and maintain solution quality within the theoretical bounds on the optimal solution.

In piecewise linearization based reachable set computation, different linear approximations are computed around smaller pieces of the reachable set to reduce the linearization error in reachability analysis. However, this approach suffers from curse of dimensionality because the number of pieces required to restrict the linearization error below a threshold can blow up intractably for high-dimensional systems. Alternatively, we can fix the maximum number of divisions of the reachable set and optimize the division vector to minimize the linearization error. But the functions projecting the linearization error along different directions can be different, which have different optimal solutions for the division vector. Still, we may need to minimize the linearization error along multiple directions to achieve good accuracy along any one direction because the differential equations can be coupled. Therefore, we develop a new method of piecewise linearization based reachable set computation that incorporates different optimized divisions of reachable set for different projections of linearization error to improve accuracy. To do so, we use intersection of unions of sets (IoU) to approximate reachable sets such that different unions in the intersection are obtained from optimized division along different directions and forward propagation. We develop an algorithm to propagate the reachable set of the IoU in a coupled way, such that each intersecting union complements the approximation accuracy of other unions. We validate the advantage of using multiple optimal divisions instead of one optimized division. For this, we compare the performance on high dimensional examples, of the proposed algorithm with a variant of the algorithm which uses only one division vector at each time step. We also draw comparison with state-of-the-art methods and demonstrate that the accuracy of our algorithm is at par or better for the benchmarks.

We present a method to find the optimal control strategy for a robot using prior information of localization that maximizes the probability of satisfaction of a temporal logic specification while considering the uncertainty in both motion and sensing, two major causes for localization uncertainty. The specifications are given in the probabilistic computation tree logic (PCTL) formulae over a set of propositions, which capture the presence of the robot in some key locations in the environment. A computation model that can deal with the uncertainty in both motion and sensing is the Partially Observable Markov Decision Process (POMDP), which is computationally expensive. We approximate the underlying POMDP using Augmented Markov Decision Process (AMDP) and present a control synthesis algorithm for AMDP. We carry out numerous experiments on workspaces with sizes up to 100 × 100 and three different PCTL specifications to evaluate the efficacy of our technique. Experimental results show that our technique for computing robot control policy using localization prior can deal with localization uncertainty effectively and scale to large environments.

We address the path planning problem for a team of robots satisfying a complex high-level mission specification given in the form of a Linear Temporal Logic (LTL) formula. The state-of-the-art approach to this problem employs the automata-theoretic model checking technique to solve this problem. This approach involves computation of a product graph of the Büchi automaton generated from the LTL specification and a joint transition system that captures the collective motion of the robots and then computation of the shortest path using Di-jkstra's shortest path algorithm. We propose MT*, an algorithm that reduces the computation burden for generating such plans for multi-robot systems significantly. Our approach generates a reduced version of the product graph without computing the complete joint transition system, which is computationally expensive. It then divides the complete mission specification among the participating robots and generates the trajectories for the individual robots independently. Our approach demonstrates substantial speedup in terms of computation time over the state-of-the-art approach and scales well with both the number of robots and the size of the workspace.

Online coverage path planning to explore an unknown workspace with multiple homogeneous robots could be either centralized or distributed. While distributed planners are computationally faster, centralized planners can produce more efficient paths, reducing the duration of completing a coverage mission significantly. To exploit the power of a centralized framework, we propose a receding horizon centralized online multi-robot planner. In each planning horizon, it generates collision-free paths that guide the robots to visit some obstacle-free locations (aka goals) not visited so far, which in turn help them explore some new regions with their laser rangefinders. We formally prove that, under reasonable conditions, it enables the robots to cover a workspace completely and subsequently analyze its time complexity. We evaluate our planner for ground and aerial robots by performing experiments with up to 128 robots on six 2D grid-based benchmark obstacle maps, establishing scalability. We also perform Gazebo simulations with 10 quadcopters and real experiments with 2 four-wheel ground robots, demonstrating its practical feasibility. Further-more, a comparison with a state-of-the-art distributed planner establishes its superiority in coverage completion time.

Quantized deep neural networks (DNNs) have the potential to find wide applications in safety-critical cyber–physical systems implemented on processors supporting only integer arithmetic. The significant challenge therein is to ensure the correctness of the operation of the network with its approximated computation. To address this verification challenge formally, we present a methodology to encode the verification problem into a mixed-integer linear programming (MILP) problem. Our encoding is based on the bit-precise semantics of quantized neural networks, which ensures the soundness of our method. We implement our verification methodology using the Gurobi MILP solver and evaluate it on several widely used DNN benchmarks. We compare our method with state-of-the-art bit-vector encodings, which are outperformed by our MILP-based verification methodology by an order of magnitude in most cases. These experimental results establish our MILP-based verification technique as a powerful tool for developing formally verified safety-critical systems with quantized DNNs as a component.

Efficient recharging is an essential requirement for autonomous mobile robots. In an indoor robotic application, charging stations can be installed offline. However, frequent trips to the charging stations cause inefficiency in the performance of the mobile robots. In an outdoor environment, a charging station cannot even be installed easily. We propose a framework and algorithms for enabling a group of mobile wireless rechargers to fulfill the energy requirement of autonomous mobile robots in a workspace efficiently. Our algorithm finds the optimal trajectories for the mobile rechargers in such a way that once there is a need for a recharge, the robots do not need to spend significant time and energy to get access to a recharger. Our algorithm is based on a reduction of the problems to Satisfiability Modulo Theory (SMT) solving problems. We present extensive experimental results to show that the optimal trajectories for mobile rechargers can be generated successfully for different types of robots and workspaces within a reasonable time. Moreover, a comparison with the performance of static charging stations establishes that mobile rechargers are more effective in terms of allowing the autonomous robot to continue their work for a longer time.

In many multi-robot applications, mobile worker robots are often engaged in performing some tasks repetitively by following pre-computed trajectories. As these robots are battery-powered, they need to get recharged at regular intervals. We envision that, in the future, a few mobile recharger robots will be employed to supply charge to the energy-deficient worker robots recurrently to keep the overall efficiency of the system optimized. In this setup, we need to find the time instants and locations for the meeting of the worker robots and recharger robots optimally. We present a Satisfiability Modulo Theory (SMT)-based approach that captures the activities of the robots in the form of constraints in a sufficiently long finite-length time window (hypercycle) whose repetitions provide their perpetual behavior. Our SMT encoding ensures that for a chosen length of the hypercycle, the total waiting time of the worker robots due to charge constraints is minimized under certain condition, and close to optimal when the condition does not hold. Moreover, the recharger robots follow the most energy-efficient trajectories. We show the efficacy of our approach by comparing it with another variant of the SMT-based method which is not scalable but provides an optimal solution globally, and with a greedy algorithm.

Path planning for a robot is one of the major problems in the area of robotics. When a robot is given a task in the form of a Linear Temporal Logic (LTL) specification such that the task needs to be carried out repetitively, we want the robot to follow the shortest cyclic path so that the number of times the robot completes the mission within a given duration gets maximized. In this paper, we address the LTL path planning problem in a dynamic environment where the newly arrived dynamic obstacles may invalidate some of the available paths at any arbitrary point in time. We present DT*, an SMT-based receding horizon planning strategy that solves an optimization problem repetitively based on the current status of the workspace to lead the robot to follow the best available path in the current situation. We implement our algorithm using the Z3 SMT solver and evaluate it extensively on an LTL specification capturing a pick-and-drop application in a warehouse environment and an office environment2. We compare our SMT-based algorithm with two carefully crafted greedy algorithms. Our experimental results show that the proposed algorithm can deal with the dynamism in the workspace in LTL path planning effectively.

The growing use of complex Cyber-Physical Systems (CPSs) in safety-critical applications has led to the demand for the automatic synthesis of robust feedback controllers that satisfy a given set of formal specifications. Controller synthesis from the high-level specification is an NP-Hard problem. We propose a heuristic-based automated technique that synthesizes feedback controllers guided by Signal Temporal Logic (STL) specifications. Our technique involves rigorous analysis of the traces generated by the closed-loop system, matrix decomposition, and an incremental multi-parameter tuning procedure. In case a controller cannot be found to satisfy all the specifications, we propose a technique for modifying the unsatisfiable specifications so that the controller synthesized for the satisfiable subset of specifications now also satisfies the modified specifications. We demonstrate our technique on eleven controllers used as standard closed-loop control system benchmarks, including complex controllers having multiple independent or nested control loops. Our experimental results establish that the proposed algorithm can automatically solve complex feedback controller synthesis problems within a few minutes.

The fundamental path planning problem for a mobile robot involves generating a trajectory for point-to-point navigation while avoiding obstacles. Heuristic-based search algorithms like A* have been shown to be efficient in solving such planning problems. Recently, there has been an increased interest in specifying complex path planning problem using temporal logic. In the state-of-the-art algorithm, the temporal logic path planning problem is reduced to a graph search problem, and Dijkstra's shortest path algorithm is used to compute the optimal trajectory satisfying the specification.The A* algorithm, when used with an appropriate heuristic for the distance from the destination, can generate an optimal path in a graph more efficiently than Dijkstra's shortest path algorithm. The primary challenge for using A* algorithm in temporal logic path planning is that there is no notion of a single destination state for the robot. We present a novel path planning algorithm T* that uses the A* search procedure opportunistically to generate an optimal trajectory satisfying a temporal logic query. Our experimental results demonstrate that T* achieves an order of magnitude improvement over the state-of-the-art algorithm to solve many temporal logic path planning problems in 2-D as well as 3-D workspaces.

Simulink/Stateflow is the de facto tool for developing software for safety-critical real-time cyber-physical systems (CPSs). In Simulink, the model of a CPS is captured in a block diagram-based language, the model is simulated using the associated simulators and then the software code is generated automatically for the embedded controller. The presence of a bug in the Simulink model may lead to catastrophic failure during the execution of the system developed based on the model. Unlike in application software, finding bugs in Simulink models is challenging due to the hybrid nature of the model. We present an automated debugging methodology of a CPS model captured in Simulink. Our methodology has two main components-bug localization and model repair. For bug localization, we capture the requirements of the system in signal temporal logic (STL) and employ the runtime monitoring technique to generate a trace that violates the specification. The violating trace is used to identify the internal signals that have the potential to contribute to the violation. For precise bug localization by narrowing down the offending signals, we employ a matrix decomposition technique to find the signals contributing to the bug accurately. Our bug localization technique is precise enough to enable us to repair the model. If the bug is due to an inappropriate value for a model parameter, we employ a parameter tuning method to find a value for the parameter that repairs the model automatically. We carry out numerous case studies on Simulink models obtained from different sources and demonstrate that our automated debugging technology can fix the bugs in the Simulink models effectively.

This paper presents a methodology for synthesizing a motion plan for a mobile robot to ensure that the robot never gets depleted with battery charge while carrying out its mission successfully. The specification of the robot is provided in the form of an LTL (Linear Temporal Logic) formula. A trajectory satisfying an LTL formula may contain a loop whose repetitive execution causes the depletion of battery charge in the robot. The motion plan generated by our methodology ensures that the robot visits the charging station periodically in such a way that it never gets depleted with battery charge while carrying out its mission optimally. Given a set of potential charging station locations and an LTL specification, our algorithm also finds the best location for the charging station along with the optimal trajectory for the robot. We encode the motion planning problem as an SMT (Satisfiability Modulo Theory) solving problem and use the off-the-shelf SMT solver Z3 to solve the constraints to find the location of the charging station and generate an optimal trajectory for the robot. We apply our methodology to synthesize energy-aware trajectories for robots with different dynamics in various workspaces and for various LTL specifications.

Synthesis of a feedback controller for nonlinear dynamical systems like a quadrotor requires to deal with the trade-off between performance and online computation requirement of the controller. Model predictive controllers (MPC) provide excellent control performance, but at the cost of high online computation. In this paper, we present our experience in approximating the behavior of an MPC for a quadrotor with a feed-forward neural network. To facilitate the collection of training data, we create a faithful model of the quadrotor and use Gazebo simulator to collect sufficient training data. The deep neural network (DNN) controller learned from the training data has been tested on various trajectories to compare its performance with a model-predictive controller. Our experimental results show that our DNN controller can provide almost similar trajectory tracking performance at a lower control computation cost, which helps in increasing the flight time of the quadrotor. Moreover, the hardware requirement for our DNN controller is significantly less than that for the MPC controller. Thus, the use of DNN based controller also helps in reducing the overall price of a quadrotor.

This paper surveys recent challenges and solutions in the design, implementation, and verification of embedded software for robotics. Emphasis is placed on mobile robots, like self-driving cars. In design, it addresses programming support for robotic systems, secure state estimation, and ROS-based monitor generation. In the implementation phase, it describes the synthesis of control software using finite precision arithmetic, real-time platforms and architectures for safety-critical robotics, efficient implementation of neural network based-controllers, and standards for computer vision applications. The issues in verification include verification of neural network-based robotic controllers, and falsification of closed-loop control systems. The paper also describes notable open-source robotic platforms. Along the way, we highlight important research problems for developing the next generation of high-performance, low-resource-usage, correct embedded software.

For an autonomous mobile robot, when the available power goes below a certain threshold, the robot needs to abort its current task and move towards a charging station to recharge its battery. The efficiency of an autonomous mobile robot depends significantly on the location of the charging stations. In this paper, we address the charging station placement problem for mobile robots in a controlled workspace. We propose two algorithms to place a number of charging stations so that a robot is always capable of reaching one of the charging stations from any obstacle-free location in the workspace without aborting its task too early. We reduce the charging-station placement problem to a series of Satisfiability Modulo Theory (SMT) problems and use the off-the-shelf SMT solver Z3 to implement our algorithm. The algorithm produces as output the locations of the charging stations in the workspace and the trajectories from any obstacle-free locations to one of the charging stations. Our experimental results show how our algorithm can efficiently find the locations of the charging stations and robot trajectories to reach the charging stations. We demonstrate through simulation how the generated trajectories can be effectively used by a robot to reach a charging stations autonomously without getting depleted with power.

We present Antlab, an end-to-end system that takes streams of user task requests and executes them using collections of robots. In Antlab, each request is specified declaratively in linear temporal logic extended with quantifiers over robots. The user does not program robots individually, nor know how many robots are available at any time or the precise state of the robots. The Antlab runtime system manages the set of robots, schedules robots to perform tasks, automatically synthesizes robot motion plans from the task specification, and manages the co-ordinated execution of the plan. We provide a constraint-based formulation for simultaneous task assignment and plan generation for multiple robots working together to satisfy a task specification. In order to scalably handle multiple concurrent tasks, we take a separation of concerns view to plan generation. First, we solve each planning problem in isolation, with an “ideal world” hypothesis that says there are no unspecified dynamic obstacles or adversarial environment actions. Second, to deal with imprecisions of the real world, we implement the plans in receding horizon fashion on top of a standard robot navigation stack. The motion planner dynamically detects environment actions or dynamic obstacles from the environment or from other robots and locally corrects the ideal planned path. It triggers a re-planning step dynamically if the current path deviates from the planned path or if planner assumptions are violated. We have implemented Antlab as a C++ and Python library on top of robots running on ROS, using SMT-based and AI planning-based implementations for task and path planning. We evaluated Antlab both in simulation as well as on a set of TurtleBot robots. We demonstrate that it can provide a scalable and robust infrastructure for declarative multi-robot programming.

Time-triggered architectures form an important component of many distributed computing platforms for safety-critical real-time applications such as avionics and automotive control systems. TTA, FlexRay, and TTCAN are examples of such time-triggered architectures that have been popular in recent times. These architectures involve a number of algorithms for synchronizing a set of distributed computing nodes for meaningful exchange of data among them. The algorithms include a startup algorithm whose job is to integrate one or more nodes into the group of communicating nodes. The startup algorithm runs on every node when the system is powered up, and again after a failure occurs. Some critical issues need to be considered in the design of the startup algorithms, for example, the algorithms should be robust under reasonable assumptions of failures of nodes and channels. The safety-critical nature of the applications where these algorithms are used demands rigorous verification of these algorithms, and there have been numerous attempts to use formal verification techniques for this purpose. This paper focuses on various formal verification efforts carried out for ensuring the correctness of the startup algorithms. In particular, the verification of different startup algorithms used in three time-triggered architectures, TTA, FlexRay, and TTCAN, is studied, compared, and contrasted. Besides presenting the various verification approaches for these algorithms, the gaps and possible improvements on the verification efforts are also indicated.

Summary We revisit the problem of real‐time verification with dense‐time dynamics using timeout and calendar‐based models and simplify this to a finite state verification problem. We introduce a specification formalism for these models and capture their behaviour in terms of semantics of timed transition systems. We discuss a technique, which reduces the problem of verification of qualitative temporal properties on infinite state space of a large fragment of these timeout and calender‐based transition systems into that on clock‐less finite state models through a two‐step process comprising of digitization and finitary reduction. This technique enables us to verifysafetyinvariants for real‐time systems using finite state model checking avoiding the complexity of infinite state (bounded) model checking and scale up models without applying techniques from induction‐based proof methodology. In the same manner, we verify timeliness properties. Moreover, we can verifylivenessfor real‐time systems, which are not possible by using induction with infinite state model checkers. Copyright © 2016 John Wiley & Sons, Ltd.

An integrated approach, embracing both control and scheduling theories, is proposed to implement multiple control loops upon shared network and computational resources, where the network may additionally introduce packet losses. Each control system is first analyzed from a control-theoretic perspective in order to determine the asymptotic rate at which control signals must be computed to maintain stability and optimal performance despite network losses. Since required completion rates for control tasks are asymptotic, and network packet drops uncertain, the problem of scheduling multiple such control tasks upon shared computational resources does not map to known problems in real-time scheduling. It is therefore formalized here as a new form of periodic task scheduling problem -- one in which each task has an associated asymptotic completion rate requirement. Sufficient schedulability conditions are derived, and a dynamic scheduling algorithm designed, for solving such scheduling problems. This integrated methodology thus provides an effective way to incorporate network loss in the design of cyber-physical systems over integrated architectures. The use of this methodology is illustrated, and its efficacy demonstrated, upon an example system of five inverted pendulums.

We present a compositional motion planning framework for multi-robot systems based on an encoding to satisfiability modulo theories (SMT). In our framework, the desired behavior of a group of robots is specified using a set of safe linear temporal logic (LTL) properties. Our method relies on a library of motion primitives, each of which corresponds to a controller that ensures a particular trajectory in a given configuration. Using the closed-loop behavior of the robots under the action of different controllers, we formulate the motion planning problem as an SMT solving problem and use an off-the-shelf SMT solver to generate trajectories for the robots. Our approach can also be extended to synthesize optimal cost trajectories where optimality is defined with respect to the available motion primitives. Experimental results show that our framework can efficiently solve complex motion planning problems in the context of multi-robot systems.

Several problems in the implementations of control systems, signal-processing systems, and scientific computing systems reduce to compiling a polynomial expression over the reals into an imperative program using fixed-point arithmetic. Fixed-point arithmetic only approximates real values, and its operators do not have the fundamental properties of real arithmetic, such as associativity. Consequently, a naive compilation process can yield a program that significantly deviates from the real polynomial, whereas a different order of evaluation can result in a program that is close to the real value on all inputs in its domain. We present a compilation scheme for real-valued arithmetic expressions to fixed-point arithmetic programs. Given a real-valued polynomial expression t, we find an expression t' that is equivalent to t over the reals, but whose implementation as a series of fixed-point operations minimizes the error between the fixed-point value and the value of t over the space of all inputs. We show that the corresponding decision problem, checking whether there is an implementation t' of t whose error is less than a given constant, is NP-hard. We then propose a solution technique based on genetic programming. Our technique evaluates the fitness of each candidate program using a static analysis based on affine arithmetic. We show that our tool can significantly reduce the error in the fixed-point implementation on a set of linear control system benchmarks. For example, our tool found implementations whose errors are only one half of the errors in the original fixed-point expressions.

Software implementations of controllers for physical systems are at the core of many embedded systems. The design of controllers uses the theory of dynamical systems to construct a mathematical control law that ensures that the controlled system has certain properties, such as asymptotic convergence to an equilibrium point, and optimizes some performance criteria such as LQR-LQG. However, owing to quantization errors arising from the use of fixed-point arithmetic, the implementation of this control law can only guarantee practical stability: under the actions of the implementation, the trajectories of the controlled system converge to a bounded set around the equilibrium point, and the size of the bounded set is proportional to the error in the implementation. The problem of verifying whether a controller implementation achieves practical stability for a given bounded set has been studied before. In this paper, we change the emphasis from verification to automatic synthesis. We give a technique to synthesize embedded control software that is Pareto optimal w.r.t. both performance criteria and practical stability regions. Our technique uses static analysis to estimate quantization-related errors for specific controller implementations, and performs stochastic local search over the space of possible controllers using particle swarm optimization. The effectiveness of our technique is illustrated using several standard control system examples: in most examples, we find controllers with close-to-optimal LQR-LQG performance but with implementation errors, hence regions of practical stability, several times as small.

Self-triggered implementations of controllers have been proposed as an alternative to traditional time-triggered implementations. In a self-triggered implementation, the control task computes the actuator signal as well as a triggering time that specifies the next time instant at which the control task should be run. Self-triggered implementations have the potential to decrease communication costs and CPU requirements over time-triggered ones, e.g., by running the steady-state plant in open loop for long intervals if there is no disturbance. We show that commonly claimed gains for self-triggered implementations are too optimistic. The analysis of most self-triggering algorithms ignore the execution times for computing the trigger times. We show, using implementations of several self-triggering algorithms proposed in the literature on common embedded platforms, that the execution time to compute the trigger time can be non-negligible compared to the trigger times, and may even be higher than the trigger time itself, rendering a naive implementation infeasible.

Robot manipulators are widely used in many industrial automation applications. A robot manipulator moves the end-effector to the configuration instructed by the user. The user input from a master unit is transformed into the desired configuration through forward kinematics. This configuration is communicated to the robot controller, which employs inverse kinematics to transform the configuration into joint angles. The control algorithm is implemented as software and embedded into the robot controller. The software is typically written in traditional programming languages like C or C++. We introduce a Simulink Library ModelRob that provides basic building blocks to model kinematics of a robot manipulator. Availability of such a library enables Model-Based Development (MBD) of robot manipulator software, where the manipulator controller can be modeled using ModelRob library blocks, and production code can be automatically generated using existing code generators for Simulink. We enlist the existing tools that can be useful in the verification and validation stage of the MBD process, and outline the need for tool-support for verification activities specific to building robust robot manipulator software. Using ModelRob library we have modeled Cartesian space motion controller of a robot manipulator in Simulink and successfully generated C code from the model.

We consider the problem of designing a cyber-physical system where several control loops share the same architectural resources. Typically, the design of such systems proceeds in two steps. In the platform independent step, for each control loop in the system, the control designer calculates a control law and a sampling time that together ensure that the control loop has certain desired performance. Then, in the platform dependent step, these control tasks are scheduled on the platform, and a schedulability analysis determines if (and how) the control laws can be implemented and scheduled without missing the sampling deadlines.

Software implementations of controllers for physical subsystems form the core of many modern safety-critical systems such as aircraft flight control and automotive engine control. A fundamental property of such implementations is stability, the guarantee that the physical plant converges to a desired behavior under the actions of the controller. We present a methodology and a tool to perform automated static analysis of embedded controller code for stability of the controlled physical system.

Abstract—Software controllers for physical processes are at the core of many safety-critical systems such as avionics, automotive engine control, and process control. Despite their importance, the design and implementation of software controllers remains an art form; dependability is generally poor, and the cost of verifying systems is prohibitive. We illustrate the potential of applying program analysis tools on problems in controller design and implementation by focusing on concolic execution, a technique for systematic testing for software. In particular, we demonstrate how a concolic execution tool can be modified to automatically analyze controller implementations and (a) produce test cases achieving a coverage goal, (b) synthesize ranges for controller variables that can be used to allocate bits in a fixed-point implementation, and (c) verify robustness of an implementation under input uncertainties. We have implemented these algorithms on top of the Splat test generation tool and have carried out preliminary experiments on control software that demonstrates feasibility of the techniques. I.

This paper presents a principled approach to one of the many littlestudied aspects of computer security which relate to human behavior. Advantages of involving users who usually have strong analytic ability to detect violations and threats but not primarily responsible for security have been well emphasized in the literature. In this work we propose a reinforcement framework for enabling collaborative monitoring of violations by the users. We define a payoff model to formalize the reinforcement framework. The model stipulates appropriate payoffs as reward, punishment, and community price according to reporting of genuine or false violations, non-reporting of the detected violations, and proactive reporting of vulnerabilities and threats by the users. We define probabilistic robustness property of the resulting system and constraints for economic feasibility of the payoffs. For estimating the parameters

A key feature of control systems is robustness, the property that small perturbations in the system inputs cause only small changes in its outputs. Robustness is key to designing systems that work under uncertain or imprecise environments. While continuous control design algorithms can explicitly incorporate robustness as a design goal, it is not clear if robustness is maintained at the software implementation level of the controller: two ``close'' inputs can execute very different code paths which may potentially produce vastly different outputs. We present an algorithm and a tool to characterize the robustness of a control software implementation. Our algorithm is based on symbolic execution and non-linear optimization, and computes the maximum difference in program outputs over all program paths when a program input is perturbed. As a by-product, our algorithm generates a set of test vectors which demonstrate the worst-case deviations in outputs for small deviations in inputs. We have implemented our approach on top of the Splat test generation tool and we describe an evaluation of our implementation on two examples of automotive control code.

We describe the modeling and verification of TTCAN startup protocol using SAL model checker. For the modeling purposes we propose a new modeling framework called Synchronous Calendar which can be seen as an adaptation of Calendar based models introduced by Duterte and Sorea. A Synchronous Calendar can express dense time systems without relying on continuously varying clocks and supports synchronous message transmission. We capture both fault-free and fault-tolerant aspects of startup algorithm of TTCAN in two different models and verify the safety and liveness properties for them. Our verification technique relies on induction and abstraction methods which are supported by SAL model checker. To our knowledge this is the first work towards a formal analysis of TTCAN startup protocol.

Performance and fault tolerance are two major issues that need to be addressed while designing highly available and reliable systems. The network topology or the notion of connectedness among the network nodes defines the system communication architecture and is an important design consideration for fault tolerant systems. A number of fault tolerant designs for specific multi-processor architecture exists in the literature, but none of them discriminates between stateless and stateful failover. In this paper, we propose a reliable network topology and a high availability framework which is tolerant up to a maximum of k node faults in a network and is designed specifically to meet the needs of stateful failover. Assuming the nodes in the network are capable of handling multiple processes, through our design we have been able to prove that in the event of k node failures the load can be uniformly distributed across the network - ensuring load balance. We also provide an useful characterization for the network, which under the proposed framework ensures one hop communication between the required nodes