Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Formal models are in principle accepted as the only way to specify in a precise and rigorous way the informal system requirements: they help to understand what has to be developed and to prove properties already at the early stages of the system development. However, formal specification languages are not widely used in industry, and practitioners largely consider formal methods “too hard to understand and use in practice”. Limiting factors are the lack of simplicity, learnability, readability, easiness of use of formal notations [24]. All these qualities are fundamental to achieve easiness of development and comprehension of models, particularly for large, complex software systems. Requirement models should act as a communication medium among customers, users, designers, developers, and this common understanding is fundamental for the success of the system realization. However, since the mathematical notation is not always intuitive, and the size of the specification often consists of several pages of rules and formulas, model comprehension is threatened.

Visualization is considered as a good means for people to communicate and to get a common understanding. Indeed, the use of diagrams and graphical blocks is at the base of the mostly used notations in industry, as FSMs (and their extensions) or UML, the latter nowadays accepted as the industrial standard for system design. However, their shortcomings, as limited expressiveness for FSM w.r.t. other formal notations [5] or semantics lack for UML [6], are well-known.

Ever since UML appeared, many modeling approaches have been developed which try to use UML (or one of its profiles or domain-specific UML-like notations) as front-end of the requirements specification and formal notations as back-end of the process, to provide rigor and preciseness to lightweight models and make model validation and verification possible [13, 19, 21,22,23].

Abstract State Machines (ASMs) are an extension of FSMs, obtained by replacing unstructured control states by states comprising arbitrarily complex data [5]. ASMs have been widely used as requirement specification formalism. Despite of their mathematical foundation, a practitioner needs no special training to use the method since ASMs can be correctly understood as pseudo-code (or virtual machines) working over abstract data structures. Furthermore, to ease its use by non-experts, a series of integrated tools (for editing, validation, and verification) have been developed around ASMs [4].

Although the ASM textual notation [10] has been designed with readability in mind, our experience in trying to build and read very large system specifications [1, 3] has shown that the complexity of the behavior being described overwhelms the reader, and most users (even the authors of the specification) need help in navigating and understanding it. This also happened while we were developing the ABZ 2016 case study [2], that motivated the current work. We tried, at first, to directly specify the ASM models from the textual description of the requirements. Although the refinement process helped us in managing the complexity of the case study, we still had some problems in discussing among us about the solution. So, we started making some drawings, whose notation was inspired by different sources: control flow graphs, UML state machines, sequence diagrams, etc. The lack of a way to graphically represent ASM models was clear.

A further observation we have made is that most of the new ASM users start developing ASM models as control state ASMs, a particular frequent class of ASMs – proposed by Börger in [5] – useful to model system modes (or control states). Control state ASMs have an intuitive graphical representation by means of FSM-like state diagrams. However, when the system to model is very complex, the resulting control state is too complicated and fails in achieving its main aim, i.e., easily communicating the behavior of the system. Moreover, a systematic use of control state ASMs is missing, and there is no algorithmic support to build or reconstruct such machines from models written in textual notations.

Starting from the motivations that (a) formality is important but also understanding and communicating among stakeholders is fundamental, (b) visualization of formal models can surely aid the understanding of model structure and behaviors, (c) visual editing is often used to help designers and developers to graphically build complex models [8], we here propose a graphical notation for ASMs. The overall visualization of a model is given in terms of a graph. In addition, we define structural patterns, useful to visualize the structure of a model in a more compact way, and semantic patterns to be used when additional information on the machine workflow can be inferred from the model.

The paper is organized as follows. Section 2 gives a brief background on ASMs. In Sect. 3, we introduce our proposal of a visual notation for ASMs, whose basic constituents (i.e., visual trees) are defined in Sect. 4. Section 5 shows that ASM models usually contain particular recurring patterns of ASM rules that can be visualized in a proper way: some patterns are simply structural, whereas others permit to infer some of the behavioral semantics of the ASM. Section 6 presents the prototypical implementation of a tool supporting the proposed visual notation. Section 7 describes a preliminary evaluation of the tool. Section 8 discusses some related work, and Sect. 9 concludes the paper.

2 Abstract State Machines

Abstract State Machines (ASMs) [5] are an extension of FSMs, where unstructured control states are replaced by states with arbitrary complex data. Although the method has a rigorous mathematical foundation, a practitioner can simply understand ASMs as pseudo-code working over abstract data structures.

ASM states are algebraic structures, i.e., domains of objects with functions and predicates defined on them. An ASM location, defined as the pair (function-name, list-of-parameter-values), represents the abstract ASM concept of basic object container. The couple (location, value) represents a machine memory unit. Therefore, ASM states can be viewed as abstract memories.

