Rule-Based Translational Semantics 

  Practical Information

The goal of this assignment is to build a rule-based transformation that translates railway models to Petrinets. You then use this Petrinet to prove properties on railway models that are not trivially proved 'on sight' or by other methods. Use the MoTiF and TransformationRule formalisms in combination with your RAMifi ed domain-speci c language to create the rules and schedule of your transformation. Write a report that includes a clear explanation of your complete solution, as well as an explanation of your testing process. Please also mention possible difficulties you encountered during the assignment, and how you solved them. You will have to complete this assignment in groups of 2. Submit your assignment (report in pdf, abstract and concrete syntax definition, example models, and the complete rule-based transformation) on Blackboard before November 20, 13:00h. Contact Simon Van Mierlo ( if you have a question.


The di fferent parts of this assignment are listed below:
  1. Implement a rule-based transformation that transforms railway models into Petrinets models.
    • Make sure this transformation is complete (i.e., every well-formed railway model produces a well-formed Petrinet (in the PN formalism)). For this assignment, you only have to consider models with two trains, whose end station is reachable from the start station.
    • Do not remove your railway model during transformation. Instead, keep it and create traceability links between created Places and Transitions and the railway element they correspond to. Use the GenericGraph formalism for traceability links. These links will greatly help in implementing your transformation.
    • Petrinets are used to analyse safety properties of a system, such as deadlock. Needless to say, the Petrinets resulting from your railway models will be abstractions. These abstractions need to be useful with respect to the properties you want to prove. For this exercise, you will have to prove, for a model with two trains, whether there is a way to schedule these trains fully independently. This means that they will, on their way from the start to the end station, never enter a segment that was entered by the other train. Knowing that two trains can run fully independently is useful, as a scheduler then would not need to worry about those two trains ever crashing. Make sure to fully explain in your report how your Petrinets representation can be used to prove this property.

    • Your transformation starts from a railway model with two trains and a simplified schedule: only the start and end stations for each train are known. This is because we don't want to constraint ourselves to one particular scheduling of the trains, we want to consider all of them. Encode your Petrinet in a way that allows to prove the property "the two trains can drive independently". This means that there for both trains, a path can be found from the start to end station that contains no segment the other train enters on its way from the start to end station. If one such pair of paths can be found, the property is proven.

  2. Create test cases that test your Railway-to-PetriNet mapping.

  Useful Links