Le développement et l’application des langages formels sont un défi à long terme pour la science informatique. Un enjeu particulier est l’acceptation par l’industrie. Cette thèse présente une approche pour la modélisation et la vérification des postes d’aiguillage français. La première question est la modélisation du système d’enclenchement par les réseaux de Petri colorés (RdPC). Un cadre de modélisation générique et compact est introduit, dans lequel les règles d’enclenchement sont modélisées dans une structure hiérarchique, tandis que les installations sont modélisées dans une perspective géographique. Ensuite, un patron de modèle est présenté. C’est un modèle paramétré qui intègre les règles nationales françaises qui peut être appliquée pour différentes gares. Puis, un concept basé sur l’événement est présenté dans le processus de modélisation des parties basses des postes d’aiguillage. La deuxième question est la transformation des RdPCs en machines B, qui va aider les concepteurs sur la route de l’analyse à application. Tout d’abord, une méthodologie détaillée, s’appuyant sur une table de correspondance, du RdPCs non-hiérarchiques vers les notations B est présentée. Ensuite, la hiérarchie et la priorité des transitions du RdPC sont successivement intégrées dans le processus de mapping, afin d’enrichir les possibilités de types de modèles en entrées de la transformation. Les machines B produites par la transformation permettent la preuve automatique intégrale par l’Atelier B. L’ensemble de ces travaux, chacun à leur niveau, contribuent à renforcer l’efficacité d’un cadre global d’analyse sécuritaire / Development and application of formal languages are a long-standing challenge within the computer science domain. One particular challenge is the acceptance of industry. This thesis presents some model-based methodologies for modelling and verification of the French railway interlocking systems (RIS). The first issue is the modellization of interlocking system by coloured Petri nets (CPNs). A generic and compact modelling framework is introduced, in which the interlocking rules are modelled in a hierarchical structure while the railway layout is modelled in a geographical perspective. Then, a modelling pattern is presented, which is a parameterized model respecting the French national rules. It is a reusable solution that can be applied in different stations. Then, an event-based concept is brought into the modelling process of low-level part of RIS to better describe internal interactions of relay-based logic. The second issue is the transformation of coloured Petri nets into B machines, which can help designers on the way from analysis to implementation. Firstly, a detailed mapping methodology from non-hierarchical CPNs to abstract B machine notations is presented. Then the hierarchy and the transition priority of CPNs are successively integrated into the mapping process, in order to enrich the adaptability of the transformation. This transformation is compatible with various types of colour sets and the transformed B machines can be automatically proved by Atelier B. All these works at different levels contribute towards a global safe analysis framework

Developing software without considering the potential changes it mighthave to undergo in the future can be a costly mistake. This is becauseits maintenance costs can become very expensive as they can consumeover 90% of the total life-cycle costs. Incorporating maintainability insoftware has for this reason become highly attractive since it can significantlyreduce the maintenance costs and therefore save companies andsoftware developers a fortune. This thesis presents a software tool thathas been developed to aid Bombardier in the verification of computerbasedinterlocking (CBI) systems. The tool automatically generates testcases which represent the different tests that verify the interlocking system.The paper is divided into two parts. The first part focuses on themaintainability of the tool while the second part investigates whetherthe tool can speed up the testing process of CBI-systems at Bombardier.The results show that the tool is highly maintainable and that tests onCBI-systems can be performed significantly faster with it. / Att utveckla mjukvara utan hänsyn till de eventuella förändringar somden måste genomgå i framtiden kan bli ett kostsamt misstag. Dettaberor på att dess underhållskostnader kan bli mycket dyra eftersom dekan konsumera över 90% av de totala kostnaderna. Det har därför blivitväldigt attraktivt att lägga fokus på underhållbarhet när man utvecklarmjukvara eftersom det kan avsevärt minska underhållskostnadernaoch därmed spara mjukvaruutvecklare och företag en förmögenhet. Idenna uppsats presenteras ett verktyg som har utvecklats för att hjälpaBombardier med verifiering av datorställverk. Verktyget automatisktgenererar testfall som representerar de olika testen som verifierar ställverket.Uppsatsen är uppdelad i två delar. Den första delen fokuserarpå verktygets underhållbarhet medan den andra delen undersöker omverktyget kan påskynda testprocessen för datorställverk på Bombardier.Resultaten visar att verktyget är väldigt underhållbart och att