Values of locations can be changed by firing transition rules. They express the modification of functions interpretation from one state to the next one. Location updates are the basic units of rules construction and are given as assignments of the form \( loc \,{:}{=}\,v\), where \( loc \) is a location and v its new value. The description of all basic ASM transition rules is given in Table 1.

An ASM computation is a finite or infinite sequence \(S_0,\) \(S_1,\) \(\ldots ,\) \(S_n,\) \(\ldots \) of states of the machine, where \(S_0\) is an initial state and each \(S_{n + 1}\) is obtained from \(S_n\) by firing the unique main rule which can fire other transitions rules.

There exists a classification of ASM functions that, however, is not relevant for understanding the current work and, therefore, is here skipped.

The ASM modeling process is supported by tools of the ASMETA frameworkFootnote 1 [4] that are strongly integrated in order to permit reusing information about models during different development phases. ASMETA provides functionalities for ASM models creation and manipulation (as editing using the AsmetaL textual syntax [10], storage, interchange, etc.), and supports model analysis techniques (as validation, (runtime) verification, testing, requirements analysis, etc.).

3 A Visual Notation for ASMs

In this section, we introduce the meaning, the goals, and the possible usage scenarios of the proposed visual notation for ASM models.

The proposed visual notation is defined in terms of a set of construction rules and schemas that give a graphical representation of an ASM and its rules. We assume that the graphical information is represented by a visual graph in which nodes represent syntactic elements (like rules, conditions, rule invocations) or states, while edges represent bindings between syntactic elements or state transitions. We do not introduce a graphical representation for the signature (functions and domains) and properties, since we believe that they can be already easily understood from the textual model.

In the following sections, we propose a set of procedures that allow to automatically derive a visual graph from an ASM model. Section 4 introduces procedures that recursively visit the ASM rules and build a visual tree representing the syntactical structure of the model. In Sect. 5, we introduce some visual patterns that permit to identify recurring graphical schemas, and to obtain a more compact and meaningful representation, possibly capturing some behavioral information. Such representation may be no longer a tree, but a general graph.

The final goal is to have a textual representation together with a graphical visualization as shown in Fig. 1. To be more precise, we have devised two possible usage scenarios of the proposed visual notation.

Fig. 1.
figure 1

Visual notation

Full size image

Visualization – From Textual to Graphical Representation. The first usage scenario consists in writing an ASM model in a textual representation (AsmetaL) and then derive a graph from it. Such approach can be used when the modeler is familiar with the ASM syntax, but (s)he wants to have a graphical representation of the model for its better understanding and communication. If the ASM model is syntactically correct, also the produced graph is correct. In the visualizer, the user can activate some optimizations (presented in the following sections), in order to have different views of the same model: structural (with different levels of optimization), or semantic (behavioral).

Visual Editing – From Graphical to Textual Representation. The second usage scenario consists in graphically specifying the ASM by drawing the graph. In this way, the modeler can focus on the high level structure of the model, similarly to what is done in code with control flow graphs. Note that the usage of semantic patterns allows the user to also graphically model some evolutions of the system, which are usually difficult to get by writing textual ASM models (at least without simulating it). Of course, the graph produced by the developer is not complete, as it does not specify the signature; moreover, it could also be not correct. Some trivial syntactical violations can be automatically detected on the graph by checking some consistency rules, but other faults may be more difficult to find. Once the modeler has produced the graph, a translator can translate the graph in an AsmetaL textual model. The produced model contains (most of) the transition rules, and the modeler is only required to add the signature (and the initialization). Then, the AsmetaL parser may find some faults that passed undetected during graph validation.

4 Visual Trees

We here introduce the relevant concepts which bring to a graphical representation of an ASM model in terms of a navigable forest of tree structures, i.e., a forest of trees connected by navigation links.

Definition 1

The visual notation for ASMs is given by the bijective function \(\mathsf {vis_T}\) between an ASM rule and a visual tree.

Definition 2

The function \(\mathsf {vis_T}\) is given by Table 1.

  1. 1.

    For basic rules (update, skip and macro call) the function simply returns a tree with only one node (the root).

  2. 2.

    For compound rules (conditional, block, forall, choose, let), one must apply the schema given in Table 1 and recursively call the function \(\mathsf {vis_T}\) on component rules.

