Synchronization of musical words

We study the synchronization of musical sequences by means of an operation defined on finite or infinite words called superimposition. This operation can formalize basic musical structures such as melodic canons and serial counterpoint. In the case of circular canons, we introduce the superimposition of infinite words, and we present an enumeration algorithm involving Lyndon words, which appear to be a useful tool for enumerating periodic musical structures. We also define the superimposition of finite words, the superimposition of languages, and the iterated superimposition of a language, which is applied to the study of basic aspects of serial music. This leads to the study of closure properties of rational languages of finite words under superimposition and iterated superimposition. The rationality of the transduction associated with the superimposition appears to be a powerful argument in the proof of these properties. Since the superimposition of finite words is the max operation of a sup-semilattice, the last section addresses the link between the rationality of a sup-semilattice operation and the rationality of the order relation associated with it.     

基于并发事务逻辑的Web服务编制验证

 服务编制解决的是组织之间的业务集成问题,面临的是一个广泛分布、动态、自治、异构的网络环境,保障组合服务的正确执行以及相关特性的验证问题显得尤为重要.形式化方法是一种有效的解决方法,服务编制需要建立在严格的形式化模型的基础上,可以通过具有明确的、形式化语义的形式化模型研制验证工具来完成组合服务正确性的验证.本文基于并发事务逻辑(CTR:Concurrent TRansaction Logic)对服务编制的元素进行了描述和建模,给出了从WS-BPEL到并发事务逻辑的转换规则,讨论了服务编制在CTR中的验证问题以及WS-BPEL和CTR的表达能力,最后给出了一个实际的服务编制在CTR中建模的例子,验证了服务编制的CTR模型的有效性.     

网络管理服务行为建模与实现

基于服务的软件开发方法,围绕网络管理服务系统形式化建模,通过对网管服务活动建模,实现了一个基于服务的网络管理系统。提出的网络管理服务系统建模方法可以较好的实现服务行为分析,确保系统的安全性、可靠性。     

人工智能中的上下文推理

对上下文推理的原理和形式进行了阐述,讨论了上下文推理的形式化问题,并给出一个利用MCS对问题进行形式化表示和求解的实例。     

需求工程研究新进展

需求工程研究进展日渐显著，它可归结为需求工程的对象化、形式化和自动化三个主要方面．文中在讨论了需求工程有关的基本问题之后，围绕着上述三方面总结了其代表性工作、研究现状和发展趋势，并简要介绍了作者近期在面向对象需求工程及其自动化方面所做的一些工作．     

Classifying and Formally Verifying Integer Constant Folding

Constant folding is a well-known optimization of compilers which evaluates constant expressions already at compile time. Constant folding is valid only if the results computed by the compiler are exactly the same as the results which would be computed at run-time by the target machine arithmetic. We classify different arithmetics by deriving a general condition under which a target-machine arithmetic can be replaced by a compiler arithmetic. Furthermore, we consider integer arithmetics as a special case. They can be described by residue class arithmetics. We show that these arithmetics form a lattice. Using the order relation in this lattice, we establish a necessary and sufficient criterion under which constant folding can be done in a residue class arithmetic that is different from the one of the target machine. Concerning formal verification, we have formalized our proofs in the Isabelle/HOL system. As examples, we discuss the Java and C integer arithmetics and show which compiler arithmetics are valid for constant folding. This discussion reveals also potential sources of incorrect behavior of C compilers.     

一种形式化逆推的逻辑方法

本文讨论逆绎推理的形式化问题，指出这一问题的认知基础，然后证明逆绎推理可通过建立必要性假设来完成；ＮＨ构成了对已有知识订的扩充，必须构造必要性假设理论来捕捉逆绎推理的逻辑特征，本文选择缺席逻辑作为形式化ＮＬ的理论框架，并指出ＮＬ的基本性质。     

基于MDA和可执行形式化的可信软件设计

提出基于模型驱动架构的软件开发过程,利用可执行形式化规范,有效提高软件开发效率和可测试性,并通过基于可执行规范的运行时监控技术保证系统行为的可信性,降低由于软件测试阶段遗留的错误以及系统受到非法入侵所带来的风险。     

运输态势交互模型及其CSP形式化研究

人机交互（HCI）技术的迅猛发展为自然高效和谐的HCI提供了基础支持,随着HCI行为的日益复杂,如何验证其过程的正确性成为研究HCI领域的重心。根据双手触摸光感应触控平台在运输态势的HCI,提出一种体现用户操作与设备响应相结合的运输态势HCI模型,该模型采用通信顺序进程形式化描述,并结合甘特图验证其单用户操作的逻辑正确性和稳定性。