A framework and tool support for the systematic testing of model-based specifications

Formal specifications can precisely and unambiguously define the required behavior of a software system or component. However, formal specifications are complex artifacts that need to be verified to ensure that they are consistent, complete, and validated against the requirements. Specification testing or animation tools exist to assist with this by allowing the specifier to interpret or execute the specification. However, currently little is known about how to do this effectively. This article presents a framework and tool support for the systematic testing of formal, model-based specifications. Several important generic properties that should be satisfied by model-based specifications are first identified. Following the idea of mutation analysis, we then use variants or mutants of the specification to check that these properties are satisfied. The framework also allows the specifier to test application-specific properties. All properties are tested for a range of states that are defined by the tester in the form of a testgraph, which is a directed graph that partially models the states and transitions of the specification being tested. Tool support is provided for the generation of the mutants, for automatically traversing the testgraph and executing the test cases, and for reporting any errors. The framework is demonstrated on a small specification and its application to three larger specifications is discussed. Experience indicates that the framework can be used effectively to test small to medium-sized specifications and that it can reveal a significant number of problems in these specifications.

Off-diagonal long-range order in a supersymmetric integrable model of correlated electrons

A new model for correlated electrons is presented which is integrable in one-dimension. The symmetry algebra of the model is the Lie superalgebra gl(2\1) which depends on a continuous free parameter. This symmetry algebra contains the eta pairing algebra as a subalgebra which is used to show that the model exhibits Off-Diagonal Long-Range Order in any number of dimensions.

A modified pore-filling isotherm for liquid-phase adsorption in activated carbon

This article modifies the usual form of the Dubinin-Radushkevich pore-filling model for application to liquid-phase adsorption data, where large molecules are often involved. In such cases it is necessary to include the repulsive part of the energy in the micropores, which is accomplished here by relating the pore potential to the fluid-solid interaction potential. The model also considers the nonideality of the bulk liquid phase through the UNIFAC activity coefficient model, as well as structural heterogeneity of the carbon. For the latter the generalized adsorption integral is used while incorporating the pore-size distribution obtained by density functional theory analysis of argon adsorption data. The model is applied here to the interpretation of aqueous phase adsorption isotherms of three different esters on three commercial activated carbons. Excellent agreement between the model and experimental data is observed, and the fitted Lennard-Jones size parameter for the adsorbate-adsorbate interactions compares well with that estimated from known critical properties, supporting the modified approach. On the other hand, the model without consideration of bulk nonideality, or when using classical models of the characteristic energy, gives much poorer bts of the data and unrealistic parameter values.

Supporting the software testing process through specification animation

Achieving consistency between a specification and its implementation is an important part of software development. In this paper, we present a method for generating passive test oracles that act as self-checking implementations. The implementation is verified using an animation tool to check that the behavior of the implementation matches the behavior of the specification. We discuss how to integrate this method into a framework developed for systematically animating specifications, which means a tester can significantly reduce testing time and effort by reusing work products from the animation. One such work product is a testgraph: a directed graph that partially models the states and transitions of the specification. Testgraphs are used to generate sequences for animation, and during testing, to execute these same sequences on the implementation.

Site-directed mutants of RTP of Bacillus subtilis and the mechanism of replication fork arrest

DNA replication fork arrest during the termination phase of chromosome replication in Bacillus subtilis is brought about by the replication terminator protein (RTP) bound to specific DNA terminator sequences (Tev sites) distributed throughout the terminus region. An attractive suggestion by others was that crucial to the functioning of the RTP-Ter complex is a specific interaction between RTP positioned on the DNA and the helicase associated with the approaching replication fork. Ln support of this was the behaviour of two site-directed mutants of RTP. They appeared to bind Ter DNA normally but were ineffective in fork arrest as ascertained by in vitro Escherichia coli DnaB helicase and replication assays. We describe here a system for assessing the fork-arrest behaviour of RTP mutants in a bona fide in vivo assay in B. subtilis. One of the previously studied mutants, RTP.Y33N, was non-functional in fork arrest in vivo, as predicted. But through extensive analyses, this RTP mutant was shown to be severely defective in binding to Ter DNA, contrary to expectation. Taken in conjunction with recent findings on the other mutant (RTP.E30K), it is concluded that there is as yet no substantive evidence from the behaviour of RTP mutants to support the Rm-helicase interaction model for fork arrest. In an extension of the present work on RTP.Y33N, we determined the dissociation rates of complexes formed by wild-type (wt) RTP and another RTP mutant with various terminator sequences. The functional wtRTP-TerI complex was quite stable (half-life of 182 minutes), reminiscent of the great stability of the E. coli Tus-Ter complex. More significant were the exceptional stabilities of complexes comprising wtRTP and an RTP double-mutant (E39K.R42Q) bound to some particular terminator sequences. From the measurement of in vivo fork-arrest activities of the various complexes, it is concluded that the stability (half-life) of the whole RTP-Ter complex is not the overriding determinant of arrest, and that the RTP-Ter complex must be actively disrupted, or RTP removed, by the action of the approaching replication fork. (C) 1999 Academic Press.

A new integrable model of strongly correlated electrons with Hubbard-like interaction

