Safety logic software

Distributed Logic

Component owner: Beni
Date of assessment: 2016-05-10

Current status

• This component contains the state machines that hold the safety logic for the train.

  • Requires the switch states, occupancy states

  • Controls the segments in order to avoid train collision and to stop trains that would arrive from the unselected section to the switch

• Needed information for operation:

  • Switch status

  • Section occupancy

• Can send high level commands to the desk

• State machines are implemented using Yakindu

• This java code is then adapted to the embedded programming interface of the desk

• Generated components:

  • Yakindu-Codes-Normal-Turnout: state machines for a switch and the corresponding 3 sections. This component is ready to deploy to the hardware

  • Yakindu-Codes-English-Turnout: state machines for an English switch and the corresponding 4 sections. This component is ready to deploy to the hardware

  • Yakindu-MQTT-Client: code required for communication between state machines. This is not modeled in Yakindu (glue code)

• Documentation:

  • MoDeS3 main repository readme contains links to the documentation

  • Signals used in the state machines

  • Generated and glue codes from the state machines

  • Rules implemented in the safety logic

Issues

• Detailed documentation is done:

  • Especially for the rules implemented in the safety logic: done

  • Signals used in the state machines: done

  • Relationship of the glue code and the generated code: done

• Testing

Development directions and plans

• Verification of the state machines

  • Bence Graics can help with Yakindu2Uppaal transformation

  • The product of the transformation needs to be validated (make sure that the transformation is correct)

  • Create traceability between the design model (State chart in Yakindu) and the formal model (timed automata in Uppaal)

  • Run model checking on the generated models

• Section occupancy currently is a boolean true/false, so that the state machines are not prepared for fine-grained position information (e.g. opto sensors embedded to the track)

• Beni: available until 2016. June 4. and between 2016. Aug. 22 — 2016. Sept. 30. He already has the task of "providing detailed documentation for this component" in his agenda; and is done with the documentation (both javadoc and github wiki for the distributed, statechart based safety logic, and the embedded java programming interface) as of 25.05.2016.