An incremental approach to automatic algorithm design

This paper presents an incremental approach to automatic algorithm design,which can be described by algebraic specifications precisely and conveniently.The definitions of selection operator and extension operator which ca be defined by strategy relations and transformations are given in order to model the process of finding the solution of a problem.Also discussed is its object-oriented implementation.The functional specification and the design specification for an algorithm are given in one framework so that the correctness of the algorithm can be easily proved.     

Structured Development Environment Based on the Object-Oriented Concepts

The object-oriented software development is a kind of promising software methodology and leading to a wholly new way for solving problems.In the research on the rapid construction of Structured Development Environment(SDE)that supports detailed design and coding in software development,a generator that can generate the SE has been applied as a metatool.The kernel of SDE is a syntax-directed editor based on the object-oriented concepts.The key issue in the design of SDE is how to represent the elements of target language with the class concept and a program internally.In this paper,the key concepts and design of the SDE and its generator as well as the implementation of a prototype are to be discussed.     

Semantic specification and verification of data flow diagrams

Data Flow Diagram (DFD) has been widely used in Software Engineering as means of requirement analysis and system specification.However,one defect of DFD approach remains untackled:the lack of formal semantics has brought about a lot of problems.In this paper,we model Data Flow Diagram as networks of concurrent processes.With the use of temporal logic language XYZ/E,the formal basis of the semantic specification of DFD can be ensured,and the system properties such as safety and liveness can be easily characterized.The main part of this paper is devoted to the study of the hierarchical decomposition of semantic specification and its correctness.A verification methodology is proposed and several examples are analyzed.The implementation of the tools which can support the formal specification,verification and simulation of DFD are also briefly described.     

Optimal stopping of multi-project software testing in the context of software cybernetics

Software cybernetics explores the interplay between control theory/engineering and software theory/engineering. The controlled Markov chains (CMC) approach to software testing follows the idea of software cybernetics and treats software testing as a control problem. The software under test serves as a controlled object and the software testing strategy serves as the corresponding controller. The software under test and the software testing strategy make up a closed-loop feedback control system, and the theory of controlled Markov chains can be used to design and optimize software testing strategies in accordance with testing/reliability goals given a priori. In this paper we apply the CMC approach to the optimal stopping problem of multi-project software testing. The problem under consideration assumes that a single stopping action can stop testing of all the software systems under test simultaneously. The theoretical results presented in this paper describe how to test multiple software systems and whe     

Software Engineering in the Application of Virtual Instrument-Based Dynamics Testing System for UAV

Complex dynamics testing system for UAV can be constructed based on the virtual instrument and the software is the core LabVIEW is a graphical-based programming language with a convenient user interaction and shorter development cycle than the text-based programming language. This paper uses LabVIEW as the software development platform of the dynamics testing system for UAV. The idea of software engineering is used in the design of the testing system for UAV, and then is used to improve the reliability, stability and scalability of the testing system. The experimental results show that this system is practical, convenient to operate, able to meet the needs of the engineering and teaching for UAV research and development.     

A metamodeling approach for pattern specification and management

The formal specification of design patterns is central to pattern research and is the foundation of solving various pattern-related problems.In this paper,we propose a metamodeling approach for pattern specification,in which a pattern is modeled as a meta-level class and its participants are meta-level references.Instead of defining a new metamodel,we reuse the Unified Modeling Language(UML)metamodel and incorporate the concepts of Variable and Set into our approach,which are unavailable in the UML but essential for pattern specification.Our approach provides straightforward solutions for pattern-related problems,such as pattern instantiation,evolution,and implementation.By integrating the solutions into a single framework,we can construct a pattern management system,in which patterns can be instantiated,evolved,and implemented in a correct and manageable way.     

A formal software development approach using refinement calculus

The advantage of COOZ(Complete Object-Oriented Z) is to specify large scale software,but it does not support refinement calculus.Thus its application is comfined for software development.Including refinement calculus into COOZ overcomes its disadvantage during design and implementation.The separation between the design and implementation for structure and notation is removed as well .Then the software can be developed smoothly in the same frame.The combination of COOZ and refinement calculus can build object-oriented frame,in which the specification in COOZ is refined stepwise to code by calculus.In this paper,the development model is established.which is based on COOZ and refinement calculus.Data refinement is harder to deal with in a refinement tool than ordinary algorithmic refinement,since data refinement usually has to be done on a large program component at once.As to the implementation technology of refinement calculus,the data refinement calculator is constructed and an approach for data refinement which is based on data refinement calculus and program window inference is offered.     

A generic approach of integrating 3D models into virtual manufacturing

Various 3D modeling software has been developed for design and manufacturing.Most of the commercially available software uses native file formats,which may not be able to be read or understood by other software.This paper deals with the development of a generic approach of a 3D model conversion program for virtual manufacturing(VM),using a lexical analyzer generator Lex and the Open Graphic Library(OpenGL).The program is able to convert 3D mesh data between four universal file formats,i.e.,Stereolithography(STL),Virtual Reality Modeling Language(VRML),eXtensible Markup Language(XML),and Object(OBJ).Simple assembly functions can be applied to the imported models.The quaternion angle is used for object rotation to overcome the problem of gimbal lock or a loss of one degree of rotational freedom.The program has been validated by importing the neutral format models into the program,applying the transformation,saving the new models with a new coordinate system,and lastly exporting into other commercial software.The results showed that the program is able to render and re-arrange accurately the geometry data from the different universal file formats and that it can be used in VM.Therefore,the output models from a VM system can be transferred or imported to another VM system in a universal file format.     

