On the formal interpretation and behavioural consistency checking of SysML blocks

Abstract

The Systems Modeling Language (SysML) is a semi-formal, graphical modelling language used in the specification and design of systems. We describe how Communicating Sequential Processes (CSP) and its associated refinement checker, FDR3, may be used to underpin an approach that facilitates the refinement checking of the behavioural consistency of SysML diagrams. We achieve this by utilising CSP as a semantic domain for reasoning about SysML behavioural aspects: activities and state machines are given a formal, process-algebraic semantics. These behaviours execute within the context of the structural diagrams to which they relate, and this is reflected in the CSP descriptions that depict their characteristic patterns of interaction. We describe how CSP and FDR3 can be used in conjunction with SysML in a formal, top-down approach to systems engineering. Moreover, the compositionality afforded by CSP alleviates the state space explosion problem frequently encountered with complex formal models and complements the top-down approach of SysML. Typically, a system is composed from constituent systems using the concept of blocks. SysML permits two alternative interpretations with regard to the behaviour of the resulting composition. We argue that the use of a process-algebraic formalism enables us to explore the relationships between these interpretations in a more rigorous fashion than would otherwise be the case.

1 Introduction

Modern systems are typically characterised as compositions of interconnecting components or systems, functioning as a whole in order to achieve a shared goal. This makes it increasingly difficult to orchestrate combined behaviour and to ensure that the intended behavioural characteristics of the complete system are adhered to, while maintaining operational independence of the components or systems that make up the whole. The need to establish solutions to technologically challenging problems, often in a short time frame, further complicates the matter. Moreover, the environment external to a system is constantly evolving and ever more demanding, resulting in external interactions of increased complexity. These interactions are more taxing, either because the systems are being used in an unfamiliar or previously unforeseen context, or because the systems themselves are more complex. Thus, it is clear that a systematic approach to deal with this inherent complexity and entanglement would be beneficial in a number of different ways.

The Systems Modeling Language (SysML) [17], which was proposed by the Object Management Group (OMG)¹, is a graphical modelling notation that can be used to describe complex, heterogeneous systems comprised of various components. Modelling a system with SysML relies on the concept of blocks—each of which has an associated set of states—communicating via events, possibly resulting in a change of state for one or more of the communicating blocks. The architecture of these systems allows a top-down design, starting from an abstract level with high-level concepts, down to levels with increasingly more detail. These successive transformations give rise to the pleasing opportunity of allowing the replacement of an abstract block with a composition of parts; however, a big drawback of this decomposition approach is that it is at best semi-formal and, as such, cannot guarantee consistency between a block and its parts.

Communicating Sequential Processes (CSP) [9, 19] is a process algebra that can be used to describe complex patterns of interaction between processes, with each process having its own characteristic behaviour. In this paper, we show how CSP can be used to precisely define the differing notions of composition outlined above. Moreover, the associated refinement checker, FDR3 [8], gives rise to a practical approach that enables us to reason about these interactions. We make use of a case study to illustrate the approach.

SysML and CSP have clear differences. We would argue, however, that it would be beneficial to develop a framework that integrates the two, with a view to offering the benefits of both. Specifically, by translating SysML into CSP, there is the potential to give a precise definition of the intended behaviour of a given SysML model, by making use of the underlying formal semantics of CSP. Consequently, this would allow us to undertake refinement checking of the SysML model. It should be noted that the intention is not to replace existing SysML modelling tools; rather, the intention is to develop a formal framework that can be used in conjunction with such tools in order to complement the modelling activity being undertaken.

Activities and state machines are the core behavioural constructs used to ascribe behaviour to SysML blocks. The aforementioned constructs are frequently used in combination: activities are used to assign behavioural features that ought to execute in a particular state, or on a given transition [17]. In this paper, we provide a behavioural semantics for the conjoined behaviour of state machines and activities. There have been several contributions where the sole focus was either the formalisation of state machines or the formalisation of activities. To the best of our knowledge, this paper is the first contribution where the intention is on the provision of a behavioural semantics that encompasses both these formalisms.

At the structural level, SysML takes a compositional approach with regard to systems specification: a block can be comprised of other blocks, which, in turn, might themselves consist of blocks. However, for the approach to be effective and useful, the behavioural conducts of these blocks need to be specified in a consistent manner. Moreover, the approach needs to enable the modeller to sufficiently abstract away details irrelevant to a particular level of abstraction. Friedenthal et al. [7] suggest two alternative interpretations with regard to the combined behaviour. These can be characterised as follows.

• 1. The classifier behaviour of the block can serve as an abstraction of the behaviours of its parts. The abstraction serves as a specification that the parts must realise: the parts must interact in such a way that their combined behaviour conforms to the abstraction.

• 2. Alternatively, the classifier behaviour of the block acts as a controller in order to actively orchestrate the behaviours of its parts. In this case, the behaviour of the block is a combination of its behaviour and that of its parts.

We argue that the use of a process-algebraic formalism enables us to explore the relationships between these interpretations in a more rigorous fashion than would otherwise be the case. CSP was selected due to its compositional nature and good tool support.

When mapping between two seemingly disparate notations, it is crucial that the source notation be adequately constrained in order to ensure that the resulting formulation in the target notation is sensible. To this end, we place certain restrictions on, or make certain assumptions about, the state machines we consider. These are detailed below.

• Every top-level state machine² in our formalisation is a simple composite state: the region of this state houses the entire state machine. This state has no associated state-based behaviours.

• Orthogonal composite states are not allowed. As such, we do not consider fork and join states.

• We do not support do behaviours.

• Transitions between regions are limited to source and target states that are simple or simple composite states themselves. Thus transitions that cross-regional boundaries are not permitted to start or terminate on pseudostates.

• Submachine states are not supported.

• We do not consider history pseudostates in our formalisation.

• Every region contains a valid state machine. In particular, this state machine is allowed only one compulsory initial state. Multiple final or terminate states are permissible, as appropriate.

• Each initial state has a single outgoing transition: by insisting on a single outgoing transition, we ensure that the first active starting state is unambiguously defined.

• The outgoing transition of an initial state may not contain explicit triggers or guards.

Similarly, we constrain the activities we consider by imposing the following restrictions.

• Every activity has a unique starting point designated either by a single initial node, or, if there is no initial node, a single parameter node from which control starts.

• Flow final nodes are not permitted.

• We do not allow for activity partitions in our formalisation.

• An action can have either outgoing object flows or outgoing control flows, but not both.

• The behaviour of a call behaviour action in our formalisation is assumed to be an activity.

• We exclude activities that have activity parameter output nodes from consideration.

• We only consider simple fork and join nodes: if a fork node splits into k separate flows, then those k flows will eventually be joined via a join node.

• Incoming flows are not allowed for initial nodes.

• Initial nodes are allowed a single outgoing control flow.

The structure of the remainder of this paper is as follows. In Sect. 2, we give the background to our work. Then, in Sect. 3, we present our CSP model of state machines. Section 4 formalises activities, while Sect. 5 considers a formal model of SysML blocks. We then illuminate and validate our approach, via a case study, in Sect. 6. Finally, in Sect. 7, we summarise the contribution of this paper and place it in the context of work undertaken by other authors.

2 Background

In this section, we give consideration to our languages of interest—CSP and SysML. We start by presenting a brief introduction to CSP.

2.1 Communicating Sequential Processes

2.1.1 Syntax

Events are at the heart of CSP—they are fundamental to the synchronisation mechanism that is employed—with an event being an indivisible communication or interaction. We denote by $\varSigma$ the set of all possible events for a particular specification. We can also give consideration to the alphabet of a process—the events that it can perform. We write $\alpha ~P$ to denote the alphabet of a process P.

A communication takes place when two or more processes agree on an event. The communication can be a primitive event, or it can take a more structured, message-passing form, utilising channels. The message-passing mechanism is based on the principle of a rendezvous between a sending and a receiving process: if the communication takes place on a channel, c, and a sending process wants to output a value, e, then the receiving process has to allow for this (by inputting on c). Once this has happened, the event is abstracted as c.e. A process indicates that it intends to output a value on a channel using the syntax c!e; the willingness to receive an input on a channel is expressed as c?x.

CSP is compositional in the sense that it provides operators that allow us to define a process in terms of other, constituent processes. In the following, we consider those operators that are of relevance to this contribution.

The CSP syntax utilised in this paper is defined as follows:

In the above, P, $P_1$, $P_n$ and $P_i$ denote processes, e denotes an event, X, Y and $X_i$ denote sets of events, and b denotes a Boolean condition.

Stop denotes the deadlocked CSP process: it refuses to participate in all events. Skip is the process that communicates the special internal event, $\checkmark$, before behaving like Stop; it is used to model successful termination.

The process , modelled using the prefixing operator, , performs the event e and subsequently behaves as the process P.

CSP provides two choice operators: the external or deterministic choice operator, , offers the environment the choice between the initial events of its argument processes; conversely, the internal or nondeterministic choice operator, , offers no such choice and the observed behaviour may be that of either of the two participating processes. Indexed versions exist for both operators. For example, is an external choice between processes $P_i$, where i serves as an index for the parameterised process P.

