Formal Aspects of Computing (2000) 12: 418–422 c 2000 BCS

Formal Aspects of Computing

What are X-Machines? Mike Holcombe Department of Computer Science, University of Sheffield, Sheffield, UK

1. Introduction X-machines were introduced by S. Eilenberg in 1974 ([Eil74]) as a mathematical framework for examining the relationships between languages and automata. The X-machine definition provided a very general concept that captured in a simple and elegant way a wide variety of existing models and their computational behaviour. Thus finite state machines, pushdown automata and Turing machines all provided different examples of X-machines obtained by varying some of the components of the X-machine’s definition. Definition 1.1. An X-Machine is a 10-tuple M = (X, Y , Z, α, β, Q, Φ, F, I, T ), where • X is the fundamental data set that the machine operates on. • Y and Z are the input and the output sets, respectively. • α and β are the input and the output (partial) functions respectively, used to convert the input and the output sets into, and from, the fundamental set: α : Y −→ X, and β : X −→ Z • Q is the (finite) set of states. • F is the type of M , a set of relations on X : Φ : P(X −→ X) • F is the next-state partial function: F : Q × F −→ PQ F is often described by means of a state-transition diagram. • I and T are the sets of initial and terminal (or final) states respectively: I ⊆ Q, T ⊆ Q The type of the machine is the class of partial functions that constitute the elementary operations that the machine is capable of performing. PQ denotes the power set of Q and (X −→ X) denotes the set of all, possibly partial, functions from X to X. Φ is viewed as an abstract alphabet. Φ may be infinite, but only a finite subset Φ0 of Φ is used (this is because M has only a finite number of edges despite the infinite number of labels available). It is sometimes helpful to think of an X-machine as a finite state machine with the arcs labelled by functions from the type Φ. A computation takes the form of a traversal of a path in the state space and the application, in turn, of the path labels (which represent basic processing functions or relations) to an initial Correspondence and offprint requests to: Mike Holcombe, Department of Computer Science, University of Sheffield, Regent Court, 211 Portobello Street, Sheffield, S1 4DP, UK. e-mail: [email protected]

What are X-Machines?

419

value of the data set X. Thus the machine transforms values of its data set according to the functions called during the state space traversal. The role of the input and output encoding relations is not crucial for many situations but it does provide a general interface mechanism that is useful in a number of applications. One interesting aspect that may be worthwhile investigating involves the use of X-machines where the type consists of functions that are not necessarily computable themselves. It is possible that the computational capability of such machines could be categorised and investigated fruitfully with these ideas. The subject of hypercomputation and super-Turing machines are cases in point [Sta90b]. One of the most useful developments in the theory so far is the development of a theory of testing based on the subclass of stream X-machines. The idea of a stream X-machine is close to some of Eilenberg’s initial thoughts and was introduced explicitly in Laycock, [Lay92]. The full testing theory was developed by Ipate ([Ipa95a]) and represents an important and practical application of the theory. The basic concept is one of comparing two stream X-machines using a finite set of input sequences so as to determine if they compute the same function. The observations of their outputs provide the mechanism for determining if they behave identically. Since one of the machines could be an implementation and the other the specification this technique becomes a practical method of testing real systems. The theory highlights the importance of design for test conditions for the specification. Given that these are satisfied then the method can be used to test a system in a systematic and complete way. Essentially the approach is one of system or integration testing and has the very powerful property that the test sets will reveal all possible faults provided the basic components (the type) is implemented correctly, ([HoI98]). This provides a hierarchical and reductionist approach to testing that is very attractive in both software engineering and in VLSI engineering. The use of X-machines, stream X-machines and Communicating X-machine systems as a notation for specifying systems has been studied quite extensively lately. The indications are very promising and have given rise to a number of successful industrial developments. Not only do X-machines provide a precise notation for describing a system but they are also flexible and simple to use. In fact, compared to many other mathematical notations they seem to be very easy to use by programmers and designers. Another advantage is the way that specifications can be managed and full advantage taken of the ability to abstract detail from the state space. Thus the state explosion problems faced by finite state machines and other low level notations can be avoided. Some examples that have been examined involved millions of transitions at the bottom level and the test set generation algorithms were able to deal with this complexity simply ([Bog00]). The idea of specification refinement is also important and the relationship between specifications and test sets is so tight that test sets can be refined in parallel with specifications ([HoI98]).

