Issue No. 04 - July-Aug. (2013 vol. 11)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/MSP.2013.77
Sayan Mitra , University of Illinois at Urbana-Champaign
Tichakorn Wongpiromsarn , Singapore-MIT Alliance for Research and Technology
Richard M. Murray , Caltech
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.
Vehicles, Urban areas, Safety, Computer viruses, Verification, Computer security, invariant checking, formal verification, simulation-based verification, autonomous vehicles
T. Wongpiromsarn, R. M. Murray and S. Mitra, "Verifying Cyber-Physical Interactions in Safety-Critical Systems," in IEEE Security & Privacy, vol. 11, no. , pp. 28-37, 2013.