I denna rapport utreds hur systemdesignen av lågspänningsfördelningen för järnvägen kan kostnadseffektiviseras. I dagsläget har det utarbetats en norm kring systemdesignen som tenderar att efterbildas från år till år vilket har medfört brist på innovation inom området. Syftet med arbetet var att designa två typstationer med signalställverken M11 respektive M95, där placering samt nominell storlek av UPS:er skulle fastställas för att tillhandahålla en kostnadseffektiv lösning. Dessutom skulle kablage dimensioneras för typstationerna samt se över möjligheten att ersätta UPS:er med likriktarsystem. Stationerna baserades på två redan existerande driftplatser, Fagersta C (M11) och Skänninge (M95). Slutligen skulle olika energilagringsalternativ för UPS-system jämföras för att tillhandahålla det lämpligaste alternativet. Genom simuleringar och beräkningar i bland annat datorprogrammet El-Vis har lågspänningsfördelningen dimensionerats för typstationerna. Arbetet visar på att ett distribuerat UPS-system är att föredra ur ett ekonomiskt perspektiv gentemot ett centraliserat UPS-system. Vidare har det konstaterats att likriktarsystemet Rectiverter kan ersätta UPS:er samt att ackumulatorer är det mest passande energilagringsalternativet. / This report identifies how the system design of low voltage power distribution of the railway can be more cost effective. In the current situation there is a norm on the system design that tends to be replicated each year. This has brought a lack of innovation in the field. The purpose of the thesis was to come up with two model stations with the interlocking system M11 respectively M95, where the positioning and nominal size of the UPS:s would be determined to provide a cost effective solution. Furthermore, the cable dimensioning of the model stations was computed as well as the possibility of replacing UPS-systems with rectifier-systems. The model stations were based on two already existing operating sites, Fagersta C (M11) and Skänninge (M95). Lastly, different energy storage alternatives for UPS-systems were compared to acquire the most appropriate choice. Through simulations and calculations in, inter alia, the computer program El-Vis, the low voltage power distribution was dimensioned for the model stations. The thesis shows that a distributed UPS-system is preferred in an economical point of view compared to a centralized UPS-system. Furthermore, the thesis establishes that the rectifier system Rectiverter can replace UPS:s. It also states that accumulators are the most suitable alternative for energy storage.

In der vorliegenden Arbeit werden eine sichere FPGA-Stellwerksplattform und ein Transformationsverfahren entwickelt, mit dem die Schaltungen bestehender Relaisstellwerke in eine FPGA-Logik überführt werden können. Die FPGA-Stellwerksplattform ersetzt die Innenanlage eines Relaisstellwerks. Ihre Schnittstellen entsprechen den bisherigen Schnittstellen am Kabelabschlussgestell und zur Bedien- und Meldeeinrichtung. Damit ist eine einfache Migration bestehender Stellwerke möglich. Das Sicherheitskonzept basiert auf einer zweikanaligen Struktur mit sicherem Vergleicher und zusätzlichen Selbsttests zur schnellen, datenflussunabhängigen Ausfalloffenbarung. Die erreichbare Gefährdungsrate liegt im Bereich von SIL 4 und entspricht damit dem Sicherheitsziel für Stellwerke der Deutschen Bahn. Die Transformation sieht eine Trennung der Stellwerkslogik in Logik- und Leistungsteil vor. Der Logikteil wird auf dem FPGA realisiert. Die im Leistungsteil verbliebenen Kontakte und Überwacherrelais werden durch sichere Stellteile ersetzt. Die logischen Ansteuerbedingungen der Relais werden in Schaltnetze überführt. Die gesteuerten Relais werden durch Instanzen generischer Zustandsmodelle ersetzt. Für jeden verwendeten Relaistyp wurde ein entsprechendes Modell entwickelt, das bei der Transformation als Baustein eingesetzt werden kann. Die generischen Zustandsmodelle berücksichtigen auch die sicherheitsrelevanten konstruktiven Eigenschaften der Relais. So wird bei der Auftrennung einer Schaltung in Logik- und Leistungsteil sichergestellt, dass die in getrennte Schaltungsteile überführten Öffner und Schließer eines Relais nie gleichzeitig geschlossen sein können (Zwangsführung der Kontakte). Dies ist eine Voraussetzung für die Beibehaltung der sicherheitsrelevanten Funktionsbedingungen der Originalschaltung. Das Transformationsverfahren und die implementierten Mechanismen zur Ausfalloffenbarung sind unabhängig von der Anwenderlogik und vom gewählten Schaltkreistyp. Damit kann der generierte VHDL-Code bei Obsoleszenz eines Schaltkreises auch auf andere FPGA-Typen portiert werden. In einer Ressourcenabschätzung wird gezeigt, dass der gewählte Lösungsansatz geeignet ist, die Schaltungen kleinerer Relaisstellwerke vollständig auf einem FPGA zu realisieren. Die Anwendung des vorgestellten Verfahrens wird am Beispiel der Weichengruppe des Stellwerkstyps GS II DR demonstriert. Das Transformationsverfahren ist aber auch für andere Stellwerksbauformen geeignet. Dabei ist es unerheblich, ob diese nach dem tabellarischen Verschlussplanprinzip oder dem Spurplanprinzip arbeiten.