The application of the hiding operator, , in the process conceals the events of X from the view of the external environment of P.

The process represents the sequential composition of processes $P_1$ and $P_2$. This process behaves as $P_1$ until it terminates successfully, after which it behaves as $P_2$.

Several parallel operators exist in CSP.

First, the process uses the generalised parallel operator to define an interface, consisting of the events of X, on which $P_1$ and $P_2$ must synchronise. Events outside X may occur independently in either process. The process denotes alphabetised parallel, where synchronisation takes place on events in the set $X \cap Y$. Finally, the interleaving operator, , expresses the unsynchronised concurrent interleaving of the events of its two constituent processes.

Indexed forms exist for all of these parallel operators. For example, represents the indexed interleaving of processes of the form $P_x$, where $x \in X$.

A conditional choice construct is available in the form , where a process behaves as $P_1$ if b is true and $P_2$ otherwise.

The let within construct allows us to use local definitions (of the form of ) in the definition of a complex process: .

2.1.2 Semantics

CSP allows us to compare the behaviour of one process against that of another. Several semantic models exist, but the consideration of traces and failures is sufficient for our purposes in this paper.

The traces of a process, P, written , are the set of all finite sequences of observable events.

For example, is the set

$P\mathrm {/}t$ represents the state of the process P after the observation of the trace t, and represents the initial set of events refused by P, no matter how long they are offered. To quote Roscoe [18]: “A refusal set is a set of events that a process can fail to accept anything from however long it is offered” [18]. It follows that the elements of are the pairs of the form (t, X) for some , and such that . As an example, the pair $(\langle a \rangle , \{ a, c, d \})$ is a failure of the above internal choice, as is $(\langle c \rangle , \{ a, b, c \})$.

We define traces-refinement, using reverse containment, as

For example, the process —the traces of which are given by the set $\{ \langle \rangle , \langle a \rangle , \langle a, b \rangle \}$—is a traces-refinement of the process :

We define failures-refinement similarly:

For example, the following refinement holds as the second process is more deterministic than the first:

The traces of both processes are given by

The failures of are given by

In the above, denotes the power set of $\{ a, b, d \}$, i.e. the set of all subsets of $\{ a, b, d \}$.

The failures of are given by

The refinement checking tool FDR3 [8]—which uses the machine-readable dialect of CSP, CSP$_{M}$—uses this theory of refinement to investigate whether a potential design meets its specification. A pleasing feature of FDR3 is that if such a test fails, a counter-example is returned to indicate why this is so. The interested reader should refer to [9] for a comprehensive introduction to the semantics of CSP.

2.2 Systems Modelling Language

SysML is a more compact language than UML. This fact is reflected by the total number of diagrams and constructs present in the specification: SysML has a total of nine diagrams, whereas UML has 14.

SysML is an extension of a subset of UML: some of the UML diagrams are reused (state machine diagram, sequence diagram and package diagram); some are extended (activity diagram); some are modified (block definition diagram and internal block diagram modify the class diagram and composite structure diagram, respectively); and others are newly introduced (requirement diagram and parametric diagram).

Blocks are the core modelling constructs of SysML and provide the context in which behaviours execute. A block is often composed of other blocks, termed parts, each of which has its own associated behaviour. As per Sect. 1, there are two alternative interpretations with regard to the combined behaviour [7]: the classifier behaviour of the block can serve as an abstraction of the behaviours of its parts; alternatively, the classifier behaviour of the block acts as a controller in order to actively orchestrate the behaviours of its parts.

Classifier behaviours are the main behaviours of blocks. They execute from the instant the instance is created until the point of destruction. The modelling construct most frequently used to represent the classifier behaviour is a state machine. In most systems engineering methodologies, activities are typically used as a complementary modelling notation to state machines: it is the behavioural formalism normally associated with the effect component of a transition; alternatively, it is used to model behaviours related to a particular state.

A signal is a classifier that types the asynchronous messages that are communicated between blocks. Each signal optionally has an associated set of attributes that correspond to the parameters that make up the content of the message.

Typically, two block instances communicate using signal events—instances of signals. The initiating block sends a signal event to a target block. This signal event is defined as part of the supplementary behaviours—described using activities—associated with the initiating state machine: the entry or exit behaviours of the active state or the effect component of the enabled transition. The receipt of the signal event in the target block may subsequently trigger a transition in its state machine. The approach described above is popular when modelling event-based systems.

A connector connects two or more parts or references. The connection formally allows the connected components to interact, although the connector does not characterise the nature of the interaction. Instead, the interaction is stipulated by the behaviours of the connected blocks.

State machines allow one to depict state-dependent behaviour in a graphical fashion in terms of nodes and labelled edges: nodes represent states, whereas the edges correspond to transitions between states.

Activities provide the modeller with the ability to describe complex routes (termed flows) along which actions execute. In SysML activities, there are two types of flows: control flows and object flows.

We defer detailed discussions on state machines and activities until Sects. 3 and 4, respectively, where the relevant concepts will be introduced alongside the respective formal models.

3 A CSP model for SysML state machines

Our formalisation of state machines can be considered to be a hybrid of the semantics previously presented by Ng and Butler [15] and those previously presented by Bolton Davies [4], and Davies and Crichton [6]. Specifically, we use the semantics of [15] as a basis, extended with an event queuing mechanism proposed in [4] and [6].

3.1 Abstract syntax

Let $\mathcal {M}$ denote the set containing all state machines. In the following, we consider the formalisation as it relates to a single state machine, $M \in \mathcal {M}$.

A state machine describes state-based, event-driven behaviour in terms of a finite collection of states, and transitions between those states. A state machine M is thus an ordered pair $(S_M, T_M)$, where:

• $S_M$ represents the set of states;

• $T_M$ represents the set of transitions.

3.1.1 Transitions

Every transition exists between a source and a target state:

A transition consists of a trigger, a guard ³ and an effect:

In the above, $\mathcal {S}$ is the set of signals and $\mathcal {A}$ is the set of activities. We denote by $\mathcal {Bool}$ the set $\{ true, false \}$.

3.1.2 States

We partition $S_M$ such that:

• $S_M^I$ represents the set of initial states;

• $S_M^F$ represents the set of final states;

• $S_M^T$ represents the set of terminate states;

• $S_M^J$ represents the set of junction states;

• $S_M^C$ represents the set of choice states;

• $S_M^S$ represents the set of simple states; and

• $S_M^{SC}$ represents the set of simple composite states.

The aforementioned sets are pairwise disjoint and fully partition $S_M$.

Every state in our formalisation has a unique name (i.e. name is an injective function):

In the above, $N_M$ denotes the set of state names of state machine M.

Every simple or simple composite state has an optional entry and exit behaviour; do behaviours are excluded from consideration. All state-based behaviours are modelled via activities.

In each case, an activity modelling the state-based behaviour is returned.

The function

returns the set of outgoing transitions for a given state. The transitions returned are those emanating from the state at a syntactical level, as per the graphical depiction. In other words, the function does not return transitions emanating from states that transitively enclose the input state.

Our formalisation makes use of the concept of a pseudostate. A pseudostate is a state in which a state machine may temporarily find itself. For example, all initial, junction and choice states are considered pseudostates.

3.2 Modelling concepts

3.2.1 Enclosing states

A simple composite state has exactly one region:

Note that the concept of region only exists for composite states. A state machine has an enclosing top state $s \in S_M^{SC}$ at the root of the state hierarchy. This state is a simple composite state. We assume the existence of a function that, given a state machine, returns the top state:

We define a helper function, surround, that associates a state with its immediately enclosing state.

The function above is partial by virtue of the fact that no state encloses the top state. We may also wish to consider all states that enclose a particular state. A second helper function

returns, for a particular state $s \in S_M$, the set containing those states that immediately or transitively enclose s. Thus

We require the functions enclose and surround to be anti-reflexive: the hierarchy imposed on states may not include circular definitions where a state is allowed to be its own enclosing state.

Hierarchical state machines need to take entry and exit behaviours of transitively enclosing/enclosed states into consideration during the firing of transitions.

A pivot state is the state, for a given transition, where the nested exit behaviour of the source state has finished execution, and the behaviour of the effect component is executed, before the nested entry behaviour of the target state begins.

We assume the existence of a function, pivot:

Before we define pivot precisely, we must introduce the $\mu$-notation. The expression

denotes the unique object x drawn from the set X such that the predicate p holds.

For a transition, $t \in T_M$, we define a pivot state to be the innermost jointly transitive enclosing state with regard to the source and target states of t. Thus

In the above, the function

returns, given a set of states, the set of states at the innermost level of the state hierarchy. More specifically, innermost returns from the input set of states only those that do not enclose any of the other states:

3.2.2 Example

As an example of the above mathematical constructs, consider Fig. 1: state machine $M_{ex}$ with top state $top_{M_{ex}}$. We have the following.

Fig. 1