A new completely integrable model of strongly correlated electrons is proposed which describes two competitive interactions: one is the correlated one-particle hopping, the other is the Hubbard-like interaction. The integrability follows from the fact that the Hamiltonian is derivable from a one-parameter family of commuting transfer matrices. The Bethe ansatz equations are derived by algebraic Bethe ansatz method.

Site-directed mutagenesis and kinetic studies of the West Nile virus NS3 protease identify key enzyme-substrate interactions

The flavivirus West Nile virus (WNV) has spread rapidly throughout the world in recent years causing fever, meningitis, encephalitis, and fatalities. Because the viral protease NS2B/NS3 is essential for replication, it is attracting attention as a potential therapeutic target, although there are currently no antiviral inhibitors for any flavivirus. This paper focuses on elucidating interactions between a hexapeptide substrate (Ae-KPGLKR-p-nitroanilide) and residues at S1 and S2 in the active site of WNV protease by comparing the catalytic activities of selected mutant recombinant proteases in vitro. Homology modeling enabled the predictions of key mutations in VWNV NS3 protease at S1 (V115A/F, D129A/ E/N, S135A, Y150A/F, S160A, and S163A) and S2 (N152A) that might influence substrate recognition and catalytic efficiency. Key conclusions are that the substrate P1 Arg strongly interacts with S1 residues Asp-129, Tyr-150, and Ser-163 and, to a lesser extent, Ser-160, and P2 Lys makes an essential interaction with Asn-152 at S2. The inferred substrate-enzyme interactions provide a basis for rational protease inhibitor design and optimization. High sequence conservation within flavivirus proteases means that this study may also be relevant to design of protease inhibitors for other flavivirus proteases.

A graphical specification of model transformations with triple graph grammars

Models and model transformations are the core concepts of OMG's MDA (TM) approach. Within this approach, most models are derived from the MOF and have a graph-based nature. In contrast, most of the current model transformations are specified textually. To enable a graphical specification of model transformation rules, this paper proposes to use triple graph grammars as declarative specification formalism. These triple graph grammars can be specified within the FUJABA tool and we argue that these rules can be more easily specified and they become more understandable and maintainable. To show the practicability of our approach, we present how to generate Tefkat rules from triple graph grammar rules, which helps to integrate triple graph grammars with a state of a art model transformation tool and shows the expressiveness of the concept.

Formal analysis of human-computer interaction using model checking

Experiments with simulators allow psychologists to better understand the causes of human errors and build models of cognitive processes to be used in human reliability assessment (HRA). This paper investigates an approach to task failure analysis based on patterns of behaviour, by contrast to more traditional event-based approaches. It considers, as a case study, a formal model of an air traffic control (ATC) system which incorporates controller behaviour. The cognitive model is formalised in the CSP process algebra. Patterns of behaviour are expressed as temporal logic properties. Then a model-checking technique is used to verify whether the decomposition of the operator's behaviour into patterns is sound and complete with respect to the cognitive model. The decomposition is shown to be incomplete and a new behavioural pattern is identified, which appears to have been overlooked in the analysis of the data provided by the experiments with the simulator. This illustrates how formal analysis of operator models can yield fresh insights into how failures may arise in interactive systems.

Adsorption in mesopores: A molecular-continuum model with application to MCM-41

The classical model of surface layering followed by capillary condensation during adsorption in mesopores, is modified here by consideration of the adsorbate solid interaction potential. The new theory accurately predicts the capillary coexistence curve as well as pore criticality, matching that predicted by density functional theory. The model also satisfactorily predicts the isotherm for nitrogen adsorption at 77.4 K on MCM-41 material of various pore sizes, synthesized and characterized in our laboratory, including the multilayer region, using only data on the variation of condensation pressures with pore diameter. The results indicate a minimum mesopore diameter for the surface layering model to hold as 14.1 Å, below which size micropore filling must occur, and a minimum pore diameter for mechanical stability of the hemispherical meniscus during desorption as 34.2 Å. For pores in-between these two sizes reversible condensation is predicted to occur, in accord with the experimental data for nitrogen adsorption on MCM-41 at 77.4 K.

The case for the ability-based model of emotional intelligence in organizational behavior

In this second counterpoint article, we refute the claims of Landy, Locke, and Conte, and make the more specific case for our perspective, which is that ability-based models of emotional intelligence have value to add in the domain of organizational psychology. In this article, we address remaining issues, such as general concerns about the tenor and tone of the debates on this topic, a tendency for detractors to collapse across emotional intelligence models when reviewing the evidence and making judgments, and subsequent penchant to thereby discount all models, including the ability-based one, as lacking validity. We specifically refute the following three claims from our critics with the most recent empirically based evidence: (1) emotional intelligence is dominated by opportunistic academics-turned-consultants who have amassed much fame and fortune based on a concept that is shabby science at best; (2) the measurement of emotional intelligence is grounded in unstable, psychometrically flawed instruments, which have not demonstrated appropriate discriminant and predictive validity to warrant/justify their use; and (3) there is weak empirical evidence that emotional intelligence is related to anything of importance in organizations. We thus end with an overview of the empirical evidence supporting the role of emotional intelligence in organizational and social behavior.