iStar Goal Model to Z Formal Model Translation and Model Checking of CBTC Moving Block Interlocking System

To ensure that the developed complex software system meets its desired goal and precisely works as stakeholders expect, the analyst must accurately understand, describe, interpret, and purify stakeholders’ requirements. Initially, these requirements are inadequate, inconsistent, ambiguous, incomplete, and informal. Later, these requirements are translated into a concrete software system. This translation requires a clear understanding of why a software system is needed, its functional requirements to carry out its goal, and the restrictions on designing and implementing a software system. This entire process is known as Requirements Engineering [38].

Discovering and analyzing non-functional and functional requirements is not an easy task. Many of the published surveys [13, 16] showed that improper identification and analysis of requirements is the reason behind the failure of complex software systems. Many cases of informal deficient requirements assessment are shown on the website Forum on Risks to the Public in Computers and Related Systems [28]. On average, 40% of the software systems do not meet their desired requirements because of improper requirements analysis [13, 31]. Requirements faults are costly to repair at later stages. According to the NASA article “Error Cost Escalation through the Project Life Cycle” [17], a requirements fault costs more than 8 times to repair during design, more than 16 times after coding, more than 21 times after testing, and more than 29 times after deployment. In 1976, Bell and Thayer did an experiential study on requirements engineering. In this study, they stated that if our identified and analyzed requirements are incomplete, inadequate, ambiguous, or inconsistent, then it significantly affects the quality of the resultant system. Finally, they confessed that “the requirements for a system do not arise naturally; instead, they need to be engineered and have continuing review and revision” [3].

Traditional requirements analysis approaches like SADT, SART, IDEF0, MERISE, SSADM, and UML focus on the WHAT dimension of requirements engineering: what are the functional services essential to satisfying the system’s goal? In these approaches, domain knowledge is learned by communicating with stakeholders and producing specification documents. Later, this document is modeled to have a conceptual schema and confirmed against requirements. These approaches are inadequate because they make system descriptions from a single perspective. Also, do not supply reasoning among multiple alternatives and do not handle requirements conflicts. These approaches are suitable when requirements are steady and remain unchanged. In today’s environment, due to the increasing complexity of systems and advancement in technology, user requirements will vary day by day. Therefore, these approaches are unsuitable for developing complex software systems [48]. In the early 1990s, the Goal-Oriented Requirement Engineering (GORE) method was introduced to address these issues. It ensures that the software system meets its desired goals and prevents using traditional methods for requirements analysis [1, 36].

The GORE method is concerned with eliciting practical goals that encourage the development of a complex software system. The GORE method focuses on all three dimensions of requirements engineering. The WHY dimension finds the system’s goals by obtaining domain knowledge, supplying reasoning among multiple alternatives, handling requirements conflicts, and producing system descriptions from various perspectives. The WHAT dimension finds functional services and constraints needed to satisfy the goals found using the WHY dimension. The WHO dimension assigns the responsibilities for achieving the goals found using the WHY dimension to different stakeholders [1, 36, 37, 38]. In GORE methods, the main problem is structuring specifications. A goal-oriented model-based approach solves the problem of structuring specifications and supplies an abstract description of the target system. It integrates multiple views of the target system to cover all three dimensions of requirements engineering [36, 38].

The goal-oriented model-based methods introduced a clear distinction between early-phase and late-phase requirements. Early-phase requirements focus on the WHY dimension of requirements engineering. That is, they focus on modeling and analysis of the environment of the software system. Also, they illustrate how stakeholders’ needs, motivations, and complex relationships may be addressed by multiple alternatives. Usually, early-phase requirements are non-functional requirements. Non-functional means not only quality requirements. It is also concerned with why functional requirements are essential and how they provide the functional services of the system. The analyst represents early-phase requirements using a semi-formal model. Late-phase requirements focus on the WHAT dimension of requirements engineering. That is, they focus on modeling the software system with its environment. They also discover functional services and constraints essential to satisfy the goals. Usually, late-phase requirements are functional requirements. They focus on adequate, complete, consistent, unambiguous, and automated verification of functional requirements. Hence, a formal model represents these requirements. The paper by Yu [45] clearly distinguished between early-phase and late-phase requirements. It highlighted the importance of the WHY dimension of requirements engineering using the i* framework.