基于J2EE平台的MDA模型转换技术

The OMG's MDA defines an approach to IT system specification that separates the specification of system functionality from the specification of the implementation of that functionality on a specific technology platform. To this end, the MA defines two kinds of models: platform independent model (PIM) and platform specific model(PSM). The MDA approach allows the same model specifying system functionality to be realized on multiple platforms through auxiliary mapping standards from PIM to PSM. This paper presents a mapping method from PIMsto PSMs based on J2EE platform. This transformation can promote the efficiency of system analysis and design.     

Structured Development Environment Based on the Object-Oriented Concepts

The object oriented software development is a kind of promising software methodology and leading to awholly new way for solving problems. In the research on the rapid construction of Structured Development Envi-ronment (SDE)that supports detailed design and coding in software development, a generator that can gener-ate the SDE has been applied as a metatool. The kernel of SDE is a syntax-directed editor based on the ob-ject-oriented concepts. The key issue in the design of SDE is how to represent the elements of target languagewith the class concept and a program internally. In this paper, the key concepts and design of the SDE and itsgenerator as well as the implementation of a prototype are to be discussed.     

核级软件的验证与确认技术研究

核级软件的验证与确认是核电数字化仪控系统研发的关键,用以确保核级软件设计过程的透明性,验证软件需求规格的完整性,确认核级软件功能与设计需求规格的一致性、正确性。核级软件的验证与确认概要地分成软件设计过程的管理技术及软件的测试技术,本文遵循IEC60880以及IAEA的核级软件的验证与确认导则,侧重研究核级软件验证与确认中的需求验证与软件测试技术,通过开发一种自动化V＆V工具,实现核级控制系统应用软件的一套自动化V＆V流程。     

Hierarchical correctness verification in multiphase real-time software design

A hierarchical approach to correctness verification of real-time software specifications is presented. The verification is distributed into successive steps that correspond to the design phases. The three languages: Rule Charts, LACTATRE (graphical specification) and Communicating Real Time State Machines are used for specification of real-time software within corresponding abstraction levels. The correctness is defined as a coincidence of a system specified in a phase w.r.t. requirements established ing the previous phase. This correctness concept leads to an application of the relative correctness methods (developed in former works) for the verification. The approach is examined in Preliminary and Detailed Design phases for the verification of several types of properties: structure, functions and time constraints.     

机载PHM系统软件设计与验证

针对现有PHM系统软件开发中存在的软件模块规范性差、复用率低和鲁棒性弱等问题,提出了一种基于OSA-CBM标准的构件化机载PHM系统软件设计方法,描述了机载PHM系统软件的构件化模型定义、功能框架、分层体系结构和软件控制流程;设计了机载PHM系统的构件接口和核心功能构件;实现了符合OSA-CBM规范接口的构件化软件。通过原型系统软件验证了构件化机载PHM系统软件设计和开发方法的正确性,表明了该方法能够提升软件的规范性、复用率、鲁棒性和可扩展性。     

基于SPIN的地下建筑设备监控系统软件验证

在地下建筑智能化系统中,设备监控系统是基本的组成部分,其软件设计的正确性十分重要。提出了一种基于SPIN的地下建筑设备监控系统软件正确性验证方法。构建了基于iFIX组态软件的设备控制系统软件Promela模型,利用SPIN模型检验方法对其安全性进行了验证。还利用简化模型进行反例追踪,找出了安全性规约中存在的错误。检验结果表明提出的验证方法是有效性。     

基于ε-互模拟的软件近似正确性模型

软件正确性是软件可信性的重要属性。在实际软件开发和设计中,需要不断地对软件进行修改,从而软件越来越正确。为了讨论软件的动态近似正确性,基于概率进程代数的ε-互模拟,建立软件越来越正确的形式化描述。定义ε-极限互模拟,用来反应软件实现与规范之间的关系,给出一些特殊的ε-极限互模拟。提出ε-互模拟极限,用其刻画规范是软件实现的极限形式,同时证明ε-互模拟极限的一些性质。     

基于结构化功能规格说明的测试方法和工具

由于程序的形式化验证技术还局限于比较小的程序，软件测试仍然是目前和今后相当长一段时间内保证大型软件质量和可靠性的主要手段．测试大型软件是一项既繁重又复杂的工作，计算机辅助软件测试将会大大降低测试工作量，提高测试效率．本文首先提出一种新的、简单有效的基于结构化功能规格说明的测试方法，然后阐述如何基于该方法设计井实现一个测试工具环境，以提高测试者的工作效率，减轻测试者的负担．     

基于Nios Ⅱ的伪随机序列信号发生器IP核设计

根据Nios Ⅱ嵌入式系统的Avalon总线规范,提出了一种伪随机序列信号发生器IP核的设计方法,详细介绍了IP核的硬件和软件设计。该方法采用自定制组件的软硬件协同设计,实现了阶次与码字时长可调的伪随机序列信号发生器IP核设计。在可控震源信号发生器设计中对IP核进行验证,证明了其可行性和正确性。     

Testing Software Design Modeled by Finite-State Machines

We propose a method of testing the correctness of control structures that can be modeled by a finite-state machine. Test results derived from the design are evaluated against the specification. No "executable" prototype is required. The method is based on a result in automata theory and can be applied to software testing. Its error-detecting capability is compared with that of other approaches. Application experience is summarized.