检索结果-南通市图书馆

并发进程指称语义的几种基于Trace模型的定义方法

在线全文

学校读者我要写书评

暂无评论

兰州大学学报（自然科学版） 1996年第1期32卷 49-52页

作者：王生原杨萍兰州大学计算机系

Ｔｒａｃｅ模型是定义并发进程指称语义的基本方法之一．在Ｔｒａｃｅ模型的基础上，为获得更广泛的表达能力，通过进程指称论域的各种变化，派生出了一系列的语义模型．并对于这些模型进行了综述．

关键词：形式语言指称语义 Trace模型进程论域

在线全文

学校读者我要写书评

暂无评论

并发事务的一种操作模型

兰州大学学报（自然科学版） 1995年第2期31卷 78-81页

作者：王生原杨萍兰州大学计算机科学系

本文定义了一种描述分布式数据库系统并发事务行为的操作模型．以此为基础讨论了并发事务的调度，共享模式的Ｌｏｃｋｉｎｇ机制，死锁等问题．

关键词：分布式数据库并发事务操作模型

同步数据流语言可信编译器Vélus与L2C的比较

在线全文

学校读者我要写书评

暂无评论

软件学报 2019年第7期30卷 2003-2017页

作者：康跃馨甘元科王生原清华大学计算机科学与技术系

同步数据流语言(如Lustre、Signal)在航空、高铁、核电等安全关键领域得到广泛应用。例如,适合这些领域实时控制系统建模和开发的Scade工具就是基于一种类Lustre语言。这类语言相关开发工具,特别是编译器的安全性问题也自然受到高度关... 详细信息

同步数据流语言(如Lustre、Signal)在航空、高铁、核电等安全关键领域得到广泛应用。例如,适合这些领域实时控制系统建模和开发的Scade工具就是基于一种类Lustre语言。这类语言相关开发工具,特别是编译器的安全性问题也自然受到高度关注。近年来,基于形式化验证实现可信编译器构造成为程序设计语言领域的研究焦点之一,也取得了瞩目的成果,如CompCert项目实现了产品级的可信C编译器。同样,人们也采用这种方法开展了同步数据流语言可信编译器的研发工作。主要关注从事这一工作的两个长线项目,二者均研发面向基于Lustre的同步数据流语言编译器,分别以Vélus和L2C代称。对Vélus和L2C从多个重要的角度进行较为深入的分析与比较。

关键词：同步数据流语言形式化验证的编译器 Lustre语言

在线全文

学校读者我要写书评

暂无评论

BSP用于分布式系统的协议规范

兰州大学学报（自然科学版） 1995年第4期31卷 89-94页

作者：王生原杨萍田存生兰州大学计算机科学系兰州大学电子与信息科学系

ＢＳＰ（ＢｒｏａｄｃａｓｔｉｎｇＳｅｑｕｅｎｔｉａｌＰｒｏｃｅｓｓｅｓ）是一种带有广播原语的分布式语言，能很好地支持分布式系统中的消息传递。本文强调了ＢＳＰ在分布式系统协议规范方面的应用，并完成了对ＯＳＩ参考模型的网... 详细信息

ＢＳＰ（ＢｒｏａｄｃａｓｔｉｎｇＳｅｑｕｅｎｔｉａｌＰｒｏｃｅｓｓｅｓ）是一种带有广播原语的分布式语言，能很好地支持分布式系统中的消息传递。本文强调了ＢＳＰ在分布式系统协议规范方面的应用，并完成了对ＯＳＩ参考模型的网络协议以及数据库并发控制的ｔｉｍｅｓｔａｍｐ协议的规范说明。

关键词：分布计算机 BSP 协议分布式语言分布式系统

用于多目标编译系统构造的目标机体系结构描述

在线全文

学校读者我要写书评

暂无评论

计算机科学 2005年第9期32卷 239-242页

作者：杨萍王生原北京语言大学信息学院清华大学计算机系北京100084

本文是关于多目标编译系统构造的目标机体系结构描述的一个综述。主要涉及的话题:机器描述应当描述什么和描述语言的设计原则,现行的体系结构描述语言的状况及分类,一个典型的机器描述示例,结构信息描述,以及机器描述所面临的挑战及机... 详细信息

本文是关于多目标编译系统构造的目标机体系结构描述的一个综述。主要涉及的话题:机器描述应当描述什么和描述语言的设计原则,现行的体系结构描述语言的状况及分类,一个典型的机器描述示例,结构信息描述,以及机器描述所面临的挑战及机遇等。

关键词：体系结构描述编译系统可重定向机器描述编译器

可信编译器L2C的核心翻译步骤及其设计与实现

在线全文

学校读者我要写书评

暂无评论

软件学报 2017年第5期28卷 1233-1246页

作者：尚书甘元科石刚王生原董渊清华大学计算机科学与技术系北京100084

同步数据流语言(如Lustre)近年来在航空、高铁、核电等安全攸关领域得到广泛应用.这些领域对相关开发工具本身的安全性有着相当高的要求.为尽力解决好"误编译"问题,近期人们借助reliable-by-construction辅助定理证明器实现常规命令式... 详细信息

