This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Verification of Cyberphysical Transportation Systems
July/August 2009 (vol. 24 no. 4)
pp. 10-13
André Platzer, Carnegie Mellon University
Cyberphysical system technology has an important share in modern intelligent transportation systems, including next generation flight, rail, and car control. This control technology is intended to help improve performance objectives like throughput and improve overall system safety. To ensure that these transportation systems operate correctly, new analysis techniques are needed that consider physical movement combined with computational control to establish properties like collision freedom. Logic-based analysis can verify the correct functioning of these cyberphysical systems.

1. C. Tomlin, G.J. Pappas, and S. Sastry, "Conflict Resolution for Air Traffic Management: A Study in Multiagent Hybrid Systems," IEEE Trans. Automatic Control, vol. 43, no. 4, 2008, pp. 509–521; doi:10.1109/9.664154.
2. ERTMS User Group, "ERTMS/ETCS System Requirements Specification," ver. 2.2.2, 2002; www.era.europa.eu.
3. E.M. Clarke, O. Grumberg, and D.A. Peled, Model Checking, MIT Press, 1999.
4. A. Platzer, "Differential Dynamic Logic for Hybrid Systems," J. Automated Reasoning, vol. 41, no. 2, 2008, pp. 143–189; doi:10.1007/s10817-008-9103-8.
5. A. Platzer, "Differential Dynamic Logics: Automated Theorem Proving for Hybrid Systems," doctoral dissertation, Dept. Computing Science, Univ. of Oldenburg, 2008.
6. G.E. Collins and H. Hong, "Partial Cylindrical Algebraic Decomposition for Quantifier Elimination," J. Symbolic Computing, vol. 12, no. 3, 1991, pp. 299–328; doi:10.1016/S0747-7171(08)80152-6.
7. A. Platzer and E.M. Clarke, "Computing Differential Invariants of Hybrid Systems as Fixedpoints," Formal Methods in System Design, 2009; doi: 10.1007/s10703009-0079-8.

Index Terms:
cyberphysical transportation systems, train control, air traffic control, logic-based analysis, verification
Citation:
André Platzer, "Verification of Cyberphysical Transportation Systems," IEEE Intelligent Systems, vol. 24, no. 4, pp. 10-13, July-Aug. 2009, doi:10.1109/MIS.2009.81
Usage of this product signifies your acceptance of the Terms of Use.