Author | Title | Year | Journal/Proceedings | DOI/URL | |
---|---|---|---|---|---|

Huang, Z., Fan, C. and Mitra, S. | Bounded invariant verification for time-delayed nonlinear networked dynamical systems | 2016 | Nonlinear analysis | ||

BibTeX:
@article{HuangMF:NA2016, author = {Zhenqi Huang and Chuchu Fan and Sayan Mitra}, title = {Bounded invariant verification for time-delayed nonlinear networked dynamical systems}, journal = {Nonlinear analysis}, year = {2016} } |
|||||

Huang, Z., Wang, Y., Mitra, S. and Dullerud, G. | Differenitial privacy and entropy in distributedfeedback systems: Minimizing mechanisms andperformance trade-offs | 2016 | |||

BibTeX:
@article{HYMD:TCONES2016, author = {Zhenqi Huang and Yu Wang and Sayan Mitra and Geir Dullerud}, title = {Differenitial privacy and entropy in distributedfeedback systems: Minimizing mechanisms andperformance trade-offs}, year = {2016} } |
|||||

Lin, Y., Ghosh, R. and Mitra, S. | StarL framework for programming, simulating and verifying distributed robotic applications | 2016 | |||

BibTeX:
@article{LGM:ACMTECS2016, author = {Yixiao Lin and Ritwika Ghosh and Sayan Mitra}, title = {StarL framework for programming, simulating and verifying distributed robotic applications}, year = {2016} } |
|||||

Liberzon, D. and Mitra, S. | Entropy and minimal data rates for state estimation and model detection | 2016 | Hybrid System: Computation and Control | ||

Abstract: We investigate the problem of constructing exponentially converging estimates of the state of a continuous-time system from state measurements transmitted via a limited-data-rate communication channel, so that only quantized and sampled measurements of continuous signals are available to the estimator. Following prior work on topological entropy of dynamical systems, we introduce a notion of estimation entropy which captures this data rate in terms of the number of system trajectories that approximate all other trajectories with desired accuracy. We also propose a novel alternative definition of estimation entropy which uses approximating functions that are not necessarily trajectories of the system. We show that the two entropy notions are actually equivalent. We establish an upper bound for the estimation entropy in terms of the sum of the system's Lipschitz constant and the desired convergence rate, multiplied by the system dimension. We propose an iterative procedure that uses quantized and sampled state measurements to generate state estimates that converge to the true state at the desired exponential rate. The average bit rate utilized by this procedure matches the derived upper bound on the estimation entropy. We also show that no other estimator (based on iterative quantized measurements) can perform the same estimation task with bit rates lower than the estimation entropy. Finally, we develop an application of the estimation procedure in determining, from the quantized state measurements, which of two competing models of a dynamical system is the true model. We show that under a mild assumption of exponential separation of the candidate models, detection is always possible in finite time. Our numerical experiments with randomly generated affine dynamical systems suggest that in practice the algorithm always works. |
|||||

BibTeX:
@inproceedings{LM:HSCC2016, author = {Daniel Liberzon and Sayan Mitra}, title = {Entropy and minimal data rates for state estimation and model detection}, booktitle = {Hybrid System: Computation and Control}, year = {2016} } |
|||||

Islam, M.A., DeFrancisco, R., Fan, C., Grosu, R., Mitra, S. and Smolka, S.A. | Model Checking Tap Withdrawal in C. Elegans | 2015 | Vol. 9271Hybrid Systems Biology - Fourth International Workshop, HSB 2015, Madrid, Spain, September 4-5, 2015., pp. 195-210 |
||

Abstract: We present what we believe to be the first formal verification of a biologically realistic (nonlinear ODE) model of a neural circuit in a multicellular organism: Tap Withdrawal (TW) in C. elegans, the common roundworm. TW is a reflexive behavior exhibited by C. elegans in response to vibrating the surface on which it is moving; the neural circuit underlying this response is the subject of this investigation. Specifically, we perform reachability analysis on the TW circuit model of Wicks et al. (1996), which enables us to estimate key circuit parameters. Underlying our approach is the use of Fan and Mitra's recently developed technique for automatically computing local discrepancy (convergence and divergence rates) of general nonlinear systems. We show that the results we obtain are in agreement with the experimental results of Wicks et al. (1995). As opposed to the fixed parameters found in most biological models, which can only produce the predominant behavior, our techniques characterize ranges of parameters that produce (and do not produce) all three observed behaviors: reversal of movement, acceleration, and lack of response. |
|||||

