The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.04 - July-Aug. (2013 vol.11)
pp: 28-37
Sayan Mitra , University of Illinois at Urbana-Champaign
Tichakorn Wongpiromsarn , Singapore-MIT Alliance for Research and Technology
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.
INDEX TERMS
Vehicles, Urban areas, Safety, Computer viruses, Verification, Computer security, invariant checking, formal verification, simulation-based verification, autonomous vehicles
CITATION
Sayan Mitra, Tichakorn Wongpiromsarn, Richard M. Murray, "Verifying Cyber-Physical Interactions in Safety-Critical Systems", IEEE Security & Privacy, vol.11, no. 4, pp. 28-37, July-Aug. 2013, doi:10.1109/MSP.2013.77
REFERENCES
1. T. Wongpiromsarn et al., “Verification of Periodically Controlled Hybrid Systems: Application to an Autonomous Vehicle,” ACM Trans. Embedded Computing Systems, vol. 11, no. S2, 2012, art. 53.
2. S. Mattsson, M. Otter, and H. Elmqvist, “Modelica Hybrid Modeling and Efficient Simulation,” Proc. 38th IEEE Conf. Decision and Control, IEEE, 1999, pp. 3502-3507.
3. E.A. Lee et al., Overview of the Ptolemy Project, tech. report UCB/ERL M01/11, Dept. Electrical Eng. and Computer Science, Univ. California, Berkeley, 2001.
4. D. Liberzon, “Switching in Systems and Control,” Systems and Control: Foundations and Applications, Birkhauser, 2003.
5. R. Goebel, R.G. Sanfelice, and A.R. Teel, Hybrid Dynamical Systems: Modeling, Stability, and Robustness, Princeton Univ. Press, 2012.
6. D.K. Kaynar et al., The Theory of Timed I/O Automata. Synthesis Lectures on Computer Science, Morgan Claypool, 2005.
7. R. Alur et al., “The Algorithmic Analysis of Hybrid Systems,” Theoretical Computer Science, vol. 138, no. 1, 1995, pp. 3-34.
8. A. Platzer, “Differential Dynamic Logic for Hybrid Systems,” J. Automated Reasoning, vol. 41, no. 2, 2008, pp. 143-189.
9. P.S. Duggirala and S. Mitra, “Lyapunov Abstractions for Inevitability of Hybrid Systems,” Hybrid Systems: Computation and Control, ACM, 2012, pp. 115-124.
10. C. Belta et al., “Symbolic Planning and Control of Robot Motion,” IEEE Robotics & Automation Magazine, vol. 14, no. 1, 2007, pp. 61-70.
11. H. Kress-Gazit, G.E. Fainekos, and G.J. Pappas, “Temporal-Logic-Based Reactive Mission and Motion Planning,” IEEE Trans. Robotics, vol. 25, no. 6, 2009, pp. 1370-1381.
12. T.A. Henzinger, P.-H. Ho, and H. Wong-Toi, “Hytech: A Model Checker for Hybrid Systems,” Computer Aided Verification (CAV 97), LNCS 1254, Springer, 1997, pp. 460-483.
13. G. Frehse, “Phaver: Algorithmic Verification of Hybrid Systems Past Hytech,” Hybrid Systems: Computation and Control, LNCS 3414, Springer, 2005, pp. 258-273.
14. T. Dang, O. Maler, and R. Testylier, “Accurate Hybridization of Nonlinear Systems,” Proc. 13th ACM Int'l Conf. Hybrid Systems: Computation and Control (HSCC 10), ACM, 2010, pp. 11-20.
15. S. Sankaranarayanan, H.B. Sipma, and Z. Manna, “Constructing Invariants for Hybrid Systems,” Formal Methods in System Design, vol. 32, no. 1, 2008, pp. 25-55.
16. T. Nghiem et al., “Monte-Carlo Techniques for Falsification of Temporal Properties of Non-Linear Hybrid Systems, Proc. 13th ACM Int'l Conf. Hybrid Systems: Computation and Control (HSCC 10), ACM, 2010, pp. 211-220.
17. P. Zuliani, A. Platzer, and E.M. Clarke, “Bayesian Statistical Model Checking with Application to Simulink/Stateflow Verification,” Proc. 13th ACM Int'l Conf. Hybrid Systems: Computation and Control (HSCC 10), ACM, 2010, pp. 243-252.
18. A. Donzé, “Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems,” Proc. 22nd Int'l Conf. Computer Aided Verification (CAV 10), Springer, 2010, pp. 167-170.
19. Z. Huang and S. Mitra, “Computing Bounded Reach Sets from Sampled Simulation Traces,” Proc. 15th ACM Int'l Conf. Hybrid Systems: Computation and Control (HSCC 12), ACM, 2012, pp. 291-294.
20. P. Duggirala, S. Mitra, and M. Viswanathan, Verification of Annotated Models from Executions, tech. report UILU-ENG-13-2204 (CRHC-13-04), Coordinated Science Laboratory, Univ. Illinois at Urbana-Champaign, June 2013; https://publish.illinois.educ2e2-tool.
27 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool