Introduction

The DARPA-supported Intent-Defined Adaptive Software (IDAS) program [1] sought to develop technologies that enable rapid adaptation of software to changes in requirements and operating environments. The main objective of this program was to develop methods for the management of requirement changes in software development. The step in the change management process that is addressed in this paper is the identification of inconsistencies in requirements. Building an ontology as a common understanding of the structure of information between stakeholders is a widely used approach in software engineering for software requirements change management [2, 3]. It allows the reuse of domain knowledge, and making explicit domain assumptions that will allow assumptions to be changed easily when the domain knowledge is changed. In the work described in this paper, we focus on the verification of the satisfaction of changes in the requirements during software development. Our approach relies on the use of ontology for this purpose.

There are two main advantages of using ontology in software engineering. First, ontologies provide common vocabularies of given domains that can be shared among software developers working on different aspects of software applications. Second, once the model of the software and the user requirements are represented as an ontology in OWL [4], requirement satisfaction can be verified automatically using an inference engine. One of the advantages of using OWL is that OWL inference is decidable.

In this paper, we focus on the latter issue. However, instead of proving that user requirements are satisfied, we will show some “reasonable assurances” to the developer that the model is correct, reserving full verification of requirement satisfaction to future work. This paper is an extension of the work originally presented in MODELSWARD 2022 [5]. We will provide a more complete picture of the map** from SysML/OCL models to OWL DL, and will show more detailed explanations for the OWL reasoning results.

Problem Statement

The Unified Modeling Language (UML) is a widely used industry standard language that provides graphical notation for software specification and design in the early phases of software development. The SysML is an extension of a subset of the UML. However, UML/SysML models alone are not expressive enough to represent constraints on the modeling concepts. The OCL is used to express constraints in UML/SysML models. Many UML/SysML tools support adding OCL constraints in UML class diagrams and SysML block diagrams. However, none of the tools supports the semantics checking of the constraints. Because UML/SysML are not formal languages (they have formal syntax but lack formal, computer-processable semantics), we cannot perform theorem proving in UML/SysML to verify the consistency of a model. In other words, the UML/SysML tools do not check if the model is correct according to these constraints.

To support software developers with automated reasoning capabilities when develo** models of software, we develop an ontology-based method to reason about the correctness of SysML models that include OCL constraints. Specifically, we map SysML block diagrams, state machine diagrams, and OCL constraints to OWL, and check the consistency of the corresponding ontology by running an OWL inference engine. Although significant amount of research on map** UML/SysML models to ontologies has been reported (e.g., [6,7,8,9]), almost all of the researchers limit their scope of investigation to class diagrams. There is a lack of widely accepted map** rules for the map** of UML/SysML behavior diagrams to OWL and thus more research in this area is needed.

In this paper, we propose a set of map** rules to interpret the components of SysML state machine diagrams, along with OCL constraints, to OWL DL. The novelty of our approach is the identification and implementation of a more complete map** of UML/SysML to OWL, than what is included with current CASE tools. There are a few papers on the map** of the UML/SysML behavior diagrams to OWL DL, however, they either use a non-OCL logic, a restricted set of OCL operators and/or do not support formal proof. Our map** rules have two advantages: (1) they show how to translate both basic state machine elements (including states, transitions, events, actions, guards, and triggers) and OCL constraints in the state machine diagrams (including the OCL invariants in states and guards) to OWL, and (2) the OCL to OWL translation rules cover relational operators (e.g equivalent, greater/less than) between variables.

The existing research on consistency checking of UML state machine diagrams primarily focuses on the detection of contradictions between: (1) the UML metamodel and state machine specifications, and (2) state machine diagrams and other types of diagrams. Verification that state machine diagrams are not contradictory with the requirements expressed as OCL constraints is also a very important issue in software development. In this paper, we check for contradictions within models that include OCL constraints on state machine diagrams. We demonstrate this capability on three exemplary inference tasks.

The rest of this paper is organized as follows. In “Related work”, we review some of the existing literature that is related to our work. In “OWL reasoning about SysML block diagrams”, we show the OWL axiom usage in reasoning about SysML block diagrams. In “State machine diagram to OWL map** rules”, we propose a set of map** rules to interpret the components of state machine diagrams along with OCL constraints to OWL DL, and demonstrate three reasoning tasks using the OWL reasoner Pellet. Finally, “Conclusions” summarizes our work.

Related Work

Consistency checking of UML/SysML models is an important step in MBSE-based system development. The definitions of types of consistency are still an open research topic, c.f., [10,11,12]. One of the UML consistency classifications is horizontal vs. vertical consistency. Horizontal consistency, also called intra-model consistency, means the lack of contradictions between different diagrams at the same level of abstraction. Vertical consistency, also called inter-model consistency, means the lack of contradictions between different diagrams at different levels of abstraction. Another basic classification of consistency in UML is syntactic vs. semantic consistency. Syntactic consistency refers to the relation between UML diagram specifications and a UML metamodel, whether the syntax of a given diagram is compatible with the syntax prescribed by the metamodel. Semantic consistency refers to the meaning of UML diagrams, i.e., to the notion of truth - whether any contradictions in the model do not exist and whether a concept can be instantiated. Other methods of consistency classification were also discussed in the literature, e.g., static versus dynamic consistency, multi-level consistency, and the nature of errors.

In this paper, we focus on the consistency of UML models that include requirements expressed in OCL. Since the OCL constraints capture the semantics of the domain, our approach falls in the semantic validation category.

Consistency Checking via Map** to Formal Languages

Many approaches rely on the map** of UML/SysML models to a formal languages and the use of automatic proof engines for reasoning on these models. We looked at these methods with respect to the support of automatic proof, model analysis, structural and behavioral modeling, and checking for consistency of models that map requirements expressed as OCL constraints. While many recent papers propose map** of UML to OWL, most of the papers seem to ignore the fact that UML and OWL have different semantics. This issue was first discussed in [13], where the authors identified similarities and differences between UML and DAML (DARPA Agent Markup Language). To close the gap between the two representations, the authors proposed extending UML by adding two metamodel elements called Property and Restriction, where a property is a grou** of association ends and a restriction is a classifier for objects. The recommendation from the [13] paper has not materialized primarily due to the fact that UML has not been modified as suggested in the paper. Moreover, DAML became OWL.

UML2Alloy [14, 15] maps UML/OCL models to Alloy notations, and then the Alloy model is automatically analysed by the Alloy Analyzer. Alloy is an object modeling language based on first-order logic (FOL), offering declaration syntax compatible with graphical object-oriented models, and state-based formulas. However, Alloy models do not provide semantic notations which are necessary during the analysis phase of software development [16].

USE [17, 18] includes an interpreter for a subset of UML and OCL. It provides its own UML/OCL user interface and lets one check constraints (invariants and pre- and post-conditions). That is, it checks model states (snapshots) making sure invariants are not contradictory. However, this is not a formal system and it uses a custom UI that does not support XMI import/export.

Rehman et al. [19, 20] modeled a smart parking system and a sewage system using UML activity diagrams, translating them to automata-based models, and then to temporal logic of actions. A (TLA)-based formal method was utilized to validate and verify system properties using the TLA+ toolbox [21]. The toolbox includes a proof system and a high level language to generate TLA code. TLA+ is a good tool for verifying code simulating state machines, but it is not clear how it could be used for model analysis, which was our objective.

Automated Reasoning on UML/OCL conceptual Schemas (AuRUS) [22] is a standalone application which allows verifying and validating UML/OCL conceptual schemas specified in ArgoUML. Verification consists in determining whether the schema satisfies a set of well-known desirable properties such as class liveliness or non-redundancy of integrity constraints. Validation consists of allowing the user to perform queries about reachable states of the schema. However, AuRUS only validates the structural part of a schema. Validation of the behavioral part of a schema is not supported.

There are many other methods surveyed in [10, 12] that are based on a formal language. In particular, the authors considered map** UML models to DL. None of the methods reviewed in that paper check the consistency of the OCL constraints. Some researchers pursue verification of consistency, e.g., [23, 24], but not of UML/SysML models.

Ontology-Based Consistency Checking

In [25], the authors investigate the method, called TwoUse, to integrate a UML model and an OWL ontology. Since OWL classes cannot be exploited through OCL expressions, the authors propose an extension to the OCL basic library, called OCL-DL, to permit operations to call the OWL reasoner. In OCL-DL, the authors propose new operations which rely on reasoning engine services to extend the boundaries of OCL toward OWL. However, their method only focuses on UML class diagrams.

In [26], the authors represent class diagram operations using three ways: (1) FOL n-ary predicate that has to satisfy some FOL assertions. These are assertions that type the input parameters and the return value, and ensure the uniqueness of the return value; (2) DLR-ifd (variation of DL) operation is represented as an n-ary relation. The same assertions as in the previous case are used; (3) ALCQI (variation of DL) approach is based on reification. An operation is expressed as an atomic concept -the ALCQI role. There are also assertions that type the input parameters and the return value. There is no consideration of names of operation parameters.

The approach that we are using in this paper is in line with [26].

Map** Behavior Models to OWL DL

The method in [9] translates UML state machines and OCL constraints to DLR—an expressive description logic (DL) that supports n-ary relations. The basic idea is that the states and transitions in a state diagram are mapped to primitive concepts in DL. We have not found tool support for the translation. Also, the translation of OCL to OWL does not allow relational operators between variables.

In [7], the authors describe a transformation of UML statechart primitives to OWL DL. In their transformation, a specific state is defined by a class expression constrained by transitions and state conditions. A specific transition is defined by an intersecting class expression standing for the source, target, event and guard of this transition. However, this work does not support translation of OCL constraints.

In [27, 28], the authors translate both the UML class and statechart diagrams of a model to a single ontology, and analyze the consistency and satisfiability of the model using OWL reasoners. However, the authors do not provide any translation of transitions in the statechart diagram. Moreover, translation of OCL to OWL does not allow relational operators between variables.

The method in [6] represents the state machine using OWL individuals. It is difficult to extend this method for OCL support, since the map** of OCL to OWL that we use is class based.

The detailed comparison of these map** rules is shown in Table 4.

OWL Reasoning about SysML Block Diagrams

Ontology Foundations

Ontology is a field of philosophy dealing with the nature of “being”. In computer science, the same term has a somewhat different meaning: an ontology is an explicit, formal specification of a shared conceptualization [29]. To represent ontologies in computer science, the five basic constructs are used to capture knowledge about a specific domain: classes, properties, instances, constraints, and axioms.

  • Classes: also called concepts or types, represent groups of things that share common characteristics. They could be either concrete objects of the real world or abstract concepts.

  • Properties: are used to express relationships between two classes in a given domain. They are the ways in which classes and instances can be related to one another.

  • Instances: are also known as individuals and are the things that the ontology describes or potentially could describe.

  • Constraints: determine which values are allowed for properties or what relations should hold for specific classes of individuals.

  • Axioms: classes, properties, and constraints can be put together to form logical statements or assertions. Axioms are formally stated descriptions of what must be true in order for some assertions to be accepted.

OWL is a family of standardized ontology languages with formal semantics that is used to formalize ontologies. To facilitate the representation of ontologies, many visualization tools have been developed. Prot\(\acute{e}\)g\(\acute{e}\) [30] is a popular open-source ontology editor and knowledge base framework. In this project, we used Prot\(\acute{e}\)g\(\acute{e}\) to develop our ontologies.

Map** of SysML Block Diagram to OWL

The Cameo Enterprise Architecture tool is widely used by software engineering teams for modeling systems. The usage of this tool follows the Model-Based Software Engineering process. It includes many useful features; in particular, it is useful for the identification of potential design flaws early in the development stage, when they are easier to fix rather than fixing them in later stages. However, the capabilities of Cameo Enterprise Architecture are limited in detecting semantic inconsistencies in SysML/OCL models. For instance, when we “validate” a model known to be inconsistent, Cameo Enterprise Architecture shows “validation was successful”. The reason for this is that Cameo Enterprise Architecture validation function is limited to checking the syntax of OCL constraints, but not their semantics. In our experiments, we used Cameo Concept Modeler plugin [31] for Cameo Enterprise Architecture to translate SysML block diagrams to OWL. Then we used rules to translate OCL contraints to OWL.

