Der Einsatz von Mikroelektronik in signaltechnischen Systemen bei Bahnen ist außerhalb Japans weit verbreitet, dort aber selten angewandt. Das RTRI hat deshalb Untersuchungen begonnen, ob der Nachweis signaltechnischer Ausfallsicherheit durch Formale Methoden erbracht werden kann. Als Untersuchungsbeispiel wurden drei mathematische Modelle von automatischen Streckenblocksystemen erstellt. Hier kam die B-Methode zur Softwareentwicklung zum Einsatz, die auch bei europäischen Bahnen erfolgreich angewandt wird. Weiter wurde SAT in der Booleschen Algebra eingesetzt (SATisfiability = Erfüllbarkeit der Aussagenlogik) sowie SMT (Satisfiability Modulo Theories) zur Behandlung der mathematischen Variablen. Die Untersuchungen über den Einsatz dieser mathematischen Methoden zur Sofwareentwicklung werden fortgesetzt.
Application of verification methods to specifications of signalling equipment
Anwendung von Verifizierungsmethoden für Anforderungen von signaltechnischer Ausrüstung
Quarterly Report of RTRI ; 2013 , 4 ; 202-207
2013-01-01
6 pages
Aufsatz (Zeitschrift)
Englisch
© Metadata Copyright Deutsche Bahn AG. All rights reserved.
Application of Verification Methods to Speficiations of Signalling Equipment
British Library Online Contents | 2013
|Formal specifications of railway signalling systems using Stateflow
Tema Archiv | 2007
|Online Contents | 1996
British Library Conference Proceedings | 2008
|