An Algebraic Hardware/Software Partitioning Algorithm

Hardware and software co-design is a design technique which delivers computer systems comprising hardware and software components.A critical phase of the co-design process is to decompose a program into hardware and software .This paper proposes an algebraic partitioning algorithm whose correctness is verified in program algebra.The authors inroduce a program analysis phase before program partitioning and deveop a collection of syntax-based splitting rules.The former provides the information for moving operations from software to hardware and reducing the interaction between compoents,and th latter supports a compositional approach to program partitioning.     

基于SMT的区域控制器同步反应式模型的形式化验证

在安全关键系统的软件开发过程中,形式化验证是一种经检验的提高软件质量的技术.然而,无论从理论上还是从应用角度来看,软件的验证都必须是完整的,数据流验证应该是对实现层软件模型进行验证的必要体现.因此,环境输入、泛型函数、高阶迭代运算和中间变量对于分析形式化验证的可用性至关重要.为了验证同步反应式模型,工程师很容易验证控制流模型(即安全状态机).现有工作表明,这类工作无法全面地验证安全关键系统的同步反应式模型,尤其是数据流模型,导致这些方法没有达到工业应用的要求,这成为对工业安全软件进行形式化验证的一个挑战.提出了一种自动化验证方法.该方法可以实现对安全状态机和数据流模型的集成进行验证.采用了一种基于程序综合的方法,其中,SCADE模型描述了功能需求、安全性质和环境输入,可以通过对Lustre模型的程序综合,采用基于SMT的模型检查器进行验证.该技术将程序合成作为一种通用原理来提高形式化验证的完整性.在轨道交通的工业级应用(近200万行Lustre代码)上评估了该方法.实验结果表明,该方法在大规模同步反应式模型长期存在的复杂验证问题上是有效的.     

可信机器学习的公平性综述

人工智能在与人类生活息息相关的场景中自主决策时,正逐渐面临法律或伦理的问题或风险.可信机器学习是建立安全人工智能系统的核心技术,是人工智能领域的热门研究方向,而公平性是可信机器学习的重要考量.公平性旨在研究机器学习算法决策对个人或群体不存在因其固有或后天属性所引起的偏见或偏爱.本文从公平表征、公平建模和公平决策三个角度出发,以典型案例中不公平问题及其危害为驱动,分析数据和算法中造成不公平的潜在原因,建立机器学习中的公平性抽象定义及其分类体系,进一步研究用于消除不公平的机制.可信机器学习中的公平性研究在人工智能多个领域中处于起步阶段,如计算机视觉、自然语言处理、推荐系统、多智能体系统和联邦学习等.建立具备公平决策能力的人工智能算法,是加速推广人工智能落地的必要条件,且极具理论意义和应用价值.     

基于事件驱动的系统级仿真器的操作语义

SystemC是一系统级描述语言.与传统的编程语言相比,它具有一些新的编程特性:延迟的事件通告、延迟事件通告的重载、延迟事件通告的取消以及delta-cycle.研究它的操作语义可以为进一步的形式化方面的研究提供基础.     

基于形式化方法的需求分析

利用形式化规格说明语言——B语言对软件需求进行了严格定义，在严格的数学基础上进行软件开发，以获得更好的软件性能。利用形式化方法的需求分析，有助于发现需求中隐含的不一致性、二义性和不完整性，对其进行更深入精确的理解，从而进行规范化管理。     

Verilog操作语义研究

提出了一个结构化操作语义模型,用于描述Verilog核心子集的语言特征,此子集包含了事件驱动、基于共享变量的并发特性、时间延迟等Verilog的主要语言成分.在此操作语义模型中,所有的Verilog程序将被统一地认为是开放式系统,所以在此操作语义模型的基础上能够进一步提出Verilog开放进程的观察模型,并提出基于互模拟的观察等价概念来判定进程之间的等价关系.最后证明了所定义的观察等价关系对所有的Verilog构造子而言是一个同余关系,从而为发展相应的进程代数理论提供了一个可靠性基础.     

汉字关系数据库管理系统ECNIS

本文介绍为微机系统研制的汉字关系数据库管理系统ECNIS。该系统可在配有UNIX操作系统的68000系统或配有UNFLEX操作系统的S/09系统上运行。它为用户提供了一个关系数据库,其中数据的组织从用户看来是一张张表,表由若干个记录组成,每个记录包括一些属性域,对数据的访问是通过完备的数据操作子语言DML来实现的,为了解决易用性问题,系统为用户提供了动态数据定义语言DDL,多种用户—系统界面及系统的中文信息处理能力,从而使得ECNIS适用于企业管理、图书流通管理,情报检索和统计报表处理等领域,该系统使用C语言编制,并通过虚拟操作系统VMS与主机操作系统连接,因此具有较强的可移植性。该系统已在S-09微型机上实现。     

企业信息管理系统的软件设计

本文讨论了小型计算机上企业信息管理系统的软件设计中若干问题:调度程序的设计、内存文件的管理,信息的保护及恢复和系统可靠性机制。     

面向服务的计算专刊前言

何积丰,金芝,李宣东.面向服务的计算专刊前言.软件学报,2007,18(12):2965-2966.http://www.jos.org.cn/ 1000-9825/18/2965.htm随着Internet的普及和基于Internet的应用的延伸,以Web服务为基础的分布式计算模式SOC应运而生,其目的是有效解决在分布、动态、异构环境下,数据、应用和系统集成的问题.SOC将WWW上静态的、无结构的Web页面扩展到拥有自主行为的、具备执行任务能力的Web服务,融合了网格计算中"无处不在的、集成的计算与资源环境"的思想,在面向对象、基于构件的开发、分布式对象计算及Web技术基础上,提出了一种新的软件开发、部署和集成的模式.     

使用延时演算的时间化RSL的指称语义

使用扩展的持续时间演算(EDC)模型,给出了时间化的RAISE描述语言(RSL)的一个子集的指称语义.在扩展的持续时间演算模型中加入了一些新的特征,并探究了它们的代数定律.这些定律在形式化实时程序和验证实时性质中起着重要作用.最后还给出了时间化RSL的一些代数定律.这些定律可以从其指称语义证明,并用于程序的转化和优化.