The map** from UML class diagrams to OWL and DL has been studied by many papers, as described in “Related work”. We summarize the widely accepted rules described in these papers in Table 1. The first column shows UML concepts, the second shows to what it is mapped in DL and the third shows a corresponding concept in OWL.

Table 1 The map** of UML components to OWL components
Full size table

The OCL is used to express constraints on UML/SysML models, for example, the restrictions on the value of object attributes, and the restrictions on the existence of objects. In this paper, we only consider a subset of OCL constraints, the OCL invariants. The OCL invariant is associated with a Classifier (also referred to as a “type”) in UML/SysML models. An OCL expression that is an invariant evaluates to be true if the condition is met. All invariants of a type must be true for all instances of that type at any time. Therefore, OCL invariants can help us to check for design contradictions of UML/SysML models. OCL invariants were manually translated into OWL 2 DL axioms based on [25] and [32]. Specifically, for a block diagram, the OCL invariants of a block are translated into OWL object property restrictions. In addition, our translation introduces relational operators between variables. Table 2 shows the map** principles that we follow in this paper. Here, \(C_1\), \(C_2\), C are SysML blocks, p is either a block value or an association end, and V is a SysML value type. In the case that V is an instance of the SysML value type, the map** of the third invariant in Table 2 should be \(C \sqsubseteq \exists p.\{V\}\), and the map** of the fourth invariant in Table 2 should be \(C \sqsubseteq \lnot \exists p.\{V\}\).

Table 2 Principles of map** of OCL to OWL
Full size table

The Use of OWL Axioms for Consistency Checking

The reason for map** SysML models and OCL constraints to OWL is to support the software developers with automatic consistency checking by using OWL reasoners. Inconsistencies of the OWL axioms indicate that there are errors in the models. We could invoke OWL reasoners to show expectations when the ontology mapped from SysML/OCL models is inconsistent. OWL DL provides three types of class axioms to construct a class description—SubclassOf, EquivalentClasses, DisjointClasses—that can be used for checking consistency.

Generalization associations between two blocks are translated into SubclassOf axioms of the corresponding OWL classes. Moreover, OCL invariants of a block are translated into SubclassOf axioms of the corresponding OWL class. In DL, we represent this as \(C_1 \sqsubseteq C_2\). When such a subclass axiom is part of an OWL model, for any individual x of \(C_1\), the fact (x rdf:type \(C_2\)) is inferred by an OWL reasoner. If the class description of \(C_1\) has conflicts with the class description of \(C_2\), the OWL reasoner will detect this as an inconsistency.

Generalizations with the “Equivalient Class” stereotype in SysML are translated into EquivalentClasses axioms of the corresponding OWL classes. In DL, we represent this as \(C_1 \equiv C_2\). If the class description of \(C_1\) has conflicts with the class description of \(C_2\) (i.e., the sets of the individuals from these two classes do not fully overlap), the OWL reasoner will detect this as an inconsistency.

Dependencies with the “Disjoint With” stereotype in SysML are translated into DisjointClasses axioms of the corresponding OWL classes. In DL, we represent this as \(C_1 \equiv \lnot C_2\). In such a case, if the class description of \(C_1\) has any overlap with the class description of \(C_2\), the OWL reasoner will detect this as an inconsistency.

An Example

Here, we consider an example based on the cloud agility baseline (CAB) model [1] that SNC and Northeastern developed to provide an adaptable framework which can be molded to meet typical logistics and cloud applications and changes to those requirements. This CAB model provided the flexibility for the various exercises to promote reuse of microservice components. For a logistics example, it might be hosted (initially) in AWS and provide a web-based interface for routing military supplies given a certain workflow and certain geopolitical realities. Figure 1 shows the SysML block diagram of the CAB model. A shipment requests the dispatcher to schedule an assignment for it. An assignment is a shipment–transporter pair to transit and deliver a shipment. Shipments have three possible states: pending, in transit, or delivered, and transporters have two possible states: busy or idle. The question we are investigating in this paper is - how do we verify the correctness of changes in the CAB model, e.g., are the state machines of the CAB correct?

