The formal language Alloy was developed to provide fully automatic analysis of software designs. By providing immediate feedback to users it allows early detection of design errors. The main goal of the Lightning tool is to apply the power of Alloy's automatic analysis to the domain of software language engineering. The tool allows to represent abstract syntax, concrete syntax and semantics of a modelling language in Alloy. In this paper we describe the veri cation capabilities of Lightning with the help of a concrete modelling language, namely the language of structured business processes.
The formal language Alloy was developed to "capture the essence of software
abstractions simply and succinctly, with an analysis that is fully automatic,
and can expose the subtlest of aws" [
The goal of the Lightning tool[
One can consider Lightning as an important step towards a language
workbench based on Alloy. The emphasis of the tool is currently on automatic
validation of language de nitions using Alloy's SAT-based analysis. All basic
components of a modelling language can be de ned in the tool: abstract syntax,
concrete syntax and semantics. Concrete syntax is currently restricted to
visualising language models. Semantics can be speci ed in the style of operational
semantics and its execution can be visualised as well. All speci cations of
language components and accompanying transformations are de ned in Alloy. The
tool is, however, not limited to language speci cations expressed in Alloy since
it allows importing metamodels expressed in Ecore (feature not described in the
present paper). For Lightning to become a full- edged language workbench [
The main purpose of this paper is a description of the veri cation capabilities of the Lightning tool. We will examine how the tool assists the user in writing correct language speci cations.
This paper is organised as follows: we rst describe the case study we will use in this paper. In section 3 we introduce the Lightning tool. We then describe how Lightning assists the user in designing the abstract syntax (section 4), concrete syntax (section 5), and semantics (section 6). We wrap up the paper with a discussion of our contribution in the context of related work and present concluding remarks and future work in the nal section. 2
In this paper, we illustrate Lightning's veri cation features by designing a Structured Business Process (SBP) language.
SBPs consist of tasks representing actions performed towards the completion of the process and of control nodes structuring the process. Those tasks and control nodes are interconnected using transitions so that the following holds: { The process has a unique start and end, represented by the Start and End control nodes, so that no transition is incoming to Start or outgoing from End. { Each task has exactly one incoming and one outgoing transition. { XOR and AND are control nodes used to delimit blocks representing the nesting of processes. The di erence between XOR and AND is purely semantical. While AND means that all sub-processes (outgoing transitions) need to be processed, XOR speci es that exactly one of them has to be processed. { XOR and AND control nodes have one incoming and more than one outgoing transition if they are used to open a new block (in which case they are called XOR split and AND split), or more than one incoming and one outgoing transition if they are used to close a new block (in which case they are called XOR join and AND join) { A Block opened by an AND split or XOR split needs to be closed by an
AND join or XOR join, respectively.
{ The process is acyclic (all tasks are traversed at most once) An example business process representing a model expressed in this language is represented in g. 1 using traditional notation from the business process community.
This choice of case study is based on the fact that:
{ The SBP's speci cation has been formalized in [
This case study has been implemented using Lightning in the context of a master thesis. The concrete veri cation examples presented in this paper have actually been encountered during that work. 3
The Lightning tool is a language workbench based on Alloy. It is distributed as an Eclipse plugin 1. It provides support to formally express all the components of a language (Abstract Syntax, Concrete Syntax, and Semantics), and allows to verify these using Alloy's SAT based model nding mechanism. Amongst the notable features of Lightning are : { A complete Alloy editor (with outline, error markers and syntax highlighting) { Ecore support { An editor allowing to modify generated instances.
The signature trait of Lightning, however, is to allow incremental language
development (depicted in g. 2) by coupling the instance generation of Alloy with
the domain speci c visualization and model execution induced by the concrete
syntax and semantics de nition, respectively . This approach facilitates the
identi cation of design errors [
In the following sections, we will delve into the details of the design process shown in g. 2 and describe associated veri cation tasks. 1 Freely available at : http://lightning.gforge.uni.lu
Design
SM 3 2 1 error detection
Language model generation
Legend ASM: Abstract Syntax Model CSM: Concrete Syntax Model SM : Semantics Model In Lightning the abstract syntax of a language consists of an Alloy model de ning the set of valid language models. We can view this model as the metamodel of the language. In our SBP case study, the abstract syntax model (ASM) de nes concepts of the language (Tasks, Flows, Control nodes, ...), relations between those concepts (e.g., Flows have Nodes as source and target), and well-formedness rules expressed as constraints (e.g., to ensure acyclicity of the process). The following is an excerpt of the abstract syntax model: 1 abstract s i g Nodefg 2 abstract s i g C on t r ol extends Nodefg 3 one s i g S t a r t extends Nodefgf t h i s not in Flow . t a r g e t g 4 one s i g End extends Nodefgf t h i s not in Flow . s o u r c e g 5 s i g Task extends Nodefg 6 s i g AND JOIN , AND SPLIT , XOR JOIN , XOR SPLIT extends C on t r ol fg 7 s i g Flowf 8 s o u r c e : Node , 9 t a r g e t : Node 10 g 11 f a c t a c y c l i c f 12 a l l n: Node j n not in n . ^ ( ( ~ t a r g e t ) . s o u r c e ) 13 g
Listing 1.1. Abstract Syntax Model excerpt We can use Alloy's instance generation mechanism to verify the abstract syntax. This scenario corresponds to the cycle labelled 1 in g. 2. Figure 3 depicts one of the language models thus obtained from our SBP speci cation. Although it is still possible to interpret this model correctly, it is a bit tedious since it is not presented in the traditional way but re ects the structure of the abstract syntax. The more complex a language model is (in terms of number of elements and links present), the harder it becomes to comprehend it. This is why it is advised to start de ning the concrete syntax of a language (transit to cycle 2 in g. 2) once its models become hard to check through their default visualization.
In the next section we de ne how domain speci c visualizations are speci ed
in Lightning.
The Concrete Syntax of a language consists of an Alloy model de ning a
transformation from the previously de ned Abstract Syntax Model (ASM) to a
predened Visual Language Model (VLM). This de nition follows the approach that
Kleppe describes in [
The transformation model enforces that all of its instances contain a given ASM instance and its corresponding VLM instance via the use of mapping rules and integration predicates; these predicates specify the values of elds of atoms in the VLM instance. The VLM instance can then be interpreted by Lightning in order to be rendered graphically. This process is the essence of the concrete syntax support the tool provides and is depicted in g. 4. Note that in the current version of Lightning the concrete syntax is used only for visualisation and cannot be directly edited.
In order to be processed in a reasonable time, the Alloy model de ning this
ASM to VLM transformation can be written following a sub-syntax of Alloy,
such that interpretation can be used rather than SAT-solving. This approach
called functional module is introduced in [
Below we provide a selection of the mapping rules and their integration predicates (pre xed with the prop keyword) de ned in order to provide a concrete syntax to our SBP language. 1 / each t a s k i s represented by a r e c t a n g l e , and each node has i t s corresponding l a b e l / 2 one sig Transformation f 3 mapTask: Task one > one RECTANGLE, 4 mapNodeText: Node one > one TEXT 5 g 6 / a t a s k i s represented by a r e c t a n g l e with a white 7 background t h a t contains the corresponding t e x t / 8 pred prop mapTask ( n: Task , r : RECTANGLE) f 9 r . l a y o u t = VERTICAL LAYOUT 10 r . c o l o r = WHITE
Once the concrete syntax is de ned in this way, it becomes easier to detect errors in an instance model. Figure 5 depicts the language model previously shown in g. 3, visualized this time using its concrete syntax de nition.
Only one glance at g. 5 su ces to notice that our SBP language is underspeci ed. Indeed, in this language model, two XOR splits are converging into a single join. Moreover this join, which is an AND join, doesn't have the same nature than the converging splits. In order to x this design error, we need to associate splits and joins together. We do this via the de nition of control boxes: 1 s i g ControlBox f 2 s p l i t : Control , 3 j o i n : C o n t r o l 4 gf ( 5 6 7 8 9 10 11 g // SPLIT AND JOIN HAVE SAME NATURE s p l i t in AND SPLIT and j o i n in AND JOIN) or ( s p l i t in XOR SPLIT and j o i n in XOR JOIN) // PAIRING EACH SPLIT WITH A GIVEN JOIN a l l s : ( s u c c [ s p l i t ] ) j s in ( p r e d s [ j o i n ] ) a l l j : ( pre [ j o i n ] ) j j in ( s u c c s [ s p l i t ] )
Adding the concept of a control box to the abstract syntax and repeating the instance generation shows us that the error has been well identi ed and xed. The error processing we just discussed illustrates a transit to the cycle 1 of g. 2., i.e., to the case where an error found in the visualisation reveals an error in the underlying abstract syntax. Of course the transformation model describing the visualisation may be faulty itself. In this case the error in the visual representation may point to an error in the concrete syntax model. This situation corresponds to a transit to the cycle 2 of g. 2, leading to redesigning the Concrete Syntax model. Checking if the error seen in the concrete syntax visualization is also present in the concrete-syntax-less visualization (described in the previous section) allows to decide whether or not the error has been introduced by the concrete syntax de nition. 6
Lightning currently o ers the possibility to de ne the operational semantics of languages.
The semantics de nition in Lightning consists of: { a Semantics Model (SM) in which the concepts of state and trace are de ned.
A step predicate is speci ed that expresses the condition that one state follows another state in the trace. { a Semantics visualization transformation model, reusing most of the rules present in the ASM to VLM transformation but adding rules to represent the properties of the semantics state.
For our case study each state consists of a set of nodes that are currently active in the execution of the business process. The corresponding eld of the Alloy signature is called currentNodes. That is, for a given state s, the expression s.currentNodes denotes the set of active nodes in state s. The visualisation represents the currently active nodes by highlighting them in the business process model.
To verify the correctness of the operational semantics, one can visualize its possible executions. To illustrate this veri cation, let us consider the following predicate as a rst attempt to de ne the semantics of XORs: 1 pred XORNodes( c u r r e n t : Node , s2 : S t at e ) f 2 c u r r e n t in XOR SPLIT and one node: c u r r e n t . ( ~ s o u r c e ) . t a r g e t j node in s2 . currentNodes 3 g
This predicate ensures that given a current node that is a XOR SPLIT, the set of current nodes belonging to the next semantics state contains exactly one of the nodes directly following the XOR SPLIT (mutual exclusion). Figure 6 gives an example of an erroneous execution.
Although the transition from (a) to (b) is performed as expected, the transition from (b) to (c) shows us that our XOR semantics is underspeci ed. Indeed, the predicate previously shown enforces that only one of the nodes directly following an active XOR SPLIT should be part of the current nodes. This predicate thus does not specify the state of the other nodes, thus allowing extraneous nodes to appear in the set of current nodes for a given state. To x this, one simply needs to enforce that the set of current nodes of a given state is contained in the set of successors of all the current nodes present in the previous semantics state (code omitted for lack of space).
The example above illustrates the case where an error in the concrete syntax representation of the semantic state points to an error in the underlying semantic model. This case corresponds to the cycle 3 of g. 2. 7
The term "language workbench" was made popular by Martin Fowler [
Our work is based on the premise that developing modelling languages bene ts from the lightweight formal modelling approach o ered by Alloy because it gives language developers immediate feedback on design decisions using automatic formal analysis and thus allows to detect design errors early. We can thus view Lightning as an attempt to provide agile modelling of software languages in a way similar to the initial intent of Alloy, namely providing agile modelling of software designs.
Because our tool is based on Alloy it also inherits the inherent limitations of Alloy. Indeed veri cation is based on instance nding via SAT solving. The e ectiveness of this approach intimately depends on the small scope hypothesis, stating that most of the design errors can be found in small models. Assuming the small scope hypothesis holds, the approach will allow to reduce the scopes of signatures in Alloy so that a correct answer can be found in reasonable time. Of course a negative answer in the search of a counterexample does not exclude the possibility that there may be one but may point instead to the need for trying out larger scopes, resulting of course in longer running times.
In the context of language design, though every aspect of a language is written
in Alloy, the performance limitations of Alloy we just mentioned only apply
to the generation of language models (ASM instances). The visualisation and
semantics, bene ting from functional modules, can be processed e ciently [
We have presented in this paper how Lightning allows the application of a lightweight veri cation technique based on Alloy from the earliest stages of a domain speci c language design process to its completion. In particular we have given concrete examples of veri cation tasks that were carried out during the design of a language for structured business processes.
Regarding future work much remains to be done. One obvious hindrance to the use of our tool is the fact that it requires prior knowledge of Alloy. We are currently trying to see to what extent we can provide graphical interfaces to most of the modelling tasks in the tool. In particular we have already partially implemented such an interface for de ning transformations.
Another fundamental question that needs to be investigated concerns
performance. Indeed, once the metamodel becomes a bit larger (with, say, tens of
signatures) Alloy's instance generation tends to slow down appreciably. Recent
work on model slicing (such as [