| Wongpiromsarn T, Mitra S, Murray R and Lamperski A (2009), "Periodically Controlled Hybrid Systems: Verifying A Controller for An Autonomous Vehicle", In 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}
}
|
| Gilbert S, Lynch N, Mitra S and Nolte T (2008), "Self-stabilizing Mobile Robot Formations with Virtual Nodes", In 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/}
}
|
| Grosu R, Mitra S, Ye P, Entcheva E, Ramakrishnan IV and Smolka SA (2007), "Learning Cycle-Linear Hybrid Automata for Excitable Cells.", In 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, Liberzon D and Lynch N (2006), "Verifying Average Dwell Time by Solving Optimization Problems", In 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/}
}
|
| Mitra S, Wang Y, Lynch N and Feron E (2003), "Safety Verification of Model Helicopter Controller using Hybrid Input/Output Automata", In 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/}
}
|
| Qi B (2018), "Building DryVR: A Verification and Controller Synthesis Engine for Cyber-Physical Systems and Safety-Critical Autonomous Vehicle Features". Thesis at: University of Illinois as Urbana-Champaign., May, 2018.
[BibTeX] |
BibTeX:
@mastersthesis{BolunMasters,
author = {Bolun Qi},
title = {Building DryVR: A Verification and Controller Synthesis Engine for Cyber-Physical Systems and Safety-Critical Autonomous Vehicle Features},
school = {University of Illinois as Urbana-Champaign},
year = {2018}
}
|
| Fan C, Huang Z and Mitra S (2018), "Approximate Partial Order Reduction", In proceedings of 22nd International Symposium on Formal Methods (FM). |
| Abstract: We present a new partial order reduction method for reachability analysis of nondeterministic labeled transition systems over metric spaces. Nondeterminism arises from both the choice of the initial state and the choice of actions, and the number of executions to be explored grows exponentially with their length. We introduce a notion of independence relation over actions that relates approximately commutative actions; equivalent action sequences are obtained by swapping "-independent consecutive action pairs. Our reachability algorithm generalizes individual executions to cover sets of executions that start from different, but close initial states, and follow different, but independent, action sequences. The constructed over-approximations can be made arbitrarily precise by reducing δ and epsilon. Exploiting both the continuity of actions and their approximate independence, the algorithm can yield an exponential reduction in the number of executions explored. We illustrate this with experiments on consensus, platooning, and distributed control examples. |
BibTeX:
@inproceedings{FanHM:approxPOR,
author = {Chuchu Fan and Zhenqi Huang and Sayan Mitra},
title = {Approximate Partial Order Reduction},
booktitle = {proceedings of 22nd International Symposium on Formal Methods (FM)},
year = {2018}
}
|
| Fan C, Meng Y, Maier J, Bartocci E, Mitra S and Schmid U (2018), "A technique for verifying nonlinear analog and mixed-signal circuits with inputs", In proceedings of ADHS. |
| Abstract: There has been progress in verification of nonlinear and hybrid systems in the recent years using algorithms that combine simulation data with model-based sensitivity analysis. These approaches only handle closed models, that is, models without inputs. The naïve introduction of models of input signals breaks these approaches, as typical inputs (fast sigmoids, discontinuous functions) for analog and mixed-signal circuits make the system highly sensitive and the number of needed simulations grow rapidly. In this paper, we present a new technique for verifying nonlinear and hybrid circuit models with inputs. A key result in the paper shows that once an input signal is fixed, the sensitivity analysis of the model can be performed much more precisely. Based on this observation, we extend a discrepancy-based verification algorithm and apply it to a suite of nonlinear and hybrid models of CMOS digital circuits under different input signals. The models are low-dimensional but involve highly nonlinear ODEs, with nearly hundreds of logarithmic and exponential terms, and therefore, have challenged existing verification approaches and tools. Our implementation of the new algorithm is able to verify these models; some of our experiments analyze the metastability of bistable circuits, which involve very sensitive ODEs. Our results not only demonstrate the feasibility of our approach but also provided interesting insights like the close connection between metastability recovery time and sensitivity. |
BibTeX:
@inproceedings{FanM:ADHS2018,
author = {Chuchu Fan and Yu Meng and Jürgen Maier and Ezio Bartocci and Sayan Mitra and Ulrich Schmid},
title = {A technique for verifying nonlinear analog and mixed-signal circuits with inputs},
booktitle = {proceedings of ADHS},
year = {2018}
}
|
| Fan C, Mathur U, Mitra S and Viswanathan M (2018), "Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics", In proceedings of 30th International Conference on Computer Aided Verification (CAV). |
| Abstract: We address the problem of synthesizing provably correct controllers for linear systems with reach-avoid specifications. Our solution uses a combination of an open-loop controller and a tracking controller, thereby reducing the problem to smaller tractable problems. We show that, once a tracking controller is fixed, the reachable states from an initial neighborhood, subject to any disturbance, can be over-approximated by a sequence of ellipsoids, with sizes that are independent of the open-loop controller. Hence, the open-loop controller can be synthesized independently to meet the reach-avoid specification for an initial neighborhood. Exploiting several techniques for tightening the over-approximations, we reduce the open-loop controller synthesis problem to satisfiability over quantifier-free linear real arithmetic. The overall synthesis algorithm, computes a tracking controller, and then iteratively covers the entire initial set to find open-loop controllers for initial neighborhoods. The algorithm is sound and, for a class of robust systems, is also complete. We present tool, a tool implementing this synthesis algorithm, and we show that it scales to several high-dimensional systems with complex reach-avoid specifications. |
BibTeX:
@inproceedings{FanM:ADHS2018,
author = {Chuchu Fan and Umang Mathur and Sayan Mitra and Mahesh Viswanathan},
title = {Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics},
booktitle = {proceedings of 30th International Conference on Computer Aided Verification (CAV)},
year = {2018}
}
|
| Huang Z, Etigowni S, Zonouz S and Mitra S (2018), "Algorithmic Attack Synthesis using Hybrid Dynamics of Power Grid Critical Infrastructures", In proceedings of IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). |
| Abstract: Automated vulnerability assessment and exploit generation for computing systems have been explored for decades. However, these approaches are incomplete in assessing industrial control systems, where networks of computing devices and physical processes interact for safety-critical missions. We present1 an attack synthesis algorithm against such cyber-physical electricity grids. The algorithm explores both discrete network configurations and continuous dynamics of the plant?s embedded control system, to search for attack strategies that evade detection with conventional monitors. The algorithm enabling this exploration is rooted in recent developments in the hybrid system verification research: it effectively approximates the behavior of the system for a set of possible attacks by computing sensitivity of the system?s response to variations in the attack parameters. For parts of the attack space, the proposed algorithm can infer whether or not there exists a feasible attack that avoids triggering protection measures such as relays and steady-state monitors. The algorithm can take into account constraints on the attack space such as the power system topology and the set of controllers across the plant that can be compromised without detection. With a proof-of-concept prototype, we demonstrate the synthesis of transient attacks in several typical electricity grids and analyze the robustness of the synthesized attacks to perturbations in the network parameters. |
BibTeX:
@inproceedings{Huang:DSN2018,
author = {Zhenqi Huang and Sriharsha Etigowni and Saman Zonouz and Sayan Mitra},
title = {Algorithmic Attack Synthesis using Hybrid Dynamics of Power Grid Critical Infrastructures},
booktitle = {proceedings of IEEE/IFIP International Conference on Dependable Systems and Networks (DSN)},
year = {2018}
}
|
| Liberzon D and Mitra S (2018), "Entropy and minimal bit rates for state estimation and model detection", IEEE Transactions on Automatic Control (TAC). IEEE. |
| Abstract: We study a notion of estimation entropy for continuous-time nonlinear systems, formulated in terms of the number of system trajectories that approximate all other trajectories up to an exponentially decaying error. We also consider an alternative definition of estimation entropy which uses approximating functions that are not necessarily trajectories of the system, and show that the two entropy notions are equivalent. We establish an upper bound on the estimation entropy in terms of the sum of the desired convergence rate and an upper bound on the matrix measure of the Jacobian, multiplied by the system dimension. A lower bound on the estimation entropy is developed as well. We then turn our attention to state estimation and model detection with quantized and sampled state measurements. We describe an iterative procedure that uses such 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, and no other algorithm of this type can perform the same estimation task with bit rates lower than the estimation entropy. Finally, we discuss 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 always happens in finite time. |
BibTeX:
@article{LM:TAC2017,
author = {Daniel Liberzon and Sayan Mitra},
title = {Entropy and minimal bit rates for state estimation and model detection},
journal = {IEEE Transactions on Automatic Control (TAC)},
publisher = {IEEE},
year = {2018},
url = {http://ieeexplore.ieee.org/document/8186184/},
doi = {10.1109/TAC.2017.2782478}
}
|
| Chan N (2018), "Design and Verification of a Safe Autonomous Satellite Rendezvous Maneuver". Thesis at: University of Illinois as Urbana-Champaign., May, 2018. |
| Abstract: A fundamental maneuver in autonomous space operations is known as rendezvous, where an active spacecraft navigates towards and maneuvers within close-proximity of a free-flying passive spacecraft. Any mistake during autonomous space flight can be extremely costly, yet these systems are difficult to verify due to limitations of testing spacecraft. In this thesis, we present a benchmark model formulation for the rendezvous mission, two control solutions to achieve this mission, and a rigorous method to demonstrate that the resulting system?s behavior remains safe. The benchmark model provides both a nonlinear description of the spacecraft?s motion and a linearized approximation, and the mission objectives, or equivalently, our set of safety properties. The control solutions include a hybrid, or switched, version of linear quadratic regulator (LQR)?a fundamental result in the theory of optimal control for linear systems. We formulate a novel hybrid controller, dubbed state-dependent linear quadratic (SDLQ) control, which extends the former controller in a way that may improve its ability to generate only safe trajectories. With these choices of dynamical models and controllers, we obtain a collection of models that are shown to robustly achieve safety properties of interest using a suite of hybrid verification tools. We utilize several existing tools, each developed for different classes of hybrid models, and we implement a new tool called SDVTool which improves upon one of the former tools. We present experimental results that illustrate the promise (and ongoing challenges) of this approach, given this select number of models, safety requirements, and verification techniques. We will demonstrate both successful, safe scenarios and incomplete or unsafe examples. |
BibTeX:
@mastersthesis{NicoleMasters,
author = {Nicole Chan},
title = {Design and Verification of a Safe Autonomous Satellite Rendezvous Maneuver},
school = {University of Illinois as Urbana-Champaign},
year = {2018}
}
|
| Potok M, Chen C-Y, Mitra S and Mohan S (2018), "SDCWorks: A Formal Framework for Software Defined Control of Smart Manufacturing Systems", In International Conference on Cyberphysical Systems (ICCPS 2018). |
| Abstract: Discrete manufacturing systems are complex cyberphysical systems (CPS) and their availability, performance, and quality have a big impact on the economy. Smart manufacturing promises to improve these aspects. One key approach that is being pursued in this context is the creation of centralized software defined control (SDC) architectures and strategies that use diverse sensors and data sources to make manufacturing more adaptive, resilient, and programmable. In this paper, we present the SDCWorks?the modeling and simulation framework for SDC. It consists of the semantic structures for creating models, a baseline controller, and an open source implementation of a discrete event simulator for SDCWorks models. We provide the semantics of such a manufacturing system in terms of a discrete transition system which sets up the platform for future research in a new class of problems in formal verification, synthesis, and monitoring. We illustrate the expressive power of SDCWorks by modeling the realistic SMART manufacturing testbed of University of Michigan. We show how our open source the SDCWorks simulator can be used to evaluate relevant metrics (throughput, latency, and load) for example manufacturing systems. |
BibTeX:
@inproceedings{PotokCMM:ICCPS2018,
author = {Matthew Potok and Chien-Ying Chen and Sayan Mitra and Sibin Mohan},
title = {SDCWorks: A Formal Framework for Software Defined Control of Smart Manufacturing Systems},
booktitle = {International Conference on Cyberphysical Systems (ICCPS 2018)},
year = {2018},
url = {https://dl.acm.org/citation.cfm?id=3207896.3207907}
}
|
| Sibai H and Mitra S (2018), "State Estimation for Dynamical Systems with Unknown Inputs: Entropy and Bit Rates", In Hybrid Systems: Computation and Control (HSCC 2018), Porto, Portugal.. |
| Abstract: Finding the minimal bit rate needed for state estimation of a dynamical system is a fundamental problem in control theory. In this paper, we present a notion of topological entropy, to lower bound the bit rate necessary for estimating the state of a nonlinear dynamical system, with unknown bounded inputs, up to a constant error. Since the actual value of entropy is hard to compute in general, we compute an upper bound. We show that as the bound on the input decreases, we recover a previously known bound on estimation entropy ? a similar notion of entropy ? for nonlinear systems without inputs. For the sake of computing the bound, we present an algorithm that, given sampled and quantized measurements from a trajectory and an input signal, constructs a corresponding approximation. This algorithm can also be used for state estimation if the input signal can indeed be sensed in addition to the state. Finally, we present an improved bound for systems with linear inputs. |
BibTeX:
@inproceedings{SibaiM:HSCC2018,
author = {Hussein Sibai and Sayan Mitra},
title = {State Estimation for Dynamical Systems with Unknown Inputs: Entropy and Bit Rates},
booktitle = {Hybrid Systems: Computation and Control (HSCC 2018), Porto, Portugal.},
year = {2018},
url = {https://dl.acm.org/citation.cfm?id=3178126.3187002}
}
|
| Chan N and Mitra S (2017), "Verifying safety of an autonomous spacecraft rendezvous mission", In ARCH17. 4th International Workshop on Applied Verification of Continuous and Hybrid Systems, collocated with Cyber-Physical Systems Week (CPSWeek) on April 17, 2017 in Pittsburgh, PA, USA. , pp. 20-32. |
| Abstract: A fundamental maneuver in autonomous space operations is known as rendezvous, where a spacecraft navigates to and approaches another spacecraft. In this case study, we present linear and nonlinear benchmark models of an active chaser spacecraft performing rendezvous toward a passive, orbiting target. The system is modeled as a hybrid automaton, where the chaser must adhere to different sets of constraints in each discrete mode. A switched LQR controller is designed accordingly to meet this collection of physical and geometric safety constraints, while maintaining liveness in navigating toward the target spacecraft. We extend this benchmark problem to check for passive safety, which is collision avoidance along a passive, propulsion-free trajectory that may be followed in the event of system failures. We show that existing hybrid verification tools like SpaceEx, C2E2, and our own implementation of a simulation-driven verification tool can robustly verify this system with respect to the requirements, and a variety of relevant initial conditions. |
BibTeX:
@inproceedings{ChanM17,
author = {Nicole Chan and Sayan Mitra},
title = {Verifying safety of an autonomous spacecraft rendezvous mission},
booktitle = {ARCH17. 4th International Workshop on Applied Verification of Continuous and Hybrid Systems, collocated with Cyber-Physical Systems Week (CPSWeek) on April 17, 2017 in Pittsburgh, PA, USA},
year = {2017},
pages = {20--32},
url = {http://www.easychair.org/publications/paper/342723}
}
|
| Chan N and Mitra S (2017), "Verified hybrid LQ control for autonomous spacecraft rendezvous", In IEEE International Conference on Decision and Control (CDC`17). |
| Abstract: Rendezvous is a fundamental maneuver in autonomous space operations in which an active chaser spacecraft is required to navigate safely to the proximity of a second passive target spacecraft. Ensuring safety of such control maneuvers is challenging and design errors can be expensive. We present the first verified control solution to a benchmark formulation of spacecraft autonomous rendezvous in the form of a hybrid LQR controller verified using a data-driven algorithm. Our hybrid LQR scheme is motivated by enforcing safety constraints rather than optimizing performance, and the control law is formulated by periodically solving optimization problems that depend on the current state. The resulting hybrid system presents a challenge for existing automated formal verification tools due to its lack of a closed-form model description. We overcome this challenge by using a data-driven approach (implemented in the new verification tool DryVR). DryVR relies on simulation traces to compute reachable states of the system over bounded time horizon and initial conditions to rigorously verify that the system does not violate any safety requirements. |
BibTeX:
@inproceedings{ChanM17:CDC,
author = {Nicole Chan and Sayan Mitra},
title = {Verified hybrid LQ control for autonomous spacecraft rendezvous},
booktitle = {IEEE International Conference on Decision and Control (CDC`17)},
year = {2017},
url = {https://ieeexplore.ieee.org/document/8263854/}
}
|
| Fan C, Qi B, Mitra S and Viswanathan M (2017), "DryVR: Data-Driven Verification and Compositional Reasoning for Automotive Systems", In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I. , pp. 441-461. |
| Abstract: We present the DryVR framework for verifying hybrid control systems that are described by a combination of a black-box simulator for trajectories and a white-box transition graph specifying mode switches. The framework includes (a) a probabilistic algorithm for learning sensitivity of the continuous trajectories from simulation data, (b) a bounded reachability analysis algorithm that uses the learned sensitivity, and (c) reasoning techniques based on simulation relations and sequential composition, that enable verification of complex systems under long switching sequences, from the reachability analysis of a simpler system under shorter sequences. We demonstrate the utility of the framework by verifying a suite of automotive benchmarks that include powertrain control, automatic transmission, and several autonomous and ADAS features like automatic emergency braking, lane-merge, and auto-passing controllers. |
BibTeX:
@inproceedings{FanQMVCAV017,
author = {Chuchu Fan and Bolun Qi and Sayan Mitra and Mahesh Viswanathan},
title = {DryVR: Data-Driven Verification and Compositional Reasoning for Automotive Systems},
booktitle = {Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I},
year = {2017},
pages = {441--461},
url = {https://link.springer.com/chapter/10.1007%2F978-3-319-63387-9_22},
doi = {10.1007/978-3-319-63387-9_22}
}
|
| Huang Z, Fan C and Mitra S (2017), "Bounded invariant verification for time-delayed nonlinear networked dynamical systems", IFAC Jounral on Nonlinear analysis., February, 2017. Vol. 23, pp. 211-229. |
| Abstract: We present a technique for bounded invariant verification of nonlinear networked dynamical systems with delayed interconnections. The underlying problem in precise bounded-time verification lies with computing bounds on the sensitivity of trajectories (or solutions) to changes in initial states and inputs of the system. For large networks, computing this sensitivity with precision guarantees is challenging. We introduce the notion of input-to-state (IS) discrepancy of each module or subsystem in a larger nonlinear networked dynamical system. The IS discrepancy bounds the distance between two solutions or trajectories of a module in terms of their initial states and their inputs. Given the IS discrepancy functions of the modules, we show that it is possible to effectively construct a reduced (low dimensional) time-delayed dynamical system, such that the trajectory of this reduced model precisely bounds the distance between the trajectories of the complete network with changed initial states. Using the above results we develop a sound and relatively complete algorithm for bounded invariant verification of networked dynamical systems consisting of nonlinear modules interacting through possibly delayed signals. Finally, we introduce a local version of IS discrepancy and show that it is possible to compute them using only the Lipschitz constant and the Jacobian of the dynamic function of the modules. |
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 = {IFAC Jounral on Nonlinear analysis},
year = {2017},
volume = {23},
pages = {211--229},
url = {http://www.sciencedirect.com/science/article/pii/S1751570X16300279}
}
|
| Sibai H (2017), "State estimation of switched nonlinear systems and systems with bounded inputs: entropy and bit rates". Thesis at: University of Illinois as Urbana-Champaign., December, 2017. |
| Abstract: State estimation is a fundamental problem when monitoring and controlling dynamical systems. Engineering systems interconnect sensing and computing devices over shared bandwidth-limited channels, and therefore, estimation algorithms should strive to use bandwidth optimally. Often, the dynamics of these systems are affected by external factors. In certain cases, these factors would lead the system to switch between different modes. In other cases, they would affect the dynamics of the system continuously in time without leading to explicit mode transitions. In this thesis, we present two notions of entropy for state estimation of nonlinear switched and non-autonomous dynamical systems as lower bounds on the average number of bits needed to be sent from the sensors to the estimators to estimate the states with deterministic (worst case) error bounds. Our approach relies on the notion of topological entropy and uses techniques from control under limited information. Since the computation of these entropies is hard in general, we compute corresponding upper bounds. Additionally, we design a state estimation algorithm for switched systems when their modes cannot be observed. We show that the average bit rate used by the algorithm is optimal in the sense that the efficiency gap is within an additive constant from the gap between the entropy of the considered system and its computed upper-bound. Finally, we apply our theory and algorithms to linear and nonlinear models of systems such as a glycemic index for diabetic patients, a controller of a Harrier jet and a Pendulum. |
BibTeX:
@mastersthesis{HusseinMasters,
author = {Hussein Sibai},
title = {State estimation of switched nonlinear systems and systems with bounded inputs: entropy and bit rates},
school = {University of Illinois as Urbana-Champaign},
year = {2017},
url = {http://hdl.handle.net/2142/99265}
}
|
| Huang Z, Wang Y, Mitra S and Dullerud G (2017), "Differential Privacy in Distributed Control Systems: Entropy Minimizing Mechanisms and Performance Trade-offs", IEEE Trans. on Control of Network Systems, Special Issue on Secure Control of Cyber Physical Systems. Vol. 4(1), pp. 118-130. |
| Abstract: In distributed control systems with shared resources, participating agents can improve the overall performance of the system by sharing data about their personal preferences. In this article, we formulate and study a natural trade-off arising in these problems between the privacy of the agent’s data and the performance of the control system. We formalize privacy in terms of differential privacy of agents’ preference vectors. The overall control system consists of N agents with linear discrete-time coupled dynamics, each controlled to track its preference vector. Performance of the system is measured by the mean squared tracking error. We present a mechanism that achieves differential privacy by adding Laplace noise to the shared information in a way that depends on the sensitivity of the control system to the private data. We show that for stable systems the performance cost of using this type of privacy preserving mechanism grows as O(T^3/Ne^2), where T is the time horizon and e is the privacy parameter. For unstable systems, the cost grows exponentially with time. From an estimation point of view, we establish a lower- bound for the entropy of any unbiased estimator of the private data from any noise-adding mechanism that gives e-differential privacy. We show that the mechanism achieving this lower-bound is a randomized mechanism that also uses Laplace noise. |
BibTeX:
@article{HYMD:TCONES2017,
author = {Zhenqi Huang and Yu Wang and Sayan Mitra and Geir Dullerud},
title = {Differential Privacy in Distributed Control Systems: Entropy Minimizing Mechanisms and Performance Trade-offs},
journal = {IEEE Trans. on Control of Network Systems, Special Issue on Secure Control of Cyber Physical Systems},
year = {2017},
volume = {4},
number = {1},
pages = {118--130},
url = {http://ieeexplore.ieee.org/document/7833044/}
}
|
| Sibai H and Mitra S (2017), "Optimal data rate for state estimation of switched nonlinear systems", In Hybrid Systems: Computation and Control (HSCC 2017), Pittsburgh, PA.. , pp. 71-80. |
| Abstract: State estimation is a fundamental problem for monitoring and controlling systems. Engineering systems interconnect sensing and computing devices over a shared bandwidth-limited channels, and therefore, estimation algorithms should strive to use bandwidth optimally. We present a notion of entropy for state estimation of switched nonlinear dynamical systems, an upper bound for it and a state estimation algorithm for the case when the switching signal is unobservable. Our approach relies on the notion of topological entropy and uses techniques from the theory for control under limited information. We show that the average bit rate used is optimal in the sense that, the efficiency gap of the algorithm is within an additive constant of the gap between estimation entropy of the system and its known upper-bound. We apply the algorithm to two system models and discuss the performance implications of the number of tracked modes. |
BibTeX:
@inproceedings{SibaiM:HSCC2017,
author = {Hussein Sibai and Sayan Mitra},
title = {Optimal data rate for state estimation of switched nonlinear systems},
booktitle = {Hybrid Systems: Computation and Control (HSCC 2017), Pittsburgh, PA.},
year = {2017},
pages = {71--80},
url = {http://dl.acm.org/citation.cfm?id=3049799}
}
|
| Cortés J, Dullerud G, Han S, Le Ny J, Mitra S and Pappas GJ (2016), "Differential privacy in control and network systems", In Decision and Control (CDC), 2016 IEEE 55th Conference on. , pp. 4252-4272. |
| Abstract: As intelligent automation and large-scale distributed monitoring and control systems become more widespread, concerns are growing about the way these systems collect and make use of privacy-sensitive data obtained from individuals. This tutorial paper gives a systems and control perspective on the topic of privacy preserving data analysis, with a particular emphasis on the processing of dynamic data as well as data exchanged in networks. Specifically, we consider mechanisms enforcing differential privacy, a state-of-the-art definition of privacy initially introduced to analyze large, static datasets, and whose guarantees hold against adversaries with arbitrary side information. We discuss in particular how to perform tasks such as signal estimation, consensus and distributed optimization between multiple agents under differential privacy constraints. |
BibTeX:
@inproceedings{cortes2016differential,
author = {Cortés, Jorge and Dullerud, Geir and Han, Shuo and Le Ny, Jerome and Mitra, Sayan and Pappas, George J},
title = {Differential privacy in control and network systems},
booktitle = {Decision and Control (CDC), 2016 IEEE 55th Conference on},
year = {2016},
pages = {4252--4272},
url = {http://ieeexplore.ieee.org/abstract/document/7798915/}
}
|
| Duggirala PS, Fan C, Potok M, Qi B, Mitra S, Viswanathan M, Bak S, Bogomolov S, Johnson T, Nguyen LV and others (2016), "Tutorial: Software tools for hybrid systems verification, transformation, and synthesis: C2E2, HyST, and TuLiP", In Control Applications (CCA), 2016 IEEE Conference on. , pp. 1024-1029.
[BibTeX] |
BibTeX:
@inproceedings{duggirala2016tutorial,
author = {Duggirala, Parasara Sridhar and Fan, Chuchu and Potok, Matthew and Qi, Bolun and Mitra, Sayan and Viswanathan, Mahesh and Bak, Stanley and Bogomolov, Sergiy and Johnson, Taylor and Nguyen, Luan Viet and others},
title = {Tutorial: Software tools for hybrid systems verification, transformation, and synthesis: C2E2, HyST, and TuLiP},
booktitle = {Control Applications (CCA), 2016 IEEE Conference on},
year = {2016},
pages = {1024--1029}
}
|
| Fan C, Kapinski J, Jin X and Mitra S (2016), "Locally Optimal Reach Set Over-approximation for Nonlinear Systems", In Proceedings of the 13th ACM-SIGBED International Conference on Embedded Software (EMSOFT). New York, NY, USA , pp. 6:1-6:10. ACM. |
| Abstract: Safety verification of embedded systems modeled as hybrid systems can be scaled up by employing simulation-guided reach set over-approximation techniques. Existing methods are either applicable to only restricted classes of systems, overly conservative, or computationally expensive. We present new techniques to compute a locally optimal bloating factor based on discrepancy functions, which allow construction of reach set over-approximations from simulation traces for general nonlinear systems. The discrepancy functions are critical for tools like C2E2 to verify bounded time safety properties for complex hybrid systems with nonlinear continuous dynamics. The new discrepancy function is computed using local bounds on a matrix measure under an optimal metric such that the exponential change rate of the discrepancy function is minimized. The new technique is less time consuming and less conservative than existing techniques and does not incur significant computational overhead. We demonstrate the effectiveness of our approach by comparing the performance of a prototype implementation with the state-of-the-art reachability analysis tool Flow. |
BibTeX:
@inproceedings{FanM:EMSOFT2016,
author = {Fan, Chuchu and Kapinski, James and Jin, Xiaoqing and Mitra, Sayan},
title = {Locally Optimal Reach Set Over-approximation for Nonlinear Systems},
booktitle = {Proceedings of the 13th ACM-SIGBED International Conference on Embedded Software (EMSOFT)},
publisher = {ACM},
year = {2016},
pages = {6:1--6:10},
note = {Nominated for best paper award.},
url = {http://doi.acm.org/10.1145/2968478.2968482},
doi = {10.1145/2968478.2968482}
}
|
| Fan C, Qi B, Mitra S, Viswanathan M and Duggirala PS (2016), "Automatic Reachability Analysis for Nonlinear Hybrid Models with C2E2", In International Conference on Computer Aided Verification (CAV). Vol. 9779, pp. 531-538. |
| Abstract: C2E2 is a bounded reachability analysis tool for nonlinear dynamical systems and hybrid automaton models. Previously it required users to annotate each system of differential equations of the hybrid automaton with discrepancy functions, and since these annotations are difficult to get for general nonlinear differential equations, the tool had limited usability. This version of C2E2 is improved in several ways, the most prominent among which is the elimination of the need for user-provided discrepancy functions. It automatically computes piece-wise (or local) discrepancy functions around the reachable parts of the state space using symbolically computed Jacobian matrix and eigenvalue perturbation bounds. The special cases of linear and constant rate differential equations are handled with more efficient algorithm. In this paper, we discuss these and other new features that make the new C2E2 a usable tool for bounded reachability analysis of hybrid systems. |
BibTeX:
@inproceedings{fanQMVD2016CAV,
author = {Fan, Chuchu and Qi, Bolun and Mitra, Sayan and Viswanathan, Mahesh and Duggirala, Parasara Sridhar},
title = {Automatic Reachability Analysis for Nonlinear Hybrid Models with C2E2},
booktitle = {International Conference on Computer Aided Verification (CAV)},
year = {2016},
volume = {9779},
pages = {531--538},
url = {http://link.springer.com/chapter/10.1007/978-3-319-41528-4_29}
}
|
| Huang Z, Wang Y, Mitra S and Dullerud G (2016), "Controller Synthesis for Linear Time-varying Systems with Adversaries", In Hot topics in Science of Security (HOTSOS). |
| 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},
booktitle = {Hot topics in Science of Security (HOTSOS)},
year = {2016},
url = {http://arxiv.org/abs/1501.04925}
}
|
| Liberzon D and Mitra S (2016), "Entropy notions for state estimation and model detection with finite-data-rate measurements", In Decision and Control (CDC), 2016 IEEE 55th Conference on. , pp. 7335-7340. |
| Abstract: We study a notion of estimation entropy for continuous-time nonlinear systems, formulated in terms of the number of system trajectories that approximate all other trajectories up to an exponentially decaying error. We also consider an alternative definition of estimation entropy which uses approximating functions that are not necessarily trajec- tories of the system, and show that the two entropy notions are equivalent. We establish an upper bound on the estimation entropy in terms of the sum of the desired convergence rate and an upper bound on the matrix measure of the Jacobian, multiplied by the system dimension. We describe 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 algorithm of this type can perform the same estimation task with bit rates lower than the estimation entropy. Finally, we discuss 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 always happens in finite time. |
BibTeX:
@inproceedings{LM:Entropy:CDC16,
author = {Liberzon, Daniel and Mitra, Sayan},
title = {Entropy notions for state estimation and model detection with finite-data-rate measurements},
booktitle = {Decision and Control (CDC), 2016 IEEE 55th Conference on},
year = {2016},
pages = {7335--7340},
url = {http://ieeexplore.ieee.org/abstract/document/7799402/}
}
|
| Liberzon D and Mitra S (2016), "Entropy and minimal data rates for state estimation and model detection", In Hybrid System: Computation and Control (HSCC 2016). |
| 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 (HSCC 2016)},
year = {2016},
url = {http://dl.acm.org/citation.cfm?id=2883820&CFID=712441810&CFTOKEN=47933224}
}
|
| Lin Y (2016), "Programming platform for distributed robotics: Primitives and Portability". Thesis at: University of Illinois as Urbana-Champaign. |
| Abstract: The Stabilizing Robotics Language (StarL) programming framework aims to simplify development of distributed robotic applications by providing programming abstractions and building blocks for communication, motion control and coordination between robots. It has been used to develop applications such as formation control, automatic intersection protocol, and distributed collaborative search. In this thesis, we introduce the programming abstractions as StarL primitives that are platform independent and useful across hardware platforms, resulting in portability. We first introduce the primitives as building blocks to easily develop, simulate and debug distributed robotic applications in StarL. Then, we discuss the design of the StarL framework which enables us to achieve portability of robot programs across hardware platforms. Thus, the same application program, say, for formation control, can now be ported and deployed on multiple, heterogeneous robotic platforms. We evaluate the design of these new features by simulating several applications. |
BibTeX:
@mastersthesis{YixiaoLinMasters,
author = {Yixiao Lin},
title = {Programming platform for distributed robotics: Primitives and Portability},
school = {University of Illinois as Urbana-Champaign},
year = {2016},
url = {https://www.ideals.illinois.edu/bitstream/handle/2142/90689/LIN-THESIS-2016.pdf?sequence=1}
}
|
| Huang Z (2016), "Compositional analysis of networked cyber-physical systems: Safety and Privacy". Thesis at: University of Illinois at Urbana-Champaign. Urbana, IL |
| Abstract: Cyber-physical systems (CPS) are now commonplace in power grids, man- ufacturing, and embedded medical devices. Failures and attacks on these systems have caused significant social, environmental and financial losses. In this thesis, we develop techniques for proving invariance and privacy proper- ties of cyber-physical systems that could aid the development of more robust and reliable systems. The thesis uses three different modeling formalisms capturing different as- pects of CPS. Networked dynamical systems are used for modeling (possibly time-delayed) interaction of ordinary differential equations, such as in power system and biological networks. Labeled transition systems are used for mod- eling discrete communications and updates, such as in sampled data-based control systems. Finally, Markov chains are used for describing distributed cyber-physical systems that rely on randomized algorithms for communica- tion, such as in a crowd-sourced traffic monitoring and routing system. De- spite the differences in these formalisms, any model of a CPS can be viewed as a mapping from a parameter space (for example, the set of initial states) to a space of behaviors (also called trajectories or executions). In each formal- ism, we define a notion of sensitivity that captures the change in trajectories as a function of the change in the parameters. We develop approaches for approximating these sensitivity functions, which in turn are used for analysis of invariance and privacy. For proving invariance, we compute an over-approximation of reach set, which is the set of states visited by any trajectory. We introduce a notion of input-to-state (IS) discrepancy functions for components of large CPS, which roughly captures the sensitivity of the component to its initial state and input. We develop a method for constructing a reduced model of the entire system using the IS discrepancy functions. Then, we show that the trajectory of the reduced model over-approximates the sensitivity of the entire system with respect to the initial states. Using the above results we develop a sound and relatively complete algorithm for compositional invariant verification. In systems where distributed components take actions concurrently, there is a combinatorial explosion in the number of different action sequences (or traces). We develop a partial order reduction method for computing the reach set for these systems. Our approach uses the observation that some action pairs are approximately independent, such that executing these actions in any order results in states that are close to each other. Hence a (large) set of traces can be partitioned into a (small) set of equivalent classes, where equiv- alent traces are derived through swapping approximately independent action pairs. We quantify the sensitivity of the system with respect to swapping approximately independent action pairs, which upper-bounds the distance between executions with equivalent traces. Finally, we develop an algorithm for precisely over-approximating the reach set of these systems that only explore a reduced set of traces. In many modern systems that allow users to share data, there exists a tension between improving the global performance and compromising user privacy. We propose a mechanism that guarantees epsilon-differential privacy for the participants, where each participant adds noise to its private data before sharing. The distributions of noise are specified by the sensitivity of the trajectory of agents to the private data. We analyze the trade-off between differential privacy and performance, and show that the cost of differential privacy scales quadratically to the privacy level. The thesis illustrates that quantitative bounds on sensitivity can be used for effective reachability analysis, partial order reduction, and in the design of privacy preserving distributed cyber-physical systems. |
BibTeX:
@phdthesis{ZhenqiHuangPhD,
author = {Zhenqi Huang},
title = {Compositional analysis of networked cyber-physical systems: Safety and Privacy},
school = {University of Illinois at Urbana-Champaign},
year = {2016}
}
|
| Islam MA, DeFrancisco R, Fan C, Grosu R, Mitra S and Smolka SA (2015), "Model Checking Tap Withdrawal in C. Elegans", In Hybrid Systems Biology - Fourth International Workshop, HSB 2015, Madrid, Spain, September 4-5, 2015.. Vol. 9271, 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 PS, Fan C, Mitra S and Viswanathan M (2015), "Meeting a Powertrain Verification Challenge", In In the Proceedings of International Conference on Computer Aided Verification (CAV 2015). San Francisco Vol. 9206, pp. 536-543. Springer. |
| 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 = {In the Proceedings of International Conference on Computer Aided Verification (CAV 2015)},
publisher = {Springer},
year = {2015},
volume = {9206},
pages = {536--543}
}
|
| Duggirala PS, Mitra S and Viswanathan M (2015), "C2E2: A Verification Tool For Stateflow Models", In Proceedings of 21st International Conference Tools and Algorithms for the Construction and Analysis of Systems TACAS 2015, London, UK, April 11-18, 2015.. Vol. 9035, pp. 68-82. Springer. |
| 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 = {10.1007/978-3-662-46681-0}
}
|
| Fan C and Mitra S (2015), "Bounded Verification with On-the-Fly Discrepancy Computation", In 13th Intl. Symposium on Automated Technology for Verification and Analysis (ATVA 2015), Sanghai, China.. Vol. 9364, 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://link.springer.com/chapter/10.1007%2F978-3-319-24953-7_32#page-1}
}
|
| Fan C, Duggirala PS, Mitra S and Viswanathan M (2015), "Progress on Powertrain Verification Challenge with C2E2", In 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 (2015), "A Strategy for Automatic Verification of Stabilization of Distributed Algorithms", In Proceedings of Formal Techniques for Distributed Systems (FORTE) - Joint IFIP WG 6.1 International Conference. Vol. 9039, pp. 35-49. Springer. |
| 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.},
url = {http://link.springer.com/chapter/10.1007%2F978-3-319-19195-9_3}
}
|
| Huang Z, Fan C, Mereacre A, Mitra S and Kwiatkowska M (2015), "Simulation-based Verification of Cardiac Pacemakers with Guaranteed Coverage", IEEE Design and Test Special Issue, 32(5). Vol. 32, 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, 32(5)},
year = {2015},
volume = {32},
pages = {27--34},
url = {http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=7130608&tag=1}
}
|
| Huang Z, Mitra S and Vaidya N (2015), "Differentially Private Distributed Optimization", In International Converence on Distributed Computing and Networks (ICDCN 2015), Goa, India, January 4-7, 2015. , pp. 4:1-4:10. ACM. |
| 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 ∑ 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 (2015), "Analyzing Cost of Securing Control Systems", The Next Wave, 21(1). Vol. 21, pp. 12-17. |
BibTeX:
@article{HuangNextWaveT:2015,
author = {Zhenqi Huang and Yu Wang and Sayan Mitra and Geir Dullerud},
title = {Analyzing Cost of Securing Control Systems},
journal = {The Next Wave, 21(1)},
year = {2015},
volume = {21},
pages = {12--17},
url = {https://www.nsa.gov/research/tnw/tnw211/articles/pdfs/TNW_21-1_2015_Article4.pdf}
}
|
| Huang Z, Wang Y, Mitra S, Dullerud G and Chaudhuri S (2015), "Controller synthesis with inductive proofs for piecewise linear systems: An SMT-based algorithm", In 54th IEEE Conference on Decision and Control, CDC 2015, Osaka, Japan, December 15-18, 2015. , pp. 7434-7439. |
BibTeX:
@inproceedings{HuangWMDC15,
author = {Zhenqi Huang and Yu Wang and Sayan Mitra and Geir Dullerud and Swarat Chaudhuri},
title = {Controller synthesis with inductive proofs for piecewise linear systems: An SMT-based algorithm},
booktitle = {54th IEEE Conference on Decision and Control, CDC 2015, Osaka, Japan, December 15-18, 2015},
year = {2015},
pages = {7434--7439},
url = {http://dx.doi.org/10.1109/CDC.2015.7403394}
}
|
| Johnson T and Mitra S (2015), "Safe and Stabilizing Distributed Traffic Control", 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 PS, Mitra S and Viswanathan M (2015), "Hybrid Automata-based CEGAR for Rectangular Hybrid Systems", In Formal Methods in System Design (FMSD). Vol. 46(2), pp. 105--134. Springer. |
| 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 PS, Wang L, Mitra S, Munoz C and Viswanathan M (2014), "Temporal Precedence Checking for Switched Models and its Application to a Parallel Landing Protocol", In 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 (2014), "Synthesis and Verification of Motor-Transmission Shift Controller for Electric Vehicles", In the Proceedings of the International Conference on Cyberphysical Systems (ICCPS 2014). Berlin, Germany |
| 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 (2014), "Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells", In 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 (2014), "Proofs from Simulations and Modular Annotations", In 17th International Conference on Hybrid Systems: Computation and Control (HSCC 2014). Berlin, Germany, April, 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 (2014), "On the Cost of Differential Privacy in Distributed Control Systems", In 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 and Mitra S (2014), "Anonymized Reachability of Hybrid Automata Networks", In 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 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},
url = {http://link.springer.com/chapter/10.1007%2F978-3-319-10512-3_10#page-1}
}
|
| Mitra S (2014), "Proving Abstractions of Dynamical Systems through Numerical Simulations", In 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},
url = {http://dl.acm.org/citation.cfm?id=2600188}
}
|
| Mitra S (2014), "Developing Programming Abstractions for Cyberphysical systems". January, 2014.
[BibTeX] |
BibTeX:
@misc{MitraPosCPS2014,
author = {Sayan Mitra},
title = {Developing Programming Abstractions for Cyberphysical systems},
year = {2014}
}
|
| Wang Y, Huang Z, Mitra S and Dullerud G (2014), "Entropy-minimizing Mechanism for Differential Privacy of Discrete-time Linear Feedback Systems", In Conference on Decision and Control (CDC). IEEE. |
| 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 dpc 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 Ln. We then consider the dpc 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 dpt, 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},
url = {http://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=7039713}
}
|
| Zimmerman A (2013), "StarL for programming reliable robotic networks". Thesis at: 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 PS, Mitra S and Viswanathan M (2013), "Verificationcation of Annotated Models from Executions", In Proceedings of International Conference on Embedded Software (EMSOFT 2013). Montreal, QC, Canada, September, 2013. , pp. 1-10. IEEE. |
| 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 (2013), "Invariant Synthesis for Verification of Parameterized Cyber-Physical Systems with Application to Aerospace Systems", In Proceedings of Infotech@AIAA. Boston, MA, August, 2013.
[BibTeX] |
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 (2013), "Uniform Verification of Safety for Parameterized Networks of Hybrid Automata". Thesis at: Department of Electrical and Computer Engineering, University of Illinois at Urbana-Champaign. Urbana, IL 61801, USA, August, 2013.
[BibTeX] |
BibTeX:
@phdthesis{johnson2013thesis,
author = {Taylor 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 (2013), "Verifying Cyber-Physical Interactions in Safety-Critical Systems", 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},
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 PS, Mitra S and Viswanathan M (2013), "Hybrid Automata-based CEGAR for Rectangular Hybrid Systems", In 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 (2013), "On Simulation-Based Verification of Nonlinear Nondeterministic Hybrid Systems". Thesis at: 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 PS, Johnson T, Zimmerman A and Mitra S (2012), "Static and Dynamic Analysis of Timed Distributed Traces", In Proceedings of IEEE Real-Time Systems Symposium (RTSS 2012). San Juan, Puerto Rico, December, 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 PS and Mitra S (2012), "Lyapunov Abstractions for Inevitability of Hybrid Systems", In 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 (2012), "Computing Bounded Reach Sets from Sampled Simulation Traces", In 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 (2012), "Trace-based Bounded Verification of Embedded Systems" |
| 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 (2012), "Differentially Private Iterative Synchronous Consensus", In Proceedings of the Workshop on Differentially Private Iterative Synchronous Consensus in conjunction with the ACM CCS conference 2012. Raleigh, NC, October, 2012. ACM. |
| 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/(ε 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 (2012), "Compositional bounded reachability using time partitioning and abstraction". Thesis at: 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 RS (2012), "Verifying Satellite Rendezvous and Conjunction Avoidance: A Formal Approach to Autonomy in Space", In 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 (2012), "Parameterized Verification of Distributed Cyber-Physical Systems:An Aircraft Landing Protocol Case Study", In 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 (2012), "A Small Model Theorem for Rectangular Hybrid Automata Networks", In IFIP International Conference on Formal Techniques for Distributed Systems joint international conference: 32nd Formal Techniques for Networked and Distributed Systems (FORTE).. Vol. 7273, 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 (2012), "Verification of Periodically Controlled Hybrid Systems: Application to An Autonomous Vehicle", Special Issue of the ACM Transactions on Embedded Computing Systems (TECS)., August, 2012. 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 MB (2011), "Opportunistic clock synchronization for ad hoc networks". Thesis at: 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 (2011), "Sandboxing Controllers for Cyber-Physical Systems", In Proceedings of 2nd IEEE/ACM International Conference on Cyber-physical systems (ICCPS 2011). Chicago, IL, April, 2011. IEEE Computer Society. |
| 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 KM, Go B, Mitra S, Pilotto C and White J (2011), "Verification of Distributed Systems with Local-Global Predicates", 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 PS and Mitra S (2011), "Abstraction-Refinement for Stability", In Proceedings of 2nd IEEE/ACM International Conference on Cyber-physical systems (ICCPS 2011). Chicago, IL, April, 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 (2011), "Safe Flocking in Spite of Actuator Faults using Directional Failure Detectors", 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 (2011), "Stability of Digitally Interconnected Linear Systems", In 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 K (2011), "Translation of Simulink-Stateflow models to hybrid automata". Thesis at: 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 = {Karthik Manamcheri},
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 PR (2011), "Computing bounded epsilon-Reach Set with finite precision computations for a class of linear hybrid automata", In 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 (2011), "A step towards verification and synthesis from Simulink/Stateflow models", In 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 (2010), "Hybrid Cyberphysical System Verification With Simplex Using Discrete Abstractions", In 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 PS, Mitra S, Kumar R and Glazeski D (2010), "On The Theory of Stochastic Processors", In Seventh International Conference on the Quantitative Evaluation of Systems (QEST 2010). IEEE Press. |
| 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 (2010), "Safe and Stabilizing Distributed Flocking in Spite of Actuator Faults". Thesis at: University of Illinois at Urbana Champaign. Urbana, IL, August, 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},
school = {University of Illinois at Urbana Champaign},
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 (2010), "Safe Flocking in spite of Actuator Faults", In In proceedings of 12th International Symposium on Stabilization, Safety, and Security of Distributed Systems. Springer. |
| 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 (2010), "Safe and Stabilizing Distributed Cellular Flows", In 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 PR (2010), "Bounded epsilon-Reachability of Linear Hybrid Automata with a Deterministic and Transversal Discrete Transition Condition", In Proceedings of The 49th IEEE Conference on Decision and Control (CDC). IEEE. |
| 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 (2010), "Fault-tolerant distributed cyber-physical systems: two case studies". Thesis at: 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 REL and Mitra S (2009), "Stability of Distributed Algorithms in the face of Incessant Faults", In Proceedings of 11th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2009). Lyon, France |
| 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 (2009), "Self-stabilizing robot formations over unreliable networks", Special Issue on Self-adaptive and Self-organizing Wireless Networking Systems of ACM Transactions on Autonomous and Adaptive Systems (TAAS). New York, NY, USA Vol. 4(3), pp. 1-29. ACM. |
| 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 = {10.1145/1552297.1552300}
}
|
| Mitra S and Sastry S (2009), "Hybrid input output automata for composable conveyor systems", In 5th Annual IEEE International Conference on Automation Science and Engineering (CASE'09). Piscataway, NJ, USA , pp. 29-29. IEEE Press. |
| 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 (2009), "On Convergence of Concurrent Systems under Regular Interactions", In 20th International Conference on Concurrency Theory (CONCUR 2009). Vol. 5710, pp. 527-541. Springer. |
| 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},
editor = {Mario Bravetti and Gianluigi Zavattaro},
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}
}
|
| Archer M, Lim H, Lynch N, Mitra S and Umeno S (2008), "Specifying and Proving Properties of Timed I/O Automata Using Tempo", 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}
}
|
| Chandy KM, Mitra S and Pilotto C (2008), "Convergence Verification: From Shared Memory to Partially Synchronous Systems", In Formal Modeling and Analysis of Timed Systems (FORMATS`08). Vol. 5215, pp. 217-231. Springer Verlag. |
| 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 KM (2008), "A Formalized Theory for Verifying Stability and Convergence of Automata in PVS", In Theorem Proving in Higher Order Logics (TPHOLS 2008). , pp. 230-245. LNCS. |
| 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 (2008), "Verifying Average Dwell Time of Hybrid Systems", ACM Transactions on Embedded Computing Systems. Vol. 8 ACM. |
| 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)}
}
|
| Mitra S (2007), "A Verification Framework for Hybrid Systems". Thesis at: Massachusetts Institute of Technology. Cambridge, MA 02139, September, 2007. |
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 (2007), "Proving approximate implementation relations for Probabilistic I/O Automata.", Electronic Notes in Theoretical Computer Science. Amsterdam, The Netherlands, The Netherlands Vol. 174(8), pp. 71-93. Elsevier Science Publishers B. V.. |
| 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 = {10.1016/j.entcs.2006.11.040}
}
|
| Mitra S and Lynch N (2007), "Trace-based Semantics for Probabilistic Timed I/O Automata", In 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 (2006), " Specifying and Proving Properties of Timed I/O Automata in the TIOA Toolkit ", In In Fourth ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'06). IEEE. |
| 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 (2006), " Approximate simulations for task-structured probabilistic I/O automata", In LICS workshop on Probabilistic Automata and Logics (PAul06). Seattle, WA, August, 2006. |
| 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}
}
|
| Chockler G, Lynch N, Mitra S and Tauber J (2005), " Proving atomicity: an assertional approach", In Proceedings of Nineteenth International Symposium on Distributed Computing (DISC'05). Cracow, Poland , September, 2005. Vol. 3724, pp. 152 - 168. Springer. |
| 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},
editor = {Pierre Fraigniaud},
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 (2005), "Translating timed I/O automata specifications for theorem proving in PVS", In Proceedings of Formal Modelling and Analysis of Timed Systems (FORMATS'05). Uppsala, Sweden, September, 2005. (3829) Springer. |
| 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 (2005), "Path vector face routing: Geographic routing with local face information", In Proceedings of 13th IEEE International Conference on Network Protocols (ICNP'05). Boston, Massachusetts, November, 2005. |
| 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 (2005), "Motion coordination using virtual nodes", In Proceedings of 44th IEEE Conference on Decision and Control (CDC05). Seville, Spain, December, 2005. IEEE. |
| 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 (2005), "PVS Strategies for Proving Abstraction Properties of Automata.", 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 (2005), "Stability of hybrid automata with average dwell time: an invariant approach", In Proceedings of the 43rd IEEE Conference on Decision and Control. Paradise Island, Bahamas, February, 2005. |
| 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 (2004), "Specifying and Proving Timing Properties with TIOA Tools", In In the work in progress session of the 25th IEEE International Real-Time Systems Symposium (RTSS-WIP). Lisbon, Portugal, December, 2004.
[BibTeX] |
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 (2004), "Reusable PVS Proof Strategies for Proving Abstraction Properties of I/O Automata", In STRATEGIES 2004, IJCAR Workshop on strategies in automated deduction. Cork, Ireland, July, 2004.
[BibTeX] |
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 (2004), "Energy efficient connected clusters for mobile ad hoc networks", In Proceedings of 3rd Annual Mediterranean Ad Hoc Networking Workshop (MED-HOC-NET'04). Bodrum, Turkey |
| 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 (2003), "Developing Strategies for Specialized Theorem Proving about Untimes, Timed, and Hybrid I/O Automata", In STRATA 2003. Rome, Italy
[BibTeX] |
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 (2001), "HIOA - A Specification Language for Hybrid Input/Output Automata". Thesis at: Department of Computer Science and Automation, IISc. Indian Institute of Science, Bangalore |
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}
}
|