KAOS, AGORA, Albert II, GBRAM, NFR, and iStar goal-oriented model-based frameworks were proposed to address requirements engineering issues. Each has a different requirements analysis technique. The KAOS, AGORA, Albert II, and GBRAM frameworks focus on semi-formal and formal analysis of late-phase requirements. Several articles have witnessed it [6, 10, 14, 21, 30, 33, 40]. All these articles focus only on what a system does and how the system’s behaviors are satisfied. However, they do not address why the system requirements are needed. NFR and iStar emphasize analyzing early-phase requirements and addressing all three dimensions of requirements engineering. Analysis of early-phase requirements is essential to understand the domain, system complexity, multiple technical alternatives, business process, and strategic knowledge, as well as how the system cooperates, changes in organizational requirements, and end-user needs. The iStar framework uses NFR notations to express the rationales behind the actors and represents the system’s operational environment.

This article’s primary objectives are to provide a goal-oriented model of a complex system, translate it into a formal model, and verify the requirements specified at the early stage. To achieve these objectives, we researched several articles for choosing semi-formal and formal modeling languages. Several success stories and survey articles [11, 12, 18, 20, 42] witness the successful application of the B formal method in railway systems. For example, the “SACEM system of RER Line A in Paris” was designed using more than 100k lines of B specification code. Hence, we can use the B formal model. However, a translation of a semi-formal model into the B formal model is not an easy task. Several articles [23, 24, 33] witness mapping the UML semi-formal model notations to the B formal model. However, the UML is an object-oriented model, and this mapping only focused on functional requirements. In all the above articles, the authors’ main intention is to verify functional specifications, so they focused only on the WHAT dimension of requirements engineering. However, they did not focus on the WHY dimension of requirements engineering. They expressed late-phase requirements by a semi-formal model and later formalized them with formal specification language. Therefore, we use the iStar model in this article because it emphasizes the WHY dimension of requirements engineering.

In this article, as a case study, we use the Communication-Based Train Control (CBTC) moving block interlocking system to illustrate the synergy of the iStar and Z combination on complex software systems. We extracted functional and non-functional requirements from the IEEE 1474.1 CBTC specification document [19] and the safety-critical systems handbook [32] to develop the iStar model of the CBTC moving block interlocking system. The iStar model to Z formal model translation helps us to analyze the early-phase requirements of the CBTC moving block interlocking system. It also addresses the variability and vulnerability issues. This model translation is a one-to-one mapping of iStar model elements to the Z-schema. This mapping does not result in any data loss or changes in the meaning of iStar elements. We refine Z-schema by invariant statements and goal fulfillment criteria to formalize late-phase requirements and address vulnerability issues. Finally, we apply the ProZ model checking tool to verify the requirements specified early along with LTL safety properties.

We organize the remaining part of the article as follows: Section 2 discusses the background concepts. Section 3 encompasses the iStar model of the CBTC moving block interlocking system. Section 4 describes integrating early-phase requirements with late-phase requirements. Section 5 describes our developed formal model using the ProZ model checker. Section 6 examines several related works. In the last section, we conclude our article.

Here, we review basic concepts about iStar, Z Formal Specification, ProZ model checker, and CBTC.

Here we present the iStar model of the CBTC moving block interlocking system. In the iStar SD model, we identified all the actors around the CBTC moving block interlocking system and described their relationship with other actors. In the iStar SR model, we described each actor’s interests and concerns and how to fulfill them. piStar [29] is an online analysis and graphical editor tool for iStar models. It enables us to create high-quality goal models. Using this tool, we designed the iStar goal model of the CBTC moving block interlocking system.

As we know, iStar is well suited for analysis of early requirements, and the Z formal method is well suited for analysis of late requirements. Nowadays, to solve complex system problems, it is necessary to integrate these two different methods. This integration synergistically resolves the requirements problem. We formalize the iStar goal model into the Z formal model first and then discuss the translated Z formal model.

All iStar elements, such as actors and their intentional elements, have unique names. We use the fundamental set type ‘NAME’ to describe them in the Z notation. As a result, the names of all actors, all actors’ intentional elements, and all dependencies are included in the subsets ‘allActorNames’, ‘allElementsNames’, and ‘allDependumNames’, respectively. Figure 5 illustrates these mappings.