State machine $M_{ex}$. $M_{ex}$ is a hierarchical state machine. State $s_1$ is a simple composite state with a single region, $r_1$. We have merely labelled the transitions, omitting triggers, guards and effects. Similarly, entry and exit behaviours of the respective states are elided

Consider transition $t_9$ of Fig. 1, the source and target states of which are $s_5$ and $s_3$, respectively. The sets of states that enclose $s_5$ and $s_3$ are the following.

The function pivot returns the pivot state $s_1$ of transition $t_9$.

3.2.3 Behaviours

In our formalisation, all transition effects, entry and exit behaviours are modelled using activities. In general, an activity can be as complex as required, or may, instead, be reduced to a single, simple event. We shall discuss activities formally in Sect. 4.

The aforementioned behaviours are all optional: the effect component of a transition can be omitted if not needed; similarly, entry and exit behaviours are not compulsory. For the case where the SysML behaviour is left unspecified, we make use of the empty activity. This approach is chosen in order to make the CSP formalisation more concise.

The empty activity, process $A_\epsilon$, is defined thus.

The exit behaviour is executed upon exiting a state. In particular, this happens after the triggering event, but before the behaviour specified by the effect component of the selected transition. Exit behaviours cannot be interrupted. SysML allows the outgoing transitions of an enclosing state to be triggered from within one of the nested states. In this case, the exit behaviours of the transitively enclosing states will be triggered starting with the innermost active state until we reach the pivot state in the state hierarchy. These transitions that emanate from a composite state are termed high-level transitions.

We now formulate a CSP process that models exit behaviour.

Let s be the current active state with outgoing transition t. Furthermore, restrict the source and target states of t to simple or simple composite states. Thus

We can formalise exit behaviour as follows.

It is important to note that the above is only defined between states that are not pseudostates. By imposing this restriction, we can be confident that the function exit is defined for every state in the construction above. Moreover, integrating the semantics of high-level transitions with that of complex transitions⁴ would unnecessarily complicate the formalisation in CSP.

The entry behaviour is executed upon entering a state. Again, this behaviour is not susceptible to interruption. After the behaviour of the effect component has finished execution, the nested entry behaviour is executed starting with the outermost state inwards towards the designated target state.

We now turn to model entry behaviour and assume a current active state s with outgoing transition t. Therefore

The entry behaviour can be formalised as follows.

Again, we insist that the above is defined only for states that are not pseudostates to ensure that the construction is valid.

The effect is a behaviour, executed upon the transition between states; in this paper, such behaviours are described via activities. In particular, the behaviour of the effect component is executed after the nested exit behaviours of the source state, but before the nested entry behaviours of the target state. In the state hierarchy, this corresponds to the pivot state. In our formal model, the effect component of a transition t is given by effect(t).

3.2.4 Termination condition

The termination condition relates to the generation of a completion event. A completion event is generated only once the relevant completion criteria, defined in terms of the termination condition of the currently active state, have been met. The completion criteria can be summarised thus.

• For a simple state $s \in S_M^S$ the termination condition is, according to the standards [16, 17], the completion of the do behaviour. However, since we do not model do behaviours in our semantics, this condition is trivially satisfied upon entry into a state. We argue that the completion event should therefore be offered along with permitted explicit transitions.

• For a simple composite state $s \in S_M^{SC}$ the termination condition is satisfied, according to the standards [16, 17], if either:

  • the final state of the state machine residing in the region of the composite state is reached; or

  • the do behaviour of s terminates.

  As we do not model do behaviours, it follows that the termination condition is satisfied if and only if the state machine residing in the region of the composite state s has reached a final state.

3.2.5 Transitions

Transitions are key to our formalisation. We elaborate on the different components that constitute a transition and present basic concepts that aid in their formalisation.

The trigger is the stimulus that enables a transition to fire. In this paper, we consider triggers to be either signal events or completion events.

• A signal event corresponds to the arrival of an asynchronous message typed by a signal. A signal event is an explicit trigger. As such, we must annotate the trigger component of the transition with the signal that typed the triggering event.

• A completion event is an implicit event that signifies the exit from a state. Diagrammatically, it is annotated on a transition by omitting the trigger component.

In our formal model, implicit (or completion) events are denoted by $\pi$. The definitions for implicit and explicit transitions can be stated thus.

Consider a state $s \in S_M$ with a single outgoing transition t. Thus

We model the CSP process describing s as follows.⁵

This approach is chosen in order to provide a uniform treatment for all triggering events. Thus, for a transition $t \in T_M$, trigger(t) denotes the trigger, regardless of whether that transition is triggered explicitly or implicitly.

In our formalisation, completion events are modelled using CSP events of the form $\pi$. Explicit events correspond to CSP events that reflect the name of the classifying signal, along with any parameters communicated as part of the event; a signal with an argument associated with it will input on the CSP channel with the corresponding name. For example, if the signal is named $S_j \in \mathcal {S}$ has argument a, we use the CSP event $S_j?a$ as the trigger.

The guard of a transition must evaluate to true in order for the transition to occur; alternatively, if the guard is false, the triggering event is consumed without effect.

Consider a state $s \in S_M$ with a single outgoing transition t. Thus

We model the CSP process describing s as follows.⁶

In the above, the evaluation of the guard following the triggering event determines the next active state.

A guard is evaluated based on the arguments that are served up along with the triggering event. For example, if we had the event $S_j?a$ as a trigger, the a can be used in the evaluation of the guard. To preserve the clarity of the presentation, we simply write guard(t) to denote the evaluation of the guard. Recall that a guard is a Boolean expression to be evaluated at runtime. In the above example, the a can be used as part of an expression to be evaluated at runtime—the result of which will be one of true or false. Typically, the expression to be evaluated will involve testing the value passed as part of the triggering event for equality/inequality to known constants in the model (modelled using enumerations).

The combined behaviour of a transition can now be modelled. Consider a state with a single high-level transition t that contains a trigger, a guard and an effect; the high-level transition is between nonpseudostates.

Alternatively, if either the source or target state is a pseudostate, we know that no transitions crossing regional boundaries are permitted. It follows that entry and exit behaviours, where applicable, reduce to entry(target(t)) or exit(s), respectively.

3.2.6 Mapping function

We make use of a mapping function $\mathcal {F}$ that maps the structural constructs to their CSP counterparts. Broadly speaking: each state in SysML corresponds to a process in CSP; and each SysML event corresponds to a CSP event. Thus, the idea is that the mapping rules take us from a given SysML state to the next: in CSP, this corresponds to initially behaving like one process, and then behaving like another. In each state, the CSP process behaves like the state machine would in the corresponding SysML state. Every rule, $\mathcal {F}(M,s)$, is defined such that it describes the behaviour of state machine M at state s. These rules define process definitions, where each state is represented by a CSP process. In CSP, the name of the process describing state s is given by name(s); the behaviour of this process will be given by $\mathcal {F}(M,s)$. Therefore

The mapping rules for state machine M start from the initial state contained in the region of the top-level state, top(M). This approach is based on that taken by Ng and Butler [15].

3.3 Behavioural semantics

This section outlines an approach to integrate SysML state machines and CSP by providing a behavioural semantics for the former in terms of the latter. Throughout, we make use of the syntactical structures and modelling constructs of Sect. 3.1.

The behavioural semantics of state machines, as defined in this paper, is based on the type of the currently active state. As such, the outline of our presentation mirrors this by providing a formalisation for each of the different state types in the remainder of this section.

3.3.1 Initial state

An initial state designates the first active state of state machine M. Consider an initial state, $s \in S_M^I$, with a lone outgoing transition, $t \in outgoing(s)$. A completion event, which serves as an implicit trigger, is generated upon entry to the pseudostate. Recall that effect returns the empty behaviour if no effect component is defined for t. The CSP process modelling s follows.

Because no explicit triggers are allowed, only an implicit trigger is generated and $trigger(t) = \pi$. An explicit transition is not allowed due to the fact that a state machine is not allowed to linger in a pseudostate. Similarly, a state machine is not allowed to be hindered from transitioning out of the initial state by means of a guard that evaluates to false—guards are therefore not allowed.

We insist on the presence of a unique initial state in every region. This rule ensures that the state machine residing in the said region is well defined in the scenario where it is entered by default: an incoming transition ends on the state hosting the region.

3.3.2 Final and terminate states

A final state indicates the termination of a region. Subsequently, it has no outgoing transitions. Once a final state is reached, a completion event is generated to indicate the completion of all behaviour of the containing region, and, thus, the termination of the state machine. There is, however, no requirement for a region to contain a final state. For example, a state machine that never terminates would not have a final state.

Let $s \in S_M^F$ be a final state. If the final state resides within a simple composite state and there is at least one outgoing transition emanating from any of the transitively enclosing states, that is

then reaching the final state represents the termination of the state machine in the region of the state surround(s). The completion transition emanating from surround(s), if present, or any of the explicit transitions emanating from transitively enclosing states, may be taken. Completion transitions emanating from transitively enclosing states other than surround(s) may only be taken once their respective final states are reached.

