Modeling Symbolic Transition Systems in XML

This article explains how to model Symbolic Transition Systems (STSs) in XML. To do so a simple XML Schema has been defined. I refer here to the Schema STSchema Version 111110 which can be found here:

Such an STS written as an XML instance of that schema can be read by the model-based testing JTorX, and used there for both specifying and representing reactive systems. To simulate the STS the STSimulator library is used. The Schema does currently not support all features of the library, these limitations are present:

  • no custom initial values for location variables
  • no definition of lists
  • no definition of complex types
    The advantage of this approach is that one can define STSs without any Java knowledge. The schema is very simple and straightforward, I will exemplify it here by referring to a small example, a one-place buffer storing an enumeration value:

    You start your XML instance as usual:

<?xml version="1.0" encoding="UTF-8"?>
<ns1:STS  xmlns:xsi=''

Next you can define define enumeration types. This is optional, so if you do not use them, omit this step. Do define an enumeration with the name enum and the two values foo and bar, do this:


You may define several enumeration types here. Next we come to the locations (the word we use for states of the transition system). A location just has a name, in the example we have two locations (“1” and “2”), and define them as follows:


Every STS must have an initial location, in our example this is location “1”:


Next come the location variables (the variables which are global for the given STS). We have here just one variable with name saved_s and enumeration type enum (the enumeration we have defined above):


If there are more location variables just repeat the <ns1:locationVar> ... </ns1:locationVar> element. Message parameters are modeled via interaction variables. In our example there is one such parameter with name s and type enum. Defining them goes exactly the same way:


Messages have a name, a kind, and parameters. There are two options for the kind:

  • input
  • output
    For our example we need two messages: read(s) and write(s):


A message can have several parameters. Finally we come to the switches (the word we use for transitions of the transition system). A switch consists of a source location, a destination location, a message with a kind, a restriction (the word we use for guard), and an update of the location variables. The reason why a message comes here together with a kind is that we could define messages having the same name, but different kind. When a switch has no restriction, meaning a restriction which is logically always true, you can simply omit the <restriction> element. In the example this is the case for the switch from location “1” to “2”. When no variables shall be updated after a switch has been taken, simply omit the <update> element. In the example this is the case for the switch from location “2” to “1”. These two switches are defined as follows:

            <ns1:update>saved_s = s;</ns1:update>
            <ns1:restriction>saved_s == s</ns1:restriction>

That is it, end the XML document by:


In addition to enumerations you can use all simple types:

  • in
  • double
  • boolean
  • string
  • date
    For more information on the types and on the language for the restrictions and update mappings please refer to the documentation of the STSimulator library. Take care that you respect the treatment of special characters in XML, for instance the logical && must be written in the instance as &amp;&amp;

To define switches with unobservable messages ensure that you omit the <message> tag, and set the kind to <kind>unobservable</kind>. This is an example of an unobservable switch:

            <ns1:restriction>x &lt;= 13</ns1:restriction>

Page 1 of 1, totaling 1 entries