Table 1 describes the semantics of ASM transition rules, and shows the proposed graphical representation and the AsmetaL textual notation. The function \(\mathsf {vis_T}\) is only based on the syntactical structure of the ASM and it can always be applied. Tree leaves are always skip, update, or call rules, and they are shown in boxes. Note that a call rule invokes a macro rule that has its own tree that, however, is not part of the main tree. At the end, one can obtain a tree for every rule declaration by applying \(\mathsf {vis_T}\) to its definition. The visualization of an ASM is given by the forest compound of all the trees of the declared rules. To navigate this visual view, the entry point is the tree for the main rule and, from every call rule, one can navigate to the tree of the invoked macro rule by a virtual navigation link, which is not visualized in the graphical representation. By considering the navigation links in the visualization, the resulting structure is a graph, as a macro rule can be called by different call rules.

Table 1. \(\mathsf {vis_T}\): mapping from ASM transition rules to visual trees
Full size table

Example 1

For explanation purposes, we use the Hemodialysis Machine Case Study [2]. It describes a hemodialysis device which goes through three phases: the preparation in which the device is prepared and the patient is connected, the initiation in which the hemodialysis is performed (i.e., the patient’s blood is cleaned), and the ending in which the therapy terminates and the patient is disconnected. We can abstractly describe the device using the ASM model shown in Code 1Footnote 2. Using the \(\mathsf {vis_T}\) function, the model can be represented as shown in Fig. 2. Note that the three macro rules r_preparation, r_initiation, and r_ending have their own tree representations that are not part of the tree generated from the main rule, but are connected to their corresponding call rules by navigation links (here rendered as dashed arrows only for presentation purposes).

figure a
Fig. 2.
figure 2

Hemodialysis case study – visual trees

Full size image

5 Visual Patterns

We here introduce the notion of visual pattern for ASM visual trees. A pattern is a schema of connected tree nodes that is recurring and conveys a structural or semantic (i.e., behavioral) information. Therefore, identifying a pattern and substituting the entities belonging to it with a simplified structure is of interest.

5.1 Structural Patterns

We identify the following structural pattern that permits to obtain a more compact representation of the model structure.

Nested Guards Pattern. The pattern regards the use of nested conditional rules. Suppose that you have a conditional rule as shown in Fig. 3a. By applying the visual trees in Table 1, one would obtain the tree shown in Fig. 3b. However, one can visualize the rule in a more compact way as shown in Fig. 3c.

Fig. 3.
figure 3

Structural pattern – nested guards pattern

Full size image

The pattern is applicable to any depth of nested conditional rules. One just has to collect all the guards \(g_1, \ldots , g_n\), and create only one decision node comprising all the guards separated by commas. The decision node has as many exiting arcs as the number of conditional branches not containing another nested conditional rule, but a different rule rule i; each arc is labeled with the evaluations of the guards that permit to take that particular arc and fire rule rule i. Evaluations of guards that are not relevant for the firing of a rule rule i are depicted with symbol “–”. The decision node has up to \(n + 1\) exiting arcs. Note that the pattern does not necessarily produce a tree that is more clear to understand, but it always provides a more compact representation of the nested conditional rules. For this reason, we let the modeler decide if (s)he wants to apply it.

Example 2

Figure 4b shows the application of the pattern to macro rule r_priming (shown in Fig. 4a) of the hemodialysis machine case study.

Fig. 4.
figure 4

Hemodialysis case study – nested guards pattern

Full size image

5.2 Semantic Patterns

Any ASM model can be always represented using visual trees and possibly optimized by applying structural patterns. The resulting tree visualizes the structure of the ASM. However, sometimes it is possible to infer from the model also some hints on the behavior of the machine. For this reason, we introduce semantic patterns that can be applied when it is possible to infer from the model some information on the workflow of the machine.

We identify here three semantic patterns: mutual exclusive guards, state, and state flow patterns.

Mutual Exclusive Guards Pattern. In case of parallel conditional rules having mutual exclusive guards, it could be useful to represent that the workflow of the machine follows only one of the possible parallel execution paths.

The mutual exclusive guards pattern has been defined for this purpose. It is applicable when the rule guards check the current value of a given location that can assume disjoint values. This guarantees mutual exclusion among the guards of the conditional rules.

Fig. 5.
figure 5

Semantic pattern – mutual exclusive guards pattern

Full size image

Consider, for example, the ASM rule in Fig. 5a. It fires the parallel execution of three conditional rules guarded by the current value of the location x. Applying the visual tree in Table 1 to this rule, we obtain the representation given in Fig. 5b. However, one can understand that the three conditions on x are mutually exclusive and, therefore, visualize the rule in a more compact way as in Fig. 5c, showing that the machine workflow follows only one of the three possible pathsFootnote 3.

