云南高校图书馆联盟文献共享服务平台- LUSTRE

LUSTRE: 作品数：78被引量：73H指数：5; 导出分析报告; 相关领域：自动化与计算机技术更多>>; 相关作者：钱迎进周恩强程耀东汪璐吴庆波更多>>; 相关机构：国防科学技术大学中国科学院江南计算技术研究所华中科技大学更多>>; 相关期刊：更多>>; 相关基金：国家自然科学基金国家高技术研究发展计划国家重点基础研究发展计划国家科技重大专项更多>>

面向Lustre集群存储的错误日志分析及系统优化: 《计算机科学》2022年第10期1-9,共9页程稳李焱曾令仿王芳唐士程杨力平冯丹曾文君; 国家自然科学基金重点项目(61832020);国家自然科学基金创新研究群体项目(61821003);之江实验室中心自设科研项目(2021DA0AM01)。; 集群存储系统的错误日志信息有助于优化存储系统的可用性和稳定性。现有存储系统错误探究主要针对单机存储系统或集群存储系统的部分功能进行分析评估,缺乏在实际应用场景下,同一生产环境中,长时间、多视角的探究工作。新型功能模块的...; 关键词：LUSTRE文件系统日志分析系统优化错误可靠性

On the use of formal methods to model and verify neuronal archetypes: 《Frontiers of Computer Science》2022年第3期101-122,共22页Elisabetta DE MARIA Abdorrahim BAHRAMI Thibaud L'YVONNET Amy FELTY Daniel GAFFÉ Annie RESSOUCHE Franck GRAMMONT; This work was supported by the French government through the UCA-Jedi project managed by the National Research Agency(ANR-15-IDEX-01);in particular,by the interdisciplinary Institute for Modeling in Neuroscience and Cognition(NeuroMod)of the UniversitéCôte d'Azur.It was also supported by the Natural Sciences and Engineering Research Council of Canada.; Having a formal model of neural networks can greatly help in understanding and verifying their properties,behavior,and response to external factors such as disease and medicine.In this paper,we adopt a formal model to...; 关键词：neuronal networks leaky integrate and fire modeling synchronous languages model checking theorem proving LUSTRE COQ formal methods

面向Lustre集群存储的应用日志分析及系统自动优化框架被引量：2: 《计算机工程与科学》2022年第4期594-604,共11页程稳李焱曾令仿王芳唐士程杨力平冯丹曾文君; 国家自然科学基金(61832020);创新研究群体项目(61821003);浙江省“万人计划”(2021R2007);之江实验室自设科研项目(2021DA0AM01)。; 在科学计算、大数据处理和人工智能等领域,对相关应用负载进行研究,分析负载I/O模式,揭示应用负载变迁规律等,对指导集群存储系统性能优化十分重要。当前应用种类繁多并且应用快速迭代更新,复杂的环境使得对应用负载的特性挖掘充满挑战...; 关键词：LUSTRE文件系统日志分析系统优化服务质量资源管理

AWS中国区上线新存储服务,持续拓展广度与深度: 《中国信息化》2020年第12期10-10,共1页石菲; 数据就像石油,成为新时代最宝贵的资产。但和石油不同,数据成为资产有一个前提,那就是需要正确使用数据。如何存储呈爆发性增长的数据,并正确地使用、分析他们,成为新时代的新需求。2020年11月10日,亚马逊云服务(AWS)宣布,AWS中国(宁夏...; 关键词：文件存储存储服务 AWS AMAZON LUSTRE WINDOWS 爆发性增长 FILE

在可信编译器设计中实践CompCert编译器的语法分析器形式化验证过程被引量：2: 《计算机科学》2020年第6期8-15,共8页李凌李璜华王生原; 核高基重大专项(2017ZX01030-301-003)。; Jourdan等在其2012年发表的论文“Validating LR(1)Parsers”中提出了一种形式化验证语法分析器的方法,并将其成功地应用于CompCert编译器(2.3以上版本)的语法分析器验证中。借助这种方法,文中完成了L2C项目中的Lustre*语言语法分析器...; 关键词：语法分析 LR(1)分析器形式化验证 Lustre*语言 CompCert COQ

Lustre语言可信代码生成器研究进展被引量：1: 《仪器仪表用户》2020年第5期68-72,共5页兰林马权侯荣彬蒋维杨斐; 安全攸关的嵌入式领域广泛使用基于Lustre语言描述的图形化逻辑。工程师通过图形化逻辑建模工具编写控制逻辑,再通过代码生成器把控制逻辑转换成可执行代码下装到嵌入式设备中运行。因此,如何保证代码生成器生成代码的正确性成为关注的...; 关键词：可信代码生成 LUSTRE 形式化验证定理证明翻译验证安全攸关

同步语言Lustre的编译前端的设计与实现被引量：2: 《计算机技术与发展》2020年第2期33-36,共4页宋宇婷孙小祥冉丹; 国家自然科学基金(U1533130); 同步语言Lustre所描述的反应系统通常应用在航空航天、国防建设等领域,对系统的正确性和安全性都要求很高。如果系统在运行时出现了正确性问题,很可能会导致系统崩溃,产生非常严重的后果。系统中的任何一个词法错误或者语法错误都应该...; 关键词：同步语言Lustre 正确性编译器前端 C++语言抽象语法树

同步数据流语言可信编译器的研究进展被引量：5: 《计算机科学》2019年第5期21-28,共8页杨萍王生原; 国家民用飞机重大专项项目基金(MJ-2015-D-066);核高基重大专项(2017ZX01030-301-003)资助; 同步数据流语言(如Lustre,Signal)近年来在航空、高铁、核电等安全关键领域得到了广泛应用,因此与这类语言相关的开发工具本身的安全性问题受到高度关注。同步数据流语言到串行命令式语言的可信编译器是此类工具的典型代表(如Scade)。...; 关键词：同步数据流语言经过验证的编译器翻译确认 LUSTRE SIGNAL

A formally verified transformation to unify multiple nested clocks for a Lustre-like language被引量：1: 《Science China(Information Sciences)》2019年第1期204-206,共3页Gang SHI Yucheng ZHANG Shu SHANG Shengyuan WANG Yuan DONG Pen-Chung YEW; supported by National Natural Science Foundation of China (Grant Nos. 61272086, 61462086, MJ-2015-D-066);SinoEuropean Laboratory of Informatics, Automation and Applied Mathematics (Grants for the project Formally Certified Software Tools); Multiple nested clocks is a major language feature in synchronous data-flow languages such as Lustre[1].To build a formally verified compiler for such a language,it,is a common practice to compile the source program t...; 关键词：FORMALLY verified TRANSFORMATION UNIFY MULTIPLE nested clocks

LUSTRE