Fig. 1
figure 1

SysML block diagram of the CAB model [5]

Full size image

Cameo can translate the five blocks in the CAB SysML model and the associations between them to the classes and properties in the CAB ontology. Figure 2 shows the main structure of the CAB ontology in Prot\(\acute{e}\)g\(\acute{e}\). However, the Cameo map**-to-OWL capability is very limited and the automatic translation loses some information in translation.

Fig. 2
figure 2

Main structure of the CAB ontology [5]

Full size image

We extended the automatically generated CAB ontology by map** the OCL constraints in the Dispatcher block and the Shipment block into OWL restrictions for the corresponding classes manually (shown in Figs. 3 and 4 ). In this step, we followed the map** rules shown in Table 3. Finally, we ran Pellet, the OWL reasoner embedded in Prot\(\acute{e}\)g\(\acute{e}\). It identified the semantic inconsistency of the model (shown in Fig. 4): the Shipment block is equivalent to Nothing, i.e., the OWL class is not satisfiable (it cannot have any individuals).

Table 3 Map** of OCL invariants in CAB SysML model to OWL
Full size table
Fig. 3
figure 3

OWL restrictions for the Dispatcher class map** from OCL

Full size image
Fig. 4
figure 4

OWL restrictions for the Shipment class and the OWL reasoning results

Full size image

State Machine Diagram to OWL Map** Rules

The main concepts of state machines are state, transition, event, guard and action. These concepts are mapped to OWL following the rules shown in Table 4. A simple state is mapped to a class expression in OWL. The classes are constrained by transitions and state invariants expressed in OCL. All the state classes are disjoint. In OWL, each transition of a state machine diagram is represented by an intersection of class expressions for the source state, target state, event and guard of this transition. In addition, our translation introduces relational operators between variables.

Table 4 SysML state machine diagram to OWL map** rules comparison [5]
Full size table

A Map** Example

The statechart diagram in Fig. 5 describes the behavior of the Dispatcher block from Fig. 1. Each state in the statechart diagram is annotated with a state invariant.

Fig. 5
figure 5

Dispatcher Statechart [5]

Full size image

The six states are mapped to six OWL classes. The Allocating state is a composite state with three sub-states; it has a state invariant expressed as an OCL constraint (top right corner of the diagram). The OWL DL representation of the constraints on the states is shown in the following DL expressions.

$$\begin{aligned}&Allocating \equiv Waiting \sqcup GettingTransporters \sqcup MakingAssignment \end{aligned}$$
(1)
$$\begin{aligned}&Allocating \sqsubseteq \exists isRequestedBy.Shipment \end{aligned}$$
(2)
$$\begin{aligned}&Complete \sqsubseteq \forall isRequestedBy.1Shipment \end{aligned}$$
(3)
$$\begin{aligned}&Waiting \sqsubseteq \forall hasAssignment.0Assignment \end{aligned}$$
(4)
$$\begin{aligned}&\begin{aligned}&GettingTransporters \sqsubseteq \exists hasAssignment.(Assignment \\&\sqcap \ge hasTransporter.1Transporter) \end{aligned} \end{aligned}$$
(5)
$$\begin{aligned}&\begin{aligned}&MakingAssignment \sqsubseteq \exists hasAssignment.(Assignment \\&\sqcap \forall hasShipment.1Shipment \sqcap \forall hasTransporter.1Transporter) \end{aligned} \end{aligned}$$
(6)

The six transitions are also mapped to six OWL classes. The transition from Waiting to GettingTransporters is triggered by the event shipRequest. So the transition class WaitingToGettingTrans is defined as:

