Generalised Stream X-Machines and Cooperating Distributed Grammar Systems

Stream X-machines are a general and powerful computational model. By coupling the control structure of a stream X-machine with a set of formal grammars a new machine called a generalised stream X-machine with underlying distributed grammars, acting as a translator, is obtained. By introducing this new mechanism a hierarchy of computational models is provided. If the grammars are of a particular class, say regular or context-free, then finite sets are translated into finite sets, when ?k, = k derivation strategies are used, and regular or context-free sets, respectively, are obtained for ?k, * and terminal derivation strategies. In both cases, regular or context-free grammars, the regular sets are translated into non-context-free languages. Moreover, any language accepted by a Turing machine may be written as a translation of a regular set performed by a generalised stream X-machine with underlying distributed grammars based on context-free rules, under = k derivation strategy. On the other hand the languages generated by some classes of cooperating distributed grammar systems may be obtained as images of regular sets through some X-machines with underlying distributed grammars. Other relations of the families of languages computed by generalised stream X-machines with the families of languages generated by cooperating distributed grammar systems are established. At the end, an example dealing with the specification of a scanner system illustrates the use of the introduced mechanism as a formal specification model. Received September 1999 / Accepted in revised form October 2000     

Testing Conformance to a Quasi-Non-Deterministic Stream X-Machine

Stream X-machines have been used in order to specify a range of systems. One of the strengths of this approach is that, under certain well-defined conditions, it is possible to produce a finite test that is guaranteed to determine the correctness of the implementation under test (IUT). Initially only deterministic stream X-machines were considered in the literature. This is largely because the standard test algorithm relies on the stream X-machine being deterministic. More recently the problem of testing to determine whether the IUT is equivalent to a non-deterministic stream X-machine specification has been tackled. Since non-determinism can be important for specifications, this is an extremely useful extension. In many cases, however, we wish to test for a weaker notion of correctness called conformance. This paper considers a particular form of non-determinism, within stream X-machines, that will be called quasi-non-determinism. It then investigates the generation of tests that are guaranteed to determine whether the IUT conforms to a quasi-non-deterministic stream X-machine specification. The test generation algorithm given is a generalisation of that used for testing from a deterministic stream X-machine. Received November 1999 / Accepted in revised form December 2000     

Generating Test Sets from Non-Deterministic Stream X-Machines

X-machines were proposed by Holcombe as a possible specification language and since then a number of further investigations have demonstrated that the model is intuitive and easy to use as well as general enough to cater for a wide range of applications. In particular (generalised) stream X-machines have been found to be extremely useful as a specification method and most of the theory developed so far has concentrated on this particular class of X-machines. Furthermore, a method for testing systems specified by stream X-machines exists and is proved to detect all faults of the implementation provided that the system meets certain initial requirements. However, this method can only be used to generate test sequences from deterministic X-machine specifications. In this paper we present the theoretical basis for a method for generating test sets from non-deterministic generalised stream X-machines. Received November 1999 / Accepted in revised form September 2000     

A Structured Way to Use Channels for Communication in X-Machine Systems

This paper presents a new model for passing messages in communicating stream X-machine systems (CSXMS). The components are stream X-machines with ε-transitions, acting simultaneously. The states are partitioned into processing and communicating states. Passing messages between the X-machines involves only communicating states. A communication matrix is used as a common memory. It is shown that a structured way of using channels, namely via select constructs with guarded alternatives and terminate clause, may be implemented. An automatic scheme for writing concurrent programs in an Ada-like style, starting from a CSXMS, is proposed. Received December 1999 / Accepted in revised form January 2001     

Checking experiments for stream X-machines

Stream X-machines are a state based formalism that has associated with it a particular development process in which a system is built from trusted components. Testing thus essentially checks that these components have been combined in a correct manner and that the orders in which they can occur are consistent with the specification. Importantly, there are test generation methods that return a checking experiment: a test that is guaranteed to determine correctness as long as the implementation under test (IUT) is functionally equivalent to an unknown element of a given fault domain Ψ. Previous work has show how three methods for generating checking experiments from a finite state machine (FSM) can be adapted to testing from a stream X-machine. However, there are many other methods for generating checking experiments from an FSM and these have a variety of benefits that correspond to different testing scenarios. This paper shows how any method for generating a checking experiment from an FSM can be adapted to generate a checking experiment for testing an implementation against a stream X-machine. This is the case whether we are testing to check that the IUT is functionally equivalent to a specification or we are testing to check that every trace (input/output sequence) of the IUT is also a trace of a nondeterministic specification. Interestingly, this holds even if the fault domain Ψ used is not that traditionally associated with testing from a stream X-machine. The results also apply for both deterministic and nondeterministic implementations.     

Testing Conditions for Communicating Stream X-machine Systems

