Designing Domain Speci c Languages for Veri cation: First Steps Phillip James, Markus Roggenbach Swansea University , UK 40 45

This paper introduces a rst approach at developing a design methodology for creating domain speci c languages focused towards modelling and veri cation. The work presented is ongoing. The overall aim of the work is to show how capturing domain speci c knowledge, and then tailoring proof goals around this domain speci c knowledge, can improve automatic veri cation results, whilst also providing a graphical domain speci c language.

 To illustrate our approach we use the railway domain Here we review existing work in the area of veri cation within the railway domain and the area of domain speci c language design Introduction

Modelling and Veri cation in the Railway Domain A prominent example of where formal methods have been applied is the railway domain. Approaches that have been taken include algebraic speci cation, e.g. [ 4 ], process algebraic modelling and veri cation, e.g. [ 22, 18 ], and model oriented speci cation, where, for example the B method has been used in order to verify part of the Paris Metro railway [ 5 ] in terms of both safety and liveness properties. These approaches show the successful application of formal methods to the railway domain, but fail to comment on the applicability of such processes by domain engineers.

This work is inspired by the work of Bj rner [ 4 ]. To this end, we follow the natural language speci cation of the railway domain given by Bj rner [ 4 ]. Bj rner has also given a formal version of this natural language speci cation using the RSL speci cation language [ 20 ]. In contrast, we focus on using Casl, the Common Algebraic Speci cation Language [ 16 ] as it provides us with more features than RSL, including established tool support in the form of the Heterogeneous Toolset (Hets) [ 15 ]. The Hets environment not only provides both interactive and automatic theorem proving support, but also allows translation between di erent logics through institution maps [ 14 ]. Such a translation is shown to be useful in Section 3. 2.2

Domain Speci c Language Design The creation of domain speci c languages is often aided by the use of a development framework. There are several examples of such tools including ASF+SDF [ 21 ] a meta-environment based on a combination of the algebraic speci cation formalism ASF and the syntax de ning language SDF. ASF+SDF allows creation of domain speci c languages and tools such as parsers, compilers and static analysers for the created domain speci c language. Extending ASF+SDF, there is Rascal [ 12 ], which is currently under development at CWI. Finally, MetaEdit+ [ 2 ] is an industrial tool allowing the creation of visual domain speci c languages. Interestingly, MetaEdit+ has been used to create a domain speci c modelling for railway layouts, see [ 2 ].

With respect to our approach for creating domain speci c languages, we make use of the Graphical Modelling Framework, GMF [ 8 ]. GMF is an Eclipse plugin that provides the infrastructure to create, from a UML like model, a Java based graphical editor. This editor can then easily be extended with Java code allowing it to output Casl speci cations. The simplicity of this creation process ts well with our design methodology outlined in Section 3. 3

Towards a Design Methodology

In this section, we outline a rst proposal for a design methodology for creating domain speci c languages for veri cation. Figure 1 illustrates the proposed design and veri cation process. Capturing knowledge: The rst area that is illustrated in the left of Figure 1 is the capture of domain knowledge. A natural language speci cation can be formalised using the OWL Ontology language [ 3 ]. OWL has been designed to formalise knowledge about a given domain and thus provides a range of constructs to allow the capture of domain knowledge. It allows speci cation of concepts within a given domain via classes, speci cation of attributes of the concepts via data properties and speci cation of relations between concepts via object properties. It also allows axioms to be stated over such properties. These constructs are very similar to those within UML or any object orientated language. OWL has a well de ned formal semantics [ 17 ] meaning that every OWL speci cation has a precise and unambiguous meaning. As we wish to use only automatic tool support, we make use of a decidable fragment of full OWL known as OWL-DL [ 3 ] Creating the DSL: Given an OWL speci cation, an automatic translation to a GMF (UML like) meta-model is possible.1 This meta-model along with a set of graphical elements can be used within the GMF process to create a graphical editing tool for the domain. The production 1We are currently implementing this XML based translation. Graphical Elements

Meta Model AddedTo

EFM+GMF

DSL Editor Automatic Translation

DSLEditor Produces Natural Language Specification

Formalise

OWL Specification

Automatic Translation

CASL DS Knowledge Specification

Import

CASLPSlacnheme

Specification Import

 CASLGDoSalProof

Import

ImprovedVerification

Hets CASL DS Theorems

Verification

Result Yes/No/Maybe of this graphical editing tool is outlined in the top branch of Figure 1. Here we provide an overview of the steps involved in the GMF process and for more details we refer the reader to [ 8 ]. The rst step within the GMF creation process is to select the concepts of the domain which should become graphical constructs within the language. These graphical constructs can be split into two main classes essentially representing nodes and edges within the nal graphical editor. The next step is to associate with each chosen construct for the language, a graphical image to represent it. Finally, the attributes (or properties for a given concept) which should be attached to each graphical element can be selected. Once these steps have been completed, the GMF tool will automatically produce a Java based graphical editor. This editor consists of a drawing canvas and a palette. Graphical elements from the palette can be dragged and positioned onto the drawing canvas. Along with these features, the Java code base for the editor is readily extensible and we use this fact to extend the editor to produce Casl speci cations. Namely, we add a small amount of code for each construct that simple produces a Casl speci cation for that construct when it is added to the drawing canvas. Obtaining such a Casl speci cation for each construct is discuss below.