2. Some possible future directions The use of X-machines to model various systems is continuing and some promising avenues are opening up. VLSI systems, in particular VHDL descriptions, can be modelled using X-machines, and, in the particular context of hardware design, test sets generated which will provide a mechanism for both functional testing of hardware and efficient simulation of designs. Object-oriented software is notoriously difficult to test. Attempts are being made to develop the theory of X-machines to relate it more closely to the OO design paradigm. It is not so hard to deal with models of individual classes and objects, the problem is finding a natural way to model the integration of these. A more general problem is the modelling of agent-based systems. Again, individual reactive agents can be modelled by X-machines in a natural way but the problem is modelling communities of agents which may be collaborating or competing with one another. The X-machine model could also be the basis of a generalised type of model checking where the existence of the internal memory is explored in combination with state space exploration. It is possible that this would allow for very efficient analysis of large systems that are currently too big in terms of their state size for existing techniques. It is already clear that efficient code can be generated automatically from X-machine specifications and this is also a fruitful area for further developments. The problem of legacy systems can be attacked by reverse engineering a stream X-machine specification from source code prior to analysis and refinement into more modern languages. The fact that a strong and rigorous method of testing is closely linked to the theory is a real benefit. Even code that is produced by an approved code generator will need to be tested in its operating environment. A number of prototype tools have been developed, these include a system for checking the syntax of a

420

M. Holcombe

stream X-machine model, an animator and test generation tools. A draft X-Machine Definition Language (XMDL) has also been introduced. Below we give an extensive chronological set of references to significant work relating to X-machines.

References [Eil74] [Hol84] [Hol87a] [Hol87b] [Sta87] [Hol88a] [Hol88b] [Hol90]