The Z-free type definition ‘Type’ is applied to specify the different intentional elements of the iStar. The Z-free type definition ‘State’ specifies the states of the intentional elements both prior to and after realization. The state ‘Created’ is held after the creation of an intentional element but before realization. If realization is successful, the state ‘Fulfilled’ is maintained; if realization is unsuccessful, the state ‘NotFulfilled’ is maintained. We use the states ‘Fulfilled’, ‘NotFulfilled’, and ‘Undetermined’ for the softgoal (quality) element. If a softgoal’s realization is unclear, it is said to be an ‘Undetermined’ state. To uniquely identify each intentional element defined inside the boundary of an actor, in Z we defined a state variable ‘elementType’, which is a total function between sets ‘Name’ and ‘Type’. Similar to this, state variables ‘dependumType’, ‘dependerElement’, and ‘dependeeElement’ are used to specify the type of dependency, the depender intentional element, and the dependee intentional element, respectively. The iStar rule states that the depender intentional element cannot be refined or contributed. Hence, we restricted it to a task element only. The state variable ‘childsOfParentNode’ provides a set of child-intentional elements of a specific parent element. Figure 6 illustrates these mappings.

The Z-free type definition ‘RefinementType’ is applied to provide the refinement link type of the iStar. The Z-free type definition ‘ContributionType’ is applied to specify the type of the contribution link for the iStar. It is used to signify the effects of intentional elements on softgoals. To identify the type of refinement link, in Z we defined a state variable ‘elementRefinementType’, which is a partial function between sets ‘Name’ and ‘RefinementType’. Similarly, to identify the type of contribution link, in Z we defined a state variable ‘elementContributionType’, which is a partial function between sets ‘Name’ and ‘ContributionType’. Figure 7 illustrates these mappings.

A resource is an external physical object that an actor requires to carry out a certain task. In iStar the ‘neededby’ link is used to relate a task element to a resource. Using the Z-state schema, we formalize a resource in iStar. The ‘resourceNeededBy’ state variable, which is a total function between the sets ‘Name’ and ‘Command’, is defined inside the state schema to connect a task with a resource. A command is a ‘Boolean’ set. Figure 8 illustrates these mappings.

To identify each dependency relationship in the iStar model, we defined a Z-state schema called ‘iStarSD’. Inside the ‘iStarSD’ state schema, we defined a state variable ‘dependumState’, which is a total function between sets ‘Name’ and ‘State’, which identify the state of dependencies. Figure 9 illustrates the mapping of the iStar SD model.

To identify each actor in the iStar model, we defined a Z-state schema called ‘iStarSR’. Inside the ‘iStarSR’ state schema, we defined a state variable ‘actorsState’, which is a total function between sets ‘Name’ and ‘State’, which identify the state of actors. Figure 10 illustrates the mapping of the iStar SR model.

In iStar, all intentional elements within an actor’s boundary are interrelated and usually linked hierarchically. We are therefore formalizing these intentional elements as parent and child elements. The ‘ParentElement’ is a state schema composed of state variables and invariants. Figure 11 illustrates the mapping of iStar parent intentional elements. A variable ‘parentElementName?’ is an input variable of type ‘Name’, which takes an input of type ‘Name’ from an external source. The ‘childElementNames’ is a state variable of type ‘ \(\mathbb {P}\ Name\) ’, where ‘ \(\mathbb {P}\ Name\) ’ is the set of all the subsets of type ‘Name’. A state variable ‘childElementNames’ holds the names of all child elements of a parent element. The state variable ‘childElementsState’ is of type ‘ \(Name \rightarrow State\) ’, where ‘ \(Name \rightarrow State\) ’ is a total function between sets ‘Name’ and ‘State’. The state variable ‘childElementsState’ holds the fulfillment status of each child element. The ‘resource’ is a state variable of type ‘ResourceElement’, where ‘ResourceElement’ is a state schema. A state variable ‘resource’ is used to find the fulfillment condition of a resource. State variables ‘positiveEvidence’ and ‘negativeEvidence’ are of integer type \(\mathbb {Z}\) , which are used to count the number of positive and negative evidence of quality intentional elements. A variable ‘parentElementState!’ is an output variable of type ‘State’, which outputs the value of type ‘State’ that is a parent element state to an external source. Similarly, a variable ‘childElementState!’ is an output variable of type ‘State’, which outputs the value of type ‘State’ that is a child element state to an external source.

We list the state invariants for the ‘ParentElement’ state schema in the box’s second compartment. The first invariant informs us that the input variable ‘parentElementName?’ must be a member of a set ‘allElementsNames’. The second invariant informs us that the domain part of the variable ‘childElementsState’ should be a subset of a set ‘allElementsNames’. The third invariant informs us that the state variable ‘childElementNames’ must be a subset or equal to the range part of the variable ‘childsOfParentNode’. The fourth invariant outputs the value of the type ‘State’ that is a parent element state to an external source based on conditions. If the refinement type is“AND,” then the fulfillment of all child elements makes the parent element fulfilled; if the refinement type is“OR,” then the fulfillment of any child element makes the parent element fulfilled; if the parent element type is a“Task” and it needs a resource, then it makes the parent element fulfilled; if the parent element type is“Quality” and positive evidence is higher than negative evidence, then it makes the parent element fulfilled; if positive evidence is equal to the negative evidence, then it makes the parent element undetermined; otherwise, it makes the parent element not fulfilled.