Semantics: To provide a semantics for the graphical editing tool we propose the use of Casl [ 16 ]. The main motivation for the use of Casl is thanks to the tool support that is available in the form of the Hets environment [ 15 ]. Hets not only provides syntax checking and static analysis of CASL speci cations, but also an interface to various interactive and automated theorem provers. The central path of Figure 1 illustrates the addition of Casl to the graphical editing tool as a semantic base. Within Hets, an automatic semantic preserving translation from OWL into Casl has been implemented [ 13 ]. The motivation for using OWL and translating to Casl, rather than directly using Casl, is that OWL provides constructs suited towards capturing domain knowledge in a UML style which can be easily adopted by most domain engineers. Using the resulting Casl domain knowledge speci cation, the graphical editing tool can be extended to produce Casl speci cations for domain models created using the editor. Veri cation: Finally, veri cation of the Casl speci cations produced by the graphical editing tool is possible using the Hets framework. At this point, Figure 1 highlights the advantage of adding domain knowledge to the veri cation process. That is, there are two possibilities for veri cation. The rst { illustrated by the solid lined box { is simply verifying the given problem without any domain speci c theorems on the domain knowledge level. The second { illustrated by the dotted lined box { includes domain speci c theorems that have been proven on the domain knowledge level. These theorems provide a potential gain for automated veri cation: (1) They have the potential to remove false counter examples like those experienced in [ 10 ]; (2) They allow general domain speci c theorems to be added, these in turn improve the speed of the proof process for particular domain speci c proof goals. 4

A First Example: Domain Knowledge Helps To illustrate the advantages that can be gained through adding domain knowledge to the veri cation process, we study a common installation within the railway domain. Figure 2 shows part of a standard \double lead" junction.

R1 A R2 lu1

P lu2 lu3

R3 E F R4

Trains can travel from location A to locations E or F , or from locations E or F to location A. The path along which a train will travel is determined by the position of point P . Logically, the junction is segmented into routes. Here there are four possible routes. Route R1 can be set, i.e. trains can travel from A to E when the point is in \reverse" position and there are no trains occupying the point and track segments lu1 and lu2. Route R2 can be set, i.e. trains can travel from A to F when the point is set in \normal" position and there are no trains occupying the point and track segments lu1 and lu3. In a similar manner, routes R3 and R4 can be set to allow trains to travel from E to A and F to A respectively. spec Junction [op p: Switch; op lu1: Linear; ... ] = %% axioms for connecting components such as points and tracks ... forall t: Time . point_EnabledReverseAndLu2At n if p stateAt n = unocc /\ p positionAt n = reverse /\ (exists t :Time . n < t /\ lu2 stateAt t = unocc); ... forall n: Time . route1_enabledAt n if lu1 stateAt n = unocc /\

(exists t : Time . n < t /\ point_EnabledReverseAndLu2At t); ... then %implies ... forall n : Time . exists t: Time . n < t /\ route1_enabledAt t forall n : Time . exists t: Time . n < t /\ route2_enabledAt t forall n : Time . exists t: Time . n < t /\ route3_enabledAt t forall n : Time . exists t: Time . n < t /\ route4_enabledAt t end %(Thm1)% %(Thm2)% %(Thm3)% %(Thm4)%

As such a junction is a common installation within the railway domain, it would naturally form a concept or class within an OWL speci cation for the railway domain, e.g see [ 1 ]. Within Casl, it makes sense to capture a junction with parametrisation. Part of the parametrised Casl speci cation for the junction is given in Figure 3.

The junction speci cation illustrates the use of domain speci c theorems. These theorems capture domain knowledge about the junction. Thm1 expresses that there always exists a time in the future where route R1 is enabled, and similarly Thm2, Thm3 and Thm4 expresses this for routes R2, R3 and R4 respectively. Here, due to space constraints, we omit the behaviour of trains and points and assume they behave as expected. These theorems are provable using the Hets toolset in a few seconds.2 Via instantiation of the junction speci cation, we can now specify the example train station in Figure 4. This station consists of six junctions in total.

Platform 1 Platform 2 Platform 3 Platform 4

X Y

Over this new track plan for a station, we would like to reason about the enabling of routes allowing trains to enter or leave the station. For example we may wish to know that there always exists a time in the future when a train can leave Platform 1 and travel to X. This condition is dependent on the setting of several routes across junctions. This property can be expressed as: 8 n : Time 9 t1, t2, t3 : Time n < t1 ^ t1 < t2 ^ t2 < t3 ^

route3 1 enabledAt t1 ^ route4 3 enabledAt t2 ^ route2 5 enabledAt t3

Referring to Figure 1, if we try to verify such a condition without adding domain speci c theorems, i.e. Thm1 through to Thm4, to the veri cation process, then veri cation with Hets is not possible.3 When adding the domain speci c theorems into the process, the veri cation is possible within ten seconds. This illustrates that exploiting domain speci c knowledge of particular domain constructs can aid the veri cation process considerably. 5

 Summary and Future Work

In this paper, we have brie y introduced a rst attempt at a design methodology for creating domain speci c languages focused towards veri cation. We have also illustrated how the capture and exploitation of domain speci c knowledge obtained via this design methodology can provide gains within the automatic veri cation process. As future work, we wish to explore further examples of how domain speci c knowledge can be advantageous. The result will be a classi cation of types of knowledge and the bene ts they can bring to the veri cation process. We also wish to explore providing useful feedback to domain engineers when a prove attempt is not successful. That is, we wish to explore the production of counter-examples on the level of the graphical editing tool.

2Veri cation times are only rough guidelines and not exact scienti c benchmarks.

3Within fteen minutes. Acknowledgements: We would like to thank our industrial partner Invensys Rail for their useful co-operation throughout this work. A special thanks also goes to Erwin R. Catesbeiana (Jr.) for his re ections and comments on our design methodology.

 [1] Invensys Rail Data Model { Version 1A, 2010 . [2] MetaEdit+, Webpage, last accessed April 2011 . http://www.metacase.com/. [3] G. Antoniou and F. Harmelen . Web ontology language: Owl . Handbook on ontologies, 2009 . [4] D. Bj rner . Domain Engineering { Technology Management, Research and Engineering. JAIST Press, 2009 . [5] J. Boulanger and M. Gallardo . Validation and veri cation of METEOR safety software . In J. Allen, R. J. Hill , C. A. Brebbia , G. Sciutto, and S. Sone, editors, Computers in Railways VII , volume 7 . WIT Press, 2000 . [6] W. Fokkink and P. Hollingshead . Veri cation of interlockings: from control tables to ladder logic diagrams . In J. Groote, S. Luttik , and J. V . Wamel, editors, FMICS'98 , Formal Methods for Industrial Critical Systems . CWI, 1998 . [7] M. Fowler and R. Parsons . Domain Speci c Languages. Addison-Wesley , 2010 . [8] R. C. Gronback . Eclipse Modeling Project: A Domain-Speci c Language (DSL) Toolkit . AddisonWesley Professional , 2009 . [9] G. Holland , T. Kahsai, M. Roggenbach , and B.-H. Schlinglo . Towards formal testing of jet engine rolls-royce BR725 . In L. Czaja and M. Szczuka, editors, Proc. 18th Int. Conf on Concurrency, Speci cation and Programming , Krakow, Poland, 2009 . [10] P. James . SAT-based Model Checking and its applications to Train Control Software . Master's thesis , Swansea University, 2010 . [11] P. James and M. Roggenbach . SAT-based Model Checking of Train Control Systems . Technical report, CALCO-jnr'09 , University of Udine, n.5- 2010 , 2009 . [12] P. Klint , T. Van Der Storm , and J. Vinju. EASY Meta-programming with Rascal . Generative and Transformational Techniques in Software Engineering III , 2011 . [13] O. Kutz , D. Lucke, T. Mossakowski, and I. Normann. The OWL in the CASL - Designing Ontologies Across Logics . In C. Dolbear, A. Ruttenberg , and U. Sattler, editors, OWLED. CEUR-WS.org , 2008 . [14] T. Mossakowski . Relating CASL with other speci cation languages: the institution level . Theoretical Computer Science , 286 ( 2 ), 2002 . [15] T. Mossakowski , C. Maeder , and K. Lu ttich. The Heterogeneous Tool Set, Hets. Tools and Algorithms for the Construction and Analysis of Systems , 4424 , 2007 . [16] P. D. Mosses, editor. CASL Reference Manual , volume 2960 . Springer, 2004 . [17] P. F. Patel-Schneider , P. Hayes , and I. Horrocks. Owl web ontology language semantics and abstract syntax . Technical report, W3C , 2004 . [18] J. Peleska , D. Gro e, A. E. Haxthausen , and R. Drechsler . Automated veri cation for train control systems . In E. Schnieder and G. Tarnai, editors, Proceedings of Formal Methods for Automation and Safety in Railway and Automotive Systems . Technical University of Braunschweig, 2004 . [19] A. Simpson . A formal speci cation of an automatic train protection system . In G. Goos, J. Hartmanis , and J. V . Leeuwen, editors, FME '94: Proceedings of the Second International Symposium of Formal Methods Europe on Industrial Bene t of Formal Methods . Springer, 1994 . [20] The RAISE Language Group . The RAISE speci cation language . Prentice Hall , 1993 . [21] M. Van Den Brand , A. Van Deursen , J. Heering , H. De Jong, M. De Jonge, T. Kuipers , P. Klint , L. Moonen , P. Olivier , and J. Scheerder . The ASF+SDF Meta-environment: A Component-Based Language Development Environment . LNCS, 2027 , 2001 . [22] K. Winter . Model checking railway interlocking systems . Australian Computer Science Communications , 24 ( 1 ), 2002 .