A Domain-Oriented, Model-Based Approach for Construction and Verification of Railway Control Systems - Formal Methods and Hybrid Real-Time Systems - page 324

Input

Data Collector

1

2

Static

DSL Checking

Semantics

Document Result

Checker

3

Generators

Executable

4

Behavioural domain model Safety conditions Model checker

Controller model

Checking
Result

5 6

Object Code Checking

Result

Compiler ´

Verifier

Assembler code

Fig. 1. Toolchain overview

behavioural physical domain models with transition system semantics (Sys-
temC), and (3) safety conditions for the concurrent composition of these two
models.
4. A bounded model checker capable of verifying properties of composed con-
troller and physical domain models written in SystemC.
5. A compiler for translating SystemC models into assembler code (since Sys-
temC is embedded into C++, conventional compilers can be used for this
task).
6. An object code verifier which, given a SystemC controller model and associ-
ated assembler code, verifies that the latter is a correct implementation of
the former.

To create and verify a new control system users should apply these tools to
go through the following steps illustrated in Fig. 1:

1. The railway specialists use the data collector to produce a syntactically well-
formed DSL description D of domain-specific details of the system to be

developed.
2. The static semantics checker checks that D is statically well-formed.