基于定理证明的内存安全性动态检测算法的正确性研究

随着软件运行时验证技术的发展,出现了许多面向C语言的运行时内存安全验证工具。这些工具大多是基于源代码或者中间代码插桩技术来实现内存安全的运行时检测。但是,其中一些没有经过严格证明的验证工具往往存在两方面的问题,一是插桩程序的加入可能会改变源程序的行为及语义,二是插桩程序并不能有效保证内存安全。为了解决这些问题,文中提出了一种使用Coq定理证明器来判定内存安全验证工具算法是否正确的形式化方法,并使用该方法对C语言运行时验证工具Movec的动态检测算法的正确性进行了证明。对安全规范性质的证明结果表明了Movec的内存安全性动态检测算法是正确的。     

具有冲突约束的RBAC模型的形式化规范与证明

在实际应用"基于角色的访问控制"(RBAC)模型时,经常遇到由于责任分离等策略而引起的冲突问题,如权限间的互斥等.访问控制操作应满足某些约束条件,以避免冲突的存在.但这些冲突关系相当复杂,如何检测出冲突问题是模型安全实施的重要保证.借助Z语言,提出了基于状态的RBAC形式化模型,对状态转换函数进行了形式化规范,描述了操作的具体内容和应满足的冲突约束条件.根据安全不变量给出了安全性定理,分别进行数学的和形式化的证明.最后,通过实例分析,说明在实际系统中,如何形式化规约和验证RBAC系统并检测出冲突问题,从而为今后使用RBAC模型开发具有高安全保证的系统提供了一种形式化规范和证明方法.     

SOCKET通信程序模型抽取及可靠性验证

形式化方法是验证并发系统可靠性和安全性的重要手段。对高级语言开发的并发系统自动抽取的模型进行 形式化验证是模型检测技术领域中的一个研究热点。鉴于socket函数调用顺序不正确产生的运行时潜在问题(内存 泄漏、死锁、边界数据丢失等),针对顺序结构的socket程序,通过描述Promcla消息数据结构和通道,构建socket函数 的Promcla模型,定义socket函数到Promcla映射规则,提出socket函数调用序列抽取算法及目标Promcla模型生成 算法,用线性时态逻辑(LTI.)刻画socket函数调用顺序应满足的性质,开发基于SPIN的socket通信程序分析系统。 实验结果表明,该系统能有效检测socket通信程序的运行时潜在问题。     

序列折半划分问题的形式化推导

形式化推导是在程序正确性证明理论下所进行的程序开发,最终得到完全正确的算法程序。针对序列折半划分问题,现有的形式化推导方法将推导与证明交替进行,推导过程繁琐且大多无法直接获得可执行程序。为解决上述问题,提出了一种新的序列折半划分问题的形式化推导方法。该方法基于分划递推的核心思想,应用规约变换技术对问题规约进行变换并严格保证一致性,使得在推导过程中无需交替证明,进而导出递推关系式并得到高可靠性抽象算法程序Apla,最终通过转换工具自动生成可执行程序。实现了从程序规约到具体可执行程序的完整程序求精过程。以2个序列算法为例,验证了该方法的有效性和可行性,对相关问题的形式化推导具有指导意义。     

语义Web服务组合的形式化描述与验证研究

Web服务组合是Web服务的主要研究方向之一,对语义Web服务组合进行形式化描述并进行分析和验证是组合服务正确运行的保证.本文首先给出了基于有色Petri网的语义Web服务形式化模型,形式化描述了OWL-S的ServiceModel中8种基本的Web服务组合模式,利用这些组合模式可以构造出满足需求的组合Web服务.然后,对服务组合形式化模型的正确性分析和验证进行研究后,给出了组合模型语法正确性、可达性、活性和有界性的算法.最后,通过一个具体的建模实例展示了Web服务组合的Petri网建模.     

形式化方法和信号解释Petri 网在PLC 编程中的应用

针对传统的PLC 编程方式在解决复杂控制问题时存在的缺陷,采用一种将形式化和信号解释Petri 网(SIPN)应用于PLC 程序设计的方法. 通过一个机器人焊接单元的例子来说明这一设计过程,首先建立系统控制算法的信号解释Petri 网模型,验证其是否满足基本Petri 网的安全性、活性和可逆性的特征,然后利用模型检测工具Cadence SMV 对系统模型进行验证和确认(V&V),检验其是否满足SIPN 的确定性、终止性和输出正确性,从而避免了控制算法的设计过程中可能出现的并发、冲突和死锁等事件,由此设计出具有更高的正确性和可靠度的PLC 程序.     