In the case of a dependency relationship, the dependum is an object. Hence, we formalize it as a state schema. Figure 12 illustrates mapping of iStar dependum elements. The following ‘Dependum’ is a state schema that is composed of state variables and state invariants. A variable ‘dependumElementName?’ is an input variable of type ‘Name’ that takes an input of type ‘Name’ from an external source. Similarly, variables ‘dependerElementName?’ and ‘dependeeElementName?’ are input variables of type ‘Name’ that take an input of type ‘Name’ from an external source. A variable ‘dependumElementState!’ is an output variable of type ‘State’ that outputs the value of type ‘State’ that is a dependum element state to an external source. Boolean variables ‘constraintsOnDependerElement’ and ‘constraintsOnDependeeElement’ are used to identify where the constraints are restricted, on the depender element or the dependee element, to fulfill the dependency relationship.

We list the state invariants for the ‘Dependum’ state schema in the box’s second compartment. The first three invariants inform us that the input variables ‘dependumElementName?’, ‘dependerElementName?’, and ‘dependeeElementName?’ must be members of the domain of state variables ‘dependumType’, ‘dependerElement’, and ‘dependeeElement’, respectively. The fourth invariant outputs the value of type ‘State’ that is a dependum element state to an external source based on conditions. The vulnerability issues arise because the depender relies on the dependee to fulfill a dependum (resource, quality, goal, or task). The dependum describes the type of dependency relationship between the depender and the dependee. If the dependee fails to achieve its assigned dependum, then the depender becomes vulnerable. Hence, we put constraints in place to handle these vulnerability issues. We treat resource and goal dependencies as critical dependencies and task dependencies as committed dependencies. If we fail to achieve critical dependency, then it is the depender of all actions to achieve a goal will fail. Similarly, if we fail to achieve a committed dependency, then it is the depender of some actions to achieve a goal will fail. If the dependum type is a“Goal,” then constraints are imposed on the dependee element; if the dependum type is a“Task,” then constraints are imposed on the depender element; if the dependum type is a“Quality,” then constraints are imposed on either the depender element or the dependee element. The fulfillment of these constraints allows the fulfillment of the dependum. In the case of resource dependency, the depender element must be a“Task” that makes use of resources provided by the dependee element.

The ‘ChildElement’ schema shown in Figure 13 is an operational schema that changes the state of the ‘ParentElement’ and ‘DependumElement’ schemas. In the first compartment of this schema box, we have three identifiers. Identifiers ‘ \(\Delta ParentElement\) ’ and ‘ \(\Delta DependumElement\) ’ indicate that a schema ‘ChildElement’ is an operational schema, and it allows us to modify the state of the ‘ParentElement’ and ‘DependumElement’ schemas. An identifier ‘childElementName?’ is an input variable of type ‘Name’ that takes an input of type ‘Name’ from an external source.

In this schema box’s second compartment, we list the pre-condition and post-condition of state variables. For our convenience, we separate them with a blank line. We use pre-conditions (input assertions) to check that operations have never been used outside of their domain. We use state invariants to check the preconditions of state variables. They must be true to update state variables. The first pre-condition says that an input variable ‘childElementName?’ must belong to the subset ‘allElementsNames’ and its name is not the same as the parent element. The second pre-condition says that the parent element should not be in a fulfilled state. If these pre-conditions are true, then only the post-conditions of state variables will be updated. The first post-condition adds the child element name to the set ‘childElementNames’. The second post-condition updates the ‘resourceNeededBy’ state variable if the child element is a “Resource” and the parent element is a “Task.” The third post-condition updates the Boolean variable ‘constraintsOnDependerElement’ if the dependency relationship is a “Task” or “Quality” and the child element is a depender element. The fourth post-condition updates the Boolean variable ‘constraintsOnDependeeElement’ if the dependency relationship is a “Goal” or “Quality” and the child element is a dependee element. The fifth post-condition updates the resource dependency if the dependency relationship is a “Resource” and the child element is a dependee element. The sixth post-condition updates the integer variable ‘positiveEvidence’ if the parent element is “Quality” and the child element contribution type is “Make” or “Help.” The seventh post-condition updates the integer variable ‘negativeEvidence’ if the parent element is a “Quality” and the child element contribution type is “Break” or “Hurt.” The eighth and ninth post-conditions update the child element fulfillment status.

