数字交通规则的语义一致性与正确性验证

Lei Wan, Changjun Wang, Daxin Luo, Hang Liu, Sha Ma, Weichao Hu

工程（英文） ›› 2024, Vol. 33 ›› Issue (2) : 47-62.

PDF(3630 KB)
PDF(3630 KB)
工程（英文） ›› 2024, Vol. 33 ›› Issue (2) : 47-62. DOI: 10.1016/j.eng.2023.04.016
研究论文
Article

数字交通规则的语义一致性与正确性验证

作者信息 +

Semantic Consistency and Correctness Verification of Digital Traffic Rules

Author information +
History +

Abstract

The consensus of the automotive industry and traffic management authorities is that autonomous vehicles must follow the same traffic laws as human drivers. Using formal or digital methods, natural language traffic rules can be translated into machine language and used by autonomous vehicles. In this paper, a translation flow is designed. Beyond the translation, a deeper examination is required, because the semantics of natural languages are rich and complex, and frequently contain hidden assumptions. The issue of how to ensure that digital rules are accurate and consistent with the original intent of the traffic rules they represent is both significant and unresolved. In response, we propose a method of formal verification that combines equivalence verification with model checking. Reasonable and reassuring digital traffic rules can be obtained by utilizing the proposed traffic rule digitization flow and verification method. In addition, we offer a number of simulation applications that employ digital traffic rules to assess vehicle violations. The experimental findings indicate that our digital rules utilizing metric temporal logic (MTL) can be easily incorporated into simulation platforms and autonomous driving systems (ADS).

Keywords

Autonomous driving / Traffic rules / Digitization / Formalization / Verification

引用本文

EndNote

Ris (Procite)

Bibtex

导出引用
Lei Wan, Changjun Wang, Daxin Luo. . Engineering. 2024, 33(2): 47-62 https://doi.org/10.1016/j.eng.2023.04.016

参考文献

