facilitating formal specification acquisition by using recursive functions on context-free languages

Although formal specification techniques are very useful in software development, the acquisition of formal specifications is a difficult task. This paper presents the formal specification language LFC, which is designed to facilitate the acquisition and validation of formal specifications. LFC uses context-free languages for syntactic aspect and relies on a new kind of recursive functions, i.e. recursive functions on context-free languages, for semantic aspect of specifications. Construction and validation of LFC specifications are machine-aided. The basic ideas behind LFC, the main aspects of LFC, and the use of LFC and illustrative examples are described.

Large Eddy Simulation of Complex Turbulent Flows: Physical Aspects and Research Trends

In the current paper, we have primarily addressed one powerful simulation tool developed during the last decades-Large Eddy Simulation (LES), which is most suitable for unsteady three-dimensional complex turbulent flows in industry and natural environment. The main point in LES is that the large-scale motion is resolved while the small-scale motion is modeled or, in geophysical terminology, parameterized. With a view to devising a subgrid-scale(SGS) model of high quality, we have highlighted analyzing physical aspects in scale interaction and-energy transfer such as dissipation, backscatter, local and non-local interaction, anisotropy and resolution requirement. They are the factors responsible for where the advantages and disadvantages in existing SGS models come from. A case study on LES of turbulence in vegetative canopy is presented to illustrate that LES model is more based on physical arguments. Then, varieties of challenging complex turbulent flows in both industry and geophysical fields in the near future-are presented. In conclusion; we may say with confidence that new century shall see the flourish in the research of turbulence with the aid of LES combined with other approaches.

Computation of turbulent-flow in a square duct - aspects of the secondary flow and its origin

A numerical study of turbulent flow in a straight duct of square cross-section is made. An order-of-magnitude analysis of the 3-D, time-averaged Navier-Stokes equations resulted in a parabolic form of the Navier-Stokes equations. The governing equations, expressed in terms of a new vector-potential formulation, are expanded as a multi-deck structure with each deck characterized by its dominant physical forces. The resulting equations are solved using a finite-element approach with a bicubic element representation on each cross-sectional plane. The numerical integration along the streamwise direction is carried out with finite-difference approximations until a fully-developed state is reached. The computed results agree well with other numerical studies and compare very favorably with the available experimental data. One important outcome of the current investigation is the interpretation analytically that the driving force of the secondary flow in a square duct comes mainly from the second-order terms of the difference in the gradients of the normal and transverse Reynolds stresses in the axial vorticity equation.

Some theoretical aspects of the simplified Navier-Stokes(SNS) equations

This study deals with the formulation, mathematical property and physical meaning of the simplified Navier-Stokes (SNS) equations. The tensorial SNS equations proposed is the simplest in form and is applicable to flow fields with arbitrary body boundaries. The zones of influence and dependence of the SNS equations, which are of primary importance to numerical solutions, are expounded for the first time from the viewpoint of subcharacteristics. Besides, a detailed analysis of the diffusion process in flow fields shows that the diffusion effect has an influence zone globally windward and an upwind propagation greatly depressed by convection. The maximum upwind influential distance of the viscous effect and the relative importance of the viscous effect in the flow direction to that in the direction normal to the flow are represented by the Reynolds number, which illustrates the conversion of the complete Navier-Stokes (NS) equations to the SNS equations for flows with large Reynolds number.

Some biocybernetic aspects in gene expression and regulatory control

In eucaryotes, gene expression and control is a complex nonlinear process, where there are many control mechanisms and ways, both physic, chemical and informational control. By the exploration from the angle of biocybernetics, the authors suggest that gene expression is a co-control process. In this process, physic, chemical and informational feedback controls are associated and influential each other, and are cross and co-functional. The physic, chemical and informational control ways composed an order non-linear feedback control system in eucaryotes.

Formal specification and refinement of a safe train control function

Motivated by the design and development challenges of the BART case study, an approach for developing and analyzing a formal model for reactive systems is presented. The approach makes use of a domain specific language for specifying control algorithms able to satisfy competing properties such as safety and optimality. The domain language, called SPC, offers several key abstractions such as the state, the profile, and the constraint to facilitate problem specification. Using a high-level program transformation system such as HATS being developed at the University of Nebraska at Omaha, specifications in this modelling language can be transformed to ML code. The resulting executable specification can be further refined by applying generic transformations to the abstractions provided by the domain language. Problem dependent transformations utilizing the domain specific knowledge and properties may also be applied. The result is a significantly more efficient implementation which can be used for simulation and gaining deeper insight into design decisions and various control policies. The correctness of transformations can be established using a rewrite-rule based induction theorem prover Rewrite Rule Laboratory developed at the University of New Mexico.

an intuitive formal proof for deadline driven scheduler

United Nations University, Int. Inst. for Softw. Technol., China; Vietnam National University, Hanoi, Vietnam; Vietnam Academy of Science and Technology, Vietnam