-We present a methodology for describing executable semantics of diagrammatic modeling languages, and an execution engine based on such definition. Under proposed methodology, languages are defined using a set of pairs, composed of a query and a group of mappers. The queries, defined over the language's diagrammatic syntax, return language constructs. These constructs are mapped by the mappers to behavioral programming-based models. Resultant definition is executable, can inter-operate with similar definitions of other languages, and is accessible to practitioners who read code but shy away from transition formulae. We demonstrate our approach by defining a subset of the LSC language, and by implementing an LSC runtime engine based on that definition.
Diagrammatic modeling languages hold great promise for
software engineering, being able to depict — quite literally
— structural and behavioral specifications. While some
diagrammatic languages have been adopted for
documentation and high-level design, their promise is still largely
unrealized when it comes to describing executable
models. Almost 30 years after Harel presented StateCharts [
A few factors that might be holding back the adoption of diagrammatic languages for execution are lack of accessible definition of executable semantics, and the absence of runtimes that can interoperate with text-based code.
This paper proposes an approach for defining executable semantics for diagrammatic languages. The definition is accessible to anyone who can read procedural formulation, and lends itself to runtime engine implementation. As the runtime is based on the Behavioral Programming paradigm, it can easily integrate with text-based code.
The rest of this paper is organized as follows: Section II briefly introduces Behavioral Programming. Sections III and IV introduce and discuss the concept of querying diagrams and mapping them to BP-based code, respectively. Sections V and VI apply the approach to a subset of the Live Sequence Chart language (LSC). Section VII describes a runtime tool for LSC, implemented based on those definitions. Section VIII demonstrates how the proposed approach can be used to accommodate semantic variation points. Section IX looks at related work, and Section X concludes.
II. A QUICK INTRODUCTION TO BEHAVIORAL PROGRAMMING
Behavioral Programming (BP) [
III. SEMANTIC MAPPING TO BEHAVIORAL PROGRAMMING When defining semantics for a diagrammatic language, we propose the language developer defines a set of pairs, composed of a query and multiple mappers, and a set of BP events called Source-Semantic Events. The queries, defined over the source language’s terms and semantics, take a diagram and return a set of language constructs. The BPmappers take each returned construct and generate a set of b-threads, called construct agent b-threads, or CABs.
CABs act on behalf of their construct during program
execution. Source Semantic Events are used to signal events
in the original program, e.g. “message passed” for LSCs or
“step completed” in an Activity Diagram [
The set of query-mapper pairs define the executable semantics of the diagrammatic language. Run together, CABs generated by query-mapper pairs produce a valid execution of the mapped program. An execution of a program is considered “valid” if the order of the Source Semantic Events in its trace complies with the requirements of the diagrammatic language.
From a BP point of view, there is nothing special about a CAB or an source-semantic event. While both carry special semantics for the diagrammatic program, these semantics are only present in the interpretation of the behavioral program’s event log — not while the program is executing. BThread Registration
BProgram
Query source code result1 result2
••• resultk
Semantic Mapping
CAB C•••AB CAB CAB C•••AB CAB CAB C•••AB
CAB Source Language
Mapping
Behavioral Programming Fig. 1. Defining operational semantics for diagrammatic languages using querying and mapping. Queries select constructs from a diagram. Selected constructs are mapped to one or more Construct Agent B-threads (CABs). Run together, those CABs generate a valid execution of the original program.
Describing the semantics of a formal diagrammatic language by mapping its constructs to BP is advantageous for a number of reasons. Resultant definitions are both formal and accessible, as they use simple code snippets rather than transition formulae. Furthermore, the definitions are executable, so language developers can test and verify them, and readers can write programs to test their understanding. This combination of readability, formality and executability improves upon existing practices.
Formality and executability are crucial for removing
ambiguities. Obviously, non-formal definitions might be
ambiguous (e.g. Chan et. al. about Java [
The structure of the resultant definition is intuitive and easy to navigate, as the query-mappers pair structure is similar to that of a language reference. Our experience is that many CABs can be reused across multiple constructs. As CABs define semantics, this is not just regular code reuse, but also concept and comprehension reuse.
The proposed approach allows language developers to independently mix and match semantic variations of language constructs, as changing the semantics of a single construct is done by changing the relevant mapper only. Adding and removing language constructs can be experimented with in a similar way (See Section VIII).
Additionally, this type of definition allows for
program analysis. For example, model checking tools such as
BPMC [
Finally, since BP serves as common ground to diagrammatic languages defined using the proposed approach, these executable definitions allows for language interoperation. We have demonstrated such interoperation between LSC and UML Activity Diagram.
Our proposed approach is, of course, not perfect. When a language construct is mapped to many CABs, the reader is required to keep in mind the state of those CABs in order to fully comprehend that construct’s behavior. This issue is somewhat alleviated by CAB comprehension reuse. Another issue is that the definition relies on BP, which is still in early adoption stages.
V. CASE STUDY: SEMANTIC VARIATIONS OF LSC
We will now demonstrate our approach by creating the
operational semantics of a subset of Live Sequence Charts
(LSC). LSC is a diagrammatic programming language that
extends classical message sequence charts, mainly with
a universal interpretation and must/may, monitor/execute
modalities. The language was developed by Damm and
Harel [
An LSC system consists of scenarios and objects. Each scenario describes a facet of the system’s behavior and is described in a live sequence chart (an LSC). The overall system behavior is the result of concurrent execution of all the LSCs it contains. An example LSC is shown in Figure 2.
Objects, which appear in LSCs as lifelines, can send messages to each other or to themselves. Sending these messages is depicted in the charts by horizontal arrows between lifelines. Messages can be tagged as must occur (“hot”, red) or may occur (“cold”, blue), and as executed (“execute”, solid) or waited for (“monitor”, dashed). The Play-Engine variant supports both synchronous and asynchronous messages; in PlayGo, all messages are synchronous.
Each LSC is comprised of lifelines and messages. LSCs may contain variable assignments and flow-control elements, such as loops and conditional execution. Special kinds of lifelines represents the user and the environment. Conditional guards, shown as elongated hexagons, specify statements that must be true for the execution to continue. A special condition called SYNC, always evaluates to true and is used to synchronize lifelines.
card1:Card card2:Card click() click()
SYNC !(c1.value.equals(c2.value))
flipDown() flipDown() p:Panel beep()
The point where a lifeline intersects with a message, a condition, or any other language construct, is called a location. During execution, lifelines proceed along their locations in downward vertical order. The collection of all current lifeline locations in an LSC, called a cut, is the equivalent of a program counter in traditional code.
The execution of an LSC consists of a series of events, such as message passing or condition evaluations. An event is called enabled when all its preconditions have been met — involved lifelines have arrived at their respective locations, and variables have been bound, etc. At runtime, the LSC engine repeatedly selects an enabled event for execution. Then lifelines move to their next locations, and the chart’s cut is updated.
The system avoids executing forbidden events whenever possible. Forbidden events may be specified in various ways: A scenario of events ending in a hot false condition is considered forbidden. When an LSC is “strict”, all events that appear in it and are not enabled by its cut are forbidden. Finally, the Play-Engine variant allows tagging individual events as forbidden in some designated scope. When a forbidden event is nevertheless executed, an exception called violation occurs.
LSC is an interesting language for demonstrating our proposed approach, since it is a real-world diagrammatic language with non-trivial semantics. Additionally, it has multiple semantic variants, which allows us to mix and match semantics of specific constructs.
This paper focuses on the operational semantics of a single LSC and on a subset of the constructs. The construct subset was selected such that it contains examples for all construct types, and so it can be intuitively extended.
In this section we present a visual dictionary that lists the syntactic query and BP-mapping for each LSC construct. Query matches are highlighted with a yellow background. For example, in the Sync definition (Subsection VI-B), the SYNC hexagon and the intersection of its upper edge are matched, and are labeled snc and l1 to ln for the purpose of the BP-mapper pseudo-code that follows. CABs composing the BP-mapping for the construct matched by each query appear after the query’s diagram. Re-used CABs are referred to by name, and listed at Subsection VI-J. This graphical representation of the queries is an idea for future implementations that may allow for an intuitive specification of language constructs. In our current implementation we use a textual query language and the graphical representation is compiled manually for the sake of readability.
All CABs exit when an exit event of their parent chart is triggered. This is done using the BP idiom of break-upon: bthreads terminate when an event whose a member of their set of break-upon events is triggered. We use break-upon for readability — it is possible to simulate it using pure Request-WaitFor-Block, by adding the break-upon event set to the wait parameter of every bsync, and then exiting if the triggered event is a member of this set.
BP allows blocking and waiting for abstract sets of events. The model in this paper uses two such event sets: VisibleEvents, which contains all message passings, and ExitEvents(chart), which contains all events signaling execution termination of a chart or a subchart.
Code listings in this paper serve both as an implementation and as a specification. Thus, we invite the reader to read them as both imperative and declarative. As an imperative code, bsync(waitFor:E, block:VisibleEvents) reads “wait for E, and until then block all visible events”. When read declaratively, it says “No visible event can happen until E does”.
chartName
L1 loop until *
name Li l1 cond l2 l3 cond msg msg msg l4 ln
Ln chart
Lifeline CABs are responsible for advancing the chart’s cut. A lifelineCAB, started by its parent chart, begins by waiting for its parent chart’s start event (first bsync). It then advances along its locations, repeatedly requesting to enter and leave them. During execution, a lifelineCAB blocks its parent chart from ending normally.
During the execution of subcharts, such as Loop (Subsection VI-I), lifelineCABs wait for the subchart to be over; L1 L1
L2 L2 This CAB forces the message passing event to be enabled prior to being triggered. The concept of an event being “enabled” is part of the LSC language, and so Enabled(m) serves as a source semantic event.
A “hot” message has to be executed once it was enabled (unlike a “cold” message which may or may not happen). The difference in behavior is achieved by adding a single CAB, as shown below. The rest of the CABs are reused. m(v1,..vn) l l1 message(v1,..vn) 2 ² Same CABs as for the cold, executed message. ² A TriggeredBlockUntilCAB, where the trigger event is Enabled(m), after which the event set ExitEvents(chart) is blocked until Message(m) is selected.
E. Cold, Monitored Message inside the subchart, new lifelineCABs act on behalf of the lifelines. This is achieved by the if statement at the top of the iteration loop.
² Lifeline CAB: lifelineCAB (chart , l1 , ..., ln): bsync ( waitFor : ChartStart ( chart ) ) for ( i 2 [1.. n] ): if ( li is at bottom of subchart ): bsync ( wait : Done (subchart),
block : ChartEnd ( chart ) bsync ( request : Enter (li),
block : ChartEnd ( chart ), VisibleEvents ) bsync ( request : Leave (li),
block : ChartEnd ( chart ))
² For each i 2 {1, . . . , n} instantiate a BlockUntilCAB, blocking Enabled(snc) until Enter(li) is selected. ² For each i 2 {1, . . . , n} instantiate a BlockUntilCAB, blocking Leave(li) until snc is selected. ² Instantiate the following CAB: syncCAB ( snc ): bsync ( request : Enabled ( snc ), block : Sync ( snc )) bsync ( request : Sync ( snc ), block : VisibleEvents ) This CAB enforces the SYNC to be enabled prior to being triggered. By blocking VisibleEvents in the second bsync, this CAB ensures that once enabled, the SYNC will be triggered prior to any visible event.
² Instantiate two BlockUntilCABs, blocking Enabled(m) until Enter(li) is selected (for i 2 {1, 2}). In case the sender lifeline is also the receiver, it is possible to omit one of these CABs. ² Instantiate two BlockUntilCABs, blocking Leave(li) for i 2 {1, 2} until Message(m) is selected. ² For each variable v not affected by m, instantiate a BlockUntilCAB, blocking Enabled(m) until Bound(v) is selected. These CABs prevent m from being enabled until all variables it depends on are bound. ² For each variable v affected (bound) by m, instantiate a BindFromCAB, binding v when Message(m) is selected. These CABs announce the binding made by m for v. ² Instantiate a single ceMessageCAB (shown below): ceMessageCAB (m): bsync ( request : Enabled (m), block : Message (m)) bsync ( request : Message (m)) m(v1,..vn) l l1 message(v1,..vn) 2 ² Except for the ceMessageCAB, all CABs used for the cold, executed message (Subsection VI-C) are reused “as is” for the cold, monitored one. ² Instantiate a single cmMessageCAB (below). This CAB is identical to the ceMessageCAB, except for the second bsync call which waits for the message passing event rather than requests it. cmMessageCAB (m): bsync ( request : Enabled (m), block : Message (m)) bsync ( waitFor : Message (m))
L1
L2 m(v1,..vn) l l1 message(v1,..vn) 2 ² Same CABs as for the cold, monitored message. ² An additional TriggeredBlockUntilCAB, as for the hot, executed message.
L1
L2 l1
l2 ² For i 2 {1..n}, instantiate a BlockUntilCAB, blocking
Enabled(cnd) until Enter(li) is selected. ² For i 2 {1..n}, instantiate a BlockUntilCAB, blocking
Leave(li) until Condition(cnd) is selected. ² Instantiate a single coldConditionCAB (below) with the matched parameters. coldConditionCAB ( cnd ): bsync ( request : Enabled ( cnd ),
block : Condition ( cnd )) if ( evaluate ( cnd ) ):
resultEvent = Condition ( cnd ) else :
resultEvent = ColdViolation ( cnd ) bsync ( request : resultEvent , block : VisibleEvents )
cnd ² Same as cold condition (Subsection VI-G), except that hotConditionCAB requests a HotViolation event.
An LSC loop is a type of a subchart: It can contain any LSC construct, including other loops, but uses the lifelines of its parent chart. A cold violation of a loop terminates it, but not its parent chart.
For every match of:
L1
L2 l1,1 l2,1 loop until *x ctrl
Ln ln,1
loop l1,2 l2,2 ln,2
² BlockUntilCAB, waiting for Leave(li,1), while blocking
Enabled(loop). ² loopCAB (see below) with the matched parameters. loopCAB ( loop , ctrl ): bsync ( request : Enabled ( loop ) ) loopIteration (loop , ctrl ) bsync ( request : Done ( loop ), block : VisibleEvents ) loopIteration ( loop , ctrl ): if ( ctrl > 0 ): startCABs ( loop ) bsync ( request : ChartStart ( loop ),block : VisibleEvents ) event = bsync ( request : ChartEnd ( loop ),
waitFor : ExitEvents ( loop )) if ( event is ChartEnd ( loop ) ): loopIteration (ctrl -1, loop ) loopIteration. After the last iteration, it announces the loop is done by requesting a Done(loop) event. Blocking VisibleEvents ensures that once the loop is done, it is declared as such prior to any message being passed. The loopIteration sub-routine starts by checking whether a new iteration is needed. If so, it creates the CABs for the loop subchart, and requests its start event to be fired. This event signals the lifeline CABs of the subchart to start advancing along their location list. When the subchart execution is done, loopIteration checks whether the subchart ran to completion. If so, another iteration is attempted1. While the loop construct is executing, the lifelines of the parent chart waitFor it to end before entering their next location, below the chart.
Common behavior aspects of constructs of the LSC language are captured for reuse by the following CABs: 1) BlockUntilCAB: This CAB block an event until another one is triggered. Used in all constructs to enforce correct execution order, the code for this CAB consists of a single bsync call. blockUntilCAB ( blocked , waitedFor ): bsync ( waitFor : waitedFor , block : blocked ) 2) TriggeredBlockUntilCAB: This CAB waits for an event, and then blocks a set of events until another event is selected. triggeredBlockUntilCAB ( trigger , blocked , waitedFor ): bsync ( waitFor : trigger ) bsync ( waitFor : waitedFor , block : blocked ) 3) BindFromCAB: This CAB is responsible for binding a single variable to a value extracted from a message. It waits for the message to be sent, and then requests a binding event announcing the new binding. bindFromCAB ( message , variable ): selected = bsync ( waitFor : message ) value = selected . message . get ( variable ) bsync ( request : Bound ( variable , value ), block : VisibleEvents )
In order to test our approach, we implemented an LSC
runtime engine. The engine takes an XML description of an
LSC as input. It then uses XQuery [
Input: LSCs are described using straightforward XMLbased format. Reminiscent to a verbal description of an LSC, the format includes nodes such as <lifeline> and <message>.
A loopCAB starts by requesting its loop is enabled. It then runs the loop repeatedly, using the sub-routine 1For the special case of control value *, which means unbounded amount of iterations, we define *-1=*.
Queries and BP-Mappers: Queries over the XML files
are done using XQuery. We use the BaseX [
BP engine: Generated BP code uses Javascript and the
BPjs [
Using this engine, LSCs described using our XML format can be directly executed. The code is available at https://github.com/michbarsinai/BP-javascript-search.
Previous sections presented the concept of querying
source code and mapping the results to BP as a mechanism
for “breathing semantics into diagrammatic languages”, to
paraphrase [
The messages described in Section VI are synchronous. We will now add an asynchronous message, which allows the sending lifeline to advance passed the send location without waiting for the receiving lifeline to receive the message. This type of messages exists only in the PlayEngine variant; PlayGo does not support it.
Instantiate the following CABs: ² BlockUntilCAB, blocking Enabled(m), waiting for Enter(l1). ² BlockUntilCAB, blocking Received(m), waiting for Enter(l2). ² BlockUntilCABs, blocking Received(m), waiting for Sent(m). ² BlockUntilCAB, blocking Leave(l1), waiting for Sent(m). ² BlockUntilCAB, blocking Leave(l2), waiting for Received(m). ² For each variable v not affected by m, a BlockUntilCAB, blocking Enabled(m), waiting for Bound(v). ² For each variable v affected (bound) by m, a BindFromCAB, blocking Sent(m), waiting for v. ² A single asyncMessageSendCAB (shown below), forcing the message sending event to be enabled prior to being triggered. asyncMessageSendCAB (m): bsync ( request : Enabled (m), block : Sent (m)) bsync ( request : Sent (m)) ² A single asyncMessageReceiveCAB, requesting that the message is received. asyncMessageReceiveCAB (m):
bsync ( request : Received (m)) As there are blockUntilCABs blocking the message from being received prior to being enabled, fully bound, sent, and having a lifeline in location to receive it, this CAB does not need to handle all these preconditions and their possible orderings.
The mapping for asynchronous messages can be used either as a replacement for the synchronous message mapping, making all messages asynchronous (e.g. in a “what if we made all messages asynchronous” scenario), or as a mapping for a new type of specification idiom.
An LSC can be strict or tolerant. A Strict LSC is violated if an event that appears in it happens when it is not enabled. Such event will not cause any violation for a tolerant LSC. In PlayGO, all LSCs are strict. In Play-Engine, both modes are allowed.
Strictness can be imposed by adding b-threads to the mapping of a chart, one for each message appearing in the LSC. Each b-thread is initialized with the events that are present in its respective chart. The function cut(chart) returns the cut of chart, which is the set of all the locations its lifelines are currently in. Obtaining the cut of a given chart does not require direct communication with that chart or its lifelines — the cut can be obtained by waiting for the Enter events of that chart’s locations. A cut is considered HOT if at least one of its locations is HOT. chartEvents = events_of ( chart ) nonBlocked = ; repeat : event = bsync ( waitFor : AllEvents ,
block : chartEvents \ nonBlocked ) if ( event is Enabled (x) ):
nonBlocked = nonBlocked [ {x} else if ( event 2 nonBlocked ):
nonBlocked = nonBlocked \ { last_event } else : if ( isHot ( cut ( chart )) ):
bsync ( request : HotViolation , block : VisibleEvents ) else :
bsync ( request : ColdViolation , block : VisibleEvents ) Listing VIII-B.2. Enstrictor, a b-thread that makes an LSC strict
The LSC implementation presented so far uses dynamic typing, as it does not verify that receiving lifelines implement the messages they receive. Using event blocking, we can block messages unimplemented by their receiver in a purely incremental manner, by adding a b-thread.
BP allows b-threads to block sets of events by passing a predicate to bsync. InvalidMessages, defined in Listing VIII-C.3, is a predicate valid for all messages unimplemented by their receiver. In order to prevent these messages, the typeSystemBThread can be added to the system. InvalidMessages ( msgEvent ): return
msgEvent . message 62 msgEvent . receiver . definedMessages typeSystemBThread :
bsync ( block : InvalidMessages ) Listing VIII-C.3. Type System Event Set and BThread. This code assumes each lifeline has a list of defined operations
Traditionally, when typing constraints are imposed on a program, they are imposed on all of it. Our proposed approach of imposing typing constraints offers more flexibility: It can be lifted or imposed with no change to the rest of the code. It can be limited to parts of the code by altering the predicate. Or, it can pass the invalid method call to a special handler that can perform any arbitrary operation. This is somewhat similar to SmallTalk’s doesNotUnderstand: method, invoked when an object receives a message it has no method for.
The notion of describing semantics by mapping one
domain onto another is not new. AToM3 [
In [
This work was also partly motivated by the call expressed
in [
By querying the syntax of a diagrammatic language and mapping the result to BP-based code, we can formally define the operational semantics of said language. Resultant definition has a is executable, accessible to practitioners who shy from state change formulae but read code readily, and allows the language developer to independently experiment with different semantics of language constructs. We have demonstrated the proposed approach using a subset of the LSC language, and presented a working software tool based on that definition.