原文顺序 | 文献年度倒序 | 文中引用次数倒序
[1]
J. Claybrook, S. Kildare. Autonomous vehicles: no driver…no regulation?. Science, 361 (6397) (2018), pp. 36-37
[2]
M.L. Cummings, D. Britton. Regulating safety-critical autonomous systems: past, present, and future perspectives. R. Pak, E.J. de Visser, E. Rovira (Eds.), Living with robots, Academic Press, London (2019)
[3]
G.S. Nair, C.R. Bhat. Sharing the road with autonomous vehicles: perceived safety and regulatory preferences. Transp Res Part C, 122 (2021), Article 102885
[4]
D.W. Otter, J.R. Medina, J.K. Kalita. A survey of the usages of deep learning for natural language processing. IEEE Trans Neural Netw Learn Syst, 32 (2) (2021), pp. 604-624
[5]
E. Kumar. Natural language processing. IK International Pvt Ltd, New Delhi (2011)
[6]
R. Grishman. Computational linguistics:an introduction. Cambridge University Press, Cambridge (1986)
[7]
X. Liu, D. Wu. From natural language to programming language. S. Goschnick (Ed.), Innovative methods, user-friendly tools, coding, and design approaches in people-oriented programming, IGI Global, Hershey (2018)
[8]
Z. Manna, A. Pnueli. The temporal logic of reactive and concurrent systems. Springer, Berlin (1992)
[9]
A. Pnueli. The temporal logic of programs. Proceedings of the 18th Annual Symposium on Foundations of Computer Science (sfcs 1977); 1977 Oct 31-Nov 1; Providence, RI, USA, IEEE, New York City (1977), pp. 46-57
[10]
E.M. Clarke, E.A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. Proceedings of the Workshop on Logic of Programs; 1981 May 4-6; New York City, NY, USA, Springer, Berlin (1981), pp. 52-71
[11]
E.A. Emerson, J.Y. Halpern. “Sometimes” and “not never” revisited: on branching versus linear time temporal logic. J Assoc Comput Mach, 33 (1) (1986), pp. 151-178
[12]
R. Alur, T.A. Henzinger. A really temporal logic. J Assoc Comput Mach, 41 (1) (1994), pp. 181-203
[13]
R. Alur, T.A. Henzinger. Real-time logics: complexity and expressiveness. Inf Comput, 104 (1) (1993), pp. 35-77
[14]
R. Koymans. Specifying real-time properties with metric temporal logic. Real Time Syst, 2 (4) (1990), pp. 255-299
[15]
R. Alur, T. Feder, T.A. Henzinger. The benefits of relaxing punctuality. J Assoc Comput Mach, 43 (1) (1996), pp. 116-146
[16]
J. Ouaknine, J. Worrell. On the decidability of metric temporal logic. Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS’05); 2005 Jun 26-29; Washington, DC, USA, IEEE, New York City (2005), pp. 188-197
[17]
S. Konur. A survey on temporal logics for specifying and verifying real-time systems. Front Comput Sci, 7 (3) (2013), pp. 370-403
[18]
A. Rizaldi, M. Althoff. Formalising traffic rules for accountability of autonomous vehicles. Proceedings of the 2015 IEEE 18th International Conference on Intelligent Transportation Systems; 2015 Sep 15-18; Gran Canaria, Spain, IEEE, New York City (2015), pp. 1658-1665
[19]
K. Esterle, L. Gressenbuch, A. Knoll. Formalizing traffic rules for machine interpretability. Proceedings of the 2020 IEEE 3rd Connected and Automated Vehicles Symposium (CAVS); 2020 Oct 4-5; Victoria, BC, Canada, IEEE, New York City (2020), pp. 1-7
[20]
S. Maierhofer, A.K. Rettinger, E.C. Mayer, M. Althoff. Formalization of interstate traffic rules in temporal logic. Proceedings of the 2020 IEEE Intelligent Vehicles Symposium (IV); 2020 Oct 19-Nov 13; Las Vegas, NV, USA, IEEE, New York City (2020), pp. 752-759
[21]
A. Karimi, P.S. Duggirala. Formalizing traffic rules for uncontrolled intersections. Proceedings of the 2020 ACM/IEEE 11th International Conference on Cyber-Physical Systems (ICCPS 2020); 2020 Apr 21-25; Sydney, NSW, Australia, IEEE, New York City (2020), pp. 41-50
[22]
H. Beck, T. Eiter, T. Krennwallner. Inconsistency management for traffic regulations: formalization and complexity results. Proceedings of the 13th European Workshop on Logics in Artificial Intelligence; 2012 Sep 26-28; Toulouse, France, Springer, Berlin (2012), pp. 80-93
[23]
H. Krasowski, M. Althoff. Temporal logic formalization of marine traffic rules. Proceedings of the 2021 IEEE Intelligent Vehicles Symposium (IV); 2021 Jul 11- 17; Nagoya, Japan, IEEE, New York City (2021), pp. 186-192
[24]
K. Esterle, V. Aravantinos, A. Knoll. From specifications to behavior: maneuver verification in a semantic state space. Proceedings of the 2019 IEEE Intelligent Vehicles Symposium (IV); 2019 Jun 9-12; Paris, France, IEEE, New York City (2019), pp. 2140-2147
[25]
Hannah D, Edwards P, Khastgir S. Extended updated proposal for an approach to defining rules of the road. In: In: Proceedings of the 27th UNECE Functional Requirements for Automated and Autonomous Vehicles (FRAV) Session; 2022 Apr 19-20; online. Coventry: The University of Warwick; 2022.
[26]
P. Bjesse. What is formal verification?. ACM SIGDA Newsletter, 35 (24) (2005), pp. 1-34
[27]
L.C. Paulson. The foundation of a generic theorem prover. J Autom Reason, 5 (3) (1989), pp. 363-397
[28]
E.M. Clarke, O. Grumberg, D. Kroening, D. Peled, H. Veith. Model checking. (2nd ed.), The MIT Press, Cambridge (2018)
[29]
C. Baier, J.P. Katoen. Principles of model checking. The MIT Press, Cambridge (2008)
[30]
W. Visser, K. Havelund, G. Brat, S.J. Park, F. Lerda. Model checking programs. Autom Softw Eng, 10 (2) (2003), pp. 203-232
[31]
S.Y. Huang, K.T.T. Cheng. Formal equivalence checking and design debugging. Springer Science & Business Media, Berlin (2012)
[32]
R. Alur, T.A. Henzinger. Logics and models of real time: a survey. Proceedings of the Symposium of the REX Project (Research and Education in Concurrent Systems); 1991 Jun 3-7; Mook, The Netherlands, Springer, Berlin (1991), pp. 74-106
[33]
J. Ouaknine, J. Worrell. Some recent results in metric temporal logic. Proceedings of the 6th International Conference on Formal Modeling and Analysis of Timed Systems; 2008 Sep 15-17; Saint Malo, France, Springer, Berlin (2008), pp. 1-13
[34]
National People’s Congress. Road traffic safety law of the People’s Republic of China. Standing Committee of the National People’s Congress, Beijing (2003)Chinese
[35]
State Council of the People’s Republic of China. [Regulations on the implementation of the road traffic safety law of the People’s Republic of China]. Standing Committee of the National People’s Congress, Beijing (2004)Chinese
[36]
The Ministry of Public Security of the People’s Republic of China. GA/T 1773.1-2021: Operating specifications for safe and civilized motor vehicle drivers. Beijing: The Ministry of Public Security of the People’s Republic of China; 2021. Chinese.
[37]
E.S. Ulmasovna. The principal use of propositional and suppositional terms in the sentences. JournalNX, 6 (11) (2020), pp. 242-243
[38]
M. Scholtes, L. Westhofen, L.R. Turner, K. Lotto, M. Schuldes, H. Weber, et al.. 6-layer model for a structured description and categorization of urban traffic and environment. IEEE Access, 9 (2021), pp. 59131-59147
[39]
W. Van Winsum, A. Heino. Choice of time-headway in car-following and the role of time-to-collision information in braking. Ergonomics, 39 (4) (1996), pp. 579-592
[40]
Ayres TJ, Li L, Schleuning D, Young D. Preferred time-headway of highway drivers. In: Proceedings of the ITSC 2001. 2001 IEEE Intelligent Transportation Systems; 2001 Aug 25-29; Oakland, CA, USA. New York City: IEEE; 2001. p. 826-9.
[41]
A. Rizaldi, J. Keinholz, M. Huber, J. Feldle, F. Immler, M. Althoff, et al.. Formalising and monitoring traffic rules for autonomous vehicles in Isabelle/HOL. Proceedings of the International Conference on Integrated Formal Methods; 2017 Sep 20-22; Turin, Italy, Springer, Turin, Italy. Berlin (2017), pp. 50-66
[42]
P. Schnoebelen. The complexity of temporal logic model checking. Proceedings of the 4th Advances in Modal Logic Conference (AiML 2002); 2002 Sep 30-Oct 2, King’s College Publications, Toulouse, France. London (2003)
[43]
H. Habrias, M. Frappier. Software specification methods—an overview using a case study. Springer, Berlin (2012)
[44]
Kuppe MA, Lamport L, Ricketts D. The TLA+ toolbox. 2019. arXiv:1912.10633.
[45]
L. Lamport. Specifying systems:the TLA+ language and tools for hardware and software engineers. Addison-Wesley Professional, Boston (2002)
[46]
G. O’Regan. Concise guide to formal methods. Springer, New York City (2017)
[47]
Foster H, Uchitel S, Magee J, Kramer J. LTSA-WS: a tool for model-based verification of web service compositions and choreography. In: Osterweil LJ, Rombach HD, Soffa ML, editors. Proceedings of the 28th International Conference on Software Engineerin; 2006. p. 771-4.
[48]
G.J. Holzmann. The model checker SPIN. IEEE Trans Softw Eng, 23 (5) (1997), pp. 279-295
[49]
M. Kwiatkowska, G. Norman, D. Parker. PRISM: probabilistic symbolic model checker. Proceedings of the International Conference on Modelling Techniques and Tools for Computer Performance Evaluation; 2002 Apr 14-17, Springer, London, UK. Berlin (2002), pp. 200-204
[50]
Association for Standardization of Automation and Measuring Systems (ASAM e.V.). ASAM OpenDRIVE® V1.8.0 [Internet]. Hoehenkirchen: ASAM e.V.; 2021 Aug 3 [cited 2023 May 13]. Available from:
[51]
Association for Standardization of Automation and Measuring Systems (ASAM e.V.). ASAM OpenSCENARIO® V1.2.0 [Internet]. Hoehenkirchen: ASAM e.V.; 2022 May 13 [cited 2023 May 13]. Available from:
[52]
Z. Wu, M. Yao, H. Ma, W. Jia. Improving accuracy of the vehicle attitude estimation for low-cost INS/GPS integration aided by the GPS-measured course angle. IEEE Trans Intell Transp Syst, 14 (2) (2013), pp. 553-564
[53]
X. Xia, E. Hashemi, L. Xiong, A. Khajepour, N. Xu. Autonomous vehicles sideslip angle estimation: single antenna GNSS/IMU fusion with observability analysis. IEEE Internet Things J, 8 (19) (2021), pp. 14845-14859
[54]
K.M. Lynch, F.C. Park. Modern robotics. Cambridge University Press, Cambridge (2017)
PDF(3630 KB)

Accesses

Citation

Detail
段落导航
相关文章

/

〈 〉