基于正态分布对模糊概念自动计算的FPDA应用设计

计算机控制系统具有自动机的特征,可以用有限自动机理论来对其进行描述,有限自动机是计算机科学各个方面的重要基石。但除确定性的有限自动机理论外,还有许多模糊事件应该由模糊自动机的隶属函数来解决,文中将重点放在具有正态分布特征的事件上。提出了一种实现自动运算的模糊自动机模型,若要在正态分布中得到“可能发生”和“很可能发生”这类模糊型事件的概率,可以只用这种模型实现自动计算。     

一种层次式时间自动机模型检测方法

层次式时间自动机在软件系统建模过程中有着重要的应用.由于层次嵌套带来额外的复杂度,难以对之进行直接的形式化验证工作.提出一种平展算法,将层次式时间自动机转化为一组并行的顺序时间自动机,应用广播通道同步该自动机集合执行.在此基础之上实现一个原型系统可以将层次式时间自动机模型自动转化为模型检测工具UPPAAL的输入,从而可以对之进行验证.结合实时UML状态机图实例,证明了该方法的有效性.     

分布式客户/服务器应用软件的测试框架研究

C/S结构应用软件自身所具有的特点决定了分布式C/S软件的测试要比传统集中计算模式软件的测试复杂的多。软件测试工作不仅仅局限于单个进程或单机系统。它还要考虑各分布进程间协作和正确性和效率等问题。本文着重对面向C/S结构软件系统的测试方法和测试过程框架进行了探讨和研究。根据测试过程框架可以制定出相应的软件测试计划,以进一步指导各项测试工作的完成。     

Streett自动机确定化工具

自动机的确定化是将非确定性自动机转换为接收相同语言的确定性自动机,是自动机理论的基本问题之一.ω自动机的确定化是诸多逻辑,如SnS, CTL*,μ演算等,判定过程的基础,同时也是解决无限博弈求解问题的关键,因此对ω自动机确定化的研究具有重要意义.主要关注一类ω自动机——Streett自动机的确定化.非确定性Streett自动机可以转换为等价的确定性Rabin或Parity自动机,在前期工作中已经分别得到了状态复杂度最优以及渐进最优算法,为了验证提出的算法的实际效果,也为了形象地展示确定化过程,开发一款支持Streett自动机确定化的工具是必要的.首先介绍4种不同的Streett确定化结构:μ-Safra tree和H-Safra tree (最优)将Streett确定化为Rabin自动机, compact Streett Safra tree和LIR-H-Safra tree (渐进最优)将Streett确定化为Parity自动机;然后,根据Streett确定化算法,基于开源工具GOAL (graphical tool for omega-automata and logics),实现...     

分布式软件系统交互行为建模、验证与测试

为了确保分析与设计阶段分布式软件系统中模块之间交互行为的正确性,提出了一种分布式软件系统模块交互的抽象方法,分别通过系统状态机图和对象状态机图对各模块状态变迁进行建模,使用UML2．0序列图对模块之间交互行为进行描述．采用基于命题投影时序逻辑的模型检测技术,将对象状态机图转换为 Promela 模型,系统交互性质转换为命题投影时序逻辑公式,通过模型检测器验证交互模型是否满足于系统的性质,若不满足于该性质,则能够获得反例执行的路径．给出了一个分布式软件系统测试框架,在验证后的序列图模型基础上,使用基于模型的测试用例自动生成方法得到测试用例集合,该集合能够实现对交互行为的有效测试．实例结果表明,该方法可以提高分布式软件系统中模块交互行为的有效性和可靠性．     

Büchi自动机确定化分析工具

无限字自动机的确定化是理论计算机研究重要的一部分,在形式化验证,时序逻辑,模型检测等方面有重要应用.自Büchi自动机提出半个世纪以来,其自动机的确定化算法始终是其中的基础.有别于当初只是在理论上对其大小上下界的探索,利用日新月异的高性能计算机技术不失为一种有效的辅助手段.为了深入研究非确定性Büchi自动机确定化算法的实现过程,我们希望重点研究确定化过程中的索引能否继续被优化的问题,实现了确定化研究工具NB2DR.可以对非确定性Büchi自动机进行高效的确定化,并通过工具提供的分析其确定化过程来达到对其确定化算法改进的目的.通过对生成的确定性无限字自动机的索引的深入分析来探索相关索引的理论.该工具还实现了可以根据需要的Büchi自动机的大小与字母表参数,生成确定化的Rabin自动机族,亦可以反向根据需要的指定索引的大小来生成全部Büchi自动机族,测试生成无限字自动机的等价性等功能.     

云计算背景下分布式软件系统故障检测技术研究