反例引导的C代码空间流模型检测方法

软件验证一直是确保软件正确性和安全性的热点研究问题.然而,由于程序语言复杂的语法语义特性,应用形式化方法验证程序的正确性存在准确度低和效率差的问题.其中,由指针操作带来的地址空间的状态变化使得现有模型检测方法的检测准确度难以得到保证.为此,通过结合模型检测与稀疏值流分析方法,设计了一种空间流模型,实现了对C程序在符号变量层面和地址空间层面的状态行为的有效描述,并提出了一种反例引导的抽象细化和稀疏值流强更新算法(CEGAS),实现了C程序指向信息敏感的形式化验证.建立了包含多种指针操作的C代码基准库,并基于该基准库进行了对比实验.实验结果表明:所提出的模型检测算法CEGAS在分析含有多种C代码特性的任务中,与现有模型检测工具相比均能取得突出的结果,其检测准确度为92.9%,每行代码的平均检测时间为2.58 ms,优于现有检测工具.     

共识协议的形式化验证研究现状与展望

分布式系统在计算环境中发挥重要的作用,其中的共识协议算法用于保证节点间行为的一致性.共识协议的设计错误可能导致系统运行故障,严重时可能对人员和环境造成灾难性的后果,因此保证共识协议设计的正确性非常重要.形式化验证能够严格证明设计模型中目标性质的正确性,适合用于验证共识协议.然而,随着分布式系统的规模增大,问题复杂度提升,使得分布式共识协议的形式化验证更为困难.采用什么方法对共识协议的设计进行形式化验证、如何提升验证规模,是共识协议形式化验证的重要研究问题.对目前采用形式化方法验证共识协议的研究工作进行调研,总结其中提出的重要建模方法和关键验证技术,并展望该领域未来有潜力的研究方向.     

基于初等运动的多机器人避碰及死锁预防

该文以一实际应用为背景提出了多移动机器人避碰及死锁预防算法,该算法将机器人的运行环境形式化地描述为初等运动集、冲突图、总任务集及机器人作业集,利用集合论、图论的有关方法及技术实现了多机器人间的避碰与死锁预防。当机器人的运行环境改变时,只需要对相应的集合描述文件进行修改,而不用对程序做任何屐改动。算法的另一个特点是利用避碰算法巧妙地完成了死锁预防。仿真和实际运行证明了该算法高效可靠。     

使用模型检测方法对Paxos算法进行验证与改进

因通信的同步问题、网络分区的可靠性问题等,分布式系统难以在通信、分区等环节失效的情况下对特定的状态达成共识．Paxos是近年分布式系统中常见且有效的共识算法,本文通过使用模型检测的方法对Paxos算法进行形式化建模,分析和验证了Paxos作为共识算法所应当满足的性质,结果表明,Paxos算法满足安全性、活性,但执行过程中有发生活锁的可能,并通过模型检测器重现了算法发生活锁时的运行轨迹．最后通过对算法进行改进,以应对现有算法执行过程中可能出现的活锁问题,并通过了模型检测器的验证．     

煤矿井下安全监控分站的设计及其仿真实现

为了设计一种具有低成本、低功耗、易操作、功能强且可靠性高的煤矿井下安全分站,针对煤矿安全生产实际,文章提出了采用MCS-51系列单片机为核心、具有CAN总线通信接口的煤矿井下安全监控分站的设计方案;首先给出煤矿井下安全监控分站的整体构架设计,然后着重阐述模拟量输入信号处理系统的设计过程,最后说明单片机最小系统及其键盘、显示、报警、通信等各个组成部分的设计;为验证设计方案的可行性与有效性,使用Proteus软件对设计内容进行仿真验证,设计的煤矿井下安全监控分站具有瓦斯、温度等模拟量参数超标报警功能和电机开停、风门开闭等开关量指示功能;仿真结果表明:设计的煤矿井下安全监控分站具有一定的实际应用价值.     

View-based model-driven architecture for enhancing maintainability of data access services