同步数据流语言(如Lustre)近年来在航空、高铁、核电等安全攸关领域得到广泛应用.这些领域对相关开发工具本身的安全性有着相当高的要求.为尽力解决好"误编译"问题,近期人们借助reliable-by-construction辅助定理证明器实现常规命令式语言编译器的构造和验证,取得了很大的成功,如Comp Cert C编译器.L2C是基于这种方法开发的可信编译器.它以扩展的Lustre语言为源语言,以Clight(Comp Cert中的C语言子集)为目标语言.L2C是面向实际工业应用的同步数据流语言编译器.重点介绍L2C编译器的核心翻译步骤及其设计与实现过程中考虑的主要问题和相关经验.

关键词：经过验证的编译器同步数据流语言 L2C Coq证明辅助器核心翻译步骤

CompCert编译器目标代码生成机制分析

在线全文

学校读者我要写书评

暂无评论

计算机科学 2020年第9期47卷 17-23页

作者：杨萍王生原北京语言大学信息科学学院北京100083 清华大学计算机系北京100084

CompCert是著名的C语言可信编译器,是经过形式化验证的编译器的杰出代表,近年来被广泛应用于学术界和工业界的许多研发工作中。CompCert编译器的当前版本支持多种目标机结构。文中对CompCert编译器目标代码生成机制进行剖析,主要介绍其... 详细信息

CompCert是著名的C语言可信编译器,是经过形式化验证的编译器的杰出代表,近年来被广泛应用于学术界和工业界的许多研发工作中。CompCert编译器的当前版本支持多种目标机结构。文中对CompCert编译器目标代码生成机制进行剖析,主要介绍其设计逻辑、翻译过程、语义保持性以及代码结构,并给出了CompCert编译器重定向设计的要点。文中工作有助于实现CompCert重定向,比如实现面向重要国产处理器的后端。

关键词： CompCert 形式化验证的编译器目标代码生成编译器重定向

在线全文

学校读者我要写书评

暂无评论

同步数据流语言可信编译器的研究进展

计算机科学 2019年第5期46卷 21-28页

作者：杨萍王生原北京语言大学信息科学学院北京100083 清华大学计算机科学与技术系北京100084

同步数据流语言(如Lustre,Signal)近年来在航空、高铁、核电等安全关键领域得到了广泛应用,因此与这类语言相关的开发工具本身的安全性问题受到高度关注。同步数据流语言到串行命令式语言的可信编译器是此类工具的典型代表(如Scade)。... 详细信息

同步数据流语言(如Lustre,Signal)近年来在航空、高铁、核电等安全关键领域得到了广泛应用,因此与这类语言相关的开发工具本身的安全性问题受到高度关注。同步数据流语言到串行命令式语言的可信编译器是此类工具的典型代表(如Scade)。构造可信编译器的途径可分为两大类:一类是传统的方法,例如通过大量测试和严格的过程管理等手段来实现;另一类是通过形式化方法,例如直接对编译器本身进行形式化证明,采用翻译确认的方法等。近年来,形式化方法作为构造和验证可信编译器的关键途径而得到广泛的重视,有望最大限度地解决"误编译"问题,因而成为新的研究热点。文章在介绍可信编译器的形式化构造和验证方法的基础上,特别聚焦于同步数据流语言可信编译器的相关研究工作,对其现状进行综述和分析。

关键词：同步数据流语言经过验证的编译器翻译确认 Lustre Signal

在线全文

学校读者我要写书评

暂无评论

一种基于P/T网的低级并发程序验证模型

中国科学：信息科学 2010年第1期40卷 13-32页

作者：梁英毅王生原董渊清华大学计算机科学与技术系北京100084

随着片上多处理器/多核技术的不断发展,采用机器级语言的并发程序(低级并发程序)有了更加广阔的应用前景.然而,低级并发程序的验证问题也成为程序语言领域一种新的挑战.并发程序安全性验证领域现有的工作多数是针对高级语言、规范或者演... 详细信息

随着片上多处理器/多核技术的不断发展,采用机器级语言的并发程序(低级并发程序)有了更加广阔的应用前景.然而,低级并发程序的验证问题也成为程序语言领域一种新的挑战.并发程序安全性验证领域现有的工作多数是针对高级语言、规范或者演算,而针对机器级语言的甚少。这种情况的主要原因之一是缺少低级抽象模型.文中描述一种可验证的低级并发编程模型P-PMCC.P-PMCC程序是一个扩展的P/T网系统,其网结构用来刻画低级并发线程(原子的顺序汇编级代码)之间的并发关系.P-PMCC程序的验证采取模型检查和定理证明相结合的方法,分开考虑并发行为与顺序线程的规范和验证:前者借助于Petri网领域已有的方法,后者则借助现有的顺序程序的正确性证明方法。P-PMCC程序也可以看作并发程序的一种可验证的低级中间表示.

关键词：低级并发程序 Petri网抽象机器程序验证分离逻辑