BibTeX:
@inproceedings{DBLP:journals/corr/IslamDFGMS15, author = {Md. Ariful Islam and Richard DeFrancisco and Chuchu Fan and Radu Grosu and Sayan Mitra and Scott A. Smolka}, title = {Model Checking Tap Withdrawal in C. Elegans}, booktitle = {Hybrid Systems Biology - Fourth International Workshop, HSB 2015, Madrid, Spain, September 4-5, 2015.}, year = {2015}, volume = {9271}, pages = {195--210}, url = {http://dx.doi.org/10.1007/978-3-319-26916-0_11} } |
|||||

Duggirala, P.S., Fan, C., Mitra, S. and Viswanathan, M. | Meeting a Powertrain Verification Challenge | 2015 | Vol. 9206Proceedings of International Conference on Computer Aided Verification (CAV 2015), pp. 536-543 |
||

Abstract: We present the verification of a benchmark powertrain control system using the hybrid system verification tool C2E2. This model comes from a suite of benchmarks that were posed as a challenge problem for the hybrid systems community, and to our knowledge, we are reporting its first verification. For this work, we implemented the algorithm reported in [FanM:2015] in C2E2, to automatically compute local discrepancy (rate of convergence or divergence of trajectories) of the model. We verify the key requirements of the model, specified in signal temporal logic (STL), for a set of driver behaviors. |
|||||

BibTeX:
@inproceedings{DFMV:CAV2015, author = {Parasara Sridhar Duggirala and Chuchu Fan and Sayan Mitra and Mahesh Viswanathan}, title = {Meeting a Powertrain Verification Challenge}, booktitle = {Proceedings of International Conference on Computer Aided Verification (CAV 2015)}, publisher = {Springer}, year = {2015}, volume = {9206}, pages = {536--543} } |
|||||

Duggirala, P.S., Mitra, S. and Viswanathan, M. | C2E2: A Verification Tool For Stateflow Models | 2015 | Vol. 9035Proceedings of 21st International Conference Tools and Algorithms for the Construction and Analysis of Systems TACAS 2015, London, UK, April 11-18, 2015., pp. 68-82 |
||

Abstract: Mathwork's Stateflow is a predominant environment for modeling embedded and cyberphysical systems where control software interact with physical processes. We present Compare-Execute-Check-Engine (C2E2)---a verification tool for continuous and hybrid Stateflow models. It checks bounded time invariant properties of models with nonlinear dynamics, and discrete transitions with guards and resets. C2E2 transforms the model, computing simulations using a validated numerical solver, and then computes reachtube over-approximations with increasing precision. For this last step it uses annotations that have to be added to the model. These annotations are extensions of proof certificates studied in Control Theory and can be automatically obtained for linear dynamics. The C2E2 algorithm is sound and it is guaranteed to terminate if the system is robustly safe (or unsafe) with respect to perturbations to the of guards and invariants of the model. We present the architecture of C2E2, its workflow, and examples illustrating its potential role in model-based design, verification, and validation. |
|||||

BibTeX:
@inproceedings{DuggiralaMV:2015c2e2, author = {Parasara Sridhar Duggirala and Sayan Mitra and Mahesh Viswanathan}, title = {C2E2: A Verification Tool For Stateflow Models}, booktitle = {Proceedings of 21st International Conference Tools and Algorithms for the Construction and Analysis of Systems TACAS 2015, London, UK, April 11-18, 2015.}, publisher = {Springer}, year = {2015}, volume = {9035}, pages = {68--82}, url = {http://dx.doi.org/10.1007/978-3-662-46681-0}, doi = {http://dx.doi.org/10.1007/978-3-662-46681-0} } |
|||||

Fan, C. and Mitra, S. | Bounded Verification with On-the-Fly Discrepancy Computation | 2015 | Vol. 936413th Intl. Symposium on Automated Technology for Verification and Analysis (ATVA 2015), Sanghai, China., pp. 446-463 |
||

Abstract: Simulation-based verification algorithms can provide formal safety guarantees for nonlinear and hybrid systems. The previous algorithms rely on user provided model annotations called discrepancy function, which are crucial for computing reachtubes from simulations. In this paper, we eliminate this requirement by presenting an algorithm for computing piece-wise exponential discrepancy functions. The algorithm relies on computing local convergence or divergence rates of trajectories along a simulation using a coarse over-approximation of the reach set and bounding the maximal eigenvalue of the Jacobian over this over-approximation. The resulting discrepancy function preserves the soundness and the relative completeness of the verification algorithm. We also provide a coordinate transformation method to improve the local estimates for the convergence or divergence rates in practical examples. We extend the method to get the input-to-state discrepancy of nonlinear dynamical systems which can be used for compositional analysis. Our experiments show that the approach is effective in terms of running time for several benchmark problems, scales reasonably to larger dimensional systems, and compares favorably with respect to available tools for nonlinear models. |
|||||

BibTeX:
@inproceedings{FanMitra:2015df, author = {Chuchu Fan and Sayan Mitra}, title = {Bounded Verification with On-the-Fly Discrepancy Computation}, booktitle = {13th Intl. Symposium on Automated Technology for Verification and Analysis (ATVA 2015), Sanghai, China.}, year = {2015}, volume = {9364}, pages = {446--463}, url = {http://arxiv.org/abs/1502.01801} } |
|||||

Fan, C., Duggirala, P.S., Mitra, S. and Viswanathan, M. | Progress on Powertrain Verification Challenge with C2E2 | 2015 | Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH 2015) | ||

Abstract: In this paper, we present the progress we have made in verifying the benchmark powertrain control systems introduced in the last ARCH workshop. We implemented the algorithm reported in [FanM:2015] in the hybrid system verification tool C2E2 for automatically computing local discrepancy (rate of convergence or divergence of trajectories). We created Stateflow translations of the original models to aid the processing using C2E2 tool. We also had to encode the different driver behaviors in the form of state machines. With these customizations, we have been successful in verifying one of the easier (but still challenging) benchmarks from the powertrain suite. In this paper, we present some of the engineering challenges and describe the artifacts we created in the process. |
|||||

BibTeX:
@inproceedings{FDMV:ARCH2015, author = {Chuchu Fan and Parasara Sridhar Duggirala and Sayan Mitra and Mahesh Viswanathan}, title = {Progress on Powertrain Verification Challenge with C2E2}, booktitle = {Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH 2015)}, year = {2015} } |
|||||

Ghosh, R. and Mitra, S. | A Strategy for Automatic Verification of Stabilization of Distributed Algorithms | 2015 | Vol. 9039Proceedings of Formal Techniques for Distributed Systems (FORTE) - Joint IFIP WG 6.1 International Conference, pp. 35-49 |
||

Abstract: Automatic verification of convergence and stabilization properties of distributed algorithms has received less attention than verification of invariance properties. We present a semi-automatic strategy for verification of stabilization properties of arbitrarily large networks under structural and fairness constraints. We introduce a sufficient condition that guarantees that every fair execution of any (arbitrarily large) instance of the system stabilizes to the target set of states. In addition to specifying the protocol executed by each agent in the network and the stabilizing set, the user also has to provide a measure function or a ranking function. With this, we show that for a restricted but useful class of distributed algorithms, the sufficient condition can be automatically checked for arbitrarily large networks, by exploiting the small model properties of these conditions. We illustrate the method by automatically verifying several well-known distributed algorithms including link-reversal, shortest path computation, distributed coloring, leader election and spanning-tree construction. |
|||||

BibTeX:
@inproceedings{GhoshMit:FORTE2015, author = {Ritwika Ghosh and Sayan Mitra}, title = {A Strategy for Automatic Verification of Stabilization of Distributed Algorithms}, booktitle = {Proceedings of Formal Techniques for Distributed Systems (FORTE) - Joint IFIP WG 6.1 International Conference}, publisher = {Springer}, year = {2015}, volume = {9039}, pages = {35--49}, note = {Nominated for best paper award} } |
|||||

Huang, Z., Fan, C., Mereacre, A., Mitra, S. and Kwiatkowska, M. | Simulation-based Verification of Cardiac Pacemakers with Guaranteed Coverage | 2015 | IEEE Design and Test Special Issue, pp. 27-34 | ||

Abstract: Design and testing of pacemaker is challenging because of the need to capture the interaction between the physical processes (e.g. voltage signal in cardiac tissue) and the embedded software (e.g. a pacemaker). At the same time, there is a growing need for design and certification methodologies that can provide quality assurance for the embedded software. We describe recent progress in simulation-based techniques that are capable of ensuring guaranteed coverage. Our methods employ discrepancy functions, which impose bounds on system dynamics, and proceed through iteratively constructing over-approximations of the reachable set of states. We are able to prove time bounded safety or produce counterexamples. We illustrate the techniques by analyzing a family of pacemaker designs against time duration requirements and synthesize safe parameter ranges. We conclude by outlining the potential uses of this technology to improve the safety of medical device designs. |
|||||

BibTeX:
@article{HuangIEEEDT:2015, author = {Zhenqi Huang and Chuchu Fan and Alexandru Mereacre and Sayan Mitra and Marta Kwiatkowska}, title = {Simulation-based Verification of Cardiac Pacemakers with Guaranteed Coverage}, journal = {IEEE Design and Test Special Issue}, year = {2015}, pages = {27--34} } |
|||||

Huang, Z., Mitra, S. and Vaidya, N. | Differentially Private Distributed Optimization | 2015 | International Converence on Distributed Computing and Networks (ICDCN 2015), Goa, India, January 4-7, 2015, pp. 4:1-4:10 | ||

Abstract: In distributed optimization and iterative consensus literature, a standard problem is for $N$ agents to minimize a function $f$ over a subset of Euclidean space, where the cost function is expressed as a sum $sum f_i$. In this paper, we study the private distributed optimization (PDOP) problem with the additional requirement that the cost function of the individual agents should remain differentially private. The adversary attempts to infer information about the private cost functions from the messages that the agents exchange. Achieving differential privacy requires that any change of an individual's cost function only results in unsubstantial changes in the statistics of the messages. We propose a class of iterative algorithms for solving PDOP, which achieves differential privacy and convergence to the optimal value. Our analysis reveals the dependence of the achieved accuracy and the privacy levels on the the parameters of the algorithm. We observe that to achieve $-differential privacy the accuracy of the algorithm has the order of $O(1)$. |
|||||

BibTeX:
@inproceedings{HuangMV:ICDCN2015, author = {Zhenqi Huang and Sayan Mitra and Nitin Vaidya}, title = {Differentially Private Distributed Optimization}, booktitle = {International Converence on Distributed Computing and Networks (ICDCN 2015), Goa, India, January 4-7, 2015}, publisher = {ACM}, year = {2015}, pages = {4:1--4:10}, url = {http://doi.acm.org/10.1145/2684464.2684480} } |
|||||

Huang, Z., Wang, Y., Mitra, S. and Dullerud, G. | A Framework for Analyzing Cost of Securing Control Systems | 2015 | Next Wave | ||

BibTeX:
@article{HuangNextWaveT:2015, author = {Zhenqi Huang and Yu Wang and Sayan Mitra and Geir Dullerud}, title = {A Framework for Analyzing Cost of Securing Control Systems}, journal = {Next Wave}, year = {2015} } |
|||||

Huang, Z., Wang, Y., Mitra, S. and Dullerud, G. | Controller Synthesis for Linear Time-varying Systems with Adversaries | 2015 | |||

Abstract: We present a controller synthesis algorithm for a discrete time reach-avoid problem in the presence of adversaries. Our model of the adversary captures typical malicious attacks envisioned on cyber-physical systems such as sensor spoofing, controller corruption, and actuator intrusion. After formulating the problem in a general setting, we present a sound and complete algorithm for the case with linear dynamics and an adversary with a budget on the total L2-norm of its actions. The algorithm relies on a result from linear control theory that enables us to decompose and precisely compute the reachable states of the system in terms of a symbolic simulation of the adversary-free dynamics and the total uncertainty induced by the adversary. With this decomposition, the synthesis problem eliminates the universal quantifier on the adversary's choices and the symbolic controller actions can be effectively solved using an SMT solver. The constraints induced by the adversary are computed by solving second-order cone programmings. The algorithm is later extended to synthesize state-dependent controller and to generate attacks for the adversary. We present preliminary experimental results that show the effectiveness of this approach on several example problems. |
|||||

BibTeX:
@inproceedings{HuangWMD:Synth2015, author = {Zhenqi Huang and Yu Wang and Sayan Mitra and Geir Dullerud}, title = {Controller Synthesis for Linear Time-varying Systems with Adversaries}, year = {2015}, note = {Under Review}, url = {http://arxiv.org/abs/1501.04925} } |
|||||

Johnson, T. and Mitra, S. | Safe and Stabilizing Distributed Traffic Control | 2015 | Theoretical Computer Science (TCS) Vol. 579, pp. 9-32 |
||

Abstract: We study the problem of distributed traffic control in the partitioned plane, where the movement of all entities (vehicles) within each partition (cell) is coupled. Establishing liveness in such systems is challenging, but such analysis will be necessary to apply such distributed traffic control algorithms in applications like the intelligent highway system and for coordinating robot swarms. We present a distributed traffic control protocol that guarantees minimum separation between vehicles, even as some cells fail. Once new failures cease occurring, in the case of a single target, the protocol is guaranteed to self-stabilize and the vehicles with feasible paths to the target cell make progress towards it. For multiple targets, failures may cause deadlocks in the system, so we identify a class of non-deadlocking failures where all vehicles are able to make progress to their respective targets. The algorithm relies on two general principles: temporary blocking for maintenance of safety and local geographical routing for guaranteeing progress. Our assertional proofs may serve as a template for the analysis of other distributed traffic control protocols.We present simulation results that provide estimates of throughput as a function of vehicle velocity, safety separation, single-target path complexity, failure-recovery rates, and multi-target path complexity. |
|||||

BibTeX:
@article{JM2012:DTC, author = {Taylor Johnson and Sayan Mitra}, title = {Safe and Stabilizing Distributed Traffic Control}, journal = {Theoretical Computer Science (TCS)}, year = {2015}, volume = {579}, pages = {9-32}, url = {http://dx.doi.org/10.1016/j.tcs.2015.01.023} } |
|||||

Prabhakar, P., Duggirala, P.S., Mitra, S. and Viswanathan, M. | Hybrid Automata-based CEGAR for Rectangular Hybrid Systems | 2015 | In Formal Methods in System Design (FMSD) Vol. 46(2), pp. 105--134 |
||

Abstract: In this paper we present a framework for carrying out counterexample guided abstraction-refinement (CEGAR) for systems modelled as hybrid automata. The main difference, between our approach and previous proposals for CEGAR for hybrid automata, is that we consider the abstractions to be hybrid automata as well. We present a counterexample guided abstraction refinement method for systems modelled as initialized rectangular hybrid automata along the lines of the general framework and show the completeness of the method. The advantages of our approach are illustrated by examples where it performs better than existing methods. Finally, we demonstrate the feasibility of our approach by performing several experiments using a prototype tool that implements our CEGAR algorithm. |
|||||

BibTeX:
@article{PDMV:FMSD2015, author = {Pavithra Prabhakar and Parasara Sridhar Duggirala and Sayan Mitra and Mahesh Viswanathan}, title = {Hybrid Automata-based CEGAR for Rectangular Hybrid Systems}, journal = {In Formal Methods in System Design (FMSD)}, publisher = {Springer}, year = {2015}, volume = {46}, number = {2}, pages = {105---134}, url = {http://link.springer.com/article/10.1007/s10703-015-0225-4} } |
|||||

Duggirala, P.S., Wang, L., Mitra, S., Munoz, C. and Viswanathan, M. | Temporal Precedence Checking for Switched Models and its Application to a Parallel Landing Protocol | 2014 | International Conference on Formal Methods (FM 2014), Singapore | ||

Abstract: We present an algorithm for checking temporal precedence properties of nonlinear switched systems. This class of properties subsume bounded safety and capture requirements about visiting a sequence of predicates within given time intervals. Our algorithm handles nonlinear predicates that arise from dynamics-based predictions used in alerting protocols for state-of-the-art transportation systems. It is sound and relatively complete for nonlinear switch systems that robustly satisfy the given property. The algorithm is implemented in our Compare Execute Check Engine (C2E2) using validated simulations. As a case study, we consider NASA's Adjacent Landing Alerting System (ALAS), which is an alerting protocol for closely spaced parallel runways.Using our approach, we study the performance of the ALAS protocol with respect to false and missed alerts for different operating conditions such as initial velocities, bankangles, initial longitudinal separation, and runway configurations. |
|||||

BibTeX:
@inproceedings{ALAS2014, author = {Parasara Sridhar Duggirala and Le Wang and Sayan Mitra and Cesar Munoz and Mahesh Viswanathan}, title = {Temporal Precedence Checking for Switched Models and its Application to a Parallel Landing Protocol}, booktitle = {International Conference on Formal Methods (FM 2014), Singapore}, year = {2014}, url = {http://link.springer.com/chapter/10.1007%2F978-3-319-06410-9_16} } |
|||||

Chen, H. and Mitra, S. | Synthesis and Verification of Motor-Transmission Shift Controller for Electric Vehicles | 2014 | the Proceedings of the International Conference on Cyberphysical Systems (ICCPS 2014) | ||

Abstract: Motor transmission-based drive systems are attractive for electric vehicles but, as the motor is directly connected to the transmission shaft which meshes with the gears, controlling gear shifts is challenging. In this paper, we present a methodology for synthesis and verification of open-loop optimal control of the electric motor in a motor-transmission drive system. The key steps in this methodology are (a) developing a continuous-time model of the trajectory of the sleeve during the meshing process based on appropriate coefficients of restitution, (b) discrete-time controller synthesis for finitely many initial states using model predictive control (MPC) and (c) verification of the synthesized controller for a higher-fidelity continuous time hybrid automaton model. First, we develop a model of the motor-transmission drive system as a continuous-time hybrid automaton (CHA) with uncertain initial states. Next, this model is transformed to a piece-wise affine (PWA) form for solving an optimal control problem using the multi-parametric toolbox. Finally, the delay bound for the synthesized controller is verified by computing a bounded time over-approximation of the reach set using an existing algorithm for linear deterministic hybrid automata. Our results show that on an average our synthesized controller can shorten the meshing duration by 71.05% and reduce impacts impulse by 85.72% compared to an existing controller and the sleeve can mesh with the gear within a desired time from every initial state. |
|||||

BibTeX:
@inproceedings{CH:ICCPS2014, author = {Hongxu Chen and Sayan Mitra}, title = {Synthesis and Verification of Motor-Transmission Shift Controller for Electric Vehicles}, booktitle = {the Proceedings of the International Conference on Cyberphysical Systems (ICCPS 2014)}, year = {2014} } |
|||||

Huang, Z., Fan, C., Mereacre, A., Mitra, S. and Kwiatkowska, M. | Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells | 2014 | Computer Aided Verification (CAV 2014) | ||

Abstract: Verification algorithms for networks of nonlinear hybrid automata (HA) can aid us understand and control biological processes such as cardiac arrhythmia, formation of memory, and genetic regulation. We present an algorithm for over-approximating reach sets of networks of nonlinear HA which can be used for sound and relatively complete invariant checking. First, it uses automatically computed input-to-state discrepancy functions for the individual automata modules in the network A for constructing a low-dimensional model M. Simulations of both A and M are then used to compute the reach tubes for A. These techniques enable us to handle a challenging verification problem involving a network of cardiac cells, where each cell has four continuous variables and twenty nine locations. Our prototype tool can check bounded-time invariants for networks with 5 cells (20 continuous variables, 29^5 locations) typically in less than $15$ minutes for up to reasonable time horizons. From the computed reach tubes we can infer biologically relevant properties of the network from a set of initial states. |
|||||

BibTeX:
@inproceedings{HFMMK:CAV2014, author = {Zhenqi Huang and Chuchu Fan and Alexandru Mereacre and Sayan Mitra and Marta Kwiatkowska}, title = {Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells}, booktitle = {Computer Aided Verification (CAV 2014)}, year = {2014}, url = {http://link.springer.com/chapter/10.1007%2F978-3-319-08867-9_25} } |
|||||

Huang, Z. and Mitra, S. | Proofs from Simulations and Modular Annotations | 2014 | 17th International Conference on Hybrid Systems: Computation and Control (HSCC 2014) | ||

Abstract: We present a modular technique for simulation-based bounded verification for nonlinear dynamical systems. Consider a large dynamical system $A$ consisting of several interacting subsystems. We introduce the notion of input-to-state discrepancy of each subsystem $A_i$ in a larger nonlinear dynamical system A which bounds the distance between two (possibly diverging) trajectories of $A_i$ in terms of their initial states and inputs. Using the IS discrepancy functions, we construct a low dimensional deterministic dynamical system M(. For any two trajectories of $A$ starting $ distance apart, we show that one of them bloated by a factor determined by the trajectory of $M$ contains the other. Further, by choosing appropriately small $'s the overapproximations computed by the above method can be made arbitrarily precise. Using the above results we develop a sound and relatively complete algorithm for bounded safety verification of nonlinear ODEs. Our preliminary experiments with a prototype implementation of the algorithm show that the approach can be effective for verification of nonlinear models. |
|||||

BibTeX:
@inproceedings{HM:HSCC2014, author = {Zhenqi Huang and Sayan Mitra}, title = {Proofs from Simulations and Modular Annotations}, booktitle = {17th International Conference on Hybrid Systems: Computation and Control (HSCC 2014)}, year = {2014}, url = {http://doi.acm.org/10.1145/2562059.2562126} } |
|||||

Huang, Z., Wang, Y., Mitra, S. and Dullerud, G. | On the Cost of Differential Privacy in Distributed Control Systems | 2014 | The 3rd ACM International Conference on High Confidence Networked Systems (HiCoNS 2014) at CPSWeek | ||

Abstract: Individuals sharing information can improve the cost or performance of a distributed control system. But, sharing may also violate privacy. We develop a general framework for studying the cost of differential privacy in systems where a collection of agents, with coupled dynamics, communicate for sensing their shared environment while pursuing individual preferences. First, we propose a communication strategy that relies on adding carefully chosen random noise to agent states and show that it preserves differential privacy. Of course, the higher the standard deviation of the noise, the higher the cost of privacy. For linear distributed control systems with quadratic cost functions, the standard deviation becomes independent of the number agents and it decays with the maximum eigenvalue of the dynamics matrix. Furthermore, for stable dynamics, the noise to be added is independent of the number of agents as well as the time horizon up to which privacy is desired. Finally, we show that the cost of $-differential privacy up to time $T$, for a stable system with $N$ agents, is upper bounded by $O(T^3 N )$. |
|||||

BibTeX:
@inproceedings{HYMD:HICONS2014, author = {Zhenqi Huang and Yu Wang and Sayan Mitra and Geir Dullerud}, title = {On the Cost of Differential Privacy in Distributed Control Systems}, booktitle = {The 3rd ACM International Conference on High Confidence Networked Systems (HiCoNS 2014) at CPSWeek}, year = {2014}, url = {http://doi.acm.org/10.1145/2566468.2566474} } |
|||||

Johnson, T.T. and Mitra, S. | Anonymized Reachability of Hybrid Automata Networks | 2014 | Proceedings of Formal Modelling and Analysis of Timed Systems (FORMATS 2014) | ||

Abstract: In this paper, we present a method for computing the reach set for networks composed of a finite number of hybrid automata. The method utilizes a symmetric representation of reach set modulo the automata indices, which makes it scalable. Rather than explicitly enumerating all the automata indices in formulas representing states, the representation tracks only: (a) the classes of automata, which are the states of automata represented with formulas over symbolic indices, and (b) the number of automata in each of the classes. We present an algorithm for over-approximating the reach set by computing state transitions in this representation. Unlike symmetry reduction for FSMs, the timed transition of a hybrid network causes all the automata’s continuous variables to evolve simultaneously. Our representation reduces both the discrete and continuous complexity. We evaluate a prototype implementation in an SMT-based tool. Our experimental results are promising, and in some instances, allow for scaling to networks composed of hundreds of automata. |
|||||

BibTeX:
@inproceedings{JM:FORMATS2014, author = {Taylor T.~Johnson and Sayan Mitra}, title = {Anonymized Reachability of Hybrid Automata Networks}, booktitle = {Proceedings of Formal Modelling and Analysis of Timed Systems (FORMATS 2014)}, year = {2014} } |
|||||

Mitra, S. | Proving Abstractions of Dynamical Systems through Numerical Simulations | 2014 | Hot Topics in Science of Security (HOTSOS) | ||

Abstract: A key question that arises in rigorous analysis of cyberphysical systems under attack involves establishing whether or not the attacked system deviates significantly from the ideal allowed behavior. This is the problem of deciding whether or not the ideal system is an abstraction of the attacked system. A quantitative variation of this question can capture how much the attacked system deviates from the ideal. Thus, algorithms for deciding abstraction relations can help measure the effect of attacks on cyberphysical systems and to develop attack detection strategies. In this paper, we present a decision procedure for proving that one nonlinear dynamical system is a quantitative abstraction of another. Directly computing the reach sets of these nonlinear systems are undecidable in general and reach set over-approximations do not give a direct way for proving abstraction. Our procedure uses (possibly inaccurate) numerical simulations and a model annotation to compute tight approximations of the observable behaviors of the system and then uses these approximations to decide on abstraction. We show that the procedure is sound and that it is guaranteed to terminate under reasonable robustness assumptions. |
|||||

BibTeX:
@inproceedings{MitraHOTSOS2014, author = {Sayan Mitra}, title = {Proving Abstractions of Dynamical Systems through Numerical Simulations}, booktitle = {Hot Topics in Science of Security (HOTSOS)}, year = {2014} } |
|||||

Mitra, S. | Developing Programming Abstractions for Cyberphysical Systems | 2014 | |||

BibTeX:
@misc{MitraPosCPS2014, author = {Sayan Mitra}, title = {Developing Programming Abstractions for Cyberphysical Systems}, year = {2014} } |
|||||

Wang, Y., Huang, Z., Mitra, S. and Dullerud, G. | Entropy-minimizing Mechanism for Differential Privacy of Discrete-time Linear Feedback Systems | 2014 | Conference on Decision and Control (CDC) | ||

Abstract: The concept of differential privacy stems from the study of private query of datasets. In this work, we apply this concept to metric spaces to study a mechanism which randomizes a deterministic query by adding mean-zero noise to keep differential privacy. For one-shot queries, we show that of an $n$-dimensional input implies a lower bound $n + n 2 $ on the entropy of the randomized output, and this lower bound is achieved by We then consider the of a discrete-time linear feedback system in which noise is added to the system output at each time. The adversary, modeled as a filter, estimates the system states from the output history. We show that, to keep the system , the output entropy is bounded below, and this lower bound is achieves by an explicit mechanism. |
|||||

BibTeX:
@inproceedings{WangHMD:CDC2014, author = {Yu Wang and Zhenqi Huang and Sayan Mitra and Geir Dullerud}, title = {Entropy-minimizing Mechanism for Differential Privacy of Discrete-time Linear Feedback Systems}, booktitle = {Conference on Decision and Control (CDC)}, publisher = {IEEE}, year = {2014} } |
|||||

Zimmerman, A. | StarL for programming reliable robotic networks | 2013 | School: University of Illinois at Urbana-Champaign |
||

Abstract: Reasoning about programs controlling distributed robotic systems is challenging. These systems involve the interactions of multiple programs with each other over potentially unreliable communication channels and the interactions of these programs with an unpredictable physical environment. This thesis presents the StarL programming paradigm, its software embodiment and applications. StarL is designed to simplify the process of writing and reasoning about reliable distributed robotics applications. It provides a collection of building block functions with well-defined interfaces and precise guarantees. Composing these functions, it is possible to write more sophisticated functions and applications which are amenable to assume-guarantee style reasoning. StarL is platform independent and can be used in conjunction with any mobile robotic system and communication channel. Design choices made in the current Android/Java-based open source implementation are discussed along with three exemplar applications: distributed search, geocast, and distributed painting. It is illustrated how application-level safety guarantees can be obtained from the properties of the building blocks and environmental assumptions. Experimental results establish the feasibility of the StarL approach and show that the performance of an application scales in the expected manner with an increasing number of participating robots. |
|||||

BibTeX:
@mastersthesis{AZimmerman:Masters2013, author = {Zimmerman, Adam}, title = {StarL for programming reliable robotic networks}, school = {University of Illinois at Urbana-Champaign}, year = {2013}, url = {https://www.ideals.illinois.edu/handle/2142/42380} } |
|||||

Duggirala, P.S., Mitra, S. and Viswanathan, M. | Verificationcation of Annotated Models from Executions | 2013 | Proceedings of International Conference on Embedded Software (EMSOFT 2013), pp. 1-10 | ||

Abstract: Simulations can help enhance confidence in system designs but they provide almost no formal guarantees. In this paper, we present a simulation-based verification framework for embedded systems described by nonlinear, switched systems. In our framework, users are required to annotate the dynamics in each control mode of switched system by something we call a discrepancy function that formally measures the nature of trajectory convergence/divergence of the system. Discrepancy functions generalize other measures of trajectory convergence and divergence like Contraction Metrics and Incremental Lyapunov functions. Exploiting such annotations, we present a sound and relatively complete verification procedure for robustly safe/unsafe systems. We have built a tool based on the framework that is integrated into the popular Simulink/Stateflow modeling environment. Experiments with our prototype tool shows that the approach (a) outperforms other verification tools on standard linear and nonlinear benchmarks, (b) scales reasonably to larger dimensional systems and to longer time horizons, and (c) applies to models with diverging trajectories and unknown parameters. |
|||||

BibTeX:
@inproceedings{DMV:EMSOFT2013, author = {Parasara Sridhar Duggirala and Sayan Mitra and Mahesh Viswanathan}, title = {Verificationcation of Annotated Models from Executions}, booktitle = {Proceedings of International Conference on Embedded Software (EMSOFT 2013)}, publisher = {IEEE}, year = {2013}, pages = {1-10}, url = {http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6658604} } |
|||||

Johnson, T. and Mitra, S. | Invariant Synthesis for Verification of Parameterized Cyber-Physical Systems with Application to Aerospace Systems | 2013 | Proceedings of Infotech@AIAA | ||

BibTeX:
@inproceedings{JM:AI:2013, author = {Taylor Johnson and Sayan Mitra}, title = {Invariant Synthesis for Verification of Parameterized Cyber-Physical Systems with Application to Aerospace Systems}, booktitle = {Proceedings of Infotech@AIAA}, year = {2013} } |
|||||

Johnson, T.T. | Uniform Verification of Safety for Parameterized Networks of Hybrid Automata | 2013 | School: Department of Electrical and Computer Engineering, University of Illinois at Urbana-Champaign |
||

BibTeX:
@phdthesis{johnson2013thesis, author = {Taylor T. Johnson}, title = {Uniform Verification of Safety for Parameterized Networks of Hybrid Automata}, school = {Department of Electrical and Computer Engineering, University of Illinois at Urbana-Champaign}, year = {2013} } |
|||||

Mitra, S., Wongpiromsarn, T. and Murray, R.M. | Verifying Cyber-Physical Interactions in Safety-Critical Systems | 2013 | IEEE Security & Privacy Vol. 11, pp. 28-37 |
||

Abstract: Safety-compromising bugs in software-controlled systems are often hard to detect. In a 2007 DARPA Urban Challenge vehicle, such a defect remained hidden during more than 300 miles of test-driving and hours of extensive simulations, manifesting for the first time in a particular physical environment during the competition, which led to a safety violation and its team’s disqualification. With this incident as an example, the authors discuss formalisms and techniques available for safety analysis of cyber-physical systems. They discuss simulation-based approaches, more formal approaches, and the emerging area that attempts to take advantage of both. They highlight these approaches’ merits and limitations and identify open problems, the resolution of which will bolster the development of reliable safety-critical cyber-physical systems. |
|||||

BibTeX:
@article{MWM:IEEESP2013, author = {Mitra, Sayan and Wongpiromsarn, Tichakorn and Murray, Richard M.}, title = {Verifying Cyber-Physical Interactions in Safety-Critical Systems}, journal = {IEEE Security & Privacy}, year = {2013}, volume = {11}, pages = {28-37}, url = {http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6531612&url=http%3A%2F%2Fieeexplore.ieee.org%2Fstamp%2Fstamp.jsp%3Ftp%3D%26arnumber%3D6531612} } |
|||||

Prabhakar, P., Duggirala, P.S., Mitra, S. and Viswanathan, M. | Hybrid Automata-based CEGAR for Rectangular Hybrid Systems | 2013 | the Proceedings of 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2013) | ||

Abstract: In this paper we present a framework for carrying out counter-example guided abstraction-refinement (CEGAR) for systems modelled as rectangular hybrid automata. The main difference, between our approach and previous proposals for CEGAR for hybrid automata, is that we consider the abstractions to be hybrid automata as well. We show that the CEGAR scheme is semi-complete for the class of rectangular hybrid automata and complete for the subclass of initialized rectangular automata. We have implemented the CEGAR based algorithm in a tool called HARE, that makes calls to HyTech to analyze the abstract models and validate the counterexamples. Our experiments demonstrate the usefulness of the approach. |
|||||

BibTeX:
@inproceedings{PDMV:vmcai2013, author = {Pavithra Prabhakar and Parasara Sridhar Duggirala and Sayan Mitra and Mahesh Viswanathan}, title = {Hybrid Automata-based CEGAR for Rectangular Hybrid Systems}, booktitle = {the Proceedings of 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2013)}, year = {2013}, url = {http://link.springer.com/chapter/10.1007%2F978-3-642-35873-9_6} } |
|||||

Huang, Z. | On Simulation-Based Verification of Nonlinear Nondeterministic Hybrid Systems | 2013 | School: UIUC |
||

Abstract: Automatic safety verification of hybrid systems typically involves computing precise reach sets of such systems. This computation limits scalability of verification as for many model classes it scales exponentially with the number of continuous variables. First we propose a simulation-based algorithm for computing the reach set of a class of deterministic hybrid system. The algorithm first constructs a cover of the initial set of the hybrid system. Then the reach set of executions from the same cover are over-approximated by simulation traces and tubes around them. Experiments are performed on several benchmark problems including navigation benchmarks, room heating benchmarks, non-linear satellite systems and engine hybrid control systems. The results suggest the algorithm may scale to larger systems. Finally, we present a reachability algorithm that computes precise reach set of dynamical systems A with non-linear differential inclusions. The algorithm constructs a sequence of shrink concretizations of A. Then the reach sets of the concretizations are used to construct an over-approximation of the reach set of A. Soundness and Completeness of both algorithms presented are formally proved. |
|||||

BibTeX:
@mastersthesis{Zhenqi:Masters2013, author = {Zhenqi Huang}, title = {On Simulation-Based Verification of Nonlinear Nondeterministic Hybrid Systems}, school = {UIUC}, year = {2013}, url = {https://www.ideals.illinois.edu/bitstream/handle/2142/45481/Zhenqi_Huang.pdf} } |
|||||

Duggirala, P.S., Johnson, T., Zimmerman, A. and Mitra, S. | Static and Dynamic Analysis of Timed Distributed Traces | 2012 | Proceedings of IEEE Real-Time Systems Symposium (RTSS 2012) | ||

Abstract: This paper presents an algorithm for checking global predicates from traces of distributed embedded systems. For an individual agent, such as a mobile phone, tablet, or robot, a trace is a finite sequence of state observations and message histories. Each recording has a possibly inaccurate timestamp from the agent's local clock. The challenge is to symbolically overapproximate the reachable states of the entire system from the unsynchronized traces of the individual devices. The presented algorithm first approximates the time of occurrence of each event, based on the synchronization errors of the local clocks, and then overapproximates the reach sets of the continuous variables between consecutive observations. The algorithm is shown to be sound; it is also complete for a class of agents with restricted continuous dynamics and when the traces have precise information about timing synchronization inaccuracies. The algorithm is implemented in an SMT solver-based tool for analyzing traces of distributed Android Apps. Experimental results using the tool illustrate that interesting properties like safe separation, correct geocast delivery, and distributed deadlocks can be automatically checked and potential counterexamples can be found. Analyzing these properties on a 10 second long distributed trace for 20 agents completes within a minute and often in seconds, suggesting that the approach can scale. |
|||||

BibTeX:
@inproceedings{DJZM:android2012, author = {Parasara Sridhar Duggirala and Taylor Johnson and Adam Zimmerman and Sayan Mitra}, title = {Static and Dynamic Analysis of Timed Distributed Traces}, booktitle = {Proceedings of IEEE Real-Time Systems Symposium (RTSS 2012)}, year = {2012}, url = {http://www.computer.org/csdl/proceedings/rtss/2012/4869/00/4869a173-abs.html} } |
|||||

Duggirala, P.S. and Mitra, S. | Lyapunov Abstractions for Inevitability of Hybrid Systems | 2012 | The 15th International Conference on Hybrid Systems: Computation and Control (HSCC 2012), Beijing, China. | ||

Abstract: A set of states S is said to be inevitable for a hybrid automaton A if every behavior of A ultimately reaches S within bounded time. Inevitability captures various common liveness properties. In this paper, we present an algorithm for verifying inevitability of Linear Hybrid Automata (LHA). The algorithm combines (a) Lyapunov function-based relational abstractions for the continuous dynamics with (b) automated construction of well-founded relations for the loops of the hybrid automaton. The algorithm is complete for automata that are symmetric with respect to the chosen Lyapunov functions. The algorithm is implemented in a prototype tool (LySHA ) which is integrated with a Simulink/Stateflow frontend for modeling hybrid systems. The experimental results demonstrate the effectiveness of the methodology in verifying inevitability of hybrid automata with up to five continuous dimensions and forty locations. |
|||||

BibTeX:
@inproceedings{DM:2012, author = {Parasara Sridhar Duggirala and Sayan Mitra}, title = {Lyapunov Abstractions for Inevitability of Hybrid Systems}, booktitle = {The 15th International Conference on Hybrid Systems: Computation and Control (HSCC 2012), Beijing, China.}, year = {2012}, url = {http://dl.acm.org/citation.cfm?id=2185632.2185652&coll=DL&dl=GUIDE&CFID=83491856&CFTOKEN=96152652} } |
|||||

Huang, Z. and Mitra, S. | Computing Bounded Reach Sets from Sampled Simulation Traces | 2012 | The 15th International Conference on Hybrid Systems: Computation and Control (HSCC 2012), Beijing, China. | ||

Abstract: This paper presents an algorithm which uses simulation traces and formal models for computing overapproximations of reach sets of deterministic hybrid systems. The implementation of the algorithm in a tool, Hybrid Trace Verifier (HTV), uses Mathwork’s Simulink/Stateflow (SLSF) environment for generating simulation traces and for obtaining formal models. Computation of the overapproximation relies on computing error bounds in the dynamics obtained from the formal model. Verification results from three case studies, namely, a version of the navigation benchmark, an engine control system, and a satellite system suggest that this combined formal analysis and simulation based approach may scale to larger problems. |
|||||

BibTeX:
@inproceedings{HM:2012, author = {Zhenqi Huang and Sayan Mitra}, title = {Computing Bounded Reach Sets from Sampled Simulation Traces}, booktitle = {The 15th International Conference on Hybrid Systems: Computation and Control (HSCC 2012), Beijing, China.}, year = {2012}, url = {http://dl.acm.org/citation.cfm?id=2185632.2185676&coll=DL&dl=GUIDE&CFID=83491856&CFTOKEN=96152652} } |
|||||

Huang, Z. and Mitra, S. | Trace-based Bounded Verification of Embedded Systems | 2012 | |||

Abstract: This paper presents a technique that combine simulations and formal analysis for verifying embedded systems. It presents an algorithm which takes a simulation trace and a system model as input, and computes and overapproximation of the bounded reachable states of any execution that may have produced the trace. This enables approximate verification of bounded safety properties. Implementation of the algorithm in a software tool works with traces and models from Mathworks Simulink/Stateflow. Experimental evaluation of the tool in analyzing several benchmark systems with linear and nonlinear dynamics, and with upto 10 continuous dimensions, hints at the practical applicability of this approach. |
|||||

BibTeX:
@article{HM:ESL2012, author = {Zhenqi Huang and Sayan Mitra}, title = {Trace-based Bounded Verification of Embedded Systems}, year = {2012} } |
|||||

Huang, Z., Mitra, S. and Dullerud, G. | Differentially Private Iterative Synchronous Consensus | 2012 | Proceedings of the Workshop on Differentially Private Iterative Synchronous Consensus in conjunction with the ACM CCS conference 2012 | ||

Abstract: The iterative consensus problem requires a set of processes or agents with different initial values, to interact and update their states to eventually converge to a common value. Protocols solving iterative consensus serve as building blocks in a variety of systems where distributed coordination is required for load balancing, data aggregation, sensor fusion, filtering, and synchronization. In this paper, we introduce the private iterative consensus problem where agents are required to converge while protecting the privacy of their initial values from honest but curious adversaries. Protecting the initial states, in many applications, suffice to protect all subsequent states of the individual participants. We adapt the notion of differential privacy in this setting of iterative computation. Next, we present one server-based and a second completely distributed randomized mechanism for solving differentially private iterative consensus with adversaries who can observe the messages as well as the internal states of the server and a subset of the clients. Our analysis establishes the tradeoff between privacy and the accuracy: for given b >0 the differentially private mechanism for N agents, is guaranteed to convergence to a value within O(1/(epsilon bN)) |
|||||

BibTeX:
@inproceedings{HMG:WPES2012, author = {Zhenqi Huang and Sayan Mitra and Geir Dullerud}, title = {Differentially Private Iterative Synchronous Consensus}, booktitle = {Proceedings of the Workshop on Differentially Private Iterative Synchronous Consensus in conjunction with the ACM CCS conference 2012}, publisher = {ACM}, year = {2012}, url = {http://arxiv.org/abs/1207.4262} } |
|||||

Green, J. | Compositional bounded reachability using time partitioning and abstraction | 2012 | School: University of Illinois at Urbana-Champaign |
||

Abstract: Automatic verification of cyber-physical systems (CPS) typically involves computing the reachable set of states of such systems. This computation is known to be exponential in the number of continuous variables. For systems that can be decomposed into separate components with lower dimensionality, we present an algorithm that verifies global safety properties of the complete system using the reach sets of the components. Here, the components are only coupled through a shared time variable. Using a satellite system case study, we are able to show significant savings in memory and runtime computation costs for this approach. For systems whose components are coupled through additional continuous variables, we present an abstraction to overapproximate the interaction between the components such that the aforementioned algorithm can be used. The feasibility of this abstraction is demonstrated experimentally, which also shows additional work is necessary to develop a more efficient abstraction. |
|||||

BibTeX:
@mastersthesis{JDGreen:Masters2012, author = {Jeremy Green}, title = {Compositional bounded reachability using time partitioning and abstraction}, school = {University of Illinois at Urbana-Champaign}, year = {2012}, url = {https://www.ideals.illinois.edu/bitstream/handle/2142/34351/Green_Jeremy.pdf?sequence=1} } |
|||||

Johnson, T., Green, J., Mitra, S., Dudley, R. and Erwin, R.S. | Verifying Satellite Rendezvous and Conjunction Avoidance: A Formal Approach to Autonomy in Space | 2012 | International Conference on Formal Methods (FM) | ||

Abstract: Satellite systems are beginning to incorporate complex autonomous operations, which calls for rigorous reliability assurances. Human operators usually plan satellite maneuvers in detail, but autonomous operation will require software to make decisions using noisy sensor data and problem solutions with numerical inaccuracies. For such systems, formal verification guarantees are particularly attractive. This paper presents automatic verification techniques for providing assurances in satellite maneuvers. The specific reliability criteria studied are rendezvous and conjunction avoidance for two satellites performing orbital transfers. Three factors pose challenges for verifying such systems: (a) incommensurate orbits, (b) uncertainty of orbital parameters after thrusting, and (c) nonlinear dynamics. A sequence of abstractions are proposed for contending with these challenges, namely (a) quotienting of the state-space based on periodicity of orbital dynamics, (b) aggregation of similar transfer orbits, and (c) overapproximation of nonlinear dynamics using hybridization. Experiments with a prototype tool that implement the abstractions and use existing hybrid system model checkers establish the feasibility of the proposed method. The experiments suggest future capabilities that hybrid systems verification tools should support. |
|||||

BibTeX:
@inproceedings{JGMDE:2012, author = {Taylor Johnson and Jeremy Green and Sayan Mitra and Rachel Dudley and R. Scott Erwin}, title = {Verifying Satellite Rendezvous and Conjunction Avoidance: A Formal Approach to Autonomy in Space}, booktitle = {International Conference on Formal Methods (FM)}, year = {2012} } |
|||||

Johnson, T. and Mitra, S. | Parameterized Verification of Distributed Cyber-Physical Systems:An Aircraft Landing Protocol Case Study | 2012 | ACM/IEEE Third International Conference on Cyber-Physical Systems, April 2012, Beijing, China | ||

Abstract: In this paper, we present the formal modeling and automatic parameterized verification of a distributed air traffic control protocol called the Small Aircraft Transportation System (SATS). Each aircraft is modeled as a timed automaton with (possibly unbounded) counters. SATS is then described as the composition of N such aircraft, where N is a parameter from the natural numbers. We verify several safety properties for arbitrary N, the most important of which is separation assurance, which ensures that no two aircraft may ever collide. The verification methodology relies on computing the set of backward reachable states from the set of unsafe states to a fixed point, and checking emptiness of the intersection of these reachable states and the initial set of states. We used the Model Checker Modulo Theories (MCMT) tool, which implements this technique. |
|||||

BibTeX:
@inproceedings{JM:2012, author = {Taylor Johnson and Sayan Mitra}, title = {Parameterized Verification of Distributed Cyber-Physical Systems:An Aircraft Landing Protocol Case Study}, booktitle = {ACM/IEEE Third International Conference on Cyber-Physical Systems, April 2012, Beijing, China}, year = {2012} } |
|||||

Johnson, T. and Mitra, S. | A Small Model Theorem for Rectangular Hybrid Automata Networks | 2012 | Vol. 7273IFIP International Conference on Formal Techniques for Distributed Systems joint international conference: 32nd Formal Techniques for Networked and Distributed Systems (FORTE)., pp. 18--34 |
||

Abstract: Rectangular hybrid automata (RHA) are finite state machines with additional skewed clocks that are useful for modeling real-time systems. This paper is concerned with the uniform verification of safety properties of networks with arbitrarily many interacting RHAs. Each automaton is equipped with a finite collection of pointers to other automata that enables it to read their state. This paper presents a small model result for such networks that reduces the verification problem for a system with arbitrarily many processes to a system with finitely many processes. The result is applied to verify and discover counter-examples of inductive invariant properties of distributed protocols, such as Fischer's mutual exclusion algorithm, the Small Aircraft Transportation System (SATS) protocol, and a one-dimensional flocking protocol. We have implemented a prototype tool called PASSEL relying on the satisfiability modulo theories (SMT) solver Z3 to check automatically key inductive invariants. |
|||||

BibTeX:
@inproceedings{JM:2012:small, author = {Taylor Johnson and Sayan Mitra}, title = {A Small Model Theorem for Rectangular Hybrid Automata Networks}, booktitle = {IFIP International Conference on Formal Techniques for Distributed Systems joint international conference: 32nd Formal Techniques for Networked and Distributed Systems (FORTE).}, year = {2012}, volume = {7273}, pages = {18---34}, url = {http://www.springerlink.com/content/yh36373235030543/?MUD=MP} } |
|||||

Wongpiromsarn, T., Mitra, S., Lamperski, A. and Murray, R. | Verification of Periodically Controlled Hybrid Systems: Application to An Autonomous Vehicle | 2012 | Special Issue of the ACM Transactions on Embedded Computing Systems (TECS) Vol. 11(S2) |
||

Abstract: This paper introduces Periodically Controlled Hybrid Automata (PCHA) for modular specification of embedded control systems. In a PCHA, control actions that change the control input to the plant occur roughly periodically, while other actions that update the state of the controller may occur in the interim. Such actions could model, for example, sensor updates and information received from higher-level planning modules that change the set-point of the controller. Based on periodicity and subtangential conditions, a new sufficient condition for verifying invariant properties of PCHAs is presented. For PCHAs with polynomial continuous vector fields, it is possible to check these conditions automatically using, for example, quantifier elimination or sum of squares decomposition. We examine the feasibility of this automatic approach on a small example. The proposed technique is also used to manually verify safety and progress properties of a fairly complex planner-controller subsystem of an autonomous ground vehicle. Geometric properties of planner-generated paths are derived which guarantee that such paths can be safely followed by the controller. |
|||||

BibTeX:
@article{WMLM:TECS2010, author = {Tichakorn Wongpiromsarn and Sayan Mitra and Andrew Lamperski and Richard Murray}, title = {Verification of Periodically Controlled Hybrid Systems: Application to An Autonomous Vehicle}, journal = {Special Issue of the ACM Transactions on Embedded Computing Systems (TECS)}, year = {2012}, volume = {11}, number = {S2}, url = {http://dl.acm.org/citation.cfm?id=2331163&CFID=127784079&CFTOKEN=31523745} } |
|||||

Carrasco, M.B. | Opportunistic clock synchronization for ad hoc networks | 2011 | School: UIUC |
||

Abstract: An ad hoc network is a collection of computing nodes communicating over wireless channels without relying on any fi xed infrastructure such as servers and towers. Such networks are useful in rescue operations, and in rural and military settings. Clock synchronization is an essential building block for many ad hoc wireless network applications. It provides the participating computing nodes with logical clocks whose di erences can be bounded. Several traditional distributed clock synchronization algorithms use strict communication structures such as spanning trees. In such protocols, a node corrects its logical clock when it receives a new time-stamped message from its parent. In this thesis, we present a new clock synchronization protocol that exploits the broadcast medium in wireless networks, allowing nodes to opportunistically correct their logical clocks in order to converge to a reference time provided by a designated root node. Our protocol does not rely on a communication structure and is lightweight due to its low overhead. We also propose a variation of our opportunistic protocol, which further reduces overhead through randomized broadcast techniques. Our simulation-based experimental evaluation of the protocols illustrates that our opportunistic algorithms improve the accuracy of the nodes' logical clocks, when compared to a tree-based protocol. However, we show that the level of improvement is a function of the density of the wireless network. Additionally, the results show that our algorithms can produce around half the overhead, compared to an existing protocol that achieves higher levels of precision. |
|||||

BibTeX:
@mastersthesis{Berenice:Masters2011, author = {Carrasco, Maria B.}, title = {Opportunistic clock synchronization for ad hoc networks}, school = {UIUC}, year = {2011}, url = {https://www.ideals.illinois.edu/handle/2142/26050} } |
|||||

Bak, S., Manamcheri, K., Mitra, S. and Caccamo, M. | Sandboxing Controllers for Cyber-Physical Systems | 2011 | Proceedings of 2nd IEEE/ACM International Conference on Cyber-physical systems (ICCPS 2011) | ||

Abstract: Cyber-physical systems (CPS) bridge the gap between cyber components, typically written in software, and the physical world. Software written with traditional development practices, however, likely contains bugs or unintended interactions among components, which can result in uncontrolled and possibly disastrous physical-world interactions. Complete verification of CPS is often impractical due to outsourced development, cost, lack of formal specifications, or excessively large or complex models. Rather than mandating complete modeling and verification, we advocate sandboxing of unverified controllers by augmenting the system with a verified safety wrapper that can take control of the plant in order to avoid violations of formal safety properties. The focus of this work is an automatic method, based on reachability and time-bounded reachability of hybrid systems, to generate verified sandboxes. The method is shown to be both more general than previous work, and allows the trade-off of increased computation time for improved reachability accuracy. We also present an end-to-end toolkit which performs the low-level computation to generate the sandbox source code from Simulink/Stateflow models. |
|||||

BibTeX:
@inproceedings{BMKC:sandbox:ICCPS2011, author = {Stanley Bak and Karthik Manamcheri and Sayan Mitra and Marco Caccamo}, title = {Sandboxing Controllers for Cyber-Physical Systems}, booktitle = {Proceedings of 2nd IEEE/ACM International Conference on Cyber-physical systems (ICCPS 2011)}, publisher = {IEEE Computer Society}, year = {2011}, url = {http://delivery.acm.org/10.1145/2010000/2007425/4361a003.pdf?ip=130.126.141.238&CFID=37805901&CFTOKEN=72113100&__acm__=1316019252_daa77fda5f607565c4dcde6e6a19693e} } |
|||||

Chandy, K.M., Go, B., Mitra, S., Pilotto, C. and White, J. | Verification of Distributed Systems with Local-Global Predicates | 2011 | Journal of Formal Aspects of Computing (FAC) Vol. 23(5), pp. 649-679 |
||

Abstract: This paper describes a methodology for developing and verifying a class of distributed systems in which states and state transitions may be continuous or discrete. We focus on systems where changes are local in that a small number of components change state while the remainder of the system is unchanged. A proof methodology is developed that ensures global properties, such as invariants and convergence, by guaranteeing local properties within subsystems. This methodology is used to prove the correctness of concrete examples. We present a PVS library of theorems and proofs that can be used to reduce the work required to develop and verify programs in this class. A transformation of these libraries to Java is also made. |
|||||

BibTeX:
@article{CGMPW:FACS2010, author = {K. Mani Chandy and Brian Go and Sayan Mitra and Concetta Pilotto and Jerome White}, title = {Verification of Distributed Systems with Local-Global Predicates}, journal = {Journal of Formal Aspects of Computing (FAC)}, year = {2011}, volume = {23}, number = {5}, pages = {649-679}, url = {http://www.springerlink.com/content/m37mk32q2239r96j/} } |
|||||

Duggirala, P.S. and Mitra, S. | Abstraction-Refinement for Stability | 2011 | Proceedings of 2nd IEEE/ACM International Conference on Cyber-physical systems (ICCPS 2011) | ||

Abstract: The paper presents a counterexample-guided abstraction refinement procedure for verifying stability (region stabillity) of CPS modeled as hybrid automata. It relies on a characterization of the blocking property of hybrid automata in terms of well-foundedness of a relation that combines the discrete transitions and continuous trajectories and a key assumption about the switching speed of the system in terms of average dwell time, but does not require the individual modes to be stable. This characterization enables the adaptation of program analysis techniques to the domain of hybrid systems. It is shown that the procedure is complete for rectangular initialized hybrid automata. Several illustrative examples are verified using a prototype tool that implements the methodology |
|||||

BibTeX:
@inproceedings{DM:hystab:ICCPS2011, author = {Parasara Sridhar Duggirala and Sayan Mitra}, title = {Abstraction-Refinement for Stability}, booktitle = {Proceedings of 2nd IEEE/ACM International Conference on Cyber-physical systems (ICCPS 2011)}, year = {2011}, url = {http://dl.acm.org/citation.cfm?id=2007337.2007427&coll=DL&dl=GUIDE&CFID=99228380&CFTOKEN=13940715} } |
|||||

Johnson, T. and Mitra, S. | Safe Flocking in Spite of Actuator Faults using Directional Failure Detectors | 2011 | Journal of Nonlinear Systems and Applications Vol. 2(1-2), pp. 73-95 |
||

Abstract: The safe flocking problem requires a collection of mobile agents to (a) converge to and maintain an equi-spaced lattice formation, (b) arrive at a destination, and (c) always maintain a minimum safe separation. Safe flocking in Euclidean spaces is a well-studied and difficult coordination problem. In this paper, we study one-dimensional safe flocking in the presence of actuator faults and directional failure detectors (DFDs). Actuator faults cause affected agents to move permanently with arbitrary velocities, and DFDs detect failures only when actuation and required motion are in opposing directions. First, assuming existence of a DFD for actuator faults, we present an algorithm for safe flocking. Next, we show that certain actuator faults cannot be detected with DFDs, while detecting others requires time that grows linearly with the number of participating agents. Finally, we show that our DFD algorithm achieves the latter bound. |
|||||

BibTeX:
@article{JM:JNSA2011, author = {Taylor Johnson and Sayan Mitra}, title = {Safe Flocking in Spite of Actuator Faults using Directional Failure Detectors}, journal = {Journal of Nonlinear Systems and Applications}, year = {2011}, volume = {2}, number = {1-2}, pages = {73-95}, url = {http://dcdis001.watam.org/JNSA/volumes/abstract_pdf/2011v2/v2n1-pdf/11.pdf} } |
|||||

Johnson, T., Mitra, S. and Langbort, C. | Stability of Digitally Interconnected Linear Systems | 2011 | Proceedings of 50th IEEE Conference on Decision and Control (CDC) | ||

Abstract: A sufficient condition for stability of linear subsystems interconnected by digitized signals is presented. There is a digitizer for each linear subsystem that periodically samples an input signal and produces an output that is quantized and saturated. The output of the digitizer is then fed as an input (in the usual sense) to the linear subsystem. Due to digitization, each subsystem behaves as a switched affine system, where state-dependent switches are induced by the digitizer. For each quantization region, a storage function is computed for each subsystem by solving appropriate linear matrix inequalities (LMIs), and the sum of these storage functions is a Lyapunov function for the interconnected system. Finally, using a condition on the sampling period, we specify a subset of the unsaturated state space from which all executions of the interconnected system reach a neighborhood of the quantization region containing the origin. The sampling period proves to be pivotal—if it is too small, then a dwell-time argument cannot be used to establish convergence, while if it is too large, an unstable subsystem may not receive timely-enough inputs to avoid diverging. |
|||||

BibTeX:
@inproceedings{JML:CDC2011, author = {Taylor Johnson and Sayan Mitra and Cédric Langbort}, title = {Stability of Digitally Interconnected Linear Systems}, booktitle = {Proceedings of 50th IEEE Conference on Decision and Control (CDC)}, year = {2011}, note = {To appear}, url = {http://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=06161264} } |
|||||

Manamcheri Sukumar, K. | Translation of Simulink-Stateflow models to hybrid automata | 2011 | School: UIUC |
||

Abstract: Formal analysis of Simulink/Stateflow (SLSF) diagrams requires association of semantics to these diagrams. In this thesis, we present a technique and the related tool called HyLink for translating a useful subclass of SLSF diagrams to hybrid automata. In the absence of official semantics, there are two possible interpretations of these diagrams: one is based on the ideal mathematical interpretation obtained from the syntax of the building blocks and the other is based on the simulation traces generated by the simulation engine. These two interpretations lead to two different kinds of hybrid automata---the former gives an automaton with state-dependent transitions and the latter gives a time-triggered automaton. We show that under certain assumptions, the semantics of the latter converge to the former as the simulation step size decreases. We illustrate HyLink's translation scheme, the assumptions, and the convergence result through several case studies. |
|||||

BibTeX:
@mastersthesis{Karthin:Masters2011, author = {Manamcheri Sukumar, Karthikeyan}, title = {Translation of Simulink-Stateflow models to hybrid automata}, school = {UIUC}, year = {2011}, url = {https://www.ideals.illinois.edu/handle/2142/26197} } |
|||||

Kim, K.-D., Mitra, S. and Kumar, P.R. | Computing bounded epsilon-Reach Set with finite precision computations for a class of linear hybrid automata | 2011 | Proceedings of Hybrid Systems: Computation and Control (HSCC 2011) | ||

Abstract: In a previous paper we have identified a special class of linear hybrid automata, called Deterministic Transversal Linear Hybrid Automata, and shown that an epsilon-reach set up to a finite time (i.e., bounded epsilon-reach set), can be computed using infiinfinite precision calculations. However, given the linearity of the system and the consequent presence of matrix exponentials, numerical errors are inevitable and this assumption about infinite precision calculations is impractical. In this paper we present an algorithm that uses only finite precision numerical approximations. We further develop an architecture which decouples the fundamental computational steps from the runtime adaptation strategies for setting certain parameter values. |
|||||

BibTeX:
@inproceedings{KMK:reach:HSCC2011, author = {Kyoung-Dae Kim and Sayan Mitra and P. R. Kumar}, title = {Computing bounded epsilon-Reach Set with finite precision computations for a class of linear hybrid automata}, booktitle = {Proceedings of Hybrid Systems: Computation and Control (HSCC 2011)}, year = {2011}, url = {http://dl.acm.org/citation.cfm?id=1967701.1967719&coll=DL&dl=GUIDE&CFID=99228380&CFTOKEN=13940715} } |
|||||

Manamcheri, K., Mitra, S., Bak, S. and Caccamo, M. | A step towards verification and synthesis from Simulink/Stateflow models | 2011 | Hybrid Systems: Computation and Control (HSCC 2011) | ||

Abstract: This paper describes a toolkit for synthesizing hybrid supervisory control system starting from Simulink/Stateflow. The toolkit provides a systematic strategy for translating Simulink/Stateflow models to hybrid automata and a discrete abstraction-based algorithm for synthesizing supervisory controllers. |
|||||

BibTeX:
@inproceedings{MMBC:hylink2011, author = {Karthik Manamcheri and Sayan Mitra and Stanley Bak and Marco Caccamo}, title = {A step towards verification and synthesis from Simulink/Stateflow models}, booktitle = {Hybrid Systems: Computation and Control (HSCC 2011)}, year = {2011}, url = {http://dl.acm.org/citation.cfm?id=1967701.1967749&coll=DL&dl=GUIDE&CFID=99228380&CFTOKEN=13940715} } |
|||||

Bak, S., Greer, A. and Mitra, S. | Hybrid Cyberphysical System Verification With Simplex Using Discrete Abstractions | 2010 | 16th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2010). | ||

Abstract: Providing integrity, efficiency, and performance guarantees is a key challenge in the development of next-generation cyberphysical systems. Rather than mandating complete system verification, the Simplex Architecture provides robust designs by incorporating a supervisory controller that takes corrective action only when the system is in danger of violating a desired invariant property such as safety. The central issue in applying this approach is designing the switching logic for the supervisory controller such that it guarantees safety and at the same time is not overly conservative. Previous research in the area relied on finding Lyapunov functions for the underlying continuous dynamical system. In contrast, in this paper, we present an automatic method for solving this design problem through discrete abstractions of the underlying hybrid system and model checking. We present a case study where, in collaboration with John Deere, we use the developed approach to create the Simplex decision module for an off-road vehicle, which is formally verified as both correct and timely. |
|||||

BibTeX:
@inproceedings{BGM:RTAS2010, author = {Stanley Bak and Ashley Greer and Sayan Mitra}, title = {Hybrid Cyberphysical System Verification With Simplex Using Discrete Abstractions}, booktitle = {16th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2010).}, year = {2010}, note = {To appear}, url = {http://dl.acm.org/citation.cfm?id=1828428.1829218&coll=DL&dl=GUIDE&CFID=99228380&CFTOKEN=13940715} } |
|||||

Duggirala, P.S., Mitra, S., Kumar, R. and Glazeski, D. | On The Theory of Stochastic Processors | 2010 | Seventh International Conference on the Quantitative Evaluation of Systems (QEST 2010) | ||

Abstract: Traditional architecture design approaches hide hardware uncertainties from the software stack through over-design, which is often expensive in terms of power consumption. The recently proposed quantitative alternative of stochastic computing requires circuits and processors to be correct only probabilistically and use less power. In this paper, we present the first step towards a theory of stochastic computing. Specifically, a formal model of a device which computes a deterministic function with stochastic delays is presented; the semantics of a stochastic circuit is obtained by composing such devices; finally, a quantitative notion of stochastic correctness, called correctness factor (CF), is introduced. For random data sources, a closed form expression is derived for CF of devices, which shows that there are two probabilities that contribute positively, namely, the probability of being timely with current inputs and the probability of being lucky with past inputs. Finally, we show the characteristic graphs obtained from the analytical expressions for the variation of correctness factor with clock period, for several simple circuits and sources. |
|||||

BibTeX:
@inproceedings{DMKG:QEST2010, author = {Parasara Sridhar Duggirala and Sayan Mitra and Rakesh Kumar and Dean Glazeski}, title = {On The Theory of Stochastic Processors}, booktitle = {Seventh International Conference on the Quantitative Evaluation of Systems (QEST 2010)}, publisher = {IEEE Press}, year = {2010}, url = {http://dl.acm.org/citation.cfm?id=1906816} } |
|||||

Johnson, T. and Mitra, S. | Safe and Stabilizing Distributed Flocking in Spite of Actuator Faults | 2010 | (UILU-ENG-10-2204 (CRHC-10-02)) | ||

Abstract: The safe flocking problem requires a collection of N mobile agents to (a) converge to and maintain an equi-spaced lattice formation, (b) arrive at a destination, and (c) always maintain a minimum safe separation. Safe flocking in Euclidean spaces is a well-studied and difficult coordination problem. Motivated by real-world deployment of multi-agent systems, this paper studies one-dimensional safe flocking, where agents are afflicted by actuator faults. An actuator fault is a new type of failure that causes an affected agent to be stuck moving with an arbitrary velocity. In this setting, first, a self-stabilizing solution for the problem is presented. This relies on a failure detector for actuator faults. Next, it is shown that certain actuator faults cannot be detected, while others may require O(N) time for detection. Finally, a simple failure detector that achieves the latter bound is presented. Several simulation results are presented that illustrate the algorithm in operation and the effects of failures on progress towards flocking. |
|||||

BibTeX:
@techreport{JM:2010TR, author = {Taylor Johnson and Sayan Mitra}, title = {Safe and Stabilizing Distributed Flocking in Spite of Actuator Faults}, year = {2010}, number = {UILU-ENG-10-2204 (CRHC-10-02)}, url = {http://www.computer.org/portal/web/csdl/doi/10.1109/ICDCS.2010.49} } |
|||||

Johnson, T. and Mitra, S. | Safe Flocking in spite of Actuator Faults | 2010 | In proceedings of 12th International Symposium on Stabilization, Safety, and Security of Distributed Systems | ||

Abstract: The safe flocking problem requires a collection of N mobile agents to (a) converge to and maintain an equi-spaced lattice formation, (b) arrive at a destination, and (c) always maintain a minimum safe separation. Safe flocking in Euclidean spaces is a well-studied and difficult coordination problem. Motivated by real-world deployment of multi-agent systems, this paper studies one-dimensional safe flocking, where agents are afflicted by actuator faults. An actuator fault is a newtype of failure that causes an affected agent to be stuck moving with an arbitrary velocity. In this setting, first, a self-stabilizing solution for the problem is presented. This relies on a failure detector for actuator faults. Next, it is shown that certain actuator faults cannot be detected, while others may require O(N) time for detection. Finally, a simple failure detector that achieves the latter bound is presented. Several simulation results are presented for illustrating the effects of failures on the progress towards flocking. |
|||||

BibTeX:
@inproceedings{JM:SSS2010, author = {Taylor Johnson and Sayan Mitra}, title = {Safe Flocking in spite of Actuator Faults}, booktitle = {In proceedings of 12th International Symposium on Stabilization, Safety, and Security of Distributed Systems}, publisher = {Springer}, year = {2010}, url = {http://dl.acm.org/citation.cfm?id=1926829.1926876&coll=DL&dl=GUIDE&CFID=99228380&CFTOKEN=13940715} } |
|||||

Johnson, T., Mitra, S. and Manamcheri, K. | Safe and Stabilizing Distributed Cellular Flows | 2010 | Proceedings of IEEE Internaitonal Conference on Distributed Computing Systems (ICDCS 2010) | ||

Abstract: Advances in wireless vehicular networks present us with opportunities for developing new distributed traffic control algorithms that avoid phenomena such as abrupt phase-transitions. Towards this end, we study the problem of distributed traffic control in a partitioned plane where the movement of all entities (vehicles) within each partition (or cell) is controlled by a single process. We present a distributed traffic control protocol that guarantees minimum separation between vehicles at all times, even when some cell-processes fail by crashing. Once failures cease, the protocol is guaranteed to stabilize and the packets with feasible paths to the target cell make progress towards it. The algorithm relies on two general principles: local geographical routing, and temporary blocking for maintenance of safety. Our proofs use mostly assertional reasoning and may serve as a template for analyzing other distributed traffic control protocols. We also present simulation results which provide estimates of throughput as a function of velocity, safety separation, and path complexity. Further, we present simulation results to estimate throughput as a function of failure and recovery rates. |
|||||

BibTeX:
@inproceedings{JMS:ICDCS2010, author = {Taylor Johnson and Sayan Mitra and Karthik Manamcheri}, title = {Safe and Stabilizing Distributed Cellular Flows}, booktitle = {Proceedings of IEEE Internaitonal Conference on Distributed Computing Systems (ICDCS 2010)}, year = {2010}, url = {http://dl.acm.org/citation.cfm?id=1845878.1846242&coll=DL&dl=GUIDE&CFID=83491856&CFTOKEN=96152652} } |
|||||

Kim, K.-D., Mitra, S. and Kumar, P.R. | Bounded epsilon-Reachability of Linear Hybrid Automata with a Deterministic and Transversal Discrete Transition Condition | 2010 | Proceedings of The 49th IEEE Conference on Decision and Control (CDC) | ||

Abstract: An epsilon-reach set of a hybrid automaton is a set of states such that every state in it is within epsilon-distance of some reachable state. We propose an algorithm to compute an epsilon-reach set from a given initial state of a class of deterministic linear hybrid automata that satisfy a certain transversality condition. The proposed algorithm is based on time-sampling. It over-approximates the reachable states at each sampled time instant using polyhedra, and subsequently computes an epsilon-reach set using these over-approximations, while reducing the sampling period on-the-fly. |
|||||

BibTeX:
@inproceedings{KMK:CDC2010, author = {Kyoung-Dae Kim and Sayan Mitra and P. R. Kumar}, title = {Bounded epsilon-Reachability of Linear Hybrid Automata with a Deterministic and Transversal Discrete Transition Condition}, booktitle = {Proceedings of The 49th IEEE Conference on Decision and Control (CDC)}, publisher = {IEEE}, year = {2010}, url = {http://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=05717209} } |
|||||

Johnson, T. | Fault-tolerant distributed cyber-physical systems: two case studies | 2010 | School: UIUC |
||

Abstract: Fault-tolerance in distributed computing systems has been investigated extensively in the literature and has a rich history and detailed theory. This thesis studies fault-tolerance for distributed cyber-physical systems (DCPS), where distributed computation is combined with dynamics of physical processes. Due to their interaction with the physical world, DCPS may suffer from failures that are qualitatively different from the types of failures studied in distributed computing. Failures of the components of DCPS which interact with the physical processes---such as actuators and sensors---must be considered. Failures in the cyber domain may interact with failures of sensors and actuators in adverse ways. This thesis takes a first step in analyzing fault-tolerance in DCPS through the presentation of two case studies. In each case study, the DCPS are modeled as distributed algorithms executed by a set of agents, where each agent acts independently based on information obtained from its communication neighbors and agents may suffer from various failures. The first case study is a distributed traffic control problem, where agents control regions of roadway to move vehicles toward a destination, in spite of some agents' computers crashing permanently. The second case study is a distributed flocking problem, where agents form a flock, or a roughly equally spaced distribution in one dimension, and move towards a destination, in spite of some agents' actuators becoming stuck at some value. Each algorithm incorporates self-stabilization in order to solve the problem in spite of failures. The traffic algorithm uses a local signaling mechanism to guarantee safety and a self-stabilizing routing protocol to guarantee progress. The flocking algorithm uses a failure detector combined with an additional control strategy to ensure safety and progress. |
|||||

BibTeX:
@mastersthesis{Taylor:Masters2010, author = {Taylor Johnson}, title = {Fault-tolerant distributed cyber-physical systems: two case studies}, school = {UIUC}, year = {2010}, url = {https://www.ideals.illinois.edu/handle/2142/16191} } |
|||||

DeVille, R.E.L. and Mitra, S. | Stability of Distributed Algorithms in the face of Incessant Faults | 2009 | Proceedings of 11th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2009) | ||

Abstract: For large distributed systems built from inexpensive components, one expects to see incessant failures. This paper proposes two models for such faults and analyzes two well-known self-stabilizing algorithms under these fault models. For a small number of processes, the properties of interest are verified automatically using probabilistic model-checking tools. For a large number of processes, these properties are characterized using asymptotic bounds from a direct Markov chain analysis and approximated by numerical simulations. |
|||||

BibTeX:
@inproceedings{DM:SSS09, author = {R. E. Lee DeVille and Sayan Mitra}, title = {Stability of Distributed Algorithms in the face of Incessant Faults}, booktitle = {Proceedings of 11th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2009)}, year = {2009}, url = {http://dl.acm.org/citation.cfm?id=1693564.1693582&coll=DL&dl=GUIDE&CFID=99228380&CFTOKEN=13940715} } |
|||||

Gilbert, S., Lynch, N., Mitra, S. and Nolte, T. | Self-stabilizing robot formations over unreliable networks | 2009 | Special Issue on Self-adaptive and Self-organizing Wireless Networking Systems of ACM Transactions on Autonomous and Adaptive Systems (TAAS) Vol. 4(3), pp. 1-29 |
||

Abstract: We describe how a set of mobile robots can arrange themselves on any specified curve on the plane in the presence of dynamic changes both in the underlying ad hoc network and in the set of participating robots. Our strategy is for the mobile robots to implement a self-stabilizing virtual layer consisting of mobile client nodes, stationary Virtual Nodes (VNs), and local broadcast communication. The VNs are associated with predetermined regions in the plane and coordinate among themselves to distribute the client nodes relatively uniformly among the VNsï¿½ regions. Each VN directs its local client nodes to align themselves on the local portion of the target curve. The resulting motion coordination protocol is self-stabilizing, in that each robot can begin the execution in any arbitrary state and at any arbitrary location in the plane. In addition, self-stabilization ensures that the robots can adapt to changes in the desired target formation. |
|||||

BibTeX:
@article{GLMN:TAAS09, author = {Gilbert, Seth and Lynch, Nancy and Mitra, Sayan and Nolte, Tina}, title = {Self-stabilizing robot formations over unreliable networks}, journal = {Special Issue on Self-adaptive and Self-organizing Wireless Networking Systems of ACM Transactions on Autonomous and Adaptive Systems (TAAS)}, publisher = {ACM}, year = {2009}, volume = {4}, number = {3}, pages = {1--29}, url = {http://dl.acm.org/citation.cfm?id=1552297.1552300&coll=DL&dl=GUIDE&CFID=99228380&CFTOKEN=13940715}, doi = {http://doi.acm.org/10.1145/1552297.1552300} } |
|||||

Mitra, S. and Sastry, S. | Hybrid input output automata for composable conveyor systems | 2009 | 5th Annual IEEE International Conference on Automation Science and Engineering (CASE'09), pp. 29-29 | ||

Abstract: We present Hybrid Input/Output Automata (HIOA) models as a basis for the design and analysis of a class of composable conveyor systems. These conveyor systems are realized by composing instances of two kinds of units, namely segments and turns. A microcontroller, which is physically wired to the sensors and actuators on the unit, regulates the local operations at the unit level. Microcontrollers that regulate physically adjacent units interact with each other over wireless links. Our HIOA models capture the continuous dynamics of objects moving on a unit and the discrete sequence of interactions that coordinate operations across adjacent units. Coordination messages exchange status information and transfer objects from one unit to another. We use two layers of automata. The first, called RC (Route Control), maintains system-wide routes over which objects move in the conveyor systems. This automaton is common to all units. The second automaton, called TC (Traffic Control), interacts with the local environment. Each unit has a specialized TC automaton depending on whether it is a segment or a turn. The TC automata in physically adjacent units exchange Red and Green signals to regulate the movement of objects from one unit to the other. By composing instances of these automata models, we achieve system-level models for the conveyor systems. Using the formal reasoning mechanisms in HIOA theory, we expect to establish properties of the composed conveyor systems. For example, as preliminary results, we can show that the Route Control Protocol is self-stabilizing. We can also show that the signaling mechanism in the TC automata help to maintain spatial/temporal constraints, such as minimum gap between objects moving on the conveyor system. As our next step, we are working on specifying a third automaton, called MP that is an implementation of the TC and RC automata on a microcontroller platform. We aim to shown that if the execution of MP satisfies certain temporal constraints, then the composed conveyor systems are correct by construction and deliver the properties that we can deduce via an analysis of the HIOA models of composed conveyor systems. |
|||||

BibTeX:
@inproceedings{MitraSastry09, author = {Mitra, Sayan and Sastry, Shivakumar}, title = {Hybrid input output automata for composable conveyor systems}, booktitle = {5th Annual IEEE International Conference on Automation Science and Engineering (CASE'09)}, publisher = {IEEE Press}, year = {2009}, pages = {29--29} } |
|||||

Prabhakar, P., Mitra, S. and Viswanathan, M. | On Convergence of Concurrent Systems under Regular Interactions | 2009 | Vol. 571020th International Conference on Concurrency Theory (CONCUR 2009), pp. 527-541 |
||

Abstract: Convergence is often the key liveness property for distributed systems that interact with physical processes. Techniques for proving convergence (asymptotic stability) have been extensively studied by control theorists. In particular, for the asynchronous model of computation Tsitsiklis provides a set of necessary and sufficient conditions for proving stability and convergence under the assumption that each asynchronous operator (state transition function) is applied infinitely often. This paper generalize these results to obtain necessary and sufficient conditions for systems where the in?nite sequence of operators is a member of an arbitrary omega regular language. This enables us to apply our theory to distributed systems with changing communication topology, node failures and joins. We illustrate an application of the new set of conditions in verifying the convergence of a simple (continuous) consensus protocol. |
|||||

BibTeX:
@inproceedings{PMV:CONCUR08, author = {Pavithra Prabhakar and Sayan Mitra and Mahesh Viswanathan}, title = {On Convergence of Concurrent Systems under Regular Interactions}, booktitle = {20th International Conference on Concurrency Theory (CONCUR 2009)}, publisher = {Springer}, year = {2009}, volume = {5710}, pages = {527-541}, url = {http://dl.acm.org/citation.cfm?id=1611711.1611748&coll=DL&dl=GUIDE&CFID=99228380&CFTOKEN=13940715} } |
|||||

Wongpiromsarn, T., Mitra, S., Murray, R. and Lamperski, A. | Periodically Controlled Hybrid Systems: Verifying A Controller for An Autonomous Vehicle | 2009 | 12th International Conference Hybrid Systems: Computation and Control (HSCC 2009), pp. 396-410 | ||

Abstract: This paper introduces Periodically Controlled Hybrid Automata (PCHA) for describing a class of hybrid control systems. In a PCHA, control actions occur roughly periodically while internal and input actions may occur in the interim changing the discrete-state or the setpoint. Based on periodicity and subtangential conditions, a new sufficient condition for verifying invariance of PCHAs is presented. This technique is used in verifying safety of the planner-controller subsystem of an autonomous ground vehicle, and in deriving geometric properties of planner generated paths that can be followed safely by the controller under environmental uncertainties. |
|||||

BibTeX:
@inproceedings{WMML:HSCC09, author = {Tichakorn Wongpiromsarn and Sayan Mitra and Richard Murray and Andrew Lamperski}, title = {Periodically Controlled Hybrid Systems: Verifying A Controller for An Autonomous Vehicle}, booktitle = {12th International Conference Hybrid Systems: Computation and Control (HSCC 2009)}, year = {2009}, pages = {396-410}, url = {http://dl.acm.org/citation.cfm?id=1538188.1538217&coll=DL&dl=GUIDE&CFID=99228380&CFTOKEN=13940715} } |
|||||

Archer, M., Lim, H., Lynch, N., Mitra, S. and Umeno, S. | Specifying and Proving Properties of Timed I/O Automata Using Tempo | 2008 | Design Automation for Embedded Systems Vol. 8(1-2) |
||

Abstract: Timed I/O automata (TIOA) is a mathematical framework for modeling and verification of distributed systems that involve discrete and continuous dynamics. TIOA can be used for example, to model a real-time software component controlling a physical process. The TIOA model is sufficiently general to subsume other models in use for timed systems. The Tempo Toolset, currently under development, is aimed at supporting system development based on TIOA specifications. The Tempo Toolset is an extension of the IOA toolkit, which provides a specification simulator, a code generator, and both model checking and theorem proving support for analyzing specifications. This paper focuses on the modeling of timed systems and their properties with TIOA and on the use of TAME4TIOA, the TAME (Timed Automata Modeling Environment) based theorem proving support provided in Tempo, for proving system properties, including timing properties. Several examples are provided by way of illustration. |
|||||

BibTeX:
@article{DAEM08, author = {Myla Archer and Hongping Lim and Nancy Lynch and Sayan Mitra and Shinya Umeno}, title = {Specifying and Proving Properties of Timed I/O Automata Using Tempo}, journal = {Design Automation for Embedded Systems}, year = {2008}, volume = {8}, number = {1-2}, url = {http://www.springerlink.com/content/a82q782044162874/?p=87ae03bf514f48c2a78644d7c6361d6b&pi=1} } |
|||||

Gilbert, S., Lynch, N., Mitra, S. and Nolte, T. | Self-stabilizing Mobile Robot Formations with Virtual Nodes | 2008 | 10th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2008), pp. 188-202 | ||

Abstract: In this paper, we describe how virtual infrastructure can be used to coordinate the motion of mobile robots in a 2-dimensional plane in the presence of dynamic changes in the underlying mobile ad hoc network, i.e., nodes joining, leaving, or failing. The mobile robots cooperate to implement a VSA Layer, in which a virtual stationary automaton (VSA) is associated with each region of the plane. The VSAs coordinate among themselves to distribute the robots as needed throughout the plane. The resulting motion coordination protocol is self-stabilizing, in that each robot can begin the execution in any arbitrary state and at any arbitrary location in the plane. In addition, self-stabilization ensures that the robots can adapt to changes in the desired formation. |
|||||

BibTeX:
@inproceedings{GilbertLMN08, author = {Seth Gilbert and Nancy Lynch and Sayan Mitra and Tina Nolte}, title = {Self-stabilizing Mobile Robot Formations with Virtual Nodes}, booktitle = {10th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2008)}, year = {2008}, pages = {188-202}, url = {http://www.springerlink.com/content/hk1163qut8657847/} } |
|||||

Chandy, K.M., Mitra, S. and Pilotto, C. | Convergence Verification: From Shared Memory to Partially Synchronous Systems | 2008 | Vol. 5215Formal Modeling and Analysis of Timed Systems (FORMATS`08), pp. 217-231 |
||

Abstract: Verification of partially synchronous distributed systems is difficult because of inherent concurrency and the potentially large state space of the channels. This paper identifies a subclass of such systems for which convergence properties can be verified based on the proof of convergence for the corresponding discrete-time shared state system. The proof technique extends to the class of systems in which an agent's state evolves continuously over time. The proof technique has been formalized in the PVS interface for timed I/O automata and applied to verify convergence of a mobile agent pattern formation algorithm. |
|||||

BibTeX:
@inproceedings{MC:FORMATS08, author = {K. Mani Chandy and Sayan Mitra and Concetta Pilotto}, title = {Convergence Verification: From Shared Memory to Partially Synchronous Systems}, booktitle = {Formal Modeling and Analysis of Timed Systems (FORMATS`08)}, publisher = {Springer Verlag}, year = {2008}, volume = {5215}, pages = {217--231}, url = {http://www.springerlink.com/content/f2lx31113444n520/} } |
|||||

Mitra, S. and Chandy, K.M. | A Formalized Theory for Verifying Stability and Convergence of Automata in PVS | 2008 | Theorem Proving in Higher Order Logics (TPHOLS 2008), pp. 230-245 | ||

Abstract: Correctness of many hybrid and distributed systems require stability and convergence guarantees. Unlike the standard induction principle for verifying invariance, a theory for verifying stability or convergence of automata is currently not available. In this paper, we formalize one such theory proposed by Tsitsiklis.We build on the existing PVS metatheory for untimed, timed, and hybrid input/output automata, and incorporate the concepts about fairness, stability, Lyapunov-like functions, and convergence. The resulting theory provides two sets of sufficient conditions, which when instantiated and verified for particular automata, guarantee convergence and stability, respectively. |
|||||

BibTeX:
@inproceedings{MC:TPHOLS08, author = {Sayan Mitra and K. Mani Chandy}, title = {A Formalized Theory for Verifying Stability and Convergence of Automata in PVS}, booktitle = {Theorem Proving in Higher Order Logics (TPHOLS 2008)}, publisher = {LNCS}, year = {2008}, pages = {230--245}, url = {http://www.springerlink.com/content/57175hhg02702578/} } |
|||||

Mitra, S., Liberzon, D. and Lynch, N. | Verifying Average Dwell Time of Hybrid Systems | 2008 | ACM Transactions on Embedded Computing Systems Vol. 8 |
||

Abstract: Average dwell time (ADT) properties characterize the rate at which a hybrid system performs mode switches. In this article, we present a set of techniques for verifying ADT properties. The stability of a hybrid system A can be verified by combining these techniques with standard methods for checking stability of the individual modes of A. We introduce a new type of simulation relation for hybrid automataï¿½switching simulationï¿½for establishing that a given automaton A switches more rapidly than another automaton B. We show that the question of whether a given hybrid automaton has ADT ta can be answered either by checking an invariant or by solving an optimization problem. For classes of hybrid automata for which invariants can be checked automatically, the invariant-based method yields an automatic method for verifying ADT; for automata that are outside this class, the invariant has to be checked using inductive techniques. The optimization-based method is automatic and is applicable to a restricted class of initialized hybrid automata. A solution of the optimization problem either gives a counterexample execution that violates the ADT property, or it confirms that the automaton indeed satisfies the property. The optimization and the invariant-based methods can be used in combination to find the unknown ADT of a given hybrid automaton. |
|||||

BibTeX:
@article{MLL:TECS08, author = {Sayan Mitra and Daniel Liberzon and Nancy Lynch}, title = {Verifying Average Dwell Time of Hybrid Systems}, journal = {ACM Transactions on Embedded Computing Systems}, publisher = {ACM}, year = {2008}, volume = {8}, url = {http://portal.acm.org/citation.cfm?id=1457246.1457249&coll=portal&dl=ACM&idx=J840&part=transaction&WantType=Transactions&title=ACM%20Transactions%20on%20Embedded%20Computing%20Systems%20(TECS)} } |
|||||

Grosu, R., Mitra, S., Ye, P., Entcheva, E., Ramakrishnan, I.V. and Smolka, S.A. | Learning Cycle-Linear Hybrid Automata for Excitable Cells. | 2007 | Hybrid Systems: Computation and Control (HSCC 2007), pp. 245-258 | ||

Abstract: We show how to automatically learn the class of Hybrid Automata called Cycle-Linear Hybrid Automata (CLHA) in order to model the behavior of excitable cells. Such cells, whose main purpose is to amplify and propagate an electrical signal known as the action potential (AP), serve as the biologic transistors of living organisms. The learning algorithm we propose comprises the following three phases: (1) Geometric analysis of the APs in the training set is used to identify, for each AP, the modes and switching logic of the corresponding Linear Hybrid Automata. (2) For each mode, the modified Prony's method is used to learn the coefficients of the associated linear flows. (3) The modified Prony's method is used again to learn the functions that adjust, on a per-cycle basis, the mode dynamics and switching logic of the Linear Hybrid Automata obtained in the first two phases. Our results show that the learned CLHA is able to successfully capture AP morphology and other important excitable-cell properties, such as refractoriness and restitution, up to a prescribed approximation error. Our approach is fully implemented in MATLAB and, to the best of our knowledge, provides the most accurate approximation model for ECs to date. |
|||||

BibTeX:
@inproceedings{GrosuM07, author = {Radu Grosu and Sayan Mitra and Pei Ye and Emilia Entcheva and I. V. Ramakrishnan and Scott A. Smolka}, title = {Learning Cycle-Linear Hybrid Automata for Excitable Cells.}, booktitle = {Hybrid Systems: Computation and Control (HSCC 2007)}, year = {2007}, pages = {245-258}, url = {http://www.springerlink.com/content/ft80kx37733m1486/?p=ce29728d55dd44c880214a36bcbadf70&pi=20} } |
|||||

Mitra, S. | A Verification Framework for Hybrid Systems | 2007 | School: Massachusetts Institute of Technology |
||

BibTeX:
@phdthesis{Mitra07PhD, author = {Sayan Mitra}, title = {A Verification Framework for Hybrid Systems}, school = {Massachusetts Institute of Technology}, year = {2007}, url = {http://dspace.mit.edu/handle/1721.1/42238} } |
|||||

Mitra, S. and Lynch, N. | Proving approximate implementation relations for Probabilistic I/O Automata. | 2007 | Electronic Notes in Theoretical Computer Science Vol. 174(8), pp. 71-93 |
||

Abstract: In this paper we introduce the notion of approximate implementations for Probabilistic I/O Automata (PIOA) and develop methods for proving such relationships. We employ a task structure on the locally controlled actions and a task scheduler to resolve nondeterminism. The interaction between a scheduler and an automaton gives rise to a trace distributionï¿½a probability distribution over the set of traces. We define a PIOA to be a (discounted) approximate implementation of another PIOA if the set of trace distributions produced by the first is close to that of the latter, where closeness is measured by the (resp. discounted) uniform metric over trace distributions. We propose simulation functions for proving approximate implementations corresponding to each of the above types of approximate implementation relations. Since our notion of similarity of traces is based on a metric on trace distributions, we do not require the state spaces nor the space of external actions of the automata to be metric spaces. We discuss applications of approximate implementations to verification of probabilistic safety and termination. |
|||||

BibTeX:
@article{ML:ENTCS07, author = {Sayan Mitra and Nancy Lynch}, title = {Proving approximate implementation relations for Probabilistic I/O Automata.}, journal = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier Science Publishers B. V.}, year = {2007}, volume = {174}, number = {8}, pages = {71-93}, url = {http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B75H1-4NX9C9N-7&_user=571676&_rdoc=1&_fmt=&_orig=search&_sort=d&view=c&_acct=C000029040&_version=1&_urlVersion=0&_userid=571676&md5=0a0e5c131ecbe451e5f66a10be9bfdc2}, doi = {http://dx.doi.org/10.1016/j.entcs.2006.11.040} } |
|||||

Mitra, S. and Lynch, N. | Trace-based Semantics for Probabilistic Timed I/O Automata | 2007 | Hybrid Systems: Computation and Control (HSCC 2007), pp. 718-722 | ||

Abstract: We describe the main features of the Probabilistic Timed I/O Automata (PTIOA)ï¿½a framework for modeling and analyzing discretely communicating probabilistic hybrid systems. A PTIOA can choose the post-state of a discrete transition either nondeterministically or according to (possibly continuous) probability distributions. The framework supports modeling of large systems as compositions of concurrently executing PTIOAs, which interact through shared transition labels. We develop a trace-based semantics for PTIOAs and show that PTIOAs are compositional with respect a new notion of external behavior. |
|||||

BibTeX:
@inproceedings{ML:HSCC07, author = {Sayan Mitra and Nancy Lynch}, title = {Trace-based Semantics for Probabilistic Timed I/O Automata}, booktitle = {Hybrid Systems: Computation and Control (HSCC 2007)}, year = {2007}, pages = {718--722}, url = {http://www.springerlink.com/content/4r07k692617666u0/} } |
|||||

Archer, M., Lim, H., Lynch, N., Mitra, S. and Umeno, S. | Specifying and Proving Properties of Timed I/O Automata in the TIOA Toolkit | 2006 | In Fourth ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'06) | ||

Abstract: Timed I/O Automata (TIOA) is a mathematical framework for modeling and verification of distributed systems that involve discrete and continuous dynamics. TIOA can be used for example, to model a real-time software component controlling a physical process. The TIOA model is sufficiently general to subsume other models in use for timed systems. The TIOA toolkit, currently under development, is aimed at supporting system development based on TIOA specifications. The TIOA toolkit is an extension of the IOA toolkit, which provides a specification simulator, code generator, and both model checking and theorem proving support for analyzing specifications. This paper focuses on modeling of timed systems with TIOA and the TAMEbased theorem proving support provided in the TIOA toolkit for proving system properties, including timing properties. Several examples are provided by way of illustration. |
|||||

BibTeX:
@inproceedings{ALLMU:memocode06, author = {Myla Archer and Hongping Lim and Nancy Lynch and Sayan Mitra and Shinya Umeno}, title = { Specifying and Proving Properties of Timed I/O Automata in the TIOA Toolkit }, booktitle = {In Fourth ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'06)}, publisher = {IEEE}, year = {2006}, url = {http://ieeexplore.ieee.org/search/wrapper.jsp?arnumber=1695916} } |
|||||

Mitra, S. and Lynch, N. | Approximate simulations for task-structured probabilistic I/O automata | 2006 | LICS workshop on Probabilistic Automata and Logics (PAul06) | ||

Abstract: A Probabilistic I/O Automaton (PIOA) is a countable-state automaton model that allows nondeterministic and probabilistic choices in state transitions. A task-PIOA adds a task structure on the locally controlled actions of a PIOA as a means for restricting the nondeterminism in the model. The task-PIOA framework defines exact implementation relations based on inclusion of sets of trace distributions. In this paper we develop the theory of approximate implementations and equivalences for task-PIOAs. We propose a new kind of approximate simulation between task-PIOAs and prove that it is sound with respect to approximate implementations. Our notion of similarity of traces is based on a metric on trace distributions and therefore, we do not require the state spaces nor the space of external actions (output alphabet) of the underlying automata to be metric spaces. We discuss applications of approximate implementations to probabilistic safety verification. |
|||||

BibTeX:
@inproceedings{ML:paul06, author = {Sayan Mitra and Nancy Lynch}, title = { Approximate simulations for task-structured probabilistic I/O automata}, booktitle = { LICS workshop on Probabilistic Automata and Logics (PAul06)}, year = {2006}, url = {http://theory.lcs.mit.edu/~mitras/research/PAul06-final.pdf} } |
|||||

Mitra, S., Liberzon, D. and Lynch, N. | Verifying Average Dwell Time by Solving Optimization Problems | 2006 | Proceedings of Hybrid Systems: Computation and Control (HSCC 2006), pp. 476-490 | ||

Abstract: In the switched system model, discrete mechanisms of a hybrid system are abstracted away in terms of an exogenous switching signal which brings about the mode switches. The Average Dwell time (ADT) property defines restricted classes of switching signals which provide sufficient conditions for proving stability of switched systems. In this paper, we use a specialization of the Hybrid I/O Automaton model to capture both the discrete and the continuous mechanisms of hybrid systems. Based on this model, we develop methods for automatically verifying ADT properties and present simulation relations for establishing equivalence of hybrid systems with respect to ADT. Given a candidate ADT for a hybrid system, we formulate an optimization problem; a solution of this problem either establishes the ADT property or gives an execution fragment of the system that violates it. For two special classes of hybrid systems, we show that the corresponding optimization problems can be solved using standard mathematical programming techniques.We formally define equivalence of two hybrid systems with respect to ADT and present a simulation relation-based method for proving this equivalence. The proposed methods are applied to verify ADT properties of a linear hysteresis switch and a nondeterministic thermostat. |
|||||

BibTeX:
@inproceedings{MLL:hscc06, author = {Sayan Mitra and Daniel Liberzon and Nancy Lynch}, title = {Verifying Average Dwell Time by Solving Optimization Problems}, booktitle = {Proceedings of Hybrid Systems: Computation and Control (HSCC 2006)}, year = {2006}, pages = {476-490}, url = {http://www.springerlink.com/content/x77vn1444121k38r/} } |
|||||

Chockler, G., Lynch, N., Mitra, S. and Tauber, J. | Proving atomicity: an assertional approach | 2005 | Vol. 3724Proceedings of Nineteenth International Symposium on Distributed Computing (DISC'05), pp. 152 - 168 |
||

Abstract: Atomicity (or linearizability) is a commonly used consistency criterion for distributed services and objects. Although atomic object implementations are abundant, proving that algorithms achieve atomicity has turned out to be a challenging problem. In this paper, we initiate the study of systematic ways of verifying distributed implementations of atomic objects, beginning with read/write objects (registers). Our general approach is to replace the existing operational reasoning about events and partial orders with assertional reasoning about invariants and simulation relations. To this end, we define an abstract state machine that captures the atomicity property and prove correctness of the object implementations by establishing a simulation mapping between the implementation and the specification automata. We demonstrate the generality of our specification by showing that it is implemented by three different read/write register constructions: the message-passing register emulation of Attiya, Bar-Noy and Dolev, its optimized version based on real time, and the shared memory register construction of Vitanyi and Awerbuch. In addition, we show that a simplified version of our specification is implemented by a general atomic object construction based on the Lamportï¿½s replicated state machine algorithm. |
|||||

BibTeX:
@inproceedings{CLMT:disc05, author = {Gregory Chockler and Nancy Lynch and Sayan Mitra and Joshua Tauber}, title = { Proving atomicity: an assertional approach}, booktitle = {Proceedings of Nineteenth International Symposium on Distributed Computing (DISC'05)}, publisher = {Springer}, year = {2005}, volume = { 3724}, pages = {152 - 168}, url = {http://www.springerlink.com/content/1wk299f2vemb15yj/} } |
|||||

Lim, H., Kaynar, D., Lynch, N. and Mitra, S. | Translating timed I/O automata specifications for theorem proving in PVS | 2005 | (3829)Proceedings of Formal Modelling and Analysis of Timed Systems (FORMATS'05) | ||

Abstract: Timed Input/Output Automaton (TIOA) is a mathematical framework for specification and analysis of systems that involve discrete and continuous evolution. In order to employ an interactive theorem prover in deducing properties of a TIOA, its state-transition based description has to be translated to the language of the theorem prover. In this paper, we describe a tool for translating TIOA to the language of the Prototype Verification System (PVS)---a specification system with an integrated interactive theorem prover. We describe the translation scheme, discuss the design decisions, and briefly present three case studies to illustrate the application the the translator in the verification process. |
|||||

BibTeX:
@inproceedings{LKLM:formats05, author = {Hongping Lim and Dilsun Kaynar and Nancy Lynch and Sayan Mitra}, title = {Translating timed I/O automata specifications for theorem proving in PVS}, booktitle = {Proceedings of Formal Modelling and Analysis of Timed Systems (FORMATS'05)}, publisher = {Springer}, year = {2005}, number = {3829}, url = {http://www.springerlink.com/content/f715l136524q6527/} } |
|||||

Leong, B., Mitra, S. and Liskov, B. | Path vector face routing: Geographic routing with local face information | 2005 | Proceedings of 13th IEEE International Conference on Network Protocols (ICNP'05) | ||

Abstract: Existing geographic routing algorithms depend on the planarization of the network connectivity graph for correctness, and the planarization process gives rise to a well-defined notion of faces. In this paper, we demonstrate that we can improve routing performance by storing a small amount of local face information at each node. We present a protocol, Path Vector Exchange Protocol (PVEX), that maintains local face information at each node efficiently, and a new geographic routing algorithm, Greedy Path Vector Face Routing (GPVFR), that achieves better routing performance in terms of both path stretch and hop stretch than existing geographic routing algorithms by exploiting available local face information. Our simulations demonstrate that GPVFR/PVEX achieves significantly reduced path and hop stretch than Greedy Perimeter Stateless Routing (GPSR) and somewhat better performance than Greedy Other Adaptive Face Routing (GOAFR+) over a wide range of network topologies. The cost of this improved performance is a small amount of additional storage, and the bandwidth required for our algorithm is comparable to GPSR and GOAFR+ in quasi-static networks. |
|||||

BibTeX:
@inproceedings{LML:icnp05, author = {Ben Leong and Sayan Mitra and Barbara Liskov}, title = {Path vector face routing: Geographic routing with local face information}, booktitle = { Proceedings of 13th IEEE International Conference on Network Protocols (ICNP'05)}, year = {2005}, url = {http://www2.computer.org/portal/web/csdl/doi/10.1109/ICNP.2005.32} } |
|||||

Lynch, N., Mitra, S. and Nolte, T. | Motion coordination using virtual nodes | 2005 | Proceedings of 44th IEEE Conference on Decision and Control (CDC05) | ||

Abstract: We describe how a virtual node abstraction layer can be used to coordinate the motion of real mobile nodes in a region of 2-space. In particular, we consider how nodes in a mobile ad hoc network can arrange themselves along a predetermined curve in the plane, and can maintain themselves in such a configuration in the presence of changes in the underlying mobile ad hoc network, specifically, when nodes may join or leave the system or may fail. Our strategy is to allow the mobile nodes to implement a virtual layer consisting of mobile client nodes, stationary Virtual Nodes (VNs) at predetermined locations in the plane, and local broadcast communication. The VNs coordinate among themselves to distribute the client nodes relatively evenly among the VNs' regions, and each VN directs its local client nodes to form themselves into the local portion of the target curve. |
|||||

BibTeX:
@inproceedings{LMN:cdc05, author = {Nancy Lynch and Sayan Mitra and Tina Nolte}, title = {Motion coordination using virtual nodes}, booktitle = { Proceedings of 44th IEEE Conference on Decision and Control (CDC05)}, publisher = {IEEE}, year = {2005} } |
|||||

Mitra, S. and Archer, M. | PVS Strategies for Proving Abstraction Properties of Automata. | 2005 | Electronic Notes in Theoretical Computer Science Vol. 125(2), pp. 45-65 |
||

Abstract: Abstractions are important in specifying and proving properties of complex systems. To prove that a given automaton implements an abstract specification automaton, one must first and the correct abstraction relation between the states of the automata, and then show that this relation is preserved by all corresponding action sequences of the two automata. This paper describes tool support based on the PVS theorem prover that can help users accomplish the second task: proving a candidate abstraction relation correct. This tool support relies on a clean and uniform technique for defining abstraction properties relating automata that uses library theories for defining abstraction relations and templates for specifying automata and abstraction theorems. The paper then describes how the templates and theories allow development of generic, high level PVS strategies that aid in the mechanization of abstraction proofs. These strategies first set up the standard subgoals for the abstraction proofs and then execute the standard initial proof steps for these subgoals, thus making the process of proving abstraction properties in PVS more automated. With suitable supplementary strategies to implement the natural proof steps needed to complete the proofs of any of the standard subgoals remaining to be proved, the abstraction proof strategies can form part of a set of mechanized proof steps that can be used interactively to translate high level proof sketches into PVS proofs. Using timed I/O automata examples taken from the literature, this paper illustrates use of the templates, theories, and strategies described to specify and prove two types of abstraction property: refinement and forward simulation. |
|||||

BibTeX:
@article{MitraA05, author = {Sayan Mitra and Myla Archer}, title = {PVS Strategies for Proving Abstraction Properties of Automata.}, journal = {Electronic Notes in Theoretical Computer Science}, year = {2005}, volume = {125}, number = {2}, pages = {45-65}, url = {http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B75H1-4FNNN9F-B&_user=571676&_rdoc=1&_fmt=&_orig=search&_sort=d&view=c&_acct=C000029040&_version=1&_urlVersion=0&_userid=571676&md5=6d6175f909435af03f0b9704d27a78a4} } |
|||||

Mitra, S. and Liberzon, D. | Stability of hybrid automata with average dwell time: an invariant approach | 2005 | Proceedings of the 43rd IEEE Conference on Decision and Control | ||

Abstract: A formal method based technique is presented for proving the average dwell time property of a hybrid system, which is useful for establishing stability under slow switching. The Hybrid Input/Output Automaton (HIOA) of is used as the model for hybrid systems, and it is shown that some known stability theorems from system theory can be adapted to be applied in this framework. The average dwell time property of a given automaton is formalized as an invariant of a corresponding transformed automaton, such that the former has average dwell time if and only if the latter satisfies the invariant. Formal verification techniques can be used to check this invariance property. In particular, the HIOA framework facilitates inductive invariant proofs by systematically breaking them down into cases for the discrete actions and continuous trajectories of the automaton. The invariant approach to proving the average dwell time property is illustrated by analyzing the hysteresis switching logic unit of a supervisory control system. |
|||||

BibTeX:
@inproceedings{ML:CDC04, author = {Sayan Mitra and Daniel Liberzon}, title = {Stability of hybrid automata with average dwell time: an invariant approach}, booktitle = {Proceedings of the 43rd IEEE Conference on Decision and Control}, year = {2005}, url = {http://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=01430238} } |
|||||

Kaynar, D., Lynch, N. and Mitra, S. | Specifying and Proving Timing Properties with TIOA Tools | 2004 | In the work in progress session of the 25th IEEE International Real-Time Systems Symposium (RTSS-WIP) | ||

BibTeX:
@inproceedings{KLM04, author = {Dilsun Kaynar and Nancy Lynch and Sayan Mitra}, title = {Specifying and Proving Timing Properties with TIOA Tools}, booktitle = {In the work in progress session of the 25th IEEE International Real-Time Systems Symposium (RTSS-WIP)}, year = {2004} } |
|||||

Mitra, S. and Archer, M. | Reusable PVS Proof Strategies for Proving Abstraction Properties of I/O Automata | 2004 | STRATEGIES 2004, IJCAR Workshop on strategies in automated deduction | ||

BibTeX:
@inproceedings{MA04strat, author = {Sayan Mitra and Myla Archer}, title = {Reusable PVS Proof Strategies for Proving Abstraction Properties of I/O Automata}, booktitle = {STRATEGIES 2004, IJCAR Workshop on strategies in automated deduction}, year = {2004} } |
|||||

Mitra, S. and Rabek, J. | Energy efficient connected clusters for mobile ad hoc networks | 2004 | Proceedings of 3rd Annual Mediterranean Ad Hoc Networking Workshop (MED-HOC-NET'04) | ||

Abstract: We propose a power-efficient clustering algorithm for wireless ad hoc networks. This algorithm controls the broadcast power of the nodes in such a way that the resulting network is guaranteed to be connected, clustered, and uses minimum required power for achieving that. |
|||||

BibTeX:
@inproceedings{MitraR:MEDHOC04, author = {Sayan Mitra and Jesse Rabek}, title = {Energy efficient connected clusters for mobile ad hoc networks}, booktitle = {Proceedings of 3rd Annual Mediterranean Ad Hoc Networking Workshop (MED-HOC-NET'04)}, year = {2004} } |
|||||

Mitra, S. and Archer, M. | Developing Strategies for Specialized Theorem Proving about Untimes, Timed, and Hybrid I/O Automata | 2003 | STRATA 2003 | ||

BibTeX:
@inproceedings{MA03PVS, author = {Sayan Mitra and Myla Archer}, title = {Developing Strategies for Specialized Theorem Proving about Untimes, Timed, and Hybrid I/O Automata}, booktitle = {STRATA 2003}, year = {2003} } |
|||||

Mitra, S., Wang, Y., Lynch, N. and Feron, E. | Safety Verification of Model Helicopter Controller using Hybrid Input/Output Automata | 2003 | 6th International Workshop on Hybrid Systems: Computation and Control (HSCC 2003), pp. 343-358 | ||

Abstract: This paper presents an application of the Hybrid Input/Output Automaton (HIOA) framework in verifying a realistic hybrid system. A supervisory pitch controller for a model helicopter system is designed and then verified. The design of the supervisory controller is limited by actuator bandwidth, sensor inaccuracies, and the sampling rates. Verification is carried out by induction over the length of an execution of the composed system. The HIOA model makes the inductive proofs tractable by decomposing them into independent discrete and continuous parts. The paper also presents language constructs for specifying HIOAs. |
|||||

BibTeX:
@inproceedings{MWLF-hscc03, author = {Sayan Mitra and Yong Wang and Nancy Lynch and Eric Feron}, title = {Safety Verification of Model Helicopter Controller using Hybrid Input/Output Automata}, booktitle = {6th International Workshop on Hybrid Systems: Computation and Control (HSCC 2003)}, year = {2003}, pages = {343-358}, url = {http://www.springerlink.com/content/9vlmduh36103d221/} } |
|||||

Mitra, S. | HIOA - A Specification Language for Hybrid Input/Output Automata | 2001 | School: Department of Computer Science and Automation, IISc |
||

BibTeX:
@mastersthesis{mitra01masters, author = {Sayan Mitra}, title = {HIOA - A Specification Language for Hybrid Input/Output Automata}, school = {Department of Computer Science and Automation, IISc}, year = {2001}, url = {research/mastersthesis.ps.gz} } |