Dynamic Simulation of the Aircraft Environmental Control System

The dynamic research of aircraft environmental control system (ECS) is an important step in the advanced ECS design process. Based on the thermodynamics theory, mathematical models for the dynamic performance simulating of aircraft ECS were set up and an ECS simulation toolbox (ECS_1.0) was created with MATLAB language. It consists of main component modules (ducts, valves, heat exchangers, compressor, turbine, etc.). An aircraft environmental control system computer model was developed to assist engineers with the design and development of ECS dynamic optimization. An example simulating an existing ECS was given which shows the satisfactory effects.

Decision Making as Theorem Proving

We present a method for using type theory to solve decision making problem. Our method is based on the view that decision making is a special kind of theorem proving activity. An isomorphism between problems and types, and solutions and programs has been established to support this view which is much similar to the Curry-Howard isomorphism between propositions and types, and proofs and programs. To support our method, a proof development system called PowerEpsilon has been developed, and the synthesis of a decision procedure for validity of first-order propositional logic is discussed to show the power of the system.

Defining Dynamic Graphics by a Graphical Language

A graphical language which can be used for defining dynamic picture and applying control ac- tions to it is defined with an expanded attributed grammar.Based on this,a system is built for de- veloping the presentation of application data of user interface.This system provides user interface de- signers with a friendly and high efficient programming environment.

Abstract Implementation of Algebraic Specifications in a Temporal Logic Language

A formal technique for incorporating two specification paradigms is presented,in which an algebraic specifi- cation is implemented by a set of abstract procedures specified in pre- and post-condition style.The link be- tween the two level specifications is provided via a translation from terms of algebraic specifications into tempo- ral logic formulae representing abstract programs.In terms of translation,a criterion for an abstract implementation satisfying its specification is given,which allows one to check the consistency between the two levels of specifications.The abstract implementations can be refined into executable code by refining each abstract procedure in it.It is proved that the satisfication relation between a specification and its implementations is preserved by such refinement steps.

Semantic Specification and Verification of Data Flow Diagrams

Data Flow Diagram(DFD)has been widely used in Software Engineering as means of require- ment 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 prop- erties sach 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 verifica- tion 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 des- cribed.

Improvements to the Control Techniques of Sequential Inference Machines——from Instructions to Hardware Organization

Nondeterminism of PROLOG execution requires that a block of control information or a choice point for each procedure call be stored when there are other candidate clauses to be used.When the currently selected clause fails,the bindings made by the clause must be undone and the stored choice point is reactivated,and then another clause of the candidate ones is chosen to run on it. Storing and reactivating choice points and undoing account for the great overhead are required to control PROLOG execution,which is quite different from conventional programs. This paper focuses on the techniques used in Sequential PROLOG Engine(SPE)to reduce the overhead of control operations.The control instructions of SPE store no more choice points than the necessary.Its architecture takes the approaches of analysing the potential parallelism in the con- trol operations and developing a fraction of it due to the cost-effect consideration.The results of executing two sample programs on SPE in the form of hand timings are presented,which favor the approach.

Source-to-Source Conversion Based on Formal Definition

This paper proposes the idea of source-to-source conversion between two heterogeneous high-level programming languages.The conversion is based on formal definition and oriented to multi-pairs of lan- guages.The issues in conversion from PASCAL to C are also discussed.

Processing Polynomial Algebraic Problems by Using SAC-2/ALDES

This paper discusses the portability of SAC-2/ALDES and reviews some applications in polynomial algebra.Furthermore,we indicate that the concept of the safety variable in the SAC-2/ALDES is not proper.When,for example,we used safety variable in isolating complex roots of polynomials, something wrong happened.