Example 3

The application of the mutual exclusive guards pattern to the main rule of Code 1 is shown in Fig. 6.

Fig. 6.
figure 6

Hemodialysis case study – mutual exclusive guards pattern

Full size image

State Pattern. Often, it could be desirable to represent the machine behavior as a flow of activities along a sequence of states of control, i.e., configurations (or modes) in which the machine can be. Therefore, we enrich our visual notation with a special node (an ellipse) representing information about the (control) state in which a given rule can be executed.

Suppose the model is as shown in Fig. 7a, where rule i is a macro call rule that might call (directly or indirectly) the update rule state := s j. Using only the visual trees defined in Table 1, the rule would be represented by the schema shown in Fig. 7b. However, supposing the modeler wants to use the function state to identify states of control, if rule i changes the state from s i to s j, one can build the graph as shown in Fig. 7c to explicitly represent the state change. In case rule i can bring to different states (e.g., states s j and s k), the pattern is as shown in Fig. 7d. Instead, if rule rule i leaves the mode unchanged, the pattern is as shown in Fig. 7e. Note that rule rule i will be represented as a macro call rule, if this is not already the case.

Fig. 7.
figure 7

Semantic pattern – state pattern

Full size image

Example 4

The application of the state pattern to the hemodialysis machine case study (see Code 1) is shown in Fig. 8.

Fig. 8.
figure 8

Hemodialysis case study – state pattern

Full size image

State Flow Pattern. The definition of the state pattern can be extended to graphically represent a flow of activities along a sequence of control states. Suppose to have the code reported in Fig. 9a and that rule i contains the update rule state := s j and rule j contains the update rule state := s k. By applying the state pattern explained above, one would obtain the visual graph in Fig. 9b. However, the evolution of the system from state s i to s j and then to s k can be made explicit, and the graph can be rewritten as in Fig. 9c. Note that if rule rule j does not update state, the flow ends with rule j. Instead, if rule rule j updates state to s i, the resulting structure is a graph as shown in Fig. 9d. Note that if the state flow pattern is applicable, also the mutual exclusive guards pattern is applicable.

Fig. 9.
figure 9

Semantic pattern – state flow pattern

Full size image

Example 5

The application of the state flow pattern to the hemodialysis machine case study (see Code 1) is shown in Fig. 10.

Fig. 10.
figure 10

Hemodialysis case study – state flow pattern

Full size image

6 Tool

We have developed a prototypical tool, called AsmetaVis, that permits to represent the visual trees and some of the visual patterns we have presented. At the current stage of development, the tool supports the first usage we devised in Sect. 3 for our visual notation, i.e., model visualization, that permits to obtain the graphical representation of a specification written in AsmetaL. The tool is currently able to visualize the ASM in two modes:

  • basic visualization in which the ASM is visualized using only the visual trees presented in Sect. 4; structural patterns (see Sect. 5.1) are not yet supported;

  • semantic visualization in which information on the workflow of the model is visualized using semantic patterns (see Sect. 5.2). Note that the tool automatically identifies the semantic patterns without any hint from the user. It first tries to apply the state and state flow patterns; if these are not applicable, it tries to apply the mutual exclusive pattern.

At the beginning, the tool loads the AsmetaL model and shows the graph of the main rule. A double-click on a macro call rule node causes the visualization of the corresponding macro rule graph; in this way, we provide the navigation links described in Sect. 3.

The tool is integrated in the ASMETA framework as eclipse pluginFootnote 4 and it uses Zest for implementing the visualization featuresFootnote 5.

Example 6

Figure 11 shows the basic and the semantic visualizations of the model of the hemodialysis machine case study in AsmetaVis (see Code 1). In both cases, the main window represents the main rule and the other smaller windows depict the called macro rules.

Fig. 11.
figure 11

AsmetaVis tool – hemodialysis case study

Full size image

7 Preliminary Evaluation

We conducted a preliminary experiment to evaluate whether the proposed visual notation can help in understanding a model. We interviewed 15 students who attended a course on formal system modeling and verification at the University of Milan (ten lectures on ASMs), and 11 who attended a course on principles of programming languages at the University of Bergamo (six lectures on ASMs). We took the (last refined) textual model of the hemodialysis case study [2], that consists of 163 macro rules and 1880 lines of code. We gave the textual model to half of the students and its graphical representation to the other half. Then we asked them a question in order to evaluate their understanding of the model (UQ: Which are the phases of the hemodialysis treatment and in which order are they executed?). We measured the time taken for answering the question. After this experiment, we gave them also the other representation (the textual one for those having the graphical one, and vice versa) and we asked them to identify the same elements in both representations. Then we asked them a question regarding their satisfaction about the notation they used at the beginning (SQ: Are you satisfied with the notation you used at the beginning?).