$$\begin{aligned}&\begin{aligned} WaitingToGettingTrans \equiv \exists fsm.triggeredBy.\{shipRequest\} \end{aligned} \end{aligned}$$
(7)
$$\begin{aligned}&\begin{aligned} WaitingToGettingTrans \sqsubseteq&\exists fsm.hasSource.Waiting \\&\sqcap \exists fsm.hasTarget.GettingTransporters \end{aligned} \end{aligned}$$
(8)

GettingTransporters state has two outgoing transitions. After the operation chooseTransporter of the dispatcher is invoked, if the returned transporter state is busy, the state stays at GettingTransporters. Otherwise, the state transits to MakingAssignment. So the two transition classes are defined as:

$$\begin{aligned}&\begin{aligned} GettingTrans \equiv&\exists fsm.triggeredBy.{chooseTransporter} \\&\sqcap \exists (fsm.hasGuard.fsm.EvalCmp.EQ \\&\sqcap \exists fsm.hasLeftExpr.\{transporterState\}\\&\sqcap \exists fsm.hasRightExpr.\{busy\}) \end{aligned} \end{aligned}$$
(9)
$$\begin{aligned}&\begin{aligned} GettingTrans \sqsubseteq&\exists fsm.hasSource.GettingTransporters \\&\sqcap \exists fsm.hasTarget.GettingTransporters \end{aligned} \end{aligned}$$
(10)
$$\begin{aligned}&\begin{aligned}&GettingTransToMakingAssignment \\&\quad \quad \quad \equiv \exists fsm.triggeredBy.{chooseTransporter} \\&\quad \quad \quad \sqcap \exists (fsm.hasGuard.fsm.EvalCmp.EQ \\&\quad \quad \quad \sqcap \exists fsm.hasLeftExpr.\{transporterState\}\\&\quad \quad \quad \sqcap \exists fsm.hasRightExpr.\{busy\}) \end{aligned} \end{aligned}$$
(11)
$$\begin{aligned}&\begin{aligned}&GettingTransToMakingAssignment \\&\quad \quad \quad \sqsubseteq \exists fsm.hasSource.GettingTransporters \\&\quad \quad \quad \sqcap \exists fsm.hasTarget.MakingAssignment \end{aligned} \end{aligned}$$
(12)

From the state MakingAssignment, after the dispatcher invokes the operation assignShipment, if the deliverShipment is true, then the state of the dispatcher goes back to Waiting.

$$\begin{aligned}&\begin{aligned} MakingAssignmentToWaiting&\equiv \exists fsm.triggeredBy.{assignShipment} \\&\sqcap \exists (fsm.hasGuard.fsm.EvalCmp.EQ \\&\sqcap \exists fsm.hasLeftExpr.\{deliverShipment\}\\&\sqcap \exists fsm.hasRightExpr.\{true\}) \end{aligned} \end{aligned}$$
(13)
$$\begin{aligned}&\begin{aligned} MakingAssignmentToWaiting&\sqsubseteq \exists fsm.hasSource.MakingAssignment \\&\sqcap \exists fsm.hasTarget.Waiting \end{aligned} \end{aligned}$$
(14)

OWL Reasoning with State Machine Diagrams

We check the consistency of OCL constraints in a state machine to check the consistency between the state machine and the requirements expressed as OCL constraints. For this purpose, we translate the state machine along with the OCL constraints to OWL (as shown in “A map** example”) and run the reasoner to detect inconsistency in the ontology. To show different types of inconsistencies of constraints, we developed three reasoning tasks.

The first OWL reasoning task is to check if the OCL invariants of all the states are consistent. The state invariants that may cause the object violate the constraints imposed on the state diagrams in the UML superstructure specification of state machine are considered to be inconsistent invariants. For example, for the composite state Allocating, the OCL constraint of the state invariant is:

$$\begin{aligned} isRequestedBy -> size() > 0, \end{aligned}$$
(15)

which means the dispatcher is in Allocating state if it is requested by at least one shipment (Fig. 6). The Waiting state is a substate of Allocating. The substate should not have a conflicting invariant with the composite state. Adding the following invariant to the Waiting state:

$$\begin{aligned} isRequestedBy -> size() = 0 \end{aligned}$$
(16)