自云计算被大家真正的认可后,越来越多的分布式软件系统部署在公有云计算平台,云计算环境的复杂性、动态性和开放性使得分布式软件系统更易于出现故障,造成服务失效,从而影响大量用户正常使用,甚至造成巨大经济损失.故障检测技术旨在自动及时的检测系统故障的发生,以避免或减少服务失效所带来的损失,是保障分布式软件系统性能与可靠性的关键技术之一,文章中提出了面向云计算环境的基于统计监测的分布式软件系统故障管理参考框架,包括故障检测与恢复能力的测评工具的模块划分;针对当前云计算环境的特点,分析出云计算背景下分布式软件系统故障检测技术展望了未来的研究方向。     

基于有穷自动机的面向对象软件规约的测试

尽管作为软件工程中面向对象的技术已逐步取代了面向过程的技术，但是测试和维护软件的费用并没有因此而减少。在面向对象软件的测试研究中，对如何减少面向对象软件的错误提出了许多方法，绝大多数人关注的是类测试而不是对面向对象规约的高级测试。该文提供了一个基于有穷自动机的测试框架来测试面向对象规约。该方法在一个可执行的有穷自动机上直接进行了测试，不用手动进行证明，并且可产生大量的状态空间。测试结果证明了该方法的有效性。     

基于广义有限自动机的图像压缩方法

提出一种用确定性的广义有限自动机(GFA)对灰度图像进行压缩编码的方法.对一幅输入的数字化灰度图像,检测其中的自相似性,该图像可以被表示成一个广义有限自动机.解码算法可以非常高效的由确定的广义有限自动机复原图像,且结果图像没有很明显的方块效应.这种方法与传统的有限自动机方法相比具有状态数较少、压缩比高、压缩效果较好的优点.     

使用事件自动机规约的C语言有界模型检测

提出使用事件自动机对 C 程序的安全属性进行规约,并给出了基于有界模型检测的形式化验证方法。事件自动机可以规约程序中基于事件的安全属性,且可以描述无限状态的安全属性。事件自动机将属性规约与C程序本身隔离,不会改变程序的结构。在事件自动机的基础上,提出了自动机可达树的概念。结合自动机可达树和有界模型检测技术,给出将事件自动机和C程序转化为可满足性模理论SMT(satisfiability modulo theory)模型的算法。最后,使用SMT求解器对生成的SMT模型求解,并根据求解结果给出反例路径分析算法。实例分析和实验结果表明,该方法可以有效验证软件系统中针对事件的属性规约。     

A toolset in Java2 for modelling, prototyping and implementing communicating real-time state machines

This paper proposes an approach to the development of real-time systems which depends on Communicating Real-Time State Machines (CRSMs) as the specification language, and on a customisable actor kernel for prototyping, analysis and implementation of a modelled system. CRSMs offer an intuitive and distributed specification of a system in terms of a collection of co-operating state machines interacting with one another through timed CSP-like I/O commands. On the other hand, the underlying actor framework provides a time-sensitive scheduling structure which can be tuned to CSRMs in order to support temporal validation through assertions on the recorded time-stamped event histories. The approach can be practically used through a graphical environment (jCRSM) which has been realised using Java2. The toolset facilitates editing, testing and implementation in Java of CRSM systems. The proposed methodology is novel in that it provides a seamless system development life cycle where the specification, analysis, design and implementation phases are unified by a common representation of machines in terms of actors. The paper demonstrates the use of CRSM based software components by means of examples.     

Dynamic Meta Modeling with Time: Specifying the Semantics of Multimedia Sequence Diagrams

UML offers different diagram types to model behavior and dynamics of software systems. In some domains like embedded real-time systems or multimedia systems, it is necessary to include specifications of time since the correctness of these applications depends on the fulfillment of temporal requirements in addition to functional requirements. UML thus already incorporates language features to model time and temporal constraints. Such model elements must have an equivalent in the semantic domain. We have proposed Dynamic Meta Modeling (DMM) as a means for the specification of the formal operational semantics of UML models by applying graph transformation to the meta modeling of dynamic behavior. Within this paper, we extend this approach to also account for time by building on timed graph transformations. We apply these concepts to the domain of multimedia application modeling in which we adopt UML sequence diagrams. The DMM rules with time then specify an interpreter that can be used to analyze or test a model of multimedia sequence diagrams.     

Retrieval schedules based on resource availability and flexible presentation specifications

A distributed multimedia document presentation involves retrieval of objects from one or more document servers and their presentation at the client system. The presentation of the multimedia objects has to be carried out in accordance with the specification of temporal relationships between the objects. The retrieval of multimedia objects from the document server(s) is influenced by factors such as temporal specification of objects presentations, throughput offered by the network service provider, and the buffer resources on the client system. Flexibility in the temporal specification of the multimedia document may help in deriving an object retrieval schedule that can handle variations in network throughput and buffer resource availability. In this paper, we develop techniques for deriving a flexible object retrieval schedule for a distributed multimedia document presentation. The schedule is based on flexible temporal specification of the multimedia document using the difference constrai nts approach. We show how the derived retrieval schedule can be validated and modified to ensure that it can work with the offered network throughput and the available buffer resources.     

基于XYZ/RE的多媒体同步器自动构造方法