In modern service-oriented architectures, database access is done by a special type of services, the so-called data access services (DAS). Though, particularly in data-intensive applications, using and developing DAS are very common today, the link between the DAS and their implementation, e.g. a layer of data access objects (DAOs) encapsulating the database queries, still is not sufficiently elaborated, yet. As a result, as the number of DAS grows, finding the desired DAS for reuse and/or associated documentation can become an impossible task. In this paper we focus on bridging this gap between the DAS and their implementation by presenting a view-based, model-driven data access architecture (VMDA) managing models of the DAS, DAOs and database queries in a queryable manner. Our models support tailored views of different stakeholders and are scalable with all types of DAS implementations. In this paper we show that our view-based and model driven architecture approach can enhance software development productivity and maintainability by improving DAS documentation. Moreover, our VMDA opens a wide range of applications such as evaluating DAS usage for DAS performance optimization. Furthermore, we provide tool support and illustrate the applicability of our VMDA in a large-scale case study. Finally, we quantitatively prove that our approach performs with acceptable response times.     

A pragmatic multi-method investigation of discrepant technological events: Coping,attributions, and ‘accidental’ learning

Discrepant technological events or situations that entail a problem, a misunderstanding or a difficulty with the Information Technology (IT) being employed, are common in the workplace, and can lead to frustration and avoidance behaviors. Little is known, however, about how individuals cope with these events. This paper examines these events by using a multi-method pragmatic approach informed by coping theory. The results of two studies – a critical incident study and an experiment – serve to build and test, respectively, a theoretical model that posits that individuals use a variety of strategies when dealing with these events: they experience negative emotions, make external attributions, and adopt engagement coping strategies directed at solving the event, eventually switching to a disengagement coping strategy when they feel they have no control over the situation. Furthermore, users’ efforts may result in ‘accidental’ learning as they try to overcome the discrepant IT events through engagement coping. The paper ends with a discussion of the results in light of existing literature, future opportunities for research, and implications for practice.     

The Distributed Time-Triggered Simulation Scheme: Core Principles and Supporting Execution Engine

Distributed real-time simulation is a young technology field but its practice is under increasing demands. In recent years the author and his collaborators have been establishing a new approach called the distributed time-triggered simulation (DTS) scheme which is conceptually simple and easy to use but widely applicable. The concept was initiated in the course of developing a new-generation object-oriented real-time programming scheme called the time-triggered message-triggered object (TMO) programming scheme. Some fundamental issues inherent in distributed real-time simulation that were learned during recent experimental studies are discussed along with some approaches for resolving the issues. An execution engine developed to support both the TMOs engaged in control computation and the TMOs engaged in DTS is also discussed along with its possible extensions that will enable significantly larger-scale DTSs.     

Software-Konfigurationsmanagement in großen Softwareprojekten

Zusammenfassung Mit zunehmender Größe der Softwaresysteme verschärfen sich die für die Software-Herstellung typischen Probleme: Beherrschen großer Objektmengen, Erhalten der Systemkonsistenz, Kontrolle der ständigen Änderungseinflüsse und Gewährleisten einer langen Lebensdauer. Die Disziplin Konfigurationsmanagement bildet den methodischen Ansatz, diese Probleme besser zu beherrschen. Software-Konfigurationsmanagement faßt die Herstellung von Softwaresystemen als eine Abfolge von kontrollierten Änderungen an gesicherten Zwischen- und Endergebnissen auf. Dargestellt werden die Objekte und Funktionen des Software-Konfigurationsmanagements sowie die hierfür in großen Software-Projekten benötigten Methoden, Instanzen und Hilfsmittel.     

Information for Authors

正http://www.zju.edu.cn/jzus http://www.springerlink.com Aim The Journals of Zhejiang University-SCIENCE(A/B/C)are edited by the international board of distinguished Chinese and foreign scientists,and are aimed to present the latest developments and achievements in scientific research in China and     

Editorial:Brain-machine interface(BMI) and cyborg intelligence

正Brain-machine interfaces(BMIs)aim at building a direct communication pathway between the brain and an external device,and represent an area of research where significant progress has been made during the past decade.Based on BMIs,mind information can be read out by neural signals to control     

Information for Authors

正http://www.zju.edu.cn/jzus http://www.springerlink.com Aim The Journals of Zhejiang University-SCIENCE(A/B/C)are edited by the international board of distinguished Chinese and foreign scientists,and are aimed to present the latest developments and achievements in scientific research in China and overseas to the world’s scientific circles,especially to stimulate     

SCIENCE CHINA Information Sciences SUBJECT INDEX TO VOLUME 57(2014)

正~~     

Information for Authors

正http://www.zju.edu.cn/jzus http://www.springerlink.com Aim The Journals of Zhejiang University-SCIENCE(A/B/C)are edited by the international board of distinguished Chinese and foreign scientists,and are aimed to present the latest developments and achievements in scientific research in China and overseas to the world’s scientific circles,especially to stimulate