The ‘Actor’ schema shown in Figure 14 is a read-only schema for the state ‘ParentElement’. It reads the status of the actor’s parent element; if the parent element status is fulfilled, then it outputs the actor’s status as fulfilled; otherwise, it outputs as not fulfilled.

The ‘Dependee’ schema shown in Figure 15 is an operational schema for the state ‘iStarSD’. It updates the status of the dependency relationship. A dependee is an actor who provides the dependum. Hence, the status of the dependency relationship of an actor is updated based on the fulfillment status of the dependee.

The ‘Depender’ schema shown in Figure 16 is an operational schema for the state ‘iStarSR’. It updates the status of the actor. A depender is an actor who needs the dependum to do some tasks. Hence, the status of an actor is updated based on the fulfillment status of the depender.

Verifying the software system against the requirements model built in the early stage is essential to ensure the correctness of the software system. We can use dynamic analysis techniques like simulation and model-based testing to ensure the system’s correctness. Neither of these techniques explores all system states nor demonstrates the absence of errors. Also, the quality of test case generation affects testing success. Formal verification is checking a system against its functional and system requirements. The system and its requirements are translated into a mathematical (formal) model. Later, the verification is performed algorithmically by searching through the model for requirements violations. Model checking is a formal verification method that automates the verification process [7]. It discovers all potential states of a system graphically. Hence, it is easy to find out the absence of errors. It produces a counterexample if any requirements are violated. A counterexample is a path that leads to a state that breaches a specified requirement. The drawback of model checking is the state-space explosion dilemma: the size of the system’s state-space grows exponentially as the number of system states grows. Innovative methods like symbolic and bounded model checking avoid this dilemma [4].

We translated the iStar goal model into the Z formal model to model-check the early requirements of our case study. To check the correctness of the translated model, we used the ProZ model checker. It algorithmically checks the model for requirements violations. If a violation of requirements is found, then it produces a counterexample. In addition, we employ the ProZ model checker to verify safety properties specified in LTL formulae against our Z formal model. We input Z specifications written in a Latex file to the ProZ model checker. After inputting a Latex file, it automatically type-checks Z specifications using the Fuzz Type Checker by Mike Spivey [34]. After type-checking, we use the ProZ model checker to execute the operations thoroughly and try to discover any erroneous state in the model. For model checking, we use the default search strategy ‘Mixed DF/BF’. It combines breadth- and depth-first search techniques to find an erroneous state in the model. Figure 33 depicts the results of the model-checking process; it processed 3,677 states by covering all operations. No error states are generated. To model check, it took 200 seconds and 169 Mbytes of memory.

Many researchers have tackled the problem of transforming early-phase requirements into late-phase requirements over the last few years. This section describes and compares a handful of them that are relevant to our work.

The article by Fuxman et al. [15] describes a framework for verifying early requirements using Formal Tropos. In this article, first, they integrated the semiformal model i* into the Formal Tropos. Later, they used their framework called T-Tool to verify the early requirements. As a case study, they used a course-exam management system. Formal Tropos is a language for explicitly specifying the i* model. However, they have not provided proof to guarantee that Formal Tropo’s specifications are correct. T-Tool performs verification of Formal Tropos specifications in two phases. In the first phase, it automatically translates Formal Tropos specifications into auxiliary language specifications. It then passes the auxiliary language specifications to the NuSMV model checker for verification in the second phase. While translating Formal Tropos specifications into an intermediate language specification, they did not preserve the strategic aspects of the i* model and focused only on dynamic aspects. Also, in the case of a dependency relationship, they fulfilled the dependency relationship using assertion statements but did not show how this dependency fulfillment triggers the state changes in the depender.

