While we concentrate at Control and ControlGlobal.com on process control in the batch, continuous and hybrid processing industries, I personally have wider interests in control... so it is fascinating to see how other control domains are practiced. Today at Safecomp, we are talking about other domains including railway control.
"A Domain-Specific Framework for Construction and Verification of Railway Control Systems" is the title of the "invited talk" for today. It is presented by Anne E. Haxthausen of the Technical University of Denmark.
"We are suggesting," she said, "a framework consisting of a domain-specific specfication language, some tools, and a method for using the language and the tools to construct and verify railway control systems."
"The use of domain specific languages (DSLs) as front ends for development tools is advocated," she continued. "In contrast to general purpose specification and programming languages, DSLs facilitate their utilization by domain experts who are not specialists in the field of information technology."
"Our framework provides a generic railway control system model that can be instantiated with configuration data, a domain specific language for specifying application specific parameters, and a generator from DSL specifications into configuration data."
Challenges in developing railway control systems include demad for increased traffic throughput, higher safety integrity levels and shorter time to market periods.
Haxthausen's framework is model driven, and consists of tools for automated construction, verification and test, as well as the domain specific language (DSL) and its compiler.
DSLs can be used by domain experts, independent of implementation, speeding up production time and reducing risk of errors.
Haxthausen presented a case study of a family of tramway control systems.
The specification in domain specific language consists of a network description and a route model (4 interlocking tables).
Haxthausen showed detailed examples of what programming in domain specific language looks like, and what the generation of the controller model code becomes.She then described the generation of the behavioral domain model, obtained by instantiating generic patterns for rules. She described a transition rule pattern for signals and one for sensors.
Then she described the generation of safety conditions automatically by instantiating generic patterns. She showed as an example, a pattern for two crossing segments expressing that at least one of the segments is empty.
After the creation of the model, a verification step must be accomplished. In the example of the case study, it took 392 seconds to model check the case.This, of course,means that automatic verification is practical as well as possible.
Once the model is generated and verified, it is now possible to use a compiler to convert the DSL into object code, and verify the code using object code verification techniques.