X-machines were proposed by Holcombe as a possible specification language and since then a number of further investigations have demonstrated that the model is intuitive and easy to use. In particular, stream X-machines (SXM), a particular class of X-machines, have been found to be extremely useful in practice. Furthermore, a method of testing systems specified as SXMs exists and is proved to detect all faults of the implementation provided that the system meets certain “design for test conditions”. Recently, a system of communicating SXMs was introduced as a means of modelling parallel processing. This paper proves that each communicating machine component can be transformed in a straightforward manner so that the entire system will behave like a single stream X-machine - the equivalent SXM of the system. The paper goes on to investigate the applicability of the SXM testing method to a system of communicating SXMs and identifies a class of communicating SXMs for which the equivalent SXM of the system meets the “design for test conditions”. Received November 1999 / Accepted in revised form June 2001     

Editorial

Formal Aspects of Computing marks the end of the first year of our re-launched format. It has not been an easy year either for the editors or for the ever-patient staff at Springer-Verlag; but it has certainly been successful with first class papers being published soon after acceptance. As with most computing journals, refereeing poses a (potential) bottleneck to getting an author's ideas into print but even here our colleagues at Springer-Verlag have come up with an incentive scheme from which our future referees will benefit and hopefully speed the refereeing process to everyone's advantage. Recently, most editions of the journal have been standard issues with a number of submitted papers. It has been our stated intention since the journal began to have special editions with whole editions on a single topic. We are currently planning such a special edition to mark Rod Burstall's retirement (in fact we have so many excellent papers that there will probably have to be a double edition). This special issue collects a number of papers on X-machines edited by Mike Holcombe and myself. Mike has written a brief introduction and there follow five papers which have all been refereed by experts in the area (I took personal charge of having Mike's paper refereed). The generalisation of the testing theory to non-deterministic stream X-machines is the focus of two articles. Non-determinism can be generalised in several ways. R. Hierons and M. Harman look at quasi-non-deterministic machines and describe an approach to dealing with the generation of test sets for such machines. F. Ipate and M. Holcombe look at another way to view non-determinism and also focus on test set generation, the issue of fairness becomes important if the strong claims about fault detection by the test sets are to be achieved. M. Gheorghe has investigated how a collection of formal grammars can be controlled by a type of generalised stream X-machine so that the languages generated by such a system of grammars can be determined. He has shown that relatively simple grammars can generate very complex languages using this approach. T. Balanescu explores further generalisations of Stream X-machines and discusses how the design for test conditions can be adapted for a specific type of machine. A. Cowling et al. look at communicating X-machine systems and consider how this approach can be used to model message passing using a simple communicating matrix metaphor. Models built this way can be used to generate, automatically, concurrent programs. In a paper to appear in Volume 13, F. Ipate and M. Holcombe look at how the test theory can be adapted to apply to the communicating X-machines systems case. Indeed, Volume 13 already looks to be an exciting mix of scientific contributions – we also expect to back on a more regular publication schedule by the end of 2001.     

Complete deterministic stream X-machine testing

One of the strengths of using stream X-machines to specify a system is that, under certain well defined conditions, it is possible to produce a test set that is guaranteed to determine the correctness of an implementation. However, the existing method assumes that the implementation of each processing function is proved to be correct before the actual testing can take place, so it only test the system integration. This paper presents a new method for generating test sets from a deterministic stream X-machine specification that generalises the existing integration testing method. This method no longer requires the implementations of the processing functions to be proved correct prior to the actual testing. Instead, the testing of the processing functions is performed along with the integration testing.Accepted in revised form 27 February 2004 by D.A. Duce     

Separable resolution method for checking the satisfiability of formulas in the languageL

Conclusion This paper offers an effective resolution method for checking the satisfiability of a collection of disjuncts in the languageL. The method permits one to substantially reduce the number of generated resolvents in comparison with the method ofR-resolution. One more factor ensuring the efficiency of the method is a significant reduction in the number of disjunct pairs checked for the possibility of resolving them. As for the number of generated disjuncts, its greatest reduction is obtained in the case of the use of the disjunct-set partition corresponding to the limiting system of predicate-symbol subsets given by symbol ordering. It is possible to interpret the result obtained for this case as proof of the completeness of the strategy combining an ordering of predicate symbols andR-resolution. It is necessary to note that to different orderings of predicate symbols correspond different partitions of the disjunct set giving, in turn, different numbers of generated disjuncts in the process ofSp-completion. Nevertheless, the methods described in Sec. 2, which use partition of the disjunct set into two classes, are of independent importance. As has already been said, completion of a disjunct set is used for solution of a number of problems during the design of a procedural automaton specification. For example, in the case of checking the consistency of two interacting automata [5] based on completion of a disjunct set, there exists a natural partition of the predicate symbols into input and output symbols, to which corresponds the partition of the disjunct set into subsets specifying the interacting automata. Translated from Kibernetika i Sistemnyi Analiz, No. 6, pp. 13–20, November–December, 1998.