================================================================================
P9418   L.H. Oei
        "Pruning the search tree of interlocking design and application
        language operational semantics"


An interlocking is a system used at railyards for guaranteeing safety of
train movements. This paper succeeds the study on the syntax and static
semantics of tightly related graphical specification languages for
interlockings [OBKvV94]. These languages together are known in NS documents
as the Euris method [BMS92]. The Euris method has been designed by
P. Middelraad of the Dutch railway company, NS, "de Nederlandse Spoorwegen"
(The project we are involved in we sometimes refer to as ISL: Interlocking
Specification Language). It concentrates on a graphical definition of
Raiway Interlocking by means of the so-called Logic Sequence Charts, short
LSCs, which is a derivation of the well-known Flow Charts. NS have already
developed a symbolic intermediate tool interface language, IDEAL [Mak94] to
automate processing of LSC specifications. IDEAL, Interlocking Design and
Application Language, is therefore effectively used as an "Interlingua"
within the Euris-Simulation project [Kla94].

A feasibility study of strategies of translations of IDEAL to the ExSpect
simulation specification language is made. ExSpect, Executable
Specification Tool - a formalism based upon Petri Nets -, would mean a
first step toward proof theoretical correctness of the Euris method. As in
the previous study, we have made use of the Algebraic Specification
Formalsim [BHK89] and the Syntax Definition Formalism [HK89] which has been
integrated in the ASF+SDF Meta-environment [Kli93], for this purpose. The
major question addressed is whether it is possible to apply full automated
transformation of manageable complexity of IDEAL to ExSpect, without losing
the LSC operational semantics, and at the same time gain the Petri Net
invariants.


[OBKvV94] L.H. Oei, R.N. Bol, J.W.C. Koorn, and S.F.M. van Vlijmen. Syntax
          and Semantics of Interlocking and Application Language. Technical
          report, Programming Research Group, University of Amsterdam, 1994.
          To appear.

[BMS92]   J. Berger, P. Middelraad, and A.J. Smith. EURIS, European Railway
          Interlocking Specification. Technical report, UIC,
          Committee 7A/16, 1992

[Mak94]   F. Makkinga. IDEAL, Interlocking Design and Application Language
          Guide and Reference. Technical report, Ingenieursbureau
          Nederlandse Spoorwegen, 1994. Preliminary version 0.3.

[Kla94]   H.A. Klap. Euris-Simulation Tutorial. Technical report,
          Ingenieursbureau Nederlandse Spoorwegen, 1994. Preliminary
          version 0.3.

[BHK89]   J.A. Bergstra, J. Heering, and P. Klint, editors. Algebraic
          Specification. ACM Press Frontier Series. The ACM Press in
          co-operation with Addison-Wesley, 1989.

[HK89]    J. Heering and P. Klint. The syntax definition formalism SDF.
          In [BHK89].

[Kli93]   P. Klint. A meta-environment for generating programming
          environments. ACM Transactions on Software Engineering
          Methodology, 2(2):176-201, 1993.