In der vorliegenden Arbeit werden eine sichere FPGA-Stellwerksplattform und ein Transformationsverfahren entwickelt, mit dem die Schaltungen bestehender Relaisstellwerke in eine FPGA-Logik überführt werden können. Die FPGA-Stellwerksplattform ersetzt die Innenanlage eines Relaisstellwerks. Ihre Schnittstellen entsprechen den bisherigen Schnittstellen am Kabelabschlussgestell und zur Bedien- und Meldeeinrichtung. Damit ist eine einfache Migration bestehender Stellwerke möglich. Das Sicherheitskonzept basiert auf einer zweikanaligen Struktur mit sicherem Vergleicher und zusätzlichen Selbsttests zur schnellen, datenflussunabhängigen Ausfalloffenbarung. Die erreichbare Gefährdungsrate liegt im Bereich von SIL 4 und entspricht damit dem Sicherheitsziel für Stellwerke der Deutschen Bahn. Die Transformation sieht eine Trennung der Stellwerkslogik in Logik- und Leistungsteil vor. Der Logikteil wird auf dem FPGA realisiert. Die im Leistungsteil verbliebenen Kontakte und Überwacherrelais werden durch sichere Stellteile ersetzt. Die logischen Ansteuerbedingungen der Relais werden in Schaltnetze überführt. Die gesteuerten Relais werden durch Instanzen generischer Zustandsmodelle ersetzt. Für jeden verwendeten Relaistyp wurde ein entsprechendes Modell entwickelt, das bei der Transformation als Baustein eingesetzt werden kann. Die generischen Zustandsmodelle berücksichtigen auch die sicherheitsrelevanten konstruktiven Eigenschaften der Relais. So wird bei der Auftrennung einer Schaltung in Logik- und Leistungsteil sichergestellt, dass die in getrennte Schaltungsteile überführten Öffner und Schließer eines Relais nie gleichzeitig geschlossen sein können (Zwangsführung der Kontakte). Dies ist eine Voraussetzung für die Beibehaltung der sicherheitsrelevanten Funktionsbedingungen der Originalschaltung. Das Transformationsverfahren und die implementierten Mechanismen zur Ausfalloffenbarung sind unabhängig von der Anwenderlogik und vom gewählten Schaltkreistyp. Damit kann der generierte VHDL-Code bei Obsoleszenz eines Schaltkreises auch auf andere FPGA-Typen portiert werden. In einer Ressourcenabschätzung wird gezeigt, dass der gewählte Lösungsansatz geeignet ist, die Schaltungen kleinerer Relaisstellwerke vollständig auf einem FPGA zu realisieren. Die Anwendung des vorgestellten Verfahrens wird am Beispiel der Weichengruppe des Stellwerkstyps GS II DR demonstriert. Das Transformationsverfahren ist aber auch für andere Stellwerksbauformen geeignet. Dabei ist es unerheblich, ob diese nach dem tabellarischen Verschlussplanprinzip oder dem Spurplanprinzip arbeiten.