The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.04 - July/August (2009 vol.24)
pp: 10-13
André Platzer , Carnegie Mellon University
ABSTRACT
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.
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/August 2009, doi:10.1109/MIS.2009.81
REFERENCES
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.
7 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool