Specification, refinement and verification of concurrent systems - An integration of Object-Z and CSP

This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of modelling complex data structures needed to define the component processes of such systems, and CSP enables the concise specification of process interactions. The basis of the integration is a semantics of Object-Z classes identical to that of CSP processes. This allows classes specified in Object-Z to he used directly within the CSP part of the specification. In addition to specification, we also discuss refinement and verification in this model. The common semantic basis enables a unified method of refinement to be used, based upon CSP refinement. To enable state-based techniques to be used fur the Object-Z components of a specification we develop state-based refinement relations which are sound and complete with respect to CSP refinement. In addition, a verification method for static and dynamic properties is presented. The method allows us to verify properties of the CSP system specification in terms of its component Object-Z classes by using the laws of the the CSP operators together with the logic for Object-Z.

Sludge population optimisation: a new dimension for the control of biological wastewater treatment systems

The activated sludge comprises a complex microbiological community. The structure (what types of microorganisms are present) and function (what can the organisms do and at what rates) of this community are determined by external physico -chemical features and by the influent to the sewage treatment plant. The external features we can manipulate but rarely the influent. Conventional control and operational strategies optimise activated sludge processes more as a chemical system than as a biological one. While optimising the process in a short time period, these strategies may deteriorate the long-term performance of the process due to their potentially adverse impact on the microbial properties. Through briefly reviewing the evidence available in the literature that plant design and operation affect both the structure and function of the microbial community in activated sludge, we propose to add sludge population optimisation as a new dimension to the control of biological wastewater treatment systems. We stress that optimising the microbial community structure and property should be an explicit aim for the design and operation of a treatment plant. The major limitations to sludge population optimisation revolve around inadequate microbiological data, specifically community structure, function and kinetic data. However, molecular microbiological methods that strive to provide that data are being developed rapidly. The combination of these methods with the conventional approaches for kinetic study is briefly discussed. The most pressing research questions pertaining to sludge population optimisation are outlined. (C) 2002 Elsevier Science Ltd. All rights reserved.

Interference rejection capabilities of different types of array antennas in cellular systems

The suitable use of array antennas in cellular systems results in improvement in the signal-to-interference ratio (StR), This property is the basis for introducing smart or adaptive antenna systems. in general, the SIR depends on the array configuration and is a function of the direction of the desired user and interferers. Here, the SIR performance for linear and circular arrays is analysed and compared.

Development of a novel titration and off-gas analysis (TOGA) sensor for study of biological processes in wastewater treatment systems

The development of the new TOGA (titration and off-gas analysis) sensor for the detailed study of biological processes in wastewater treatment systems is outlined. The main innovation of the sensor is the amalgamation of titrimetric and off-gas measurement techniques. The resulting measured signals are: hydrogen ion production rate (HPR), oxygen transfer rate (OTR), nitrogen transfer rate (NTR), and carbon dioxide transfer rate (CTR). While OTR and NTR are applicable to aerobic and anoxic conditions, respectively, HPR and CTR are useful signals under all of the conditions found in biological wastewater treatment systems, namely, aerobic, anoxic and anaerobic. The sensor is therefore a powerful tool for studying the key biological processes under all these conditions. A major benefit from the integration of the titrimetric and off-gas analysis methods is that the acid/base buffering systems, in particular the bicarbonate system, are properly accounted for. Experimental data resulting from the TOGA sensor in aerobic, anoxic, and anaerobic conditions demonstrates the strength of the new sensor. In the aerobic environment, carbon oxidation (using acetate as an example carbon source) and nitrification are studied. Both the carbon and ammonia removal rates measured by the sensor compare very well with those obtained from off-line chemical analysis. Further, the aerobic acetate removal process is examined at a fundamental level using the metabolic pathway and stoichiometry established in the literature, whereby the rate of formation of storage products is identified. Under anoxic conditions, the denitrification process is monitored and, again, the measured rate of nitrogen gas transfer (NTR) matches well with the removal of the oxidised nitrogen compounds (measured chemically). In the anaerobic environment, the enhanced biological phosphorus process was investigated. In this case, the measured sensor signals (HPR and CTR) resulting from acetate uptake were used to determine the ratio of the rates of carbon dioxide production by competing groups of microorganisms, which consequently is a measure of the activity of these organisms. The sensor involves the use of expensive equipment such as a mass spectrometer and requires special gases to operate, thus incurring significant capital and operational costs. This makes the sensor more an advanced laboratory tool than an on-line sensor. (C) 2003 Wiley Periodicals, Inc.

Control of nitrate recirculation flow in predenitrification systems

The control of the nitrate recirculation flow in a predenitrification system is addressed. An elementary mass balance analysis on the utilisation efficiency of the influent biodegradable COD (bCOD) for nitrate removal indicates that the control problem can be broken down into two parts: maintaining the anoxic zone anoxic (i.e. nitrate is present throughout the anoxic zone) and maximising the usage of influent soluble bCOD for denitrification. Simulation studies using the Simulation Benchmark developed in the European COST program show that both objectives can be achieved by maintaining the nitrate concentration at the outlet of the anoxic zone at around 2 mgN/L. This setpoint appears to be robust towards variations in the influent characteristics and sludge kinetics.

Benchmarking nitrogen removal suspended-carrier biofilm systems using dynamic simulation

We are witnessing an enormous growth in biological nitrogen removal from wastewater. It presents specific challenges beyond traditional COD (carbon) removal. A possibility for optimised process design is the use of biomass-supporting media. In this paper, attached growth processes (AGP) are evaluated using dynamic simulations. The advantages of these systems that were qualitatively described elsewhere, are validated quantitatively based on a simulation benchmark for activated sludge treatment systems. This simulation benchmark is extended with a biofilm model that allows for fast and accurate simulation of the conversion of different substrates in a biofilm. The economic feasibility of this system is evaluated using the data generated with the benchmark simulations. Capital savings due to volume reduction and reduced sludge production are weighed out against increased aeration costs. In this evaluation, effluent quality is integrated as well.

Slurry flow in mills: grate-pulp lifter discharge systems (Part 2)

Pulp lifters, also known, as pan lifters are an integral part of the majority of autogenous (AG), semi-autogenous (SAG) and grate discharge ball mills. The performance of the pulp lifters in conjunction with grate design determines the ultimate flow capacity of these mills. Although the function of the pulp lifters is simply to transport the slurry passed through the discharge grate into the discharge trunnion, their performance depends on their design as well as that of the grate and operating conditions such as mill speed and charge level. However, little or no work has been reported on the performance of grate-pulp lifter assemblies and in particular the influence of pulp lifter design on slurry transport. Ideally, the discharge rate through a grate-pulp lifter assembly should be equal to the discharge rate through at a given mill hold-up. However, the results obtained have shown that conventional pulp lifter designs cause considerable restrictions to flow resulting in reduced flow capacity. In this second of a two-part series of papers the performance of conventional pulp lifters (radial and spiral designs) is described and is based on extensive test work carried out in a I m diameter pilot SAG mill. (C) 2003 Elsevier Science Ltd. All rights reserved.

A practical framework for the generation and selection of strategic plans of action, The relevance of timeframe considerations and a systems thinking approach

The paper proposes a methodology especially focused on the generation of strategic plans of action, emphasizing the relevance of having a structured timeframe classification for the actions. The methodology explicitly recognizes the relevance of long-term goals as strategic drivers, which must insure that the complex system is capable to effectively respond to changes in the environment. In addition, the methodology employs engineering systems techniques in order to understand the inner working of the system and to build up alternative plans of action. Due to these different aspects, the proposed approach features higher flexibility compared to traditional methods. The validity and effectiveness of the methodology has been demonstrated by analyzing an airline company composed by 5 subsystems with the aim of defining a plan of action for the next 5 years, which can either: improve efficiency, redefine mission or increase revenues.

The GUISurfer tool: towards a language independent approach to reverse engineering GUI code

Graphical user interfaces (GUIs) are critical components of today's software. Developers are dedicating a larger portion of code to implementing them. Given their increased importance, correctness of GUIs code is becoming essential. This paper describes the latest results in the development of GUISurfer, a tool to reverse engineer the GUI layer of interactive computing systems. The ultimate goal of the tool is to enable analysis of interactive system from source code.

Combining Formal Methods and Functional Strategies Regarding the Reverse Engineering of Interactive Applications

Abstract. Graphical user interfaces (GUIs) make software easy to use by providing the user with visual controls. Therefore, correctness of GUI’s code is essential to the correct execution of the overall software. Models can help in the evaluation of interactive applications by allowing designers to concentrate on its more important aspects. This paper describes our approach to reverse engineer an abstract model of a user interface directly from the GUI’s legacy code. We also present results from a case study. These results are encouraging and give evidence that the goal of reverse engineering user interfaces can be met with more work on this technique.

Prototyping Concurrent Systems in Cw

Software architecture is currently recognized as one of the most critical design steps in Software Engineering. The specification of the overall system structure, on the one hand, and of the interactions patterns between its components, on the other, became a major concern for the working developer. Although a number of formalisms to express behaviour and supply the indispensable calculational power to reason about designs, are available, the task of deriving architectural designs on top of popular component platforms has remained largely informal. This paper introduces a systematic approach to derive, from behavioural specifications written in Cw, the corresponding architectural skeletons in the Microsoft .NET framework in the form of executable code

Knowledge and technologies in innovative information systems

7th Mediterranean Conference on Information Systems, MCIS 2012, Guimaraes, Portugal, September 8-10, 2012, Proceedings Series: Lecture Notes in Business Information Processing, Vol. 129