没有合适的资源?快使用搜索试试~ 我知道了~
用于低资源史蒂文·瓦鲁马斯引用此版本:史蒂文·瓦鲁马斯。用于低资源微控制器的高级编程模型。计算机科学与语言[cs.CL]。索邦大学,2019年。法语。NNT:2019SORUS394。电话:02426454v2HAL ID:电话:02426454https://theses.hal.science/tel-02426454v2提交日期:2020年HAL是一个多学科的开放存取档案馆,用于存放和传播科学研究论文,无论它们是否被公开。论文可以来自法国或国外的教学和研究机构,也可以来自公共或私人研究中心。L’archive ouverte pluridisciplinaire索邦大学巴黎版(ED 130)用于低资源[美]史蒂文·瓦鲁马斯著计算机科学博士论文导演:特里斯坦·克罗拉德于2019年11月5日在巴黎公开展示和支持在陪审团面前克莱尔·佩吉蒂报告员研究硕士奥内拉艾伦·施密特报告员研究总监因里亚雷恩卡洛斯·阿贡总统教授索邦大学蒂莫西·伯克审查员研究负责人巴黎因里亚米哈埃拉·西吉雷亚努审查员会议主持人巴黎狄德罗特里斯坦·克罗拉德导演教授CNAMEmmanuel Chailoux框架教授索邦大学菲利普·特雷布谢框架会议主持人索邦大学/ANSSI谢谢你首先,我要感谢本文的作者克莱尔·帕盖蒂(Claire Pagetti)和艾伦·施密特(Alan Schmitt),感谢他们同意花一点时间(甚至可能是暑假的一部分)来审阅我的手稿,感谢他们的建设性评论和反馈。我还要感谢Mihaela Sighireanu、Carlos Agon和Timothy Bourke,感谢他们同意成为我的评审团成员,并对我的工作进行我衷心感谢我的博士生导师特里斯坦,感谢他的耐心、随时可用和广泛的科学专业知识。我意识到我很幸运能和一个在人性和专业上都无可指责的人一起我还要感谢我的主管Emmanuel和Philippe,感谢他们对我的信任,感谢他们明智的建议,感谢他们一直以来的如果没有我的经理和主管的支持,也非常感谢APR团队,这么多年来我一直有宾至如归的感觉,但现在我将不得不特别感谢那些信任我和/或建议我进行所有这些小时的教学的人在那些以前没有提到的:安尼克,帕斯卡,弗雷德里克,罗曼,安托万,唐。 而且通常都很感谢过去和现在的博士生和博士后同事,他们为实验室(有时是酒吧)的生活增添了情趣,按照伪随机的顺序,我想到了马蒂厄(D)、吉尔斯、克莱门特、马丁、拉斐尔、马蒂厄(J)、朱尔斯、布巴卡尔、易亭、雷米、文森特、阿卜杜勒拉乌夫、克里斯泰尔、阿迪拉,我不可避免地还要感谢我们伟大的经理Thuy,他的反应和他完美的幽默。感谢外面的朋友们谢谢你的倾听,建议和笑话!虽然我不能说出他们的名字,但我感谢安娜、本尼迪克特、马尔万、皮埃尔和爱丽丝。当然,我也要感谢我的姐姐和父母,他们总是比我自己更感谢他们在过去和未来的考验中不断的支持和帮助最后,感谢阿德里安,他坚定不移的信任和支持是这些年来的燃料。他的善良、他的存在和他的勇气是我的主要灵感来源让S.5目录导言91初步151.1微控制器的物理和软件特性151.1.1微控制器的组成和资源1.1.2微控制器的经典编程模型181.2材料抽象和高级211.2.1L’approche machine virtuelle1.2.2用高级语言对微控制器进行1.3同步编程281.3.1实时系统291.3.2同步假设311.3.3Esterel:一种命令式同步321.3.4Lustre和Signal:声明性同步1.4程序安全381.4.1静态类型381.4.2最坏情况下的执行时间1.4.3形式规范和元理论412OMicroB:通用OCaml432.1OCaml语言442.2ZAM:OCaml虚拟机参考512.2.1ZAM51的介绍2.2.2字节码OCaml522.2.3虚拟机的结构532.2.4值的表示542.2.5执行库2.3使用OMicroB 57编译和运行2.3.1在C 58文件中表示2.3.2字节码63的解释器2.3.3执行库2.3.4可执行文件的实现2.4OMicroB 70的优化2.4.1计划的早期评估722.4.2定制虚拟机7353OCaLustre:OCaml77中的同步编程3.1在OCaLustre77中编程3.1.1语言的语法773.1.2同步时钟833.1.3程序时钟类型3.2OCaLustre语言规范用Ott和Coq92形式化3.2.1同步程序的正规形式表示3.2.2打字和计时953.2.3程序类型规则963.2.4程序的正确时间安排规则1013.2.5操作语义1044OCaLustre109程序汇编4.1标准格式1104.2订单1124.2.1因果循环的检测1174.2.2单独编译的限制1174.3时钟推理4.4翻译为OCaml1194.5示例1235用Coq 127形式化和证明OCaLustre的性质5.1打字的翻译和更正1275.1.1使用并发语句1295.1.2使用嵌套语句1355.2时钟类型验证5.2.1良好时钟的算法规则1385.2.2从时钟验证器143提取到OCaml6OCaLustre程序最坏情况执行时间的计算6.1Coq149中方法的正式验证6.1.1理想化字节码语言的定义6.1.2删除变量1526.1.3非确定性评估1546.1.4更正证明1556.2应用于OCaLustre程序的WCET计算6.2.1指令成本的计算1596.2.2Bytecrawler:字节码160的抽象解释器6.2.3OCaLustre162编译器的专用模式6.2.4应用示例7OMicroB和OCaLustre 169的性能7.1OMicroB 169的性能指标7.1.1方法16957.1.2测试程序1717.1.3计算机执行:结果和解释1737.1.4在微控制器上执行:结果和解释1747.2OCaLustre 180的性能指标7.2.1OCaLustre181中的二进制加法器7.2.2结果1828电子装置的应用1898.1穿孔卡片阅读器1898.1.1安装1898.1.2程序1908.1.3程序的静态分析1938.1.4内存消耗1948.2巧克力搅拌机1948.2.1OCALustre196计划8.2.2相互作用8.2.3内存消耗1998.2.4模拟2008.3蛇的游戏2008.3.1Arduboy 201的解剖8.3.2电气安装程序2038.3.3游戏程序2068.3.4内存消耗209结论和展望211A OCaml 217值的表示A.1 ZAM217中的值表示A.1.132位表示217A.1.2以64位表示217A.2 OMicroB218中的值表示A.2.1以16位表示218A.2.232位表示218A.2.3以64位表示219B来自加法器221的同步清晰码C 绩效指标结果223D 应用程序代码227D.1 穿孔卡片阅读器程序227D.2 228年风暴D.2.1tempereuse.ml228D.2.2Thermo_io.ml2285D.2.3考虑加热器230的循环比D.3 蛇计划231D.3.1spi.ml231D.3.2oled.ml231D.3.3arduboy.ml233D.3.4snake.ml234D.3.5main_io.ml235网站参考239参考书目2419简介本文档的读者和其他人一样,在日常生活的典型一天中这些小尺寸(几毫米到几厘米)的电子设备实际上隐藏在我们每天使用的许多物体中,并谨慎地管理着我们生活的许多方面无论读者是乘坐公共交通工具去上班,还是乘坐自己的汽车,数百个微控制器都伴随着他的旅程,执行许多自动化它们的存在并不局限于交通工具:例如,在工作中,咖啡机、空调系统,甚至计算机外围设备(屏幕、鼠标、键盘等)。... ... )可能包含数十个,负责这些不同系统的正确操作。家用电器也不例外,因为小型和大型家用电器,如洗衣机、冰箱或微波炉,都有大量的家用电器。事实上,几乎家里的每一个房间都受到影响:收音机、闹钟、散热器、恒温器、照明系统、热水器,甚至一些玩具都一些微控制器甚至可以在你身上找到,在你口袋里的移动电话中,或者在微控制器无处不在,每天都在为我们现代生活中的各种任务做出贡献。从内部看实际上,微控制器具有算术和逻辑计算单元、一组存储器,通常由允许处理程序的动态数据的RAM和用于存储程序或某些数据的非易失性存储器组成,L’environnement d’un microcontrôleurest typiquement un montage électronique constitué de multiples composants qui permettentd’intéragir avec le monde réel : des capteurs qui communiquent au microcontrôleur des propriétés ausujet de l’environnement physique du montage (valeurs ... ... 致动器,其通过其触发(发光二极管的点亮、电动机的旋转、声音或热量的发射等)来影响. .).因此,微控制器通常是电子因此,这种装置经常被用于以下目的:1. 虽然最近的移动电话包含更强大和更复杂的片上系统,但微控制器负责诸如控制触摸屏或某些传感器之类的简介10对嵌入式系统进行编程,并管理特定FIgU rE 1微控制器的物理资源通常是有限的,类似于20世纪80年代的个人因此,微控制器的时钟频率很少超过几十兆赫,其RAM被限制在几千字节,并且其用于存储程序的闪存最在一个最新的片上系统的计算速度快100倍、存储器资源大10000倍的世界里,这些资源似乎非常不合时宜,但微控制器仍然在工业世界中非常频繁地使用:它们的低能耗和低购买成本(从十分之几欧元到几十欧元)有助于它们在许多日常用品中的普遍存在。此外,越来越多... ... )或好玩(小型游戏机、无人机、LED墙等)。在新型连接对象出现的刺激下,这些用途因此,在物联网(IoT)的推动下类似于微控制器资源类似于相对过时的传统计算机硬件的事实,微控制器的开发过程也没有随着时间的推移而改变:微控制器的编程传统上是用可以被认为是低级或非常低级的语言来完成的。他2. 十亿=1012。3. 本文档中的所有Web参考前面都将有一个表示锚点的符号。11n’est en e 因此,微控制器编程是一项困难的活动,因为它迫使开发人员熟悉目标微控制器的汇编语言的指令集,通常是非表达性的L’utilisateur se doit微控制器程序的这种极端专业化,除了测试和调试微控制器程序是一个复杂且同样具有挑战性的过程。而用于个人计算机的程序的调试因此,测试用于微控制器的程序通常等同于在其预期的实际组件上执行该程序。对于业余开发人员来说,调试微控制器程序通常包括编译它、将生成的可执行文件传输然后,此过程可以重复多次,这种耗时且不安全的做法除了极其耗时之外,还可能在一些熟悉微控制器编程的开发人员社区中,简单地使用事实上,与汇编语言相比,C语言提供了一个显著的硬件抽象层,允许简化开发和调试,并为编写的程序提供了各种保证(包括对程序类型的一些简单的静态检查),使这些程序更安全,更不容易L’utilisation de langages de relativement bas niveaucomme le C 然而,许多更高级的语言在微控制器编程的上下文中具有受欢迎的优点:事实上,除了通过使用实现高级编程范例的语言(例如面向对象编程或函数式编程)而提供的增强的表达性之外,通过使用这样的语言(例如静态或动态类型检查)而提供的保证对于嵌入式系统的编程形成了明显的优点,嵌入式系统的故障可能是危险的,并且简介12会造成灾难性的后果此外,这些语言提供的硬件抽象并不一定妨碍这些资源的合理使用:事实上,由于微控制器的存储器容量很小,因此在某些情况下,能够受益于能够根据程序的需要动态重用这些资源的执行环境是有趣的由于这些原因,已经进行了几项工作,以允许在更高级的编程语言如Java、Python或Scheme中开发嵌入式程序。D’autres solutions proposent des langages spécialisés pour la program-mation de microcontrôleurs inspirés eux mêmes de modèles de programmation de plus haut niveau,comme此外,传统上使用的通用语言不一定适应微控制器应用程序编程的固有特征因此,提供适合于这样的应用的轻量级并发编程模型对于简化这样的程序的因此,由于微控制器的资源限制及其固有特性(例如缺乏操作系统),用于对微控制器进行编程的竞争模型不能系统地模仿通常用于对然而,不太常见的并发编程模型适用于微控制器编程:特别是,同步编程模型似乎特别适合于我们,因为它能够只需要非常少的硬件资源,并且它的方法基于同步假设的简单性这种范例的优点是将此外,用于嵌入式系统(有时是关键系统)的程序通常需要事实上,微控制器的一些应用(例如无人机、运输工具或一些机器人)对应于实时系统,其中对外部刺激的反应必须在特定时间间隔内发生所施加的延迟通常对应于安全约束,并且其他约束可能涉及程序的逻辑操作,对于这些逻辑操作,可以验证表示程序正确性的某些不变量。我 们 在 一 定 程 度 上 借鉴 了 民 用 航 空 电 子 设 备 的 开 发 方 法 L’utilisation de méthodes formelles(interpré- tation ... ... 此外,还鼓励使用允许检查程序的某些属性的方法例如,现在可以用证据代替测试。13DO-178标准4.这些鲁棒的分析为关键嵌入式系统的编程提供了明确的兴趣我们的方法将高级编程模型与数据流同步编程模型相结合,使用类似的分析来检查它们的操作的正确性以及与例如同步时刻的计算时间相关的某些属性L’ambition一方面是微控制器编程的世界,其具有丰富的相对简单的应用以及业余爱好者和工业用户,但是受到硬件资源的限制,并且其开发过程通常在安全性和软件保证方面相当差。另一方面是更高级的编程模型的世界,它提供了允许更丰富的表达性和更高的安全性的抽象,但产生了潜在的资源密集型我们的方法的全部因此,我们的解决方案的目标是能够在资源非常少的硬件上执行,大约只有几千字节的这种与资源有限的微控制器兼容的愿望源于这样一个事实,即即使在今天此外,通过提供在本文详细介绍了我们的解决方案,该解决方案基于一系列抽象概念,旨在简化开发过程并确保嵌入式系统程序的正确性。特别是,我们将努力形式化我们的课程的几个方面,以及这种形式化在很大程度上是通过软件手段实现的,并且已经使用Coq证明助手[ Tea19 ]实现了与这种形式化相关的几个证明在整个手稿中陈述的程序、例子和引理和定理的证明的来源可以在网上找到。4. 有关这方面的更多信息,请参见DO-333。简介14手稿计划— 第1章介绍了微控制器编程的经典方法,以及旨在提高微控制器编程的表达性和安全性的现有工作。我们讨论了— 第2章介绍了我们的OCaml虚拟机OMicroB的实现。该虚拟机设计用于在具有显著内存限制的微控制器上执行,由于其可移植性以及OCaml语言及其运行时库的特性,构成了— 在第3章中,我们提出了OCaLustre,一个同步数据流扩展。OCaml语言。该语言扩展旨在对微控制器进行编程,并受Lustre语言的启发,为嵌入式系统的并发行为开发提供了一个简单、低功耗的编程模型。在概述了该语言的功能之后— 在第4章中,我们描述了OCaLustre程序的主要编译步骤该编译过程允许将同步代码转换为与该语言的任何编译器完全兼容的顺序OCaml程序— 在第5章中,我们介绍了形式化和验证语言规范的各种属性的方法。特别地,我们将描述用于检查OCaLustre程序与两个类型系统的一致性的方法,这两个— 第6章描述了一种计算OCaLustre程序最坏情况执行时间的方法。该方法基于对编译这样的程序后生成的字节码文件的分析,利用了我们方法的可移植性在描述实现该过程的软件原型之前,我们提供了该过程的正确性证明。— 第7章分析了本文中介绍的各种软件解决方案的性能使用实现OCaml语言的每个功能的几个示例程序,我们描述了OMicroB虚拟机的接下来,我们将详细介绍OCaLustre同步扩展的低内存占用— 第8章旨在介绍几个具体的应用程序,强调与我们的各种抽象级别和验证所执行程序的保证相关的优势特别是,它们证明了描述微控制器与其环境之间的交互的容易性,并证实了所— 最后,我们通过回顾我们在工作中提出的各种方法来结束151 初步本文提出的各种抽象化方法是基于实际考虑所驱动的技术和工艺选择本章概述了与所考虑的每一个抽象级别相关的各种现有技术解决方案在描述这些不同的作品时,我们证明了在这篇论文中所做的选择是正确的,即朝着一个方向而不是另一个方向前进因此,我们首先讨论微控制器的物理组成,以及在嵌入式应用程序编程的上下文中使用的经典编程方法。然后,我们激发了抽象的欲望。通过具有高级语言的虚拟机使用的硬件,该高级语言我们希望提供一种简单而轻量级的并发编程模型,这一点得到了使用最后,我们讨论了验证和保证由这些抽象实现的程序的某些属性的不同方法。1.1微控制器的物理和软件特性为了向读者解释与微控制器编程相关的问题和技术的特殊性,我们在本节中提供了这种通用集成电路的主要硬件方面的概述我们将简要描述通用微控制器的结构我们还讨论了传统的微控制器编程方法、与之相关的开发环境以及这些开发过程的局限性1.1.1微控制器的组成和资源微控制器由几个元件组成,使其能够执行执行微控制器的主要组件— 一种中央计算单元,或CPU(中央处理单元),其作用是执行执行程序所需的算术和逻辑计算。具有有限资源的微控制器的计算速度— 一种随机存取存储器(RAM),其中包含程序执行时生成的动态、易失性数据在本文的上下文中,RAM是1. 每秒数百万第一章。初步16当然是最有限的资源:在— 用于存储程序代码的非易失性闪存。虽然闪存在技术上可以在程序运行时写入,但由于将数据和程序分开的愿望以及其物理限制,它通常被认为是只读存储器(ROM)。实际上,闪存的最大写入次数受到限制。例如,ATmega微控制器中的闪存最多可以支持大约10,000个写入周期(取决于制造商的规格),而其RAM实际上是不可磨损的。闪存的大小通常比RAM大十到一百倍。我们正在考虑的微控制器的大小是几十千字节甚至几百千字节:例如,ATmega328P微控制器具有32KB的闪存。— 用于测量持续时间的计数器(或定时器),以便使组件的各种电子元件彼此同步这些计数器以固定的时间间隔递增每次执行程序指令时出现的内部时钟信号— 一种中断机制,一旦出现特定的内部或外部刺激,就立即触发专门程序的执行来处理它。外部中断可由引脚上电信号的出现(或变化)引起— I/O端口允许与连接到微控制器的电子该通信通过交换可变电压(例如0或5伏)的电信号来实现,使得能够表示微控制器和其环境之间的二进制信号的传输这些端口对应于从微控制器外部可见的一组金属引脚端口上的每个引脚— 某些输入/输出端口还它们能够通过时间采样将引脚端子处的电压值变化转换为模拟值。类似地,通过存在数字到模拟转换器(DAC),可以将内部数字信号转换图1.1是微控制器中主要元件之间关系的简化示意图它们之间的交互基本上是通过一个(或多个)双向总线上的值传输来实现的,例如,允许将程序指令从闪存传输1.1.微控制器的物理和软件特性17中断控制器闪光灯RAM定时器总线I/O端口CPUDAC /ADC计算RAM。FIgU rE 1.1目前市场上有几个微控制器系列。其中,VAR微控制器是业余程序员广泛使用的设备,因为它们存在于Arduino/ Genuino板中。这些卡包含微控制器和预连接到微控制器的电子元件(USB端口、重置按钮、电源插头等)。它们简化了嵌入式程序的开发过程。例如,Arduino Uno板[Bad14]包含一个ATRATmega328微控制器,具有2千字节的RAM和32千字节的闪存。 PIC微控制器不太为业余爱好者所知,但由于其低成本和高效率而被工业界广泛使用。例如,图1.2中的表格显示了几个系列的一组微控制器的物理特性,其中一些微控制器资源非常贫乏(RAM小于1千字节),而另一些微控制器的物理特性接近20世纪90年代PC的物理在我们的使用环境模型建筑记忆闪烁(KO)RAM(o)CPU速度(MIPS)紧张的功能化AT89C51英特尔8051 8位4128124至6 VATmega328pAVR - 8位322048201.8至5.5 VATmega2560AVR - 8位2568192161.8至5.5 VPIC 18F4620PIC - 8位644096102至5.5 VPIC 24FJ128GA006PIC - 16位1288192162至3.6 VSTM32 L051C8ARM - 32位648192321.65 3.6 VSTM32 F091VCT6ARM - 32位25632768482至3.6 VFIgU rE 1.2第一章。初步18因此,微控制器在结构上非常接近于个人它的应用程序与传统PC甚至单板计算机(如Raspberry Pi)的应用程序非常不同:它通常既没有操作系统,也没有文件系统,也没有键盘或鼠标等传统设备微控制器通常专用于自动化任务的控制,通常在嵌入式环境中,微控制器仅连接到特定于该任务的电子电路,并且应用程序在"裸金属"上运行:在1.1.2微控制器的经典编程模型低级别实现微控制器的应用是一项相当复杂的任务,需要开发人员熟悉所使用的硬件实际上,在嵌入式系统中,程序和硬件之间的接近性传统上导致使用低级编程语言,其对于用于应用程序嵌入式系统的应用通常是用汇编语言实现的,目的是精确地控制硬件的配置及其资源消耗因此,微控制器的选择对开发过程具有重要影响,因为可用的不同微控制器系列不共享相同的汇编指令集因此,为PIC微控制器实现的程序同一系列中微控制器之间的物理差异也会限制程序的可相对更可移植的C语言子集也通常用于嵌入式应用程序编程事实上,与汇编程序相比,C语言更强的表达能力受到嵌入式应用程序开发人员的赞赏,而其对内存资源的精细控制被认为是开发在低资源设备上运行的应用程序的然而,传统上为微控制器实现的程序例如,图1.3显示了用于ATR ATmega328P微控制器的C程序的源代码该程序以规则的间隔向引脚PB5(即,D. 微控制器端口B的引脚5),以使其所连接的发光二极管(也称为LED-发光二极管)闪烁这里需要注意的是,这种程序的可读性相当差端口B的输入或输出引脚,以及PORTB对其值的修改在一个程序更复杂的是,在这种类型的操作中,最小的错误可能很难2. L’opérateur1.1.微控制器的物理和软件特性19# ifndefF_CPU#defineF_CPU20000000UL//vitedd#endif#inc llde#includeINTMAIN(您的ID){DDRB=DDRB|0b0000100 00;//ConfigurePB5ensortieWHHE(1){PORTB=PORTB|0b0000100 00;//Al llumerPB5_delay_ms(500);//attePORTB=PORTB^0b00001000 0;//EteindrePB5_delay_ms(500);//atte}}FIgU rE 1.3一些软件库,如Arduino库,为程序员提供了C原语,允许稍微抽象这种类型的操作(例如,通过使用digitalWrite()函数,将引脚的名称和要输出的信号作为参数),但仍然相当有限,并且可以与简单的宏相媲美,使程序更容易读写,但不会为实现的程序提供额外的安全性这样的程序的可移植性开发环境中的用于实现微控制器的程序及其调试的开发环境一些专有的、通常是单平台的解决方案由制造商提供。例如,AtmelStudio[8]是一个用于AVR微控制器的IDE,提供与MPLAB相同的功能。最后一个例子是Arduino IDE [7 ],这是一个多平台应用程序,允许您为Arduino开发板编写程序,编译它们,并将生成的可执行文件图1.4显示了这些消费者工具在功能上大多相当适度:它们能够为微控制器生成可执行文件,但不一定允许正确测试所执行的程序,因为这样的程序的行为与其周围的电子组件有着内在的联系。因此,更强大的软件解决方案,如
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 5
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 展开
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
最新资源
- 十种常见电感线圈电感量计算公式详解
- 军用车辆:CAN总线的集成与优势
- CAN总线在汽车智能换档系统中的作用与实现
- CAN总线数据超载问题及解决策略
- 汽车车身系统CAN总线设计与应用
- SAP企业需求深度剖析:财务会计与供应链的关键流程与改进策略
- CAN总线在发动机电控系统中的通信设计实践
- Spring与iBATIS整合:快速开发与比较分析
- CAN总线驱动的整车管理系统硬件设计详解
- CAN总线通讯智能节点设计与实现
- DSP实现电动汽车CAN总线通讯技术
- CAN协议网关设计:自动位速率检测与互连
- Xcode免证书调试iPad程序开发指南
- 分布式数据库查询优化算法探讨
- Win7安装VC++6.0完全指南:解决兼容性与Office冲突
- MFC实现学生信息管理系统:登录与数据库操作
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功