XYZ系统是一个以增强软件可靠性和提高软件生产率为目的的程序开发支撑系统.它由时序逻 辑语言(temporal logic language,简称TLL)XYZ/E和以该语言为基础的一组软件工程工具组 成.为了研究XYZ系统在多媒体领域中的应用问题,介绍了一种依据多媒体对象时序描述 自动生成用XYZ/RE表示的播放同步器的方法,XYZ/RE是时序逻辑语言族XYZ/E中表示实时系统 的子语言.与相关工作比较,该方法不仅可以处理简单的时序关系,而且可以处理嵌套的时序 关系,所产生的同步器可以复用于不同的节目.     

Modeling Distributed Multimedia Synchronization with DSPN

Multimedia synchronization is the essential technology for the integration of multimedia in distributed multimedia systems.The multimedia synchronization model has been recognized by many researchers as a premise of the implementation of multimedia synchronization.In distributed multimedia systems,the characteristic of multimedia synchronization is dynamic,and the key medium has the priority in multimedia synchronization.The previously proposed multimedia synchronization models cannot meet these requirements.So a new multimedia dynamic synchronization model-DSPN,based on the timed Petri-net has been designed in this paper.This model can not only let the distributed multimedia system keep multimedia synchronization in a more precise and effective manner according to the runtime situation of the system,but also allow the user to interact with the presentation of multimedia.     

分布多媒体系统的多媒体动态同步模型

在分布多媒体系统中，多媒体具有动态同步特性，同时关键媒体的同步要求在应用中享有优先权．现有的多媒体同步模型无法满足这些要求，现提出一个新的基于时间Ｐｅｔｒｉ网的多媒体动态同步模型——ＤＳＰＮ模型．它不仅能使分布多媒体系统依据实际运行状况和新提出的同步类型，以更准确、高效的方式来保持多媒体同步，而且允许用户对多媒体表现过程进行交互操作．     

Model continuity in the design of dynamic distributed real-time systems

Model continuity refers to the ability to transition as much as possible a model specification through the stages of a development process. In this paper, the authors show how a modeling and simulation environment, based on the discrete event system specification formalism, can support model continuity in the design of dynamic distributed real-time systems. In designing such systems, the authors restrict such continuity to the models that implement the system's real-time control and dynamic reconfiguration. The proposed methodology supports systematic modeling of dynamic systems and adopts simulation-based tests for distributed real-time software. Model continuity is emphasized during the entire process of software development $the control models of a dynamic distributed real-time system can be designed, analyzed, and tested by simulation methods, and then smoothly transitioned from simulation to distributed execution. A dynamic team formation distributed robotic system is presented as an example to show how model continuity methodology effectively manages the complexity of developing and testing the control software for this system.     

Systematic reliability analysis of a class of application-specific embedded software framework

Dramatic advances in computer and communication technologies have made it economically feasible to extend the use of embedded computer systems to more and more critical applications. At the same time, these embedded computer systems are becoming more complex and distributed. As the bulk of the complex application-specific logic of these systems is realized by software, the need for certifying software systems has grown substantially. While relatively mature techniques exist for certifying hardware systems, methods of rigorously certifying software systems are still being actively researched. Possible certification methods for embedded software systems range from formal verification to statistical testing. These methods have different strengths and weaknesses and can be used to complement each other. One potentially useful approach is to decompose the specification into distinct aspects that can be independently certified using the method that is most effective for it. Even though substantial-research has been carried out to reduce the complexity of the software system through decomposition, one major hurdle is the need to certify the overall system on the basis of the aspect properties. One way to address this issue is to focus on architectures in which the aspects are relatively independent of each other. However, complex embedded systems are typically comprised of multiple architectures. We present an alternative approach based on the use of application-oriented-frameworks for implementing embedded systems. We show that it is possible to design such frameworks for embedded applications and derive expressions for determining the system reliability from the reliabilities of the framework and the aspects. The method is illustrated using a distributed multimedia collaboration system.     

Integral: Petri-net approach to distributed software development

As the architecture of modern software systems continues to evolve in a distributed fashion, the development of such systems becomes increasingly complex, which requires the integration of more sophisticated specification techniques, tools, and procedures into the conventional methodology. An essential capability of an integrated software development environment is a formal specification method to capture effectively the system's functional requirements as well as its performance requirements. A validation and verification (V&V) system based on a formal specification method is of paramount importance to the development and maintenance of distributed systems.

There has been recent interest in integrating software techniques and tools at the specification level. It is also noted that an effective way of achieving such integration is by using wide-spectrum specification techniques. In view of these points, an integrated V&V system, called Integral, is presented that provides comprehensive and homogeneous analysis capabilities to both specification and testing phases of the life-cycle of distributed software systems. The underlying software model that supports various V&V activities in Integral is primarily based on Petri nets and is intended to be wide spectrum. The ultimate goal of this research is to demonstrate to the software industry, domestic or foreign, the availability and applicability of a new Petri-net-based software development paradigm. Integral is a prototype V&V system to support such a paradigm.