Alternatively, if the final state resides within a simple composite state and there are no outgoing transitions emanating from any of the transitively enclosing states, that is

then reaching the final state denotes the termination of M:

Reaching a final state in a nonhierarchical state machine is a special case of the last scenario.

The formalisation of a terminate state is trivial: the state machine behaves as the CSP process Skip.

3.3.3 Junction and choice states

A junction state is a transient point along a compound transition. The first leg of the compound transition contains the trigger and optional guard; note that an effect component is not allowed. Similarly, on the second leg, a trigger component is not allowed due to the fact that a complex transition must be selected in response to a single event. As the triggering event is assumed to have occurred on the first leg of the transition, it is disallowed for the second. Guard and effect components are allowed for the second leg of the compound transition.

A choice state differs from a junction state with regard to the first leg of the compound transition in that it additionally allows for an effect component. The consequence of this is that the effect component can influence the outcome of the guards on the second leg. In contrast, a junction state does not permit an effect component on the incoming transition, and, as such, the guards on the second leg are in principle evaluated the instant the triggering event is served up for processing. However, as our formalisation is centred around the outgoing transitions, there is no difference between the CSP formalisation for a junction state and that of a choice state. The distinction, however, would be made during the formalisation of the source state of the first leg of the compound transition.

Because junction and choice states are transient points along a complex transition, we do not allow explicit events to be triggered from the transitively enclosing states. Explicit events from the states that transitively enclose the junction or choice state can only be triggered once both legs of the compound transition have been taken. This semantics is in line with the notion that these are merely pseudostates along a compound transition, and that the transition must be completed before other events can be triggered.

The process modelling the junction or choice state is instantiated with the arguments passed on the trigger of the first leg of the complex transition. These arguments are used to evaluate the guards of the transitions that emanate from the state, with the parameters indicated between the square brackets following the mapping function.