The article by Vilkomir et al. [39] describes a one-to-one mapping of i* notations into the Z formal model. For each of the i* elements, they provided their corresponding general structure of the Z schema. In i*, the dependency relationship exists between the depender element and the dependee element. The depender needs a dependum (a goal, task, quality, or resource) to fulfill the need of its intentional element (depender element). Similarly, the dependee will provide a dependum by fulfilling the need of its intentional element (dependee element). They did not preserve this rule in their mapping. They have not shown how the dependee will provide the dependum by fulfilling the need of its intentional element. They only gave a general schema structure for the dependum. The dependee imposes some constraints to fulfill the need of its intentional element. On fulfillment of these constraints, the dependee will release the dependum. Hence, we mapped the dependum to the invariant constraints inside the predicate part of the dependee element schema and made the dependee element an operational schema of the depender. The fulfillment of these constraints automatically triggers state changes in the depender. According to the iStar rule, the depender element must be an unrefined intentional element, so usually, it is a task. They did not preserve this rule also in their mapping. In i*, the refinement links are used to change the state of the parent node by the child node. Hence, refinement links are guard conditions (pre-conditions) that must be true for the transition. They did not map these constraints. Finally, they unverified their translated specification.

The chapter by Lapouchnian and Lespérance [25] describes a methodology for integrating i* models into ConGolog and its extended version, Cognitive Agents Specification Language (CASL). To analyze early-phase requirements represented in the i* model, they integrated the i* model into a formal multiagent system specification language called “ConGolog”. To glue the i* model with ConGolog, they introduced an intermediate notation called “annotated SR (ASR)” diagrams. ASR diagrams include all i* elements except the softgoal and dependency relationships. Because ConGolog did not support softgoal and dependency relationships, this leads to loss of information and misuse of original aspects of the i* model. With the help of their proposed mapping rules, they translated each ASR element into the ConGolog model. The translated specifications are validated using the ConGolog simulation tool. These mapping rules are similar to those we defined for transitioning from the iStar model to the Z model. For example, the goal node they mapped to the ConGolog formula represents the desired state and procedure for achieving it. We mapped the goal to the Z-state schema. They mapped the refinement links to the guard conditions, and we did the same. For a softgoal, instead of mapping, they converted it into a goal (hard goal). We mapped the iStar softgoal to the LTL formulas and verified them during model checking. To model the goal dependency relationship, they used CASL. To glue the i* model with CASL, they devised an intermediary notation known as “intentional annotated SR (iASR) diagrams”. iASR diagrams include all i* intentional elements needed to establish goal dependency relationships. They mapped the dependum to the guard condition inside the procedural part of the dependee element, and fulfillment of these conditions automatically triggers the state changes in the depender. We did the same thing for mapping goal dependency relationships. They did not give any rules for mapping other dependencies, but we gave rules for each dependency. Finally, they verified translated specifications using the CASLve theorem prover. We verified translated specifications using the ProZ model checker.

It is easy to recognize the system’s requirements regarding its services. However, it is not easy to know how system services are provided, who provides them, and why they are provided. So, answering these questions requires analysis of early requirements and integrating them with late requirements. In this article, we illustrate the necessity of blending early-phase requirements with late-phase requirements by considering a case study of the CBTC moving block interlocking system. We used a goal-oriented modeling method called iStar to address early requirements. We translated the iStar model into the Z formal model to verify that a developed system satisfies these requirements. We also exhibited the step-by-step procedure of mapping the iStar model into the Z formal model. This integration synergistically addressed all early requirements and vulnerability issues and helped us discover variability issues. A train stops only at a conflict site in the case of the CBTC’s moving block interlocking system. It is dynamic in terms of the rear of the train ahead of it. Alternatively, it is static in the case of a point switch or buffer stop at the station. Also, a point switch is mutable, which means it is active or inactive. Active means it is a conflict point, and inactive means it is not a conflict point. Addressing this kind of variability issue is essential in the case of complex systems. Finally, we employed the ProZ model checker to verify the Z formal model of the CBTC moving block interlocking system.

The ProZ model checker is an enhanced version of the ProB model checker. It automatically type-checked Z specifications specified in the LaTeX file using the Fuzz Type Checker. After type-checking, we employed the ProZ model checker to execute the operations thoroughly and try to discover any erroneous state in the model. We used a combination of breadth- and depth-first search techniques to find an erroneous state in the model. The ProZ model checker processed 3,677 states by covering all operations. No error states were found. The safety properties were specified in the form of LTL specifications. We wrote 110 invariants and 15 LTL formulas. We specified invariants within the Z-schema in the form of a predicate formula. We verified all invariants and LTL specifications, but no properties were violated. Finally, we conclude that the iStar and Z combination is a fruitful approach for specifying and verifying early-phase and late-phase requirements regarding complex software systems. Automating one-to-one mapping rules for the iStar model to Z formal model translation, efficient handling of variability issues, and model-based testing and test case generation of a formal model requires more examination and will be one of the primary goals of our future research.