Eilenberg, S.: ‘Automata, Languages and machines’, Volume A. Academic Press, 1974. Holcombe, M.: ‘Systems, machines and algebra’, BCS-FACS (6): 1984. Holcombe, M.: ‘Formal methods in the specification of the human-machine interface’, Intl C.I.S. J. 1(2): 1987, 24–34. Holcombe, M.: ‘Goal-directed task analysis’, Intl C.I.S. J. 1(4): 1987, 14–22. Stannett, M.: ‘An organisational approach to decision-making in command systems’. Intl C.I.S. J. 1, 1987, 23–34. Holcombe, M.: ‘Algebraic techniques in system specification’, Bull. Irish Math. Soc. 21, 1988, 13–28. Holcombe, M.: ‘X-machines as a basis for dynamic systems specification’, Software Engineering Journal 3(2): 1988, 69–76. Holcombe, M.: ‘Software Engineering, in Trends in Information Technology’. Ed. D. Linkens and R. Nicolson. Peregrinus, 1990, pp. 17–36. [Sta90a] Stannett, M.: ‘Implications of X-machines and the Halting Problem: Building a super-Turing machine for computational AI’, AISB Quarterly 74. [Sta90b] Stannett, M.: ‘X-machines and the Halting Problem: Building a super-Turing machine’, Formal Aspects of Computing 2, 331–41. [Sta91] Stannett, M.: ‘An Introduction to post-Newtonian and non-Turing Computation’, Technical Report, Department of Computer Science, University of Sheffield, CS-91-02. [Cla91] Clarke, S.: ‘The Modelling and Evaluation of the Human-Computer Interface’, PhD thesis, University of Sheffield, 1991. [Lay92] Laycock, G.: ‘The Theory and Practice of Specification-Based Software Testing’, PhD thesis, University of Sheffield, 1992. [Hol93] Holcombe, M.: ‘An integrated methodology for the formal specification, verification and testing of systems’, Proc. Eurostar 93, London. [Hol94] Holcombe, M.: ‘From VLSI through machine models to cellular metabolism’, in R. Paton, Computing with biological metaphors Chapman and Hall. [HoP94] Holcombe, M. and Paton, R.: ‘Computational models of cellular information systems’, IEE Coll. Molecular Bioinformatics, London, 3/1–3/5. [PaH94] Paton, R. and Holcombe, M.: ‘Computational models of cellular information systems’, in Advances in Molecular Bioinformatics, ed. S. Schulze-Kremer, IOS Press. [ZHL94] Duan, Z., Holcombe, M. and Linkens, D.: ‘Timed interval temporal logic and the modelling of hybrid systems’, Pro. Eur. Simulation Multi-Conference, Barcelona, 534–541. [FHIJL95] Fairtlough, M., Holcombe, M., Ipate, F., Jordan, C., Laycock, G. and Duan, Z.: ‘Using an X-machine to model a video cassette recorder’, Current issues in Electronic modelling 3, 141–151. [ZHL95a] Duan, Z., Holcombe, M. and Linkens, D. A.: ‘Modelling of a Soaking Pit Furnace in Hybrid Machines’, Systems Analysis, Modelling, and Simulation. 18, 153–157. [ZHL95b] Duan, Z. H., Holcombe, M. and Linkens, D. A.: ‘Specification of a Soaking Pit System in Parallel Hybrid Machines’, in Proceedings of the 21 Euromicro Conference, IEEE/CS, pp. 241–247, Como, Italy, September 4–7. [HIG95] Holcombe, M., Ipate, F. and Grondoudis, A.: ‘Complete functional testing of safety critical systems’. Proc. IFAC Workshop on Emerging Control Technologies. Florida, 343–358. [Ipa95a] Ipate, F.: ‘Theory of X-machines and Applications in Specification and Testing’, PhD Thesis, University of Sheffield. [BeH95] Bell, A. and Holcombe, M.: Computational models of cellular processing, Proc. Conf. on Information Processing in Cells and Tissues ’95. Liverpool, 171–184. [Ipa95b] Ipate, F.: ‘X-machine Based Testing’, in Proceedings of the 10th International Conference on Control Systems and Computer Science, Vol. 2, Bucharest, 262–272. [BTWW95] Barnard, J., Theaker, C., Whitworth, J. and Woodward, M.: ‘Real-time communicating X-machines for the formal design of real-time systems’, Proceedings of DARTS ’95, Universite Libre, Brussels, Belguim, November 9–11th. [BeN95] Berki, E. and Novakovic, D.: ‘Towards an Integrated Specification Environment (ISE)’, In the Proc. of the 5th Hellenic International Conference of Informatics, Athens, GREECE. [Ipa95c] Ipate, F.: ‘X-machine based testing’, in Proceedings of 10th Int. Conf. Control Systems and Computer Science, Vol. 2, Bucharest, pp. 262–272. [DuH96] Duan, Z. H. and Holcombe, M.: ‘From Requirements to Specifications for Hybrid Systems’, Proceedings of the International Symposium on Future Software Technology, Xian, China, Oct 9–11, 239–246. [IpH96] Ipate, F. and Holcombe, M.: ‘Another look at computability’, Informatica, 20, 359–372. [BeH96] Bell, A. and Holcombe, M.: ‘Computational models of cellular processing’, in Computation in Cellular and Molecular Biological Systems. M. Holcombe, R. Paton and R. Cuthbertson (Eds.), World Scientific Press, Singapore. [BWW96] Barnard, J., Whitworth, J. and Woodward, M.: ‘Communicating X-machines’, Information and Software Technology, 38, 401–407. [Dua96] Duan, Z.: ‘Modelling of Hybrid Systems’, PhD thesis, University of Sheffield. [BeG96] Berki, E. and Georgiadou, E.: ‘Towards resolving Data Flow Diagramming Deficiencies by using Finite State Machines’, 5th Software Quality Conference, Universities of Abertay Dundee and Humberside, ISBN: 1 899796 02 9, Scotland, UK. [GeB96] Georgiadou, E. and Berki, E.: ‘Improving Systems Specification Understandability by Using a Hybrid Approach’, First International Conference on Software Process Improvement, Research, Education and Training, (INSPIRE ’96), The British Computer Society, ISBN: 1899621113, Bilbao, SPAIN.

