Research on formalization of efficient query application problems with compound condition in software development

This paper provides a formalized definition of the application problem of compound condition query (CCQ) and a formal method of applying requirements elicitation based on trace information space derived from trace algebra. With the formalized process of solving the application problem of CCQ, formal requirements specification of application of CCQ is given, a formalized and automatic mapping of the results of requirements elicitation to the formal requirements specification is performed, the software system model and the application code are developed. Through a sample application of comprehensive query on housing information, the feasibility of formalized and automatic software development for the application problem of CCQ is proved. The result has important implications for the other problems regarding formalization and automatic software development.     

Synchronization and storage models for multimedia objects

A technique is presented for the formal specification and modeling of multimedia composition with respect to intermedia timing. The proposed model is based on the logic of temporal intervals and timed Petri nets. A strategy is evinced for constructing a database schema to facilitate data storage and retrieval of media elements based on the temporal relationship established by the proposed modeling tool. An algorithm which allows the retrieval of media elements from the constructed database in a manner which preserves the temporal requirements of the initial specification is presented. Using the proposed model, the synchronization requirements of complex structures of temporally related objects can be easily specified     

Approach of generating parallel programs from parallelized algorithm design strategies

Today, parallel programming is dominated by message passing libraries, such as message passing interface （MPI）. This article intends to simplify parallel programming by generating parallel programs from parallelized algorithm design strategies. It uses skeletons to abstract parallelized algorithm design strategies, as well as parallel architectures. Starting from problem specification, an abstract parallel abstract programming language＋ （Apla＋） program is generated from parallelized algorithm design strategies and problem-specific function definitions. By combining with parallel architectures, implicity of parallelism inside the parallelized algorithm design strategies is exploited. With implementation and transformation, C＋＋ and parallel virtual machine （CPPVM） parallel program is finally generated. Parallelized branch and bound （B＆B） algorithm design strategy and paraUelized divide and conquer （D ＆ C） algorithm design strategy are studied in this article as examples. And it also illustrates the approach with a case study.     

Evolutionary algorithms for the synthesis of embedded software

This paper addresses the problem of trading off between the minimization of program and data memory requirements of single-processer Implementations of dataflow programs. Based on the formal model of synchronous dataflow (SDF) graphs, so called single appearance schedules are known to be program-memory optimal. Among these schedules, buffer memory schedules are investigated and explored based on a two-step approach: 1) an evolutionary algorithm (EA) is applied to efficiently explore the (in general) exponential search space of actor firing orders; 2) for each order, the buffer costs are evaluated by applying a dynamic programming post-optimization step (GDPPO). This iterative approach is compared to existing heuristics for buffer memory optimization     

密码协议的SPIN建模和验证

为了将模型检测这种强有力的系统验证技术应用于网络协议的安全分析,形式化建模仍然是目前的关键问题和难点所在.本文提出了一种基于高级过程描述语言的建模方法.根据入侵者角色和攻击目标的不同,从入侵者的角度分析协议的运行模式,为每个主体建立过程模型,用模型检测工具进行分析验证.对BAN-Yahalom协议的SPIN分析验证了这种方法的可行性.该方法具有一定的通用性,对其它网络协议的分析有很好的参考价值.     

基于XYZ/ADL的Web服务组合描述与验证

Web服务组合是当前Web服务领域的一个研究热点,目前已有一些相关的描述与验证方法,本文从软件体系结构角度研究Web服务组合描述与验证方法.基于软件体系结构描述语言XYZ/ADL和精化检验/模型检测方法,提出了一种Web服务组合的描述与验证方法.XYZ/ADL是时序逻辑语言XYZ/E的扩展,考虑到多数Web服务具有实时特征,采用XYZ/E的实时扩展语言XYZ/RE表示系统应满足的时间约束.针对Web服务组合系统,根据XYZ/RE到时间自动机的映射规则将系统描述转换为对应的时间自动机,分别采用精化检验和模型检测两种技术验证Web服务组合的正确性;最后通过两个实例分析分别阐述了上述方法的可行性和有效性.     

Three systems for cryptographic protocol analysis

Three experimental methods have been developed to help apply formal methods to the security verification of cryptographic protocols of the sort used for key distribution and authentication. Two of these methods are based on Prolog programs, and one is based on a general-purpose specification and verification system. All three combine algebraic with state-transition approaches. For purposes of comparison, they were used to analyze the same example protocol with a known flaw.     

基于形式规范的协议一致性测试的可靠性分析

可以用于形式规范的描述语言很多,但存在一种统一的方法对形式规范进行一致性测试。该文采用统计的方法分析基于形式规范的协议一致性测试的可靠性,通过计算给出待测实体经过这种测试后所能达到的可靠性的置信区间,特别指出在零错误下影响可靠性的条件。     

Applying formal methods within structured development

The introduction and use of formal (mathematically based) specification in substantial systems development has been hampered by the additional burdens it places on practitioners. BT and Leeds Metropolitan University have developed a framework for the gradual introduction of formal specification starting with its use as a review technique, applied to a standard range of systems development deliverables such as data and process models. The benefits of this approach are immediate and can also be more extensive. The paper describes the philosophy behind the general approach, offers an example of applying the Rigorous Review Technique, and summarises the benefits that can accrue