arnold beckmann's pages
Using Domain Specific Languages to Support Verification in the Railway Domain
Author: Phillip James, Arnold Beckmann, Markus Roggenbach
Title: Using Domain Specific Languages to Support Verification in the Railway Domain
Proceedings: Hardware and Software: Verification and Testing.
8th International Haifa Verification Conference, HVC 2012
Haifa, Israel, November 6-8, 2012.
Pages: 274 -275
We explore the support of automatic verification via careful
design of a domain specific language (DSL) in the context of algebraic
specification. Formally a DSL is a loose specification the logical closure
of which we regard as implicitly encoded “domain knowledge”. We
systematically exploit this “domain knowledge” for automatic
verification. We illustrate these ideas within the Railway Domain using the
algebraic specification language Casl and an existing DSL, designed by
Bjøerner, for modelling railways. Empirical evidence to the benefit of our
approach is given in the form of the successful automatic verification of
four railway track plans of real world complexity.