Computer Science ›› 2019, Vol. 46 ›› Issue (5): 21-28.doi: 10.11896/j.issn.1002-137X.2019.05.003
Previous Articles Next Articles
YANG Ping1, WANG Sheng-yuan2
CLC Number:
| [1]KNIGHT J C.Safety critical systems:challenges and directions[C]∥Proceedings of the 24th International Conference on Software Engineering(ICSE 2002).2002:547-550. [2]LEROY X.Verified squared:does critical software deserve verified tools?[J].ACM SIGPLAN Notices,2011,46(1):1-2. [3]Scade-suite home[EB/OL].http://www.esterel-technologies. com/products/scade-suite. [4]CASPI P,PILAUD D,HALBWACHS N,et al.Lustre:a decla-rative language for programming synchronous systems[C]∥14th ACM Symposium on Principles of Programming Languages(POPL’87).Munchen,1987. [5]HALBWACHS N,CASPI P,RAYMOND P,et al.The synchronous dataflow programming language LUSTRE[J].Proceedings of the IEEE,1991,79(9):1305-1320. [6]HALBWACHS N.Synchronous programming of reactive sys-tems,a tutorial and commented bibliography[M]∥Tenth International Conference on Computer-Aided Verification,CAV’98.Berlin:Springer Verlag,1998. [7]HALBWACHS N.A Synchronous Language at Work:the Story of Lustre[C]∥Proceedings of the 2nd ACM/IEEE International Conference on Formal Methods and models for Co-Design,MEMOCODE’05.IEEE Computer Society,Washington,DC,USA,2005. [8]BENVENISTE A,CASPI P,EDWARDS S A,et al.The Syn-chronous Languages Twelve Years Later[J].Proceedings of the IEEE,2003,91(1):64-83. [9]MILNER R.Calculi for synchrony and asynchrony[J].Theoretical Computer Science,1983,25(3):267-310. [10]BERRY G,GONTHIER G.The Esterel synchronous programming language:Design,semantics,implementation[J].Science of Computer Programming,1992,19(2):87-152. [11]BERRY G,The foundations of ESTEREL[M]∥proof,language and interaction:essays in honour of Robin Milner.Cambridge:MIT Press,2000:425-454. [12]GUERNIC P L,GAUTIER T,BORGNE M L,et al.Programming real time applications with SIGNAL[J].Proceedings of the IEEE,1991,79(9):1321-1336. [13]LE GUERNIC P,TALPIN J P,LE LANN J C.Polychrony for system design[J].Journal for Circuits,Systems and Computers,2002,12(3):261-304. [14]LUCID SYNCHRONE home[EB/OL].http://www.di.ens. fr/~pouzet/lucid-synchrone. [15]WADGE W W,ASHCROFT E A.LUCID,the dataflow pro-gramming language[M].Academic Press Professional,San Diego,CA,USA,1985. [16]ASHCROFT E A,WADGE W W.Lucid,a non procedural language with iteration[J].Communications of the ACM,1977,20(7):519-526. [17]SCHNEIDER K.The synchronous programming languageQuartz:Internal Report 375[R].Department of Computer Scien-ce,University of Kaiserslautern,Kaiserslautern,Germany,2009. [18]MARANINCHI F.the ARGOS language:graphical representation of automata and description of reactive systems[C]∥IEEE Workshop on Visual Languages.Kobe,Japan,1991. [19]HAREL D,STATECHARTS A.A visual formalism for complex systems[J].Science of Computer Programming,1987,8(3):231-274. [20]ANDRÉC.Computing SyncCharts reactions[M]∥Synchronous Languages,Applications,and Programming (SLAP’03),Electronic Notes in Theoretical Computer Science.Porto,Portugal,2003:3-19. [21]DAVID R.Grafcet:A Powerful Tool[J].IEEE Transactions on Control Systems Technology,1995,3(3):253-268. [22]GCC.the GNU Compiler Collection[EB/OL].http://gcc.gnu.org. [23]The Plum Hall Validation Suite for CTM [EB/OL].http://www.plumhall.com/stec.html. [24]Lustre V6[EB/OL].http://www-verimag.imag.fr/Lustre-V6.html. [25]YANG X J,CHEN Y,EIDE E,et al.Finding and understanding bugs in C compilers[C]∥Proceedings of the 2011 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2011).2011:283-294. [26]http://www.commoncriteriaportal.org/cc. [27]Summary of Difference Between DO-178B and DO-178C[EB/OL].http://faaconsultants.com/html/do-178c.html. [28]LEROY X.Formal verification of a realistic compiler[J].Communications of the ACM,2009,52(7):107-115. [29]MORRISETT G.Technical Perspective:A Compiler’s Story[J].Communications of the ACM,2009,52(7):106-106. [30]LEROY X.Formal certification of a compiler back-end or:programming a compiler with a proof assistant[J].Proceedings of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages,2006,41(1):42-54. [31]PNUELI A,SIEGEL M,SINGERMAN E.Translation Validation[C]∥Proceedings of TACAS’98.1998:151-166. [32]NECULA G C,LEE P.The design and implementation of a certifying compiler[C]∥Proc.Conf.Programming Language Design and Implementation.1998:333-344. [33]TRISTAN J B,PAUL G,GREG M.Forthcoming.Evaluatingvalue-graph translation validation for LLVM[C]∥Proceedings of the 32nd ACM SIGPLAN Conference on Programming and Language Design Implementation.2011:295-305. [34]KANADE A,SANYAL A,KHEDKER U.A PVS based framework for validating compiler optimizations[C]∥4th Software Engineering and Formal Methods.IEEE Computer Society,2006:108-117. [35]NECULA G C.Translation validation for an optimizing compiler[M]∥Programming Language Design and Implementation 2000.ACM Press,2000:83-95. [36]TRISTAN J B,LEROY X.Verified validation of lazy code motion[C]∥PLDI.2009:316-326. [37]TRISTAN J B,LEROY X.A simple,verified validator for software pipelining[C]∥POPL.2010:83-92. [38]TRISTAN J B,LEROY X.Formal verification of translationvalidators:A case study on instruction scheduling optimizations[C]∥35th symposium Principles of Programming Languages.ACM Press,2008:17-27. [39]RYABTSEV M,STRICHMAN O.Translation validation:From simulink to c∥Proceedings of the 21st International Conference on Computer Aided Verification(CAV 2009).Berlin:Springer,2009:696-701. [40]GIMENEZ E,LEDINOT E.Certication de SCADE V3,Rapport final du project GENIE II,Verilog SA (Janvier 2000). [41]PAULIN C,POUZET M.Certified compilation of scade/lustre[EB/OL].http://www.lri.fr/paulin/lustreincoq.pdf,2006. [42]BERTAILS A,BIERNACKI D,PAULIN C,et al.A certified compiler for the synchronous language Lustre[EB/OL].http://users.dimi.uniud.it/types07/slides/Bertails.pdf. [43]BIERNACKI D,COLACO J L,HAMON G,et al.Clock-directed Modular Code Generation of Synchronous Data-flow Languages[C]∥ACM International Conference on Languages,Compilers,and Tools for Embedded Systems(LCTES).Tucson,Arizona,2008. [44]BIERNACKI D,COLACO J L,POUZET M.Clock-directedModular Code Generation from Synchronous Block Diagrams[C]∥Workshop on Automatic Program Generation for Embedded Systems(APGES 2007).Salzburg,Austria,2007. [45]AUGER C.Compilation Certifiée de SCADE/LUSTRE[D]. Université Paris Sud,2013. [46]AUGER C,COLAÇOB J L,HAMON G,et al.A Formalization and Proof of a Modular Lustre Compiler[EB/OL].http://www.di.ens.fr/~pouzet/cours/mpri/cours4/scp12.pdf. [47]BOURKE T,BRUN L,DAGAND P é,et al.A Formally Verified Compiler for Lustre[C]∥Proceedings of the Programming Language Design and Implementation.2017:586-601. [48]SHI G,WANG S Y,DONG Y,et al.Construction for the Trustworthy Compiler of a Synchronous Data-Flow Language[J].Journal of Software,2014,25(2):341-356.(in Chinese)石刚,王生原,董渊.同步数据流语言可信编译器的构造[J].软件学报,2014,25(2):341-356. [49]SHANG S,GAN Y K,SHI G,et al.Key Translations of the Trustworthy Compiler L2C and Its Design and Implementation[J].Journal of Software,2017,28(5):1233-1246.(in Chinese)尚书,甘元科,石刚,等.可信编译器L2C的核心翻译步骤及其设计与实现[J].软件学报,2017,28(5):1233-1246. [50]Lustre V6 reference manual[EB/OL].http://www-verimag. imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/doc/lv6-ref-man.pdf. [51]Open L2C home[EB/OL].http://soft.cs.tsinghua.edu.cn:8000/. [52]The Coq Development Team.The Coq Proof Assistant Refe-rence Manual Version V8.3[EB/OL].http://coq.inria.fr/. [53]BERTOT Y,CASTÉRAN P.Interactive Theorem Proving and Program Development-Coq’Art:The Calculus of Inductive Constructions[M]∥Texts in Theoretical Computer Science.Sprin-ger Verlag,2004. [54]BLAZY S,LEROY X.Mechanized semantics for the Clight subset of the C language[J].Journal of Automated Reasoning,2009,43(3):263-288. [55]PNUELI A,SHTRICHMAN O,SIEGEL M.Translation validation for synchronous languages[C]∥Proceedings of ICALP’1998.Berlin:Springer,1998:235-246. [56]PNUELI A,SIEGEL M,SHTRICHMAN O.The code validation tool(CVT)- automatic verification of a compilation process[J].Journal of Software Tools for Technology Transfer(STTT),1999,2(2):192-201. [57]NGO V C,TALPI J P,GAUTIER T.Formal Translation validation for clock transformations in a synchronous compiler[C]∥International Conference on Fundamental Approaches to Software Engineering(ETAPS/FASE’15).Springer,2015. [58]NGO V C,TALPIN J P,GAUTIER T,et al.Formal verification of synchronous data-flow program transformations toward certified compilers[J].Frontiers of Computer Science,2013,7(5):598-616. [59]NGO V C,TALPI J P,GAUTIER T,et al.Formal Verification of Compiler Transformations on Polychronous Equations[M]∥IFM 2012.Berlin:Springer,2012:113-127. [60]NGO V C,TALPI J P,GAUTIER T,et al.Modular translation validation of a full-sized synchronous compiler using off-the-shelf verification tools (abstract)[C]∥International Workshop on Software and Compilers for Embedded Systems (SCOPES’15).ACM,2015:109-112. [61]NGO V C,TALPI J P,GAUTIER T.Translation Validation for Synchronous Data-flow Specification in the SIGNAL Compiler[C]∥International Conference on Formal Techniques for Distributed Objects,Components and Systems (FORTE’15).IFIP,2015:66-80. [62]DUTERTRE B,DE MOURA L.Yices sat-solver[EB/OL].http://yices.csl.ri.com,2009. [63] KAHN G.The semantics of a simple language for parallel programming[M]∥Information Processing 74 Congress.North-Holland Publishing Compmany,Amsterdam,1974. [64]CASPI P,POUZET M.Synchronous Kahn networks[C]∥Proceedings of the first ACM SIGPLAN International Conference on Functional Programming (ICFP’96).Philadelphia,Pennsylvania,1996:226-238. [65]COHEN A,DURANTON M,EISENBEIS M,et al.N-Sychronous Kahn Networks[C]∥33th ACM Symp.on Principles of Programming Languages (PoPL’06).Charleston,South Carolina,2006:180-193. [66]PAULIN-MOHRING C.Kahn Networks in Coq[EB/OL].http://www.lri.fr/~paulin/KahnNetworks/library.pdf. [67]PAULIN-MOHRING C.A constructive denotational semantics for Kahn networks in Coq[M]∥From Semantics to Computer Science.Essays in Honour of Gilles Kahn,2009:383-414. [68]KAHN G.Elements of domain theory[EB/OL].http://coq.inria.fr/pylons/contribs/view/DomainTheory/trunk. [69]CASPI P,POUZET M.A co-iterative characterization of syn-chronous stream functions.[J].Electronic Notes in Theoretical Computer Science,1998,11(4):1-21. [70]BOULMÉ S,HAMON C.Certifying Synchrony for Free[C]∥International Conference on Logic for Programming,Artificial Intelligence and Reasoning (LPAR).La Havana,Cuba,Springer Verlag,2001. [71]Lucid-Synchrone in Coq[EB/OL].http://www.di.ens.fr/~pouzet/lucid-synchrone/lucid_in_coq. [72]COHEN A,DURANTON M,EISENBEIS C,et al.Synchronization of Periodic Clocks[C]∥ACM Conf.on Embedded Software (EMSOFT'05).Jersey City,New York,2005:339-342. [73]COHEN A,MANDEL L,PLATEAU F,et al.Abstraction of Clocks in Synchronous Data-flow Systems[C]∥The Sixth ASIAN Symposium on Programming Languages and Systems (APLAS).2008. [74]DELAVAL G,GIRAULT A,POUZET M.A Type System for the Automatic Distribution of Higher-order Synchronous Dataflow Programs[C]∥ACM International Conference on Languages,Compilers,and Tools for Embedded Systems (LCTES).Tucson,Arizona,2008. [75]SCHNEIDER K,BRANDT J,SCHUELE T.A Verified Compi-ler for Synchronous Programs with Local Declarations[J].Electronic Notes in Theoretical Computer Science,2006,153(4):71-97. [76]HOL[EB/OL].http://www.cl.cam.ac.uk/research/hvg/HOL. [77]ZHANG Y.Source code to unify nested clocks in a lustre-like language[EB/OL].https://github.com/yczhang89/unify-clock. [78]SHI G,ZHANG Y C,SHANG S,et al.A Formally Verified Transformation to Unify Multiple Nested Clocks for a Lustre-like Language[J].Science China Information Sciences,2019,62(1):012801:1-012801:3. [79]GAN Y K,ZHANG L B,SHI G,et al.A Verified Sequentializer for Synchronous Data-Flow Programs[J].Computer Applications and Software,2014,31(5):1-5.(in Chinese)甘元科,张玲波,石刚,等.同步数据流程序的可信排序[J].计算机应用与软件,2014,31(5):1-5. [80]ZHANG L B,GAN Y K,SHI G,et al.A certified translation for eliminating temporal feature of a synchronize dataflow program[J].Computer Engineering and Design,2014,35(1):137-143.(in Chinese)张玲波,甘元科,石刚,等.同步数据流语言时态消去的可信翻译[J].计算机工程与设计,2014,35(1):137-143. [81]LIU Y,YANG F,SHI G,et al.Brief Overview of Translation Validation Method in Trusted Compiler Construction[J].Computer Science,2014,41(S1):334-338.(in Chinese)刘洋,杨斐,石刚,等.可信编译器构造的翻译确认方法简述[J].计算机科学,2014,41(S1):334-338. [82]SHI G,GAN Y K,SHANG S,et al.A formally verified sequentializer for lustre-like concurrent synchronous data-flow programs[C]∥Proceedings-2017 IEEE/ACM 39th International Conference on Software Engineering Companion(ICSE-C).2017:109-111. [83]LIU Y,GAN Y K,WANG S Y,et al.Trustworthy Translation for Eliminating High-Order Operation of a Synchronous Dataflow Language[J].Journal of Software,2015,26(2):332-347.(in Chinese)刘洋,甘元科,王生原,等.同步数据流语言高阶运算消去的可信翻译[J].软件学报,2015,26(2):332-347. |
| [1] | YIN Wen-bing, GAO Ge, ZENG Bang, WANG Xiao, CHEN Yi. Speech Enhancement Based on Time-Frequency Domain GAN [J]. Computer Science, 2022, 49(6): 187-192. |
| [2] | OUYANG Zhuo, ZHOU Si-yuan, LYU Yong, TAN Guo-ping, ZHANG Yue, XIANG Liang-liang. DRL-based Vehicle Control Strategy for Signal-free Intersections [J]. Computer Science, 2022, 49(3): 46-51. |
| [3] | WU Li-bo, HUANG Yu-fang. Logical Reasoning Based on DNA Strand Displacement [J]. Computer Science, 2022, 49(1): 259-263. |
| [4] | WANG Chao, WEI Xiang-lin, TIAN Qing, JIAO Xiang, WEI Nan, DUAN Qiang. Feature Gradient-based Adversarial Attack on Modulation Recognition-oriented Deep Neural Networks [J]. Computer Science, 2021, 48(7): 25-32. |
| [5] | GUO Fu-min, ZHANG Hua, HU Rong-hua, SONG Yan. Study on Method for Estimating Wrist Muscle Force Based on Surface EMG Signals [J]. Computer Science, 2021, 48(6A): 317-320. |
| [6] | LI Da, LEI Ying-ke, ZHANG Hai-chuan. Outdoor Fingerprint Positioning Based on LTE Networks [J]. Computer Science, 2021, 48(6A): 404-409. |
| [7] | HU De-feng, ZHANG Chen-xi, WANG Shi-tao, ZHAO Qin-pei, LI Jiang-feng. Intelligent Prediction Model of Tool Wear Based on Deep Signal Processing and Stacked-ResGRU [J]. Computer Science, 2021, 48(6): 175-183. |
| [8] | WU Guang-zhi, GUO Bin, DING Ya-san, CHENG Jia-hui, YU Zhi-wen. Cognitive Mechanisms of Fake News [J]. Computer Science, 2021, 48(6): 306-314. |
| [9] | WANG Ying-ying, CHANG Jun, WU Hao, ZHOU Xiang, PENG Yu. Intrusion Detection Method Based on WiFi-CSI [J]. Computer Science, 2021, 48(6): 343-348. |
| [10] | WANG Xing , KANG Zhao. Smooth Representation-based Semi-supervised Classification [J]. Computer Science, 2021, 48(3): 124-129. |
| [11] | ZHOU Jun, YIN Yue, XIA Bin. Acoustic Emission Signal Recognition Based on Long Short Time Memory Neural Network [J]. Computer Science, 2021, 48(11A): 319-326. |
| [12] | WANG Xin-ping, XIA Chun-ming, YAN Jian-jun. Sign Language Recognition Based on Image-interpreted Mechanomyography and Convolution Neural Network [J]. Computer Science, 2021, 48(11): 242-249. |
| [13] | JIN Wen-qing and HAN Fang. Main Melody Extraction Method Based on Saliency Enhancement [J]. Computer Science, 2020, 47(6A): 24-28. |
| [14] | LUO Jia-lei and MENG Li-min. Signal Timing Scheme Recommendation Algorithm Based on Intersection Similarity [J]. Computer Science, 2020, 47(6A): 66-69. |
| [15] | CHEN Jin-yin, CHENG Kai-hui and ZHENG Hai-bin. Deep Learning Based Modulation Recognition Method in Low SNR [J]. Computer Science, 2020, 47(6A): 283-288. |
|
||
Home