Slow-scan, a sterowanie i kontrola urządzeń na kolei (raz jeszcze)

Funkcje i opis systemu

Na polecenie operatora dostosowywać ustawienie semaforów i punktów, tak by zapewnić bezpieczny przejazd pociągów. System ma również uchronić operatora przed takim skierowaniem pociągów, które mogłoby doprowadzić do kolizji.
SSI i urządzenia współpracujące

Rys. 1

SSI (Solid State Interlocking) - system kontrolujacy
TFM (Track-side Functional Modules) - moduły przytorowe (sterujace mechanizami, np. semaforem, zwrotnica)

Wymagania stawiane systemowi

Ze względów bezpieczeństawa wymagane jest, by SSI szybko wykrywał uszkodzenia, zarówno na łączu, jak i w modułach przytorowych.

Jak to działa?

SSI odpytuje wszystkie moduly w ustalonej kolejności raz na sekunde. SSI wysyła wiadomość (TFM-adres, stan) i czeka kilka milisekund na potwierdzenie. Taki sposób działania zapewnia szybkie wykrywanie błędów, jednak wymaga szybkiego łącza.

Problem

Ze względu na duże odległości pomiędzy modułami przytorowymi, połączenie ich szybkim łączem jest bardzo kosztowne. W związku z tym rozpoczęto prace nad zastąpieniem szybkiego łącza wolniejszym i tańszym łączem. System ten nazwano Slow-Scan.

Rozwiązanie

Slow scan system
Rys. 2
SPC - konwerter protokołu po stronie SSI
TPC - konwerter protokołu po stronie modułów

Funkcje SPC:

  1. odebrać wiadomość od SSI
  2. porównać wiadomość z zapmietanym stanem, jeśli się zmieniła to zapamietać i przesłać wolnym łączem do TPC
  3. odpowiedzieć SSI ze stanem z pamięci lokalnej.
  4. sprawdzić poprawność działania wolnego łącza 

Funkcje TPC:

  1. odebrać wiadomości ze stanem przez wolne łącze i przechowywać je
  2. emulować SSI, czyli wysyłać wszystkie przechowywane wiadomości, przy tyknięciu zegara
  3. odbierać wiadomości od modułów przytorowych, porównywać z zapisanym stanem, a ewentualne zmiany przekazywać do SPC wolnym łączem
  4. sprawdzić poprawność działania wolnego łącza 

To była (mam nadzieję szybka) powtórka :)

 Modelowanie w UPPAALu

Zegar:
Zegar

  Czemu jednak zegar się przydaje? 

SSI (Solid State Interlocking):
SSI

TFM (Track Functional Module):
TFM
TPC (TFM-side Protocol Converter):
TPC


SPC (SSI-side Protocol Converter):

SPC


A w CWB potrzebne były 3 oddzielne procesy:

SPC


I łącze:
Link

Wrażenia z modelowania:

  1. Pewne wady interfejsu użytkownika - prowadzą do łatwego popełniania głupich błędów
  2. Bardzo prosto wyszukuje się błędy w systemie w trakcie budowy.  Podstawą dla powyższego systemu był brak zakleszczeń (deadlocków). Sprawdzenie własności w weryfikatorze, następnie przejrzenie błędnego przebiegu.
  3. Dzięki zegartestowy, udało mi się wychwycić niepożądane zachowanie systemu (zbędne ruchy czasu do przodu)
  4. Kłopot z dodaniem nowego miejsca. Przerabianie strzałek.

To co zrobilem:
Automaty
Weryfikacja