would imply being in the Waiting state even if there was no request by any shipment (Fig. 7). Thus, such two OCL constraints are inconsistent, and thus there cannot be a state individual that can satisfy both the constraints of Allocating and the constraints of the Waiting states.

Fig. 6
figure 6

OWL restrictions for Allocating state

Full size image
Fig. 7
figure 7

OWL restrictions for Waiting state

Full size image

When we run the Pellet in Prot\(\acute{e}\)g\(\acute{e}\), it will identify the semantic inconsistency of the OWL axioms in Allocating class and Waiting class. The inconsistency explanations are shown in Fig. 8.

Fig. 8
figure 8

Inconsistency explanations of the first reasoning task

Full size image

The second OWL reasoning task is to check whether only one transition can be taken out of a state, i.e., whether the state machine is deterministic. For a state with more than one possible outgoing transition, e.g., GettingTransporters, the state that has two outgoing transitions GettingTrans and GettingTransToMakingAssignment, adding the guard:

$$\begin{aligned} assigns.transporterState = busy \end{aligned}$$
(17)

to both transitions would make the choice of a transition not unique. In OWL, two outgoing transitions are represented by two disjoint transition classes and should have disjoint guards. Otherwise, the Pellet will identify semantic inconsistency because an individual cannot belong to both a type and its complement. The inconsistent result is shown in red in Figs. 9 and 10 , and the reasoner explanations of inconsistency are shown in Fig. 11.

Fig. 9
figure 9

OWL reasoning result in GettingTransToMakingAssignment transition

Full size image
Fig. 10
figure 10

OWL reasoning result in GettingTrans transition

Full size image
Fig. 11
figure 11

Inconsistency explanation of the second reasoning task

Full size image

The third OWL reasoning task is to check if the state machine contains deadlocks. A deadlock can happen when two or more processes have conflicting resource needs. In this paper, we consider a simple deadlock case: for a state with only one outgoing transition, the guards on this outgoing transition of a state are mutually exclusive. In other words, if the guards on the only outgoing transition of a state cannot be satisfied at the same time, the state machine for the object will be stuck in this state. For example, for the transition from MakingAssignment to Waiting, if we add the guards as follows:

$$\begin{aligned} &assigns.deliverShipment = true, \nonumber\\ & assigns.deliverShipment = false. \end{aligned}$$
(18)

Once the state machine of the dispatcher object gets into MakingAssignment, it will not be able to get out of this state because the deliverShipment attribute cannot be both true and false at the same time. When we run the Pellet, it will identify the semantic inconsistency of the OWL axioms in the MakingAssignmentToWaiting class that represents the transition, as shown in red in Fig. 12. The reasoner explanations of inconsistency are shown in Fig. 13.

Fig. 12
figure 12

OWL reasoning result in MakingAssignmentToWaiting transition

Full size image
Fig. 13
figure 13

Inconsistency explanations of the third reasoning task

Full size image

Conclusions

In this paper, we propose an ontology-based method to reason about the correctness of SysML models that include OCL constraints. Specifically, we map the SysML models with OCL constraints to OWL and check the consistency of the corresponding ontology by running an OWL inference engine. Although a number of map** rules from UML class diagrams to OWL have been reported in the subject literature and accepted by the community, still, there is a lack of widely accepted map** rules from UML behavior diagrams to OWL. In this paper, we propose a set of rules for map** components of SysML state machine diagrams along with OCL constraints to OWL DL. We also demonstrate three examples of reasoning tasks in which OWL axioms are used for consistency checking of state machine diagrams. We recognize that our current approach is a combination of automated and manual steps, in part due to the limitations of the built-in concept modeler. In the future, we plan to develop fully automatic procedures for map** SysML/OCL models to OWL DL.

Our work is aimed at providing the software developer with some reasonable assurances about the correctness of the model in the system modeling stage of software development. This is the first step of requirement change management. In the future, we plan to extend the scope of our approach to a more complete and automatic verification of SysML state machine specifications with OCL constraints as well as both theoretical analysis and experimental validation of the correctness of the map** rules.