Table 2 shows the results of the experiment. By UQ, we observe that the graphical notation permits to understand the model semantics better in less time than the textual notation. Regarding the level of satisfaction (SQ), all the students who used the graphical notation were satisfied and they would not have preferred using the textual one. Instead, only 7.6% of those using the textual notation were satisfied and 92.4% of them said that they would have preferred using the graphical one.

Table 2. Experimental results
Full size table

8 Related Work

The need of having visualization techniques for easing the work of the modeler is felt in the formal methods community [8, 18, 25]. Different experiences show that the adoption of such visualization techniques makes the use of formal methods feasible also for non-experts [18], and also helps in teaching formal methods [17].

Several graphical notations based on a formal semantics have been defined for modeling system behavior. Examples are Statecharts [12] for modeling reactive systems, and SDL [11] mainly used in telecommunications.

Regarding the visualization of formal notations, some approaches (as in [7, 13]) focus on model visualization, while others (as in [15, 16]) provide a visual representation of the model execution (or model animation). In [13], graphical notations are used as an alternative representation of Z specifications, and a mechanical translation from Z models to diagrams is supported. They share with us the idea of using visualization in two ways. A similar approach is proposed for VDM in [7] where the authors propose two kinds of diagrams: Entry-Structure Diagrams modeling the system state, and Operation-State Diagrams modeling the behavior. ProB [15] allows automatic animation of B models, and can be used for error and deadlock checking, and test-case generation. B-Motion Studio [16] allows to create visualizations for B/Event-B models by using controls, which graphically represent some aspects of the model, and observers linking controls to the model state and invoking the animator ProB. ViBBA [9] was a tool for building an animator for ASMs. Although very powerful, the approach required a great effort in order to build the animator panel (by adding, from a palette, labels for controlled variables and input widgets, like buttons, for monitored variables) and to connect it to the model. We plan in the future to integrate the animation of behavior in AsmetaVis, but we would like to make the process of building animators as automatic as possible.

Our state flow pattern is a conservative generalization of the visualization for control state machines, which are an ASMs class with an intuitive (informally defined by examples in [5]) graphical representation in FSM-like diagrams. Our tool automatically provides a correct and precise visualization of those machines.

Other directions of model visualization concern the use of UML notation as modeling front-end, due also to the wide use of the UML in industry. For example, UML-B [23] uses the B notation as an action and constraint language for the UML, and defines the semantics of UML entities via a translation into B. Similarly, in [19], transforming rules are given from UML models to Object-Z constructs; therefore, the semantics of UML models is directly expressed in the formal language Object-Z. The tool OZRose has been developed to automate the transforming process. Furthermore, in [21], ArchiTRIO is defined as a formal language which complements UML 2.0 concepts with a logic-based notation to state system properties, both static and dynamic, including real-time constraints. In [22], a framework has been proposed for modeling and executing service-oriented applications. It uses the SCA (Service Component Architecture) notation to express the components architecture, and the ASMs to model services behavior, interactions, orchestration, compensation, and context-awareness. In [14], the method SPACE and its supporting tool Arctis are presented for the development of reactive services. In this method, services are composed of collaborative building blocks that encapsulate behavioral patterns expressed as UML 2.0 collaborations and activities.

Combined approaches have also been studied. In [20], for example, an integration of UML-B and Object-Z has been proposed to define a software development process where UML-B is used as visual modeling notation at early conceptual modeling stage, and Object-Z later when requirements are better understood.

9 Conclusions

With this work we have tried to satisfy a request, felt from long time, to have a way, and a supporting tool, to graphically represent ASM models, from a structural and from a behavioral point of view. We have proposed a graphical notation for ASMs, and we have defined visual patterns that capture, in a concise way, different recurring ASM rule patterns. The representation concerns only the transition rules and not the signature of the model.

As future work, we plan to define visual trees for all the turbo rules, and identify new visual patterns. Regarding the tool, we plan to implement the second usage we devised in Sect. 3 for our visual notation, i.e., the visual editing that should allow a modeler to graphically specify the ASM using the visual components (visual trees and visual patterns) we have proposed. Finally, we plan to better evaluate the possible advantages of using the proposed visual notation by means of a controlled experiment.