A Formal Approach for the Construction and Verification of Railway Control Systems

Publication: Research - peer-reviewJournal article – Annual report year: 2010

View graph of relations

This paper describes a complete model-based development and verification approach for railway control systems. For each control system to be generated, the user makes a description of the application-specific parameters in a domain-specific language. This description is automatically transformed into an executable control system model expressed in SystemC. This model is then compiled into object code. Verification is performed using three main methods applied to different levels. (0) The domain-specific description is validated wrt. internal consistency by static analysis. (1) The crucial safety properties are verified for the SystemC model by means of bounded model checking. (2) The object code is verified to be I/O behaviourally equivalent to the SystemC model from which it was compiled.
Original languageEnglish
JournalFormal Aspects of Computing
Publication date2011
Volume23
Issue2
Pages191-219
ISSN0934-5043
DOIs
StatePublished
CitationsWeb of Science® Times Cited: 3

Keywords

  • Domain-specific languages, Domain engineering, Railway control systems, Verification, Code generation, Formal methods
Download as:
Download as PDF
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
Word

ID: 5614323