Note that in our formulation the transitions that terminated and emanated from junction or choice states are not allowed to cross-regional boundaries. In the above, the formal parameters of the signal that typed the send signal event that served as the triggering event correspond to $params(trigger('t))$. The transition $'t$ is that of the first leg of the compound transition. In addition, $eval(guard(t),params(trigger('t)))$ denotes the evaluation of the guard condition of t, by substituting the associated parameters of $trigger('t)$ in the expression guard(t).

3.3.4 Simple state

A simple state $s \in S_M^S$ does not contain a region, and, as such, cannot host nested states. The behaviour of a simple state is formalised in terms of its own outgoing transitions, and the explicit transitions of the states that transitively enclose it.

The above composition can be deconstructed as follows.

• The process offers the nondeterministic choice between all completion or implicit transitions. The indexed form of the choice operator is used as it is possible for a state to have more than one completion transition.

• The process offers the deterministic choice between all explicit, outgoing transitions of s. Deterministic choice is selected as the transition taken is dependent upon the triggering signal; the decision as to which transition to take is not internalised as is the case for completion transitions. Thus, all possible transitions ought to be offered.

• For transitively enclosing states of s, we permit only explicit transitions. Transitions emanating from the states that transitively enclose s are allowed to trigger, while s is active. When a higher level transition fires while s is active, the state s is exited and the transition followed.

Each of the above corresponds to a different scenario under which s might be exited. However, the behaviour once an exit is triggered remains the same, as described by the expositions following the guard.

3.3.5 Simple composite state

A simple composite state $s \in S_M^{SC}$ has a single region which contains nested states. For that region, only one of the nested substates is allowed to be active. Recall that each region has a unique initial state. The behaviour of the composite state is described by the behaviours of the states that it contains. It follows that a transition to a composite state is equivalent to a transition to the initial state of that composite state. The composite state thus behaves like the initial state that it contains. The subsequent behaviour is then completely described by the target state of the initial state, and so forth. This is by virtue of the fact that our formalisation for noncomposite states, like initial, final and simple states incorporate the transitions of the states that transitively enclose them.

Given , the unique initial state of s, the formalisation is as follows.

3.3.6 Execution environment

Run-to-completion semantics The execution semantics for SysML state machines is as follows. A run-to-completion semantics is defined: a state machine is only permitted to consume a single triggering event, namely the current event, at any one instant and must do so until processing of the said event is complete. For this purpose, each state machine has an associated event queue.

• An event is received when it is accepted and waiting for processing. The event is placed at the back of the event queue.

• The event at the front of the queue is removed and presented to the state machine. At this instant, it becomes the current event. We say the event is dispatched.

• The state machine finishes the processing of the current event, uninterrupted, and until completion. Once this has happened, the event is consumed. A consumed event is no longer available for processing.

In the formalisation, we assume a FIFO queue, although the standard [16] does not define the order of dequeuing.

Event queue We model the event queue of a state machine using a CSP process called EQ that communicates on a channel queue.

The above formulation is in essence a buffer process that sits between the state machine and its external environment. A triggering event e is communicated along channel queue by the external environment. The event is then consumed (and therefore removed from the buffer) by the state machine on channel local. An event can be consumed in one of two ways.

• The event can be processed: the current active state has an outgoing transition with a triggering event that corresponds to the event served up for processing. In this case, the event takes the form local.proc.e.

• The event can be discarded: the current active state has no outgoing transition corresponding to the event served up for processing. In this case, the event takes the form local.disc.e.

The event queue is willing to communicate either event by inputting on the channel; the events offered by the current active state will determine whether the event is processed or discarded.

Here, we assume a queue with a maximum capacity of 1; the queue blocks when full. Nonblocking semantics, where events are discarded when the queue becomes full, is conceivable; so are event queues with different capacities. A semantics with an unbounded queue is also conceivable, although this is not finite state, and therefore not amenable to verification with FDR3. However, animators can be used to explore the behaviour in the case of unbounded event queues.

The process definitions, as they stand in Sect. 3.3, are not entirely complete: we need to adapt these to consider whether a particular event should be processed or discarded, depending on the current active state of the state machine M. In particular, triggering events need to be extended to include communication on the channel local ⁷—an event e that is processed takes the form local.proc.e or local.disc.e, depending on whether the event is processed or discarded at the time it is served up for consumption (as determined by the active state of the state machine).

Thus, we need to consider the eventuality where the state machine M receives a signal event not expected in the current state $s \in S_M$: that is, an instance of a signal event $S_j \in \mathcal {S}$ such that . Here, the state machine discards the unexpected event.

Assume that the function

returns the set of unexpected events for state $s \in S_M$. The interpretation of unexpected events depends on the type of the current state.

If the current state is a pseudostate, that is

then unexpected events are receive signal events that are not outgoing transitions of the current state s.

Alternatively, if the current state is a nonpseudostate, that is

then unexpected events are receive signal events that are not contained within the outgoing transitions of the transitively enclosing simple or simple composite states of s, and outgoing transitions of s itself.

Thus,

State machine The overall state machine is modelled as a single process that contains, as appropriate, localised process descriptions corresponding to the state machine’s syntactic structure, with the overall structure being similar to that described in [6]. The environment external to the state machine communicates with the event queue. The state machine receives all communications via its associated event queue, which is modelled as a CSP buffer of size 1. It communicates with this buffer on a CSP channel, local. Each of the localised processes has access to this channel in order to receive communications from the event queue.

The process that models the state machine, M, first behaves as that associated with the initial state, $\mathcal {F}(M,i)$, and then as each of the subsequent processes, until it terminates in state f. The local process EQ models the event queue.

In the above, the local definitions $\mathcal {F}(M,i) \dots \mathcal {F}(M,f)$ take into consideration whether an event will be processed or discarded.

In Sect. 5.3, we discuss the communication semantics for multiple state machines, as well as integration with other constructs, such as activities.

4 A CSP model for SysML activities

4.1 Abstract syntax

Recall that $\mathcal {A}$ denotes the set containing all activities. We consider the formalisation as it relates to a single activity $A \in \mathcal {A}$. An activity A is a quintuple

where:

• $A_A$ denotes the set of action nodes;

• $R_A$ denotes the set of routing nodes;

• $P_A$ denotes the set of parameter nodes;

• $CF_A$ denotes the set of control flows; and

• $OF_A$ denotes the set of object flows.

An activity defines flow-based behaviour in terms of nodes and edges: the nodes are represented by the sets $A_A$, $R_A$ and $P_A$; the edges are denoted by $CF_A$ and $OF_A$.

4.1.1 Nodes

Actions are the building blocks of activities. The set of action nodes $A_A$ is further partitioned such that:

• $A_A^{SS}$ denotes the set of send signal event actions;

• $A_A^{RS}$ denotes the set of receive signal event actions;

• $A_A^{VS}$ denotes the set of value specification actions;

• $A_A^O$ denotes the set of opaque actions; and

• $A_A^{CB}$ denotes the set of call behaviour actions.

The aforementioned sets are pairwise disjoint and fully partition $A_A$.

Routing nodes are used to model complex flow-based logic. The set of control nodes $R_A$ is partitioned thus:

• $R_A^I$ denotes the set of initial nodes;

• $R_A^F$ denotes the set of final nodes;

• $R_A^{FK}$ denotes the set of fork nodes;

• $R_A^{JN}$ denotes the set of join nodes;

• $R_A^D$ denotes the set of decision nodes; and

• $R_A^M$ denotes the set of merge nodes.

The aforementioned sets are pairwise disjoint and fully partition $R_A$.

Activity parameter nodes, denoted by $P_A$, are used to model the input and output arguments of activities. For our purposes, we only consider activity parameter nodes that serve as inputs to activities; this is partly due to a desire to keep the semantics elegant and partly due to the context in which we use activities. We assume that a single argument is passed per node.

4.1.2 Edges

An object flow is used to model the passage of a parameter between two nodes: the parameter flows from the source or outputting node to the target or inputting node. We define the following functions for an object flow $of \in OF_A$, to yield the outputting and inputting object node, $source_{of}$ and $target_{of}$, respectively.

Note that the aforementioned are total functions: every object flow must have an associated source (or target) node.

The outgoing edges of a decision node have mutually exclusive guards that determine the next flow to be taken. The function

denotes the evaluation of the guard of an object flow emanating from a decision node. The guard is evaluated based on the value of the object passed along the incoming flow of the decision node.

Control flows model the passage of control between the constituent nodes of an activity. Control flows are permitted between action and routing nodes. We define the following functions for a control flow, $cf \in CF_A$, to yield the source and target node, respectively.

Guards on control flows are not modelled. Our formalisation of state machines evaluated guards based on the value of a parameter passed with the triggering event. In SysML, guards on control flows are used in a more general sense and typically expressed in natural language; however, we would argue that interpreting guards using natural language is unsuitable in a formal framework, where a precise meaning is desirable. Moreover, we seek to provide a semantics where guards are interpreted in a uniform manner. Activities typically execute within the context of state machines, and we will therefore interpret the guards analogously.

4.2 Modelling concepts

4.2.1 Outgoing edges

The function

returns the set of outgoing object flows for certain types of nodes.

We also define a similar auxiliary function that returns, for certain types of nodes, the set of outgoing control flow edges:

We require an action to either have an outgoing object flow or an outgoing control flow, but not both:

Fig. 2

Activity $A_{ex}$. $A_{ex}$ is not allowed in our formalisation due to the fact that action $a_1$ has an outgoing control flow $cf_2$ as well as an outgoing object flow $of_1$. However, $A_{ex}$ would have exactly the same behaviour if $cf_2$ was removed

4.2.2 Mapping function

To define behavioural semantics for activities, we once again make use of a mapping function, $\mathcal {F}$, that maps the structural constructs to their CSP counterparts. Every node in SysML corresponds to a process in CSP; similarly, every edge has an associated CSP process. The idea is that the mapping rules take us from the SysML source node to the target node: in CSP, this entails initially behaving like the source process, then behaving like the edge connecting the source and target nodes and then behaving like the target node. The behaviour of the edge is usually the behaviour of its target node; an object flow edge has an additional process parameter to model the flow of objects. Every rule, $\mathcal {F}(A,c)$, is defined such that it describes the behaviour of activity A at a particular construct c. These constructs are the nodes and edges of A. The mapping rules for activity A start from the initial node.

4.2.3 Example

Refer to Fig. 2 and activity $A_{ex}$. We have

4.3 Behavioural semantics

The behavioural semantics of activities, as defined in this paper, is based upon the type of the currently active node. As such, the outline of our presentation mirrors this by providing a formalisation for each of the different node types in the remainder of this section. The semantics further distinguishes and provides alternative interpretations based on the type of the connecting edges, activity parameter nodes and value specification actions.

4.3.1 Control flow

Control flows are used to route the flow of control between different nodes of an activity. In our formalisation, a control flow $cf \in CF_A$ can be thought of as a CSP process. The behaviour of this process is dependent on the target node of the control flow, given by $target_{cf}(cf)$. If the target is not a join node, i.e. $target_{cf}(cf) \notin R_A^{JN}$, the process simply designates its behaviour to be that of the target node.

In the case where $target_{cf}(cf) \in R_A^{JN}$, there will be $k-1$ other control flows that terminate in the same join node.⁸

Let the control flows be . Exactly one of the control flows, $cf_0$, will exhibit the behaviour of the join node.

The above construction ensures that exactly one of the previously forked flows continues after the join node.

4.3.2 Object flow

Object flows model the flow of objects between the different nodes in an activity. In our formalisation, an object flow $of \in OF_A$ behaves similarly to a control flow edge. However, the value of the object being passed along the flow is passed as a process argument between the processes representing the different constructs. We do not permit object flows to terminate on or emanate from join nodes (see the formalisation of join nodes). Thus, the behaviour of an object flow is given by the behaviour of the node that it terminates on, $target_{of}(of)$.

The process modelling the object flow simply designates its behaviour to be that of the target node, passing the object o as a process parameter.

In the above, the CSP process to the left is initialised by the source node of object flow of, $source_{of}(of)$.

4.3.3 Initial node

An initial node $i \in R_A^I$ is a routing node that designates the starting point of an activity A. Subsequently, only a single control flow is permitted to emanate from i; object flows are disallowed and can neither emanate from, nor terminate on i. Let the unique control flow be

The formalisation of the initial node follows.

Only one initial node is permitted per activity.

4.3.4 Final node

A final node $f \in R_A^F$ has no outgoing edges and a single incoming control flow edge. It is modelled trivially as the CSP process Skip.

4.3.5 Send signal event

A send signal event action is used as a means of communication between different activities that execute within the context of state machines; the action corresponds to the sending of a signal event. A send signal event action node is entered either via a control flow or an object flow edge; in the case where the node is entered via a control flow an incoming object flow is possible, provided the object flow emanates from a parameter node. Note that a send signal event action is always exited via a control flow edge.

A send signal event action has an input pin corresponding to the attribute of the signal to be sent⁹ and one input pin to specify the target for the signal.

Entry via control flow A send signal event action $ss \in A_A^{SS}$, entered via a control flow edge, with a single outgoing control flow,

can be formalised thus:

A send signal event action has an input pin that names the target of the send signal action. In CSP, this corresponds to the channel name used to communicate with the target state machine, denoted by target(ss) in the above. The name of the signal event is given by signal(ss).

Optionally, an incoming object flow of is possible. This serves as input to the send signal event action and models the parameters sent as part of the send signal event. In our semantics, the object flow of, if present, emanates from an activity parameter node $p \in P_A$ and terminates on the send signal event node ss; ss is therefore not entered via of, but of is instead used to pass a value to be used as part of the action. Note that an incoming control flow is still present and also terminates on ss. The construction par(p) is the parameter available within the context of the owning activity, as defined per the arguments of the process modelling the activity.

Entry via object flow Consider a send signal event action $ss \in A_A^{SS}$, entered via an object flow edge, with a single outgoing control flow

In this case, the process modelling the send signal event action would have an input argument, p, passed from the process modelling the incoming object flow.

4.3.6 Receive signal event

A receive signal event node represents the action of receiving a signal event. A receive signal event action node can only be entered via a control flow, but may be exited either via a control or via an object flow.

A receive signal event action may output the received signal attribute on an output pin. An input pin is used to specify the source of the event.

Exit via control flow A receive signal event node is typically exited via a control flow edge if the receive signal event has no associated attributes. Assume a receive signal event action $rs \in A_A^{RS}$ with a single outgoing control flow

and no signal attributes associated with the signal. In the following, source(rs) denotes the source specified for the receive signal event.

If a signal attribute is present, we have an input on the CSP channel corresponding to the attribute a.

Exit via object flow A receive signal event action node can only be exited via an object flow if the signal has attributes that are output along the object flow. Assume a receive signal event $rs \in A_A^{RS}$ with a single outgoing object flow

and an associated attribute a.

The attribute a is passed along the object flow by instantiating the process modelling the flow correspondingly.

4.3.7 Value specification action

A value specification action is a primitive action that outputs a constant value on its output pin. A value specification node is always entered via a control flow edge. Let $vs \in A_A^{VS}$ be a value specification action with outgoing object flow

We have

In the above, value(vs) denotes the value output by the action.

4.3.8 Opaque action

An opaque action is an action executed in a language external to SysML. An opaque action may optionally take an input and, after executing the action, produce an output. These opaque actions are modelled as CSP events.

There are three possible formalisations for opaque actions permitted in our formalisation. We consider each in turn.

Entry and exit via control flows Assume the existence of an opaque action $oa \in A_A^O$ node entered via an incoming control flow, and an outgoing control flow

In the following, action(o) denotes the event corresponding to the opaque action of node oa.

Entry and exit via object flows Assume the existence of an opaque action $oa \in A_A^O$ node with an incoming object flow and an outgoing object flow

In the composition below, o denotes the object that serves as input to the opaque action, passed via the object flow.

It is possible to view opaque actions as functional: the action takes an input and produces an output. In CSP, this can be modelled as a function g.

Entry via object flow; exit via control flow Assume the existence of an opaque action $oa \in A_A^O$ node with an incoming object flow passing object o and an outgoing control flow

We have

4.3.9 Call behaviour action

A call behaviour action allows an activity to call another behaviour as one of its actions. While this can be any behavioural formalism of SysML, we consider only the calling of activities. We restrict the activities used as call behaviour actions to contain only input pins; output pins are not permitted. Alternatively, a call behaviour action node may be entered via a control flow. In our model, call behaviour nodes are always exited using control flows.

Entry via control flow Consider a call behaviour action $cb \in A_A^{CB}$ with an incoming control flow and a single outgoing control flow

The construction behaviour(cb) represents the CSP process modelling the activity specified as part of the call behaviour action cb.

Entry via object flow Consider a call behaviour action $cb \in A_A^{CB}$ with an incoming object flow and a single outgoing control flow

The object o is passed to the CSP process behaviour(cb).

4.3.10 Fork node

A fork node splits a single flow into multiple separate flows. The flows can be either control flows or object flows. However, if the flow terminating on a fork node is a control flow, then control flows must exit the node; similarly, if an object flow terminates on the fork node, then multiple object flows must leave the fork node.

Control flows A fork node $fk \in R_A^{FK}$ operating on control flows splits the incoming control flow in k separate outgoing flows . The alphabetised indexed parallel construction ensures that all the different threads of control only synchronise on the join event; all other events are interleaved.

Object flows The formalisation for object flows is similar. The difference is that the object is passed to each of the k separate forked flows. A fork node $fk \in R_A^{FK}$ operating on object flows splits the incoming object flow in k separate outgoing object flows .

4.3.11 Join node

A join node synchronises previously forked flows: it has k incoming flows and a single outgoing flow. We only formalise join nodes that operate on control flows. The reason for this is that the semantics of join nodes that operates on object flows does not sit well with our formalisation. The object flows in our semantics essentially deal with process arguments, i.e. concrete values. However, token flow semantics on object flows via join nodes requires that each token on every flow is passed to the outgoing flow. This would be inconsistent with our treatment of object flows and are thus excluded.

A join node $jn \in R_A^{JN}$ synchronises k parallel control flows and has a single outgoing control flow, cf:

Recall that only one of the previously forked flows will behave as the join node.

4.3.12 Decision node

A decision node offers the choice between possible alternative flows, based on the evaluation of guards. A decision node has an incoming flow edge and several outgoing flow edges, with mutually exclusive guards placed on the outgoing edges. However, only one of the outgoing edges—the edge where the guard evaluates to true—is taken. Our model only incorporates object flows via decision nodes. This is intrinsically linked with the evaluation of the guards of the outgoing edges.

A decision node $d \in R_A^{D}$ over object flows passes an object along one of several possible object flows. The k alternative outgoing object flows $of_k \in outgoing_{of}(d)$ are evaluated. The following assumes mutually exclusive guards. A guard may contain an else clause, in which case it is trivially mapped to a CSP else construct. Machine-readable CSP has only an if then else conditional construct; we are therefore forced to adapt the formalisation to include the process Stop, as presented below.

4.3.13 Merge node

A merge node has several incoming flows, but only one outgoing flow edge. The merge node behaves like the process modelling its outgoing flow.

Control flow A merge node $m \in R_A^{M}$ has a single outgoing control flow, cf:

The behaviour can be modelled thus.

Object flow A merge node $m \in R_A^{M}$ has a single outgoing object flow

along which the object originating from one of the incoming flows is passed.

4.3.14 Execution environment

The activities in our formalisation execute within the context of a state machine. Each state machine has an event queue that interacts with the external environment under a run-to-completion assumption. The activities here therefore execute under that same assumption, using the event queue of the associated, owning state machine. These activities are akin to local process definitions that execute under the process M of Sect. 3.3.

The activity as a whole is modelled with a single process that contains, as appropriate, localised process descriptions corresponding to its syntactic structure. We provide two formalisations, based on whether the activity has an initial node, or whether execution starts from the activity parameter node.

Activity with initial node An activity with an initial node always starts execution from the initial node, whether an activity parameter node is present or not. Initially, the overall process behaves like the initial node $i \in R_A^{I}$. In the following, the process argument a corresponds to the argument of the activity parameter node; if no parameter node is present, the process argument is elided. The argument a is a global parameter available for use anywhere in the activity; diagrammatically, the use of this parameter would be indicated with an object flow connecting the parameter node and the node using a as input.

Activity without initial node It is possible for an activity to initially behave as an activity parameter node. In this case, we assume there is no initial node, and that a single object flow connects another node with the activity parameter node. Thus, the activity initially behaves as the activity parameter node. In this case, we assume a single activity parameter node with a single outgoing object flow. Let $p \in P_A$ be the lone activity parameter node, with argument a.

The activity parameter node behaves like the outgoing object flow:

5 A CSP model for SysML blocks

In this section, we provide formalisations for the structural counterparts of our framework. The behavioural formalisms we have introduced thus far—state machines and activities—all execute within the context of a structural counterpart. The structural constructs of interest to us are enumerations, signals, blocks, parts and connectors.

5.1 Enumerations and signals

Signal and enumeration definitions introduce the messages and associated parameters communicated between state machines and activities.

Let $\mathcal {E}$ denote the set of all enumerations. An enumeration is a user-defined type where the enumeration literals represent distinct constants in the model. The CSP counterpart of a SysML enumeration is a CSP datatype. Here, there is a one-to-one mapping between the constants of the CSP datatype, and the enumeration literals defined for the SysML enumeration.

Let $\mathcal {S}$ denote the set of all signals. Signals are communicated along the connectors that connect parts. The signals used by the communicating state machines correspond to constants of a CSP datatype definition. For each block, the signals corresponding to the provided receptions of the particular block are used. Where a signal has associated parameters, these are included in the datatype definition.

5.2 Blocks, parts and connectors

The fundamental modelling construct present in SysML is the block. Each block is assigned an associated main behaviour, called its classifier behaviour. Depending on the purpose of the block, the classifier behaviour can either be a state machine or an activity.

Let $\mathcal {B}$ denote the set of all blocks. A block $B \in \mathcal {B}$ is a classifier that describes common behavioural and structural features of its instances, and can be considered akin to a UML class. We assume that the classifier behaviour is specified using state machines, and given by the function

These blocks communicate via events (instances of signals) that act as stimuli for the respective state machines.

A block makes known the names of the receptions, each corresponding to a signal, that: it responds to (i.e. the block provides the behaviour); or, alternatively, expects its SysML environment to respond to (i.e. the environment provides the behaviour). These behavioural features are designated as provided and required behavioural features. We define the functions

to return provided and required receptions.

The internal block diagram graphically sets out the internal structure of a block from its parts. In contrast, the block definition diagram depicts the composition of a block, but abstracts away from the internal structure. A part is connected to another part via a connector; it is an instance of a block. As such, it represents a particular usage of its classifying block within the context of its owning block. Each part $P \in \mathcal {P}$ is typed by a block $B \in \mathcal {B}$; the function

reflects this.

The connector serves as a bidirectional link between the block instances and is used to convey signals between communicating block instances. The state machine of a block B only receives (through its event queue) the provided receptions, prov(B). The required features, reqd(B), are communicated across the connectors linking parts. SysML block instances are connected using connectors; connectors are modelled using CSP channels. For simplicity, we use the name of the association end for the purposes of communication and assume this to be the name of the associated block instance. For example, if another part $P_i$ provides a feature $S_j$ that a part $P_k$ requires, the state machine of $P_k$ will use the name of part $P_i$ as the CSP channel on which to send the required event.

The structure, and subsequent overall behaviour, of a block $B \in \mathcal {B}$, composed from N constituent block instances, , is expressed in CSP via parallel composition. The classifier behaviour of each part $P_j$ is modelled via a state machine $M_j$, given by

The complete system, $B_i$, can be modelled by placing in parallel the processes corresponding to each of the state machines $M_j$, where $0\le j \le N-1$:

5.3 Reasoning about blocks

We now discuss and formalise the different interpretations (abstraction and controller) attributed to the resulting composition when a block is composed of other blocks.

5.3.1 Abstraction

The first of the interpretations above assumes that the behaviour of the composite block serves as an abstraction of the behaviour of its parts. Assume a block $B_i \in \mathcal {B}$ composed of K constituent blocks , where $i \ge K$. We know that the aggregate behaviour exhibited by blocks must adhere to that of the composite block $B_i$. $B_i$ is an abstract specification block that the more concrete implementation blocks must implement. Stated in terms of CSP: the characteristic process of $B_i$ serves as the specification process and , suitably combined using parallel composition, form the implementation process.

Assume that classifier(B) represents the classifier behaviour of a SysML block. Using CSP the conformance of the implementation process to that of the specification can be stated thus.

Events introduced at the lower level of implementation are excluded from the above observation; the hiding operator of CSP can be used to conceal such events.

Using this approach, and assuming the refinement holds, $B_i$ can be safely substituted for the concrete composition . This stepwise, compositional approach to systems specification and design sits well with CSP’s approach to refinement. This statement is not necessarily true for conventional model checkers that rely on temporal logics to assert safety or liveness properties. In a system of systems, $B_i$, previously our system of interest, is now just a component block representing one of the subsystems.

5.3.2 Controller

The second interpretation assumes that a block acts as a controller for its parts. The behaviour of the block is a combination of its behaviour and that of its parts: the behaviour of its parts is considered as part of the behaviour of the composite.

Assume a block $B_i \in \mathcal {B}$, which is composed of K constituent blocks , where $i \ge K$. We known that the aggregate behaviour is that of blocks as well as the composite block $B_i$. Here, we think of all of the blocks as implementation blocks that combine in order to give the desired behaviour. This can be formalised in terms of CSP thus.

6 Consistency checking: an illustrative case study

6.1 A case study

We now give consideration to a case study, which we will use to illustrate our contribution. The case study, reprised from [13], is used as a means to evaluate and illuminate the contribution of this paper.

We study a single component—a robotic arm—of a fully fledged case study that is well known within the formal methods community. The production cell is an industrial installation of a metal processing plant located in Karlsruhe, Germany [14]. However, in the interest of brevity and clarity, we consider the Arm as our system of interest. The Arm is one subsystem of the travelling crane, which is yet another component of the much bigger system—the production cell itself.

Actuators and sensors are individual components that communicate with the system controller: actuators receive outputs from the controller in order to coordinate the operation of several components; sensors, as the name suggests, are sensory components that send inputs to the system controller. Examples of actuators include bidirectional motors, which can operate in two opposing directions, and electromagnets, which can activate or deactivate a magnetic field using an electric current. A potentiometer is an example of a sensor: it provides a value within certain limits so as to indicate the range of extension.

The Arm is equipped with a bidirectional motor responsible for vertical extension. An electromagnet is placed at the front of the Arm for handling metal objects; a potentiometer is present to indicate the range of extension of the Arm.

The case study is explored from two different perspectives, related to the different interpretations that can be attributed to the composition of the composing block.

6.2 The Arm

The Arm is the block of interest for the purposes of the case study. In this subsection, we explore the behaviours of the blocks that make up the composition: BDMotor, PDMeter and Magnet. These blocks or parts have exactly the same behaviour, regardless of the interpretation assigned to their composition. We introduce the SysML constructs common to both interpretations and their relationships to their CSP counterparts in this section. We start by looking at the structural aspects, followed by behavioural constructs, such as state machines and activities.

6.2.1 Enumerations and signals

Refer to Fig. 3. Signal and enumeration definitions introduce the messages and associated parameters communicated between state machines and activities. We introduce all the signals and enumerations utilised in both interpretations here.

Fig. 3

The block definition diagram introducing signals and enumerations

The Direction and PD enumerations of Fig. 3 can be represented with CSP datatypes:

In the above, the potential differences are denoted using different constants, with each corresponding to a reading returned by the potentiometer.

The signals used by the communicating state machines are defined similarly. For each block, the signals that correspond to the provided receptions of the particular block are used. Where a signal has associated parameters, these are included in the datatype definition.

Fig. 4

The state machine diagrams of the Magnet, BDMotor and PDMeter blocks

SysML blocks are connected using connectors, which are modelled using CSP channels. For the sake of simplicity, we use the name of the association end for the purposes of communication and assume this to be the name of the associated block. Thus, for every block, we require two CSP channels: the first models the event queue that the block uses to communicate with the external environment; the second is used for internal communication between the block and its associated event queue.

For example, the channel bdmotor is used to communicate with the state machine of the bidirectional motor via its associated event queue and the channel bdmotorlocal is used by the event queue of the bidirectional motor to dispatch events for processing. The datatype Dispatched models this: an event can either be processed, or, if the state machine is in a state where the dispatched event is not expected, discarded. Using the above assumption, any block connected to BDMotor via a connector uses the channel bdmotor to send signal events destined for BDMotor.

6.2.2 State machines

The classifier behaviour is the main behaviour of a block and executes as soon as the instance is created until the point of destruction. The modelling construct that is most frequently used to represent the classifier behaviour is a state machine. In most systems engineering methodologies, activities are typically used as a complementary modelling notation to state machines: it is the behavioural formalism normally associated with the effect component of a transition; alternatively, it is used to model behaviours related to a particular state.

Figure 4 shows the state machines of the magnet, the bidirectional motor and the potentiometer. Activities that execute on the transitions as the effect component are italicised after the trigger, which is set in bold typeface. Activities are shown in Fig. 5 and are discussed in Sect. 6.2.3. For now, it is sufficient to assume that these are modelled using CSP processes.

Fig. 5

Activity diagrams modelling additional behaviours executed within the context of state machines

The CSP processes modelling the state machines for the BDMotor, the Magnet and the PDMeter blocks follow. Local process definitions model each state in the associated state machine. The deterministic choice between permissible triggers is offered to the external environment. Recall that if a CSP event corresponding to a permitted SysML triggering event is received:

• the process modelling the exit behaviour of the source state executes;

• the process modelling the effect of the transition executes;

• the process modelling the entry behaviour of the target state executes; and

• the target state is entered.

The above is modelled using the sequential composition operator. The aforementioned behaviours are all SysML activities with corresponding CSP processes; if a behaviour is not present, it is simply not included in the sequential composition.¹⁰ Note that, in every state, the dispatched, unexpected events are discarded and thus removed from the event queue without effect: this corresponds to communications of the form local.disc.e, where e is an signal event. Events that are served up for processing and successfully processed by the state machine correspond to communications of the form local.proc.e.

Alphabets of the individual processes are defined below each process definition. The alphabet of a state machine is the set of events that it can communicate, as well as the alphabets of its associated activities.

The channel pdmeter is used for communication with the state machine of the potentiometer, and pdmeterlocal is used for internal communication between the event queue and state machine.

6.2.3 Activities

The activities that serve to augment the classifier behaviour of the blocks introduced in Sect. 6.2.2 are formalised in the following.

Each activity has an associated CSP process with localised process definitions corresponding to the actions. Activity parameter nodes are modelled with local process variables. Opaque actions are communicated on the CSP channel, opaque.

The activities of the bidirectional motor—TurnOnBDMotor and TurnOffBDMotor—can be modelled thus.

The processes corresponding to the remainder of the activities of Fig. 5—ActivateMagnet, DeactivateMagnet and OnSense—are defined similarly. We omit the definitions here in the interest of brevity.

6.3 Interpretations

We now give consideration to the different notions that can be attributed to the behavioural composition of a collection of blocks using a process-algebraic approach.

Fig. 6

The block definition diagram of the Arm system

6.3.1 Abstraction

We now explore the behavioural composition of the Arm block with the first interpretation of Sect. 1—“The classifier behaviour of the block can serve as an abstraction of the behaviours of its parts”—in mind.

The block definition diagram showing the composition of the Arm is given Fig. 6; the interconnections among the parts are depicted with the internal block definition diagram of Fig. 7. The structural aspects of the system are modelled using blocks for the controller, the bidirectional motor, the electromagnet and the potentiometer. The classifier behaviour of the Arm is to serve as an abstraction of the behaviours of its parts: the BDMotor, Magnet, PDMeter and Controller. We have seen CSP definitions modelling the behaviours of the BDMotor, Magnet and PDMeter; the controller is introduced below.

Fig. 7

The internal block definition diagram of the Arm block

The channel and datatype definitions are similar to those defined earlier.

The provided and required receptions of the Controller and Arm blocks are shown below.¹¹ There is a clear correspondence between the CSP datatype definitions and the provided receptions of the SysML blocks. Required receptions should appear in the CSP datatype definitions of other blocks in the system that receive these signal events as triggers in their classifying state machines (Fig. 8, 9).

Fig. 8

The block definition diagram of the Arm block

The CSP process describing the characteristic behaviour of the controller’s state machine follows. The activity Extend is associated with the effect component of the transitions emanating from the idle state; the activity Magnetise represents the entry behaviour of the grasp state. Activities are shown in Fig. 4.

Fig. 9

The block definition diagram of the Controller block

Fig. 10

The state machine diagrams of the classifier behaviours of the Arm and Controller blocks

The blocks described above—Controller, BDMotor, Magnet and PDMeter—are all concrete implementation blocks in SysML (Fig. 10). The abstract block, Arm, which serves as an implementation that the parts must realise, is modelled below.

The process SetReady used within the ARM process follows.

The processes responsible for modelling the activities used in the CONTROLLER process follow.

All activities in this paper execute within the context of their owning state machine. An activity can take parameters, passed from the arguments of the triggering event of the owning state machine, as input. Some activities have receive signal events as actions; these receive signal events need to be passed via the event queue mechanism of the state machine. It follows that the channel used for local communication with the state machine ought to be passed in as an argument to the activity.

Send signal event actions may have input object pins that determine the argument sent as part of the event; similarly, receive signal event actions may receive arguments and therefore have object output pins. Value specification actions¹² are used in object flows to output a constant value that serve as input to another action. In every case, the internal channel is used to receive events using the event passing mechanism. Signal events¹³ are sent using the channel with the same name as the target block, similar to the approach taken for state machines.¹⁴

Assuming that

we then have

The set of processes, P, represent the concrete implementation blocks whose conjoined behaviour must be that of the block arm that serves as its specification. The similarity with CSP here is striking: refinement in CSP is expressed between specification and implementation processes.

$CONCRETE^R$ is the process with events suitably renamed to ensure compatible alphabets.

The set Hidden contains those events not present in the alphabet of the concrete specification process, ARM; $\varSigma$ denotes the set of all CSP events within the context of the specification. Thus

FDR3 verifies the assertion

As the traces-refinement holds, ARM can be substituted for its parts in the complete system: the behaviour of the concrete implementation processes (which is captured by $CONCRETE^R$) can neither accept nor refuse an event unless ARM can. Stated another way, the characteristic behaviour of $CONCRETE^R$ is completely contained within that of ARM. The compositional approach presented above is effective in alleviating the state space explosion problem: subsystems can be developed and formally verified in isolation and subsequently combined to form an integrated system description.

Fig. 11

The state machine diagram of the classifier behaviour of the Arm’ block

Fig. 12

The block definition diagram of the Arm’ system

Fig. 13

The internal block definition diagram of the Arm’ block

6.3.2 Controller

We explore the behavioural composition of the Arm block with the second interpretation of Sect. 1—“the classifier behaviour of the block acts as a controller in order to actively orchestrate the behaviours of its parts”—in mind. The second interpretation calls for the classifier behaviour of the Arm block to act as a controller in order to actively orchestrate the behaviours of its parts. Thus, the behaviour of the Arm block must be a combination of its own behaviour and that of its parts (Fig 11).

Figure 12 shows the new composition of the Arm using the second interpretation. The Arm is still composed from instances of the potentiometer, bidirectional motor and magnet blocks. The controller block, however, is missing. The interconnection between the parts is depicted in Fig. 13: the parts now directly communicate with the composite block. The resulting composition thus behaves as a combination of its own behaviour (the classifying behaviour of the Arm) and that of its parts (the behaviours of the magnet, the potentiometer and the bidirectional motor).

The behaviour of the state machine for the Arm in the second interpretation is exactly the behaviour of the controller in the first interpretation. In the first interpretation, the controller orchestrated the behaviour of the rest of the parts, and the Arm block served as the specification. Here, the Arm block itself orchestrates the behaviours of its parts.

The behaviour of the state machine for the Arm using the second interpretation follows.

The complete behaviour of the Arm and all its parts can be expressed in CSP as follows. Assuming that

we then have

The set of processes, P, represent the Arm that acts as a controller and its constituent parts: the magnet, the bidirectional motor and the potentiometer. The behaviour is a combination of the Arm and that of the magnet, the bidirectional motor and the potentiometer.

Fig. 14

The compositional approach afforded by CSP. The white ellipses denote the behavioural interpretation of blocks using the abstraction approach. The system of interest, block D, is composed of abstract blocks and serves as a controller that orchestrates the behaviour. The second interpretation, shown inside the dark ellipse, applies here. The behavioural of the overall system is the combined behaviour of blocks A, B, C and D. Furthermore, block A serves as a behavioural specification that must be satisfied by its constituted blocks A1 and A2. Block A can be substituted for its components in the overall system. A similar line of argument can be followed for blocks B and C, together with their component blocks. Safety requirements can be allocated behavioural constructs to further refine the intentions of the modeller and checked for conformance using CSP [10]

The second interpretation above has the drawback that there is no specification process that can be substituted for the composition. However, this interpretation sits well where the overall system architecture is described in terms of high-level blocks. These high-level blocks might be specification level or abstract blocks, each obtained from previous refinements using the first interpretation. At the architectural level, however, the integrated behaviour of all the components would be of interest to the modeller. Here, techniques that would assist in assured requirements traceability would be beneficial [10].

Figure 14 depicts these concepts. For example, the designers of a travelling crane might use the first interpretation above that results in an abstract block that denotes the robotic arm. This block might then be substituted in place of its components¹⁵ in the system of interest—the travelling crane—along with other blocks, such as sensors and bidirectional motors, using the second interpretation. Alternatively, the first interpretation might be used again to obtain a single abstract block, modelling the travelling crane, when the system of interest is the production cell. At this level, one might have refinements modelling behavioural safety requirements, as outlined in, for example [10].

7 Conclusions

We have shown how the refinement checker FDR3 can be used in a practical setting to ensure that different behavioural formalisms—activities and state machines—are consistent. Moreover, we have demonstrated how refinement can be used to decompose a complex design problem to give rise to a top-down approach to designing a system comprised of subsystems. In doing this, we have defined the semantics of state machines and activities that execute within this context. This paper represents a significant extension to the contribution of [12]. The interested reader is referred to [10] for a consideration of how this approach can support formal requirements traceability via refinement checking.

Table 1 Comparison of CSP formalisations of state machines

To the best of our knowledge, this is the first contribution that has explored the different notions of behavioural integration from a formal, process-algebraic perspective. Furthermore, we are not aware of any other contribution that integrates the combined behaviour of the formalisms explored in this paper—state machines and activities—using CSP.

Formal semantics for some of the SysML diagrams has been given in terms of the COMPASS Modelling Language (CML) [21]. A set of translation rules are given that maps SysML diagrams to their counterparts in CML. The work described in this paper differs in that CML integrates state-based, as well as process-algebraic description techniques. Our work, on the other hand, is concerned solely with defining a process-algebraic approach to ensure behavioural conformance among the behaviour diagrams of SysML.

Ng and Butler [15] proposed the formalisation of UML state machine diagrams, with CSP being used as the semantic domain [15]. They define the translation in terms of a mapping from structural diagrammatic constructs to their CSP counterparts. The translation starts from an initial state and then proceeds to deduce the behaviour of the entire state machine in terms of CSP descriptions. Broadly speaking, each state is mapped to a process and each UML event is mapped to a CSP event. The work of Yeung et al. [25] builds on that of Ng and Butler by generalising inter-level transitions and prioritising transitions at different levels of the state hierarchy. The authors therefore provide an alternative semantics for state machines. However, their approach only takes into account those constructs formalised in [15].

Table 2 Comparison of CSP formalisations of activities

Zang and Liu [26] mapped state machine diagrams to CSP using the model checker PAT [20]. A state machine is modelled by a single CSP process; translation rules are presented that map state machine constructs to CSP# [20], which is the input language of the Process Analysis Toolkit (PAT) [20]. Refinement checking, as well as model checking, is possible: both are natively supported by the model checker. The transformation methodology is presented via a set of rules.

Xu et al. [22, 23] formalised activity diagrams in CSP. A transformation function is defined that maps the mathematical representation of an activity to the semantic domain of CSP. The goal of the work described in [22, 23] is on providing a formal semantics for activities in terms of CSP, rather than checking behavioural conformance. Only a limited number of diagrammatic constructs are considered, and object flows are omitted. Constructs such as send and receive event actions are not addressed.

Our work differs from that of the aforementioned contributions in a number of ways. Primarily, we present a compositional approach to refinement and specification, evaluated within the context of SysML. In addition, we consider the behaviour of several interacting state machines, supplemented with behaviours described via activities. In contrast, previous approaches placed emphasis on the formalisation of a single state machine (or activity); considering the execution semantics in terms of interaction with other state machines (or activities) was not the primary focus. Tables 1 and 2 attempt to draw comparisons between our work and that of others, with respect to the constructs addressed in the various contributions.

With respect to future work, we plan to integrate the semantics of state machine and activity diagrams with that of sequence diagrams in a CSP framework that encompasses all behavioural diagrams of SysML. To this end, a formal semantics for sequence diagrams in terms of CSP has already been given in [11].

The work described in this paper significantly extends the work of [12] by providing a more comprehensive semantics for both SysML activities and state machines. The purpose of [12] was to demonstrate an integrated semantics for activities and state machines, rather than formulate a comprehensive semantics of each. In this paper, we aim to demonstrate a comprehensive, integrated semantics considering both behavioural constructs. The case study presented in [13] is employed to illuminate and validate the contribution of this paper.

Another formal method often used to formalise UML and SysML diagrams is Petri nets: state machine diagrams are given a formal semantics in [3] and [5]; activity diagrams are formalised in [24].

In conclusion, the contributions of this paper are as follows.

• We have presented a formal model of SysML blocks using CSP. In particular, we have demonstrated one interpretation of SysML blocks for modelling and integrating system behaviour in a formal setting.

• We have presented an overarching behavioural semantics for state machines and activities. To the best of our knowledge, this is the first formalisation that encompasses and considers the combined behaviour of both of these constructs.

• We have demonstrated how CSP can be used in conjunction with SysML in a compositional, refinement-based approach to specification. The proposed methodology was evaluated using a case study that we would argue is ideally suited to illustrate the principles of systems engineering.