What are X-Machines?

[BFHIJ97] [IpH97] [Hol97] [Ipa97a] [SBGS97] [BGS97] [BBGM97] [Ipa97b] [IpH98a] [IpH98b] [BoH98] [BeH98] [HoI98] [Bel98] [Bar98] [BeG98] [BCG99] [KeK99] [Bar99] [Ipa99a] [Ipa99b] [Ipa99c] [BGH00a] [IpH00] [Hol00] [BGH00b] [DHB00] [Ele00] [KEK00a] [KeS00] [Kef00a] [KeK00] [GeV00] [Kef00b] [BoH00]

421

Bogdanov, K., Fairtlough, M., Holcombe, M., Ipate, F. and Jordan, C.: ‘X-machine Specification and Refinement of Digital Devices’, Department of Computer Science Internal Report, CS-97-16, University of Sheffield. Ipate, F. and Holcombe, M.: ‘An Integration Testing method which is proved to find all faults’. Intl J. Comp. Math. 63, 159–178. Holcombe, M.: ‘When testing is done’. Proc. EuroSTAR97, Edinburgh. Ipate, F.: ‘Is software testing effective?’, in Proceedings of the 3rd International Symposium of Economic Informatics, Bucharest, 173–179. Siakas, K., Berki, E., Georgiadou, E. and Sadler, C.: ‘The Complete Alphabet of Quality Information Systems’: Conflicts and Compromises ”, 7th World Congress on Total Quality Management (TQM ’97), McGraw-Hill, ISBN 0-07-463186-1, N. Delhi, INDIA. Berki, E., Georgiadou, E. and Siakas, K.: ‘A Methodology is as strong as the degree of user involvement it supports’, Proceedings of the International Symposium on Software Engineering in the Universities (ISSEU ’97), Rovaniemi, FINLAND. Bavan, S., Berki, E., Georgiadou, E., Milankovic-Atkinson, M. and Walker, M.: ‘Towards a Formal Specification of an Object-Oriented Parallel Architecture’, International Conference for Parallel and Distributed Processing Techniques and Applications (PDPTA), Volume II, ISBN: 0-9648666-6-8, Las Vegas, USA. Ipate, F.: ‘Is Software Testing Effective?’ in proceedings of 3rd. Int. Symposium of Economic Informatics, Bucharest, pp. 173–179. Ipate, F. and Holcombe, M.: ‘A method for refining and testing generalised machine specifications’. Intl J. Comp. Math. 68, 197–219. Ipate, F. and Holcombe, M.: ‘Specification and testing using generalised machines’: a presentation and a case study. Software testing, Verification and Reliability, 8, 61–81. Bogdanov, K. and Holcombe, M.: ‘Automated Test Set Generation for Statecharts’, in Applied Formal Methods FM-Trends 98 (Boppard, Germany), D. Hutter, W. Stephan, P. Traverso and M. Ullmann (Editors), Springer LNCS Series, 1641. Bell, A. and Holcombe, M.: ‘Computational models of immunological systems’. In Information Processing in Cells and Tissues, (eds.) M. Holcombe and R. Paton, 213–226. Plenum Press. Holcombe, M. and Ipate, F.: ‘Correct systems - building a business process solution’. Springer, Applied Computing Series. Bell, A.: ‘Formal Computational Models of Biological Systems’, PhD thesis, University of Sheffield. Barnard, J.: ‘COMX: a design methodology using communicating X-machines’, Inform. Software Tech. 40(5–6): 271–280. Berki, E. and Georgiadou, E.: ‘A Comparison of Qualitative Frameworks for Information Systems Development Methodologies’, Proceedings of The Twelfth International Conference of The Israel Society for Quality, Jerusalem, ISRAEL. Balanescu, T., Cowling, A. J., Georgescu, H., Gheorghe, M., Holcombe, M. and Vertan, C.: ‘Communicating Stream X-machines Systems are no more than X-machines’. Journal of Universal Computer Science, Volume 5, no. 9, 494–507. Kefalas, P. and Kapeti, E.: ‘A Design Language and Tool for X-Machines Specification in Advances in Informatics’, edited by D. I. Fotiadis, S. D. Nikolopoulos, World Scientific. Barnard, J.: ‘Object COMX: Methodology using communicating X-machine objects’, J. Object-oriented Prog. 12(7): 12–17. Ipate, F.: ‘Using Hybrid Machines for specifying Hybrid Software Systems’, in Proceedings of the 4th International Symposium of Economic Informatics, Bucharest, 679–686. Ipate, F.: ‘Using Hybrid Machines for Specifying Hybrid Software Systems’, in Proceedings of 4th Int. Symp. of Economic Informatics, Bucharest, pp. 679–686. Ipate, F.: ‘A method for testing non-deterministic X-machines that finds all faults’, to appear in Proc. CAIM 1999, Pitesti. Balanescu, T., Gheorghe, M., Holcombe, M.: ‘Deterministic stream X-machines based on grammar systems in Words’, sequences, grammars, languages: where biology, computer science, linguistics and mathematics meet, Volume I, Ed. C. Martin-Vide and V. Mitrana, Kluwer. Ipate, F. and Holcombe, M.: ‘Testing non-deterministic X-machines’, in Words, sequences, grammars, languages: where biology, computer science, linguistics and mathematics meet, Volume II, Ed. C. Martin-Vide and V. Mitrana, Kluwer. Holcombe, M.: ‘X-machines in Computing’, Biology and Art. Proceedings, Grammar Systems 2000, ed. R. Freund and A. Kelemenova, Silesian University at Opava, Czech Republic, ISBN 80-7248-067-7, 343–346. Balanescu, T., Gheorghe, M. and Holcombe, M.: ‘A subclass of stream X-machines with underlying distributed grammars’, Proceedings, Grammar Systems 2000, ed. R. Freund and A. Kelemenova, Silesian University at Opava, Czech republic, ISBN 80-7248-067-7, 93–112. Duan, Z., Holcombe, M., Bell, A.: ‘A logic for Biological Systems’, Biosystems, 55(1–3): 93–105. Eleftherakis, G.: ‘Model Checking and X-machine Specification’, Technical Report, CS-02/00, City College, Thessaloniki, Greece. Kehris, E., Eleftherakis, G. and Kefalas, P.: ‘Using X-machines to Model and Test Discrete Event Simulation Programs’, in Proceedings of the 4th World MultiConference on Circuits, Systems, Communications and Computers (CSCC), Athens. Kefalas, P. and Sotiriadou, A.: ‘Transforming X-machines to Z Specifications’, Technical Report, CS-06/00, City College, Thessaloniki, Greece. Kefalas, P.: ‘X-machine Description Language’: User Manual, version 1.6, Technical Report, CS-07/00, City College, Thessaloniki, Greece. Kefalas, P. and Kapeti, E.: ‘A Design Language and Tool for X-machine Specification’, in Advances in Informatics, (D. I. Fotadis and S. D. Nikolopoulos eds.), World Scientific, 134–145. Georgescu, H. and Vertan, C.: ‘A New Approach to Communicating Stream X-machines’, Journal of Universal Computer Science, 6(5): 490–502. Kefalas, P.: ‘Automatic translation from X-machines to Prolog’, Technical Report, CS-01/00, City College, Thessaloniki, Greece. Bogdanov, K. and Holcombe, M.: ‘Statechart Testing Method for Aircraft Control’, To appear, Software Testing, Verification and Reliability.

422

[Kef00c] [KEK00b] [Van00] [Bog00] [Ch-S00] [Ch-C00] [Gro00] [HBGR00] [IpP00] [Ipa00] [Ber00] [HiH00] [Ghe00] [Bal00] [IpH00] [CHV00] [HIB01] [ElK01]

M. Holcombe

Kefalas, P.: ‘Modelling an Agent Reactive Architecture with X-machines’, Technical Report, CS-01/00, City College, Thessaloniki, Greece. Kefalas, P., Eleftherakis, G. and Kehris, E.: ‘Communicating X-machines: a Practical Approach for Modular Specification of Large Systems’, Technical Report, CS-09/00, City College, Thessaloniki, Greece. Vanak, S.: ‘X-Machines + L-Systems = XL-Systems’, International Conference on Computer Graphics 2000, Geneva, Switzerland, 127–134. Bogdanov, K.: ‘Automated Testing of Harel’s Statecharts’, PhD thesis, University of Sheffield. Chambers, S.: ‘Applying X-Machines in the Retrospective Analysis and Testing of Computer Software’, PhD thesis, University of Sheffield. Chambers, C.: ‘Industrial Strength Techniques for the Development of PLC-Based Safety-Related Control and Protection Systems’, PhD thesis, University of Sheffield. Grondoudis, A.: ‘X-Machine Based Specification and Design for Testing of the CATV Protocol’, PhD thesis, University of Sheffield. Holcombe, M., Balanescu, T., Gheorghe, M. and Radovici-Marculescu, P.: ‘On testing generalized stream X-machines’, in Gh Paun (Ed), Recent topics in Mathematical Computational Linguistics, Romanian Academy Publishing House, 130–141. Ipate, F. and Popescu, M.: ‘A Z Type Language for Specifying X-Machines’, in Proceedings of CITTI, Constanta, Romania, 82–88. Ipate, F.: ‘A Theory of Testing for X-machines’, in Proceedings of CAIM 2000 (Conference on Applied and Industrial Mathematics), Pitesti, Romania. Berki, E.: ‘Process Metamodels and Method Engineering in Software Process Improvement’, in the Proc. of the BCS INSPIRE IV Conference: Training and Teaching for the Understanding of Software Quality, ISBN 1-902505-36-0, Sep. 2000, University of North London, UK. Hierons, R. and Harman, M.: ‘Testing against non-deterministic stream X-machines’. Formal Aspects of Computing, 12(6): 423–442, 2000. Gheorghe, M.: ‘Generalised stream X-machines and cooperating distributed grammar systems’. Formal Aspects of Computing, 12(6): 459–472, 2000. Balanescu, T.: ‘Generalised stream X-machines with output delimited type’. Formal Aspects of Computing, 12(6): 473–484, 2000. Ipate, F. and Holcombe, M.: ‘Generating test sequences from non-deterministic X-machines’. Formal Aspects of Computing, 12(6): 443–458, 2000. Cowling, A., Georgescu, H. and Vertan, C.: ‘A structured way to use channels for communication in X-machine systems’. Formal Aspects of Computing, 12(6): 485–500, 2000. Holcombe, M., Ipate, F. and Bogdanov, K.: ‘Total Software Testing’, to appear in Proc. ICSTEST, Bonn, Germany. Eleftherakis, G. and Kefalas, P.: ‘Model Checking Safety-Critical Systems Specified as X-Machines’, to appear in Annals of Bucharest University.