Construction of formal models and verifying property specifications through an example of railway interlocking systems

Lukács, Gábor and Bartha, Tamás (2019) Construction of formal models and verifying property specifications through an example of railway interlocking systems. Pollack Periodica, 14 (2). pp. 39-50. ISSN 1788-1994

Preview

Text 606.2019.14.2.4.pdf Download (1MB) | Preview

Abstract

Abstract The use of formal modeling has seen an increasing interest in the development of safety-critical, embedded microcomputer-controlled railway interlocking systems, due to its ability to specify the behavior of the systems using mathematically precise rules. The research goal is to prepare a specification-verification environment, which supports the developer of the railway interlocking systems in the creation of a formally-proven correct design and at the same time hides the inherent mathematical-computer since related background knowledge. The case study is presented with the aim to summarize the process of formalizing a domain specification, and to show further application possibilities (e.g. verification methods).

Actions (login required)

Edit Item