A AHigh-LevelPetriNets-BasedApproachtoVerifyingTaskStructures

A High-Level Petri Nets-Based Approach to Verifying Task Structures

Jonathan Lee, Senior Member, IEEE, and Lein F. Lai

AbstractÐAs knowledge-based system technology gains wider acceptance, there is an increasing need for verifying knowledge- based systems to improve the reliability and quality. Traditionally, attention has been given on verifying knowledge-based systems at the knowledge level, which only addresses structural errors such as redundancy, conflict, and circularity in rule bases. No semantic error such as inconsistency in the requirements specification level has been checked. In this paper, we propose the use of task structures for modeling user requirements and domain knowledge at the requirements specification level, and the use of high-level Petri nets for expressing and verifying the task structure-based specifications. Issues in mapping task structures into high-level Petri nets are identified, for example, the representation of task decomposition, constraints, and state model; the distinction between follow and immediately follow operators; and the composition operator in task structures. The verification of task structures using high-level Petri nets is performed on model specifications of a task through constraints satisfaction and relaxation techniques and on process specifications of the task based on the reachability property and the notion of specificity.

Index TermsÐVerification, requirements specifications, task structures, high-level Petri nets, knowledge-based systems.

æ 1 I

NTRODUCTION

A

^S knowledge-based system technology gains wider acceptance, there is a growing need for verifying knowledge-based systems to improve the reliability and quality [2], [14], [26], [36]. Traditionally, attention has been concentrated on verifying knowledge-based systems at the knowledge level [4], [15], [31], [32], [44], [46]. The verifica- tion at the knowledge level addresses only structural errors containing redundancy, conflict, and circularity in rule bases. Unfortunately, most of these verification techniques are somewhat limited in verifying knowledge-based sys- tems at the requirements specification level.

There are several benefits for performing the verification of knowledge-based systems at the level of requirements specification. First, verifying requirements specification facilitates the detection of semantic errors that are not addressed by traditional verification at the knowledge level.

Second, the quality and the reliability of end products depend greatly on the accuracy of their requirements specification, as all products originate from these specifica- tions. Third, it is easier for developers and users to inspect and validate problem domain knowledge at the require- ments specification level since the meaning of problem domain knowledge is not obscured by issues of implemen- tation. Finally, verifying requirements specification of a knowledge-based system helps detect errors early in the software life cycle, thus helping to eliminate design failures

and reduce product cost. As a result, several researchers have reported progress on the verification in process specifications of knowledge-based systems [4], [11], [42], [44]. Verifying process specifications examines the dynamic behavior of a system. However, the verification of static properties, including the models of domain knowledge and problem solving states, is still overleapt in these ap- proaches. Tsai, Slagle, and their colleagues have conducted an empirical case study on requirements specification of knowledge-based systems [35], [41]. These works are important in demonstrating the feasibility of developing specifications for knowledge-based systems. Meanwhile, Chandrasekaran and several other researchers have advo- cated using task structures as a general modeling approach to knowledge-based systems [5], [37], [39]. The task structure is a tree of tasks, methods, and subtasks, which provides a framework for organizing knowledge in knowl- edge-based systems in a stepwise refinement fashion.

However, these approaches are limited in formally verify- ing the intended functionality and behavior of a knowl- edge-based system.

We have proposed a formal treatment of task structures to formally specify functional specifications and dynamic behaviors of knowledge-based systems modeled using task structures [20]. Our approach (task-based specification methodology, TBSM) acquires and organizes domain knowledge, functional requirements, and problem solving methods around the general notion of tasks. For a requirements specification driven by task structures, pieces of the specification can be refined iteratively and verifica- tion can be performed for a single layer or between layers.

As was pointed out in [7], [13], [21], our approach offers several benefits which are useful for constructing and verifying knowledge-based systems at the requirements specification level.

. J. Lee is with the Department of Computer Science and Information Engineering, National Central University, Chungli 32054, Taiwan.

E-mail: yjlee@se01.csie.ncu.edu.tw.

. L.F. Lai is with the Department of Information Management, Chienkuo Institute of Technology, Changhua 500, Taiwan.

E-mail: lflai@cc.ckit.edu.tw.

Manuscript received 1 June 1999; revised 9 Aug. 2000; accepted 30 Oct. 2000;

posted to Digital Library 10 Sept. 2001.

For information on obtaining reprints of this article, please send e-mail to:

tkde@computer.org, and reference IEEECS Log Number 109968.

1041-4347/02/$17.00 ß 2002 IEEE

. Incorporating the task structure provides a de- tailed functional decomposition technique for organizing and refining functional and behavioral specifications.

. The distinction between soft and rigid conditions lets us specify conflicting functional requirements.

. Task state expressions (TSE) help us not only document the expected control flow and module interactions, but also verify that the behavioral specification is consistent with the system's func- tional specification.

. The state model makes it easier to describe complex state conditions. Terminology defined in the state model can easily be reused for specifying the functionality of different tasks. Without using such a state model, describing the state conditions before and after a functional unit of an expert system is too cumbersome to be practical.

The focus of this paper is to propose the use of task structures for modeling knowledge-based systems at the requirements specification level, and the use of high-level Petri nets for the verification of the task-structure based specifications. High-level Petri nets is a graphical and mathematical modeling tool. Its ability to capture structural and dynamic aspects of systems makes it attractive for modeling knowledge-based systems. In our approach, high- level Petri nets is chosen for 1) its visual and formal representation in modeling task structures at the specifica- tion level, 2) its reasoning capability in simulating the dynamic behavior of task structures, and 3) its properties analysis mechanism in verifying task structures at the specification level.

The verification of task structures using high-level Petri nets is performed on:

. model specifications of a task by checking the consistency of constraints network through the constraint satisfaction algorithm, and by repairing constraint violation using the constraint relaxation method; and

. process specifications of a task by checking the interlevel and intralevel consistency based on the

reachability property of high-level Petri nets and the notion of specificity.

We choose the configuration task in R1/SOAR as an example throughout this paper to illustrate our approach for two main reasons: First, as was pointed out by [23], the research community has adopted the R1/SOAR problem as a benchmark, and the requirements illustrate problems typical of requirements for real systems. Second, the R1/

SOAR problem can help us to demonstrate several im- portant components in our approach, including the state changes through satisfying a constraints network, various information flow using TSE operators, and the verification of model specifications and process specifications.

In the sequel, we first discuss related work in the next section. The overview of task structures in TBSM is described in Section 3. In Section 4, the modeling of task structures using high-level Petri nets is fully discussed.

Verification of task structures at the requirements specifica- tion level is presented in Section 5. Finally, we summarize the proposed approach and outline the plan for our future research.

2 R

ELATED

W

ORK

To verify task structures at the requirements specification level, an appropriate modeling mechanism and an effective verification technique are required. In this section, we review and discuss two groups of related work: the modeling of task structures and the verification of knowl- edge-based systems.

2.1 Related Literature to the Modeling of Task Structures

Variations of task structures have been proposed, e.g., [5], [37], [40] (Fig. 1). Steels [37] (see Fig. 1a) has proposed work along lines that build on the notion of tasks and task structures. In his formulation, the task structure is intended to specify the task/subtask decomposition of a complex task. There is no explicit notion of alternate methods, that is, the method (M in Fig. 1a) is chosen implicitly in the analysis. The task sequencing relationship in a method cannot be specified.

Fig. 1. Variations of task structures.

In [5], Chandrasekaran et al. has described a task structure in which we can explicitly identify alternative methods for each tasks in a task structure. A method can set up subtasks, which themselves can be accomplished by various methods. Only search control knowledge can be described, for instance, the task sequencing relationship between subtasks B and C in Fig. 1b.

Hofsted and Nieuwiand [40] have presented a task structure diagram, in which tasks can be recursively defined in terms of subtasks and can be decomposed into a hierarchy of subtasks. Decisions are used if performing a task involves choices between subtasks (denoted as a circle in Fig. 1c). In task structure diagrams, sequential execution, iteration, choice, parallelism, and synchronization can be expressed. For example, task sequencing relationship among subtasks B, C, D, and E is graphically documented in the task structure diagram, namely, task B is executed first, which is followed by the task C and decision d1 in parallel fashion, and, in turn, is followed by the choice between task D or E. Similar to Steels's approach, there is no explicit notion of alternative methods. The local task sequencing is expressed using the task structure diagram.

Problems with these approaches can be summarized below:

. They cannot verify the consistency of system behaviors due to the lack of a formal foundation of task structures (and tasks).

. They lack of a mechanism that can describe incomplete system behavior and can fill in the missing detail as the information is available.

. They are unable to describe global interactions between tasks at different levels.

Meanwhile, several researchers have proposed the use of Petri nets to represent the control flow in task structures [9], [10], [18], [42]. To achieve highly parallel computation, Dennis [9], [10] develops an architecture for a data-flow processor in MAC project to allow the execution of programs represented in data-flow form. Dennis uses Petri nets to describe common control structures for the incorporation of conditional and iteration mechanisms into the data-flow language. Various operations performed in computers can thus be captured by a set of primitive modules in Petri nets.

ADEPT [18] is an integrated design environment that supports the design and analysis of digital systems from initial concept to the final implementation. A system model is constructed by interconnecting a collection of predefined elements called ADEPT modules. Each ADEPT module has a VHDL behavioral description and a corresponding mathe- matical description in the form of Jensen's colored Petri nets [17]. The control module, which is a basic ADEPT module and is adopted from Dennis's work, can also describe the information flow of a system in colored Petri nets.

In [42], task structures are applied to model and verify the process control specification of workflow management systems. The control flow in task structures is mapped onto Petri nets and verified using properties of Petri nets. They focused upon the verification of domain independent errors for satisfying four types of properties: connection, termina- tion, no dead tasks, and liveness.

The focus of these approaches is on the representation of process aspects in task structures based on Petri nets.

Process specifications describe the dynamic behavior of a system modeled using task structures. However, a task structure, in our opinion, can be composed of two kinds of specification: model specification and process specification.

A model specification captures static properties of a system, including a domain model and a state model. The domain model represents domain knowledge relevant to the task, while the state model describes problem solving states of a system. In this paper, we focus on representing and verifying task structures at the requirements specification level, including process specifications and model specifica- tions. Both aspects in task structures are captured in Petri nets for the purpose of verification.

2.2 Related Literature to the Verification of Knowledge-Based Systems

Two dimensions of verification techniques for knowledge- based systems are identified: one based on the types of knowledge that a technique focus on; the other based on the nature of the errors a technique intends to check. These dimensions will serve as a framework for us to discuss existing works in verifying knowledge bases.

2.2.1 Verifying Model vs. Verifying Behavior

A knowledge-based system consists of two types of knowledge: a model of the problem domain and a set of problem solving knowledge that determines the reasoning behavior of the system. Based on this distinction between the model and the behavior, we can classify various verification techniques for knowledge-based systems into two categories: techniques for verifying model and techni- ques for verifying behavior. The domain model is the static portion of the knowledge. For example, if an expert system is to monitor and diagnose a car engine while it is running, then the domain knowledge/model will describe what is meant by a car engine. The problem solving knowledge representation is dynamic in nature. As the example notes previously, this representation would describe what is meant by a running engine.

Verifying rule-based systems through Petri nets models has received a lot of attentions [4], [11], [31], [44]. In their approaches, the behavioral and structural properties of Petri nets are utilized to automatically verify and validate knowledge bases. However, most of these techniques concentrate on the verification of behavior rather than on that of model. That is, these approaches address only structural errors concerning redundancy, conflict, and circularity. To support the V&V of both types of knowledge, an expert system design method needs to provide a specification of the expected dynamic behavior of the knowledge bases. This issue has been addressed in several related researches, such as [22], [34], and [45].

Our previous work on task-based specifications in conceptual graphs (TBCG) [22] is used to construct and verify conceptual models. First order logic, CG's operators, and rules of inference are adopted to verify both model and behavior. First order logic helps to automate the consistency checking; whereas, CG's operators and rules of inference

prompt a more powerful reasoning capability for the purpose of verification.

Preece and Shinghal [34] argues that: 1) the performance requirements of a system need to be specified so that it can be established that the system meets its requirements, and 2) the knowledge of an expert system needs to be specified so that the internal correctness and completeness of the knowledge base can be checked.

Since the most difficult aspect of knowledge bases, the analysis of rule relationships, does not appear to be as straightforward, there is a need to provide expressions that are attached to rules in order to provide something that amounts to local metaconstraints which is local to a given rule similar to the expressions used in Flavor Analysis and is called ªRule State Expressionsº [45].

2.2.2 Universal Verification vs. Domain-Specific Verification

Most of existing works in the area of verification and validation of knowledge-based system focus on verifying whether the knowledge base contains any universally undesirable information. For example, several V&V tools could detect inconsistent rules and unreachable conditions/

goals. In [15], [32], [36], [38], relative little work has been done in verifying the knowledge base for domain-specific incorrectness.

Suwa et al. [38] describe a program for checking the rule- based of an expert system. Their program, which was used in the development of the ONCOCIN expert system, first partitions rules into disjoint sets based on the attribute that is assigned a value on the conclusion. It then makes a table, displaying all possible combinations of attributes used in the antecedents and the corresponding values that will be concluded in the conclusion of the rule. The table is checked for conflicts, redundancy, subsumption, and missing rules.

The CHECK program described by Nguyen et al. [32] is a side-product of the ªLockheed Expert Systemº shell that extends the rule-base checks used in the ONCOCIN project.

It checks for the consistency and completeness for the rule- bases by performing the following tests:

. Situations that are considered to indicate problems of consistency in goal-driven rules are:

1. Redundancy: two rules have the same antece- dent, and the conclusions of one subsume those of the other (e.g., x ! y; x ! y ^ z).

2. Conflict: two rules have the same antecedent, but their conclusions are contradictory (e.g., x ^ z ! y; x ^ :y).

3. Subsumption: two rules have similar conclu- sions, but the antecedent of one subsumes that of the other (e.g., x ^ y; x ^ z ! y).

4. Unnecessary IF rules: two rules have the same conclusions, and their antecedents contain con- tradictory clauses, but are otherwise the same (e.g., x ^ z ! y; x ^ :z ! y).

5. Circularity: a set of rules forms a cycle.

. Situations that are likely to indicate problems of completeness in goal-driven rules are:

1. Unreferenced attribute values: some values in the set of possible values for an object's attribute are not covered in the set of rules.

2. Illegal attribute values: a rule refers to an attribute value that is not on the set legal values.

3. Unreachable conclusions: the conclusion of a rule should either match a goal or an if condition in some other rule.

4. Dead-end goals and dead-end IF conditions:

either the attributes of a goal must be askable (the system can request information from the user) or the goal must match the conclusion of a rule.

A problem with all these rule-checking systems is that they incorporate rather limited, local, interpretations of completeness and consistency: Inconsistency, for example, is considered as a property of pairs of rules which is insufficient. Stachowitz et al. [36], Nazareth [30], Ginsberg [15], and Bellman [1] have pointed out that redundancy and inconsistency are properties of sets of rules.

The Expert Systems Validation Association (EVA) [36] is an extension work of CHECK which is a validation system under development at the Lockheed Artificial Intelligence Center. EVA provides a wide range of validation tools to check the correctness, consistency, and completeness of a knowledge-based system. EVA, for example, provides ªbehavior verifierº to check for the correctness which is in accordance with the verification of behavior under the universal domain. EVA also provides consistency checking by employing structure checker, logic checker, extended structure checker, extended logic checker, semantics check- er, and control checker. In order to check for the complete- ness, EVA has the omission checker and rule refiner. And recently, the EVA group came up with an extension version of EVA for nonmonotonic knowledge-based systems [6]

which applies default reasoning and least-commitment for deriving for resolution.

Nazareth [30] approaches this problem using graph- theoretical methods. Nazareth proposed that 1) transform the rule sets into directed graph: the rule set was represented as digraph, with the nodes for rules and clauses, with arcs representing the relationship between antecedent and consequent clauses and specific rules; 2) use matrix to represent graph: adjacency matrix is used to represent graph, and then is converted to trace matrix (T) by summing up the adjacency matrices raised to a relatively higher power; and 3) check errors by employing the following rules:

. Redundancy: Tvi;vj> 1.

. Conflict: Tvi;vj6ˆ 0, with vi; vjincompatible.

. Circularity: T_vi;vj6ˆ 0.

Ginsberg [15] gives an algorithm, based on ªknowledge- based reductionº (KB-reduction), for detecting these more complex inconsistency and redundancy problems in which he makes use of concepts and techniques of assumption- based truth maintenance for anomaly detection. KB-reduc- tion is based upon some recent advances in thinking about problems of truth maintenance for problem-solving systems due mainly to de Kleer [8], and is also related to the notion

of ªoperationalizationº found in the literature on explana- tion-based learning [28]. If one views an expert system as implicitly specifying a function, having all possible input sets as domain and all possible set of conclusions as range, then KB-reduction may be seen as a transformation of this implicit function to a function.

Bellman et al. describe techniques for detecting various kinds of incompleteness and inconsistency in a rule-base. In summary, Bellman's procedure for testing consistency can be described as follows:

1. For each distinct attribute value, form the disjunc- tion of the antecedents of the rules that assert that value (call this disjunction the ªcombined antece- dentº for that attribute value).

2. For each incompatible pair of attribute values, show that the conjunction of their combined antecedents is unsatisfiable.

3 T

^ASK

S

TRUCTURES IN

TBSM

We have proposed a formal treatment of task structures to formally specify functional specifications and dynamic behaviors of knowledge-based systems modeled using task structures [20]. The specification of a knowledge-based system modeled using task structures has two components:

a model specification that describes static properties of the system and a process specification that characterizes dynamic properties of the system. The static properties of a system are described by two models: a model about domain objects (domain model) and a model about the problem solving states (state model). The dynamic proper- ties of the system are characterized by 1) using the notion of state transition to explicitly describe what the functionality of a task is and 2) specifying the sequence of tasks and interactions between tasks (i.e., behaviors of a system) using task state expressions (TSE). Our approach (task-based specification methodology, TBSM) not only provides a basis for detailed functional decomposition with procedure abstraction embedded in, but also facilitates the verification of the intended functionality and behavior of a knowledge- based system.

3.1 Formal Semantics of Tasks in Task Structures To explicitly specify what a task is in a task structure, a task is treated as 1) a state-transition which can take one state to another through a sequence of intermediate states and 2) a functional unit that can be specified by using preconditions, protections, and postconditions, which are partial state descriptions about the state before, during, and after performing the task. Thus, state transition model is adopted for the purpose of formulating and analyzing the proposed specification methodology. In the general form of the model (e.g., [33]), the world is viewed as being in one of a potentially infinite number of states. The effect of a task is to cause the world to make a transition from one state to another. Therefore, each task is modeled by a set of triples

< b; ^d; a > , where b and a are states and ^d is a sequence of states, b being the ªbefore state,º ^d being the ªduring state,º and a being the ªafter state.º

Definition 1 (State Transition). A task T is defined as a set of triples < b; ^d; a > , where b and a denote the state before and after an invocation of T, and ^d denotes the sequence of states during the invocation of T.

Formulas in first-order logic are used for state descrip- tions. The precondition of a task is a condition (i.e., a formula) that needs to be true for all states before the task.

The postcondition of a task describes desirable state changes that should be achieved by the task, which can thus be classified into two categories: rigid and soft. A rigid postcondition is a condition that must always be satisfied by the states after applying the task. A soft postcondition describes properties that can be satisfied to a degree [21], [24], [25]. The protection of a task is a condition that needs to be held before, during, and after the execution of the task.

These are formally defined below:

Definition 2 (Functional Specification). Let a task T be a set of triples < b; ^d; a > .

1. A formula ' is a precondition of a task T, denoted as BT, if and only if ' is true in state b, for every triple

< b; ^d; a > 2 T.

2. A formula ' is a protection of a task T, denoted as P_T, if and only if for every triple < b; ^d; a > 2 T, ' is true in state b, ' is true in state sequence ^d, and ' is true in state a.

3. A formula ' is a rigid postcondition of a task T, denoted as RT, if and only if for every < b; ^d; a > 2 T, ' is true in state a.

4. A formula ' is a soft postcondition of a task T, denoted as ST, if and only if for every < b; ^d; a > 2 T, the degree to which ' is true in state a is a real number 2 ‰0; 1Š.

3.2 Task State Expression

Task state expression (TSE), based on regular expressions, is to describe the dynamic behavior of a system modeled using task structures. A TSE is an expression that defines 1) the desirable sequencing of tasks that are expected to have been processed before the given task, 2) the interaction of tasks at different levels, and 3) disallowed sequencing by preceding a TSE with a negation (denoted as :). We formally define TSE below.

Definition 3 (Task State Expression). The task state expression, E, over a set of tasks, T ˆ fT1; T2; . . . ; Tng, is defined as follows:

1.  is a task state expression, where  stands for null.

2. For each task T 2 T , …T† is a task state expression.

3. If Eiand Ejare task state expressions, then …Ei; Ej† is a task state expressions, where ª,º denotes immediately follow.

4. For each expression E; E is a task state expression, where  is a well-formed formula to be attached to a TSE, E, to represent the conditional branching. For a TSE, E, ª1E1_ 2E2. . . _ nEnº means ªIf 1 then E₁else if ₂then E₂ . . . else if _nthen E_nº where ª_º denotes selection, and 1; 2; . . . ; n are mutually exclusive.

5. For each expression E, ‰EŠ is a task state expression and is a short hand notation for … _ E†, where ª[ ]º denotes optional.

6. If Eiand Ejare task state expressions, then …Ei†^and …E_i; E_j†^are task state expressions, where ªº denotes iteration and ªº is an iteration condition.

7. If Ei and Ej are task state expressions, then …Ei†; …Ej† are task state expressions, where ª;º denotes follow.

Graphical notations of TSE operators in a task structure diagram are shown in Fig. 2. The relationship between subtasks B and C of method M1is a sequential relationship (that is, …B; C†). Selectional relationship is illustrated using the relationship between the subtasks of method M2, denoted by conditions 1; 2 and a ªº within a rectangle (e.g., …₁D _ ₂E†). As for iteration, there are two cases:

1) the iteration condition is associated with the whole expression (namely, ₃…F; G†), and 2) the iteration condition is associated with a subtask of its method (e.g., …F; ₄G†).

We call the relationship between task F and B a global interaction (denoted using a dotted line), because the interaction is between tasks at different levels. This kind of relationship can be expressed using a follow operator (e.g., …F; B†).

A TSE can be described at either the task level (a global TSE) or at the method level (a local TSE). In Fig. 2, E_F ˆ …F; B† and EM2ˆ …1D _ 2E† are examples of global and local TSEs, respectively. A task-level TSE associated with a task T documents global interactions between the current task and tasks at different levels. Task-level TSEs often use the follow operator to describe partial task sequences. A method-level TSE documents the local control flow among the method's subtasks but typically does not contain the follow operator.

3.3 Composition Operators

Multiple TSEs often need to be combined to obtain a global view of the system's behavior from pieces of local behavior

specifications. To achieve this, we develop a composition operator for a task T, denoted as T, for combining T's TSE, denoted as E_T, and the TSE of T's parent method, denoted as EM. The composition operator synthesizes ET with components of EM in which T is always invoked. Some general cases of the composition results are shown below. A formal treatment of the TSEs composition operator can be found in [20].

1. E TET ˆ E _ ET, if E does not contain T.

2. …; T; … ₁; ₂†† T…T; … 1; !†† ˆ …; T; … 1; 2; !††.

3. …E1_ E2† TETˆ …E1T ET† _ …E2T ET†.

3.4 Model Specification

Static properties of a system are described by a model specification which includes a domain model and a state model. The domain model describes terms, relations, and constraints relevant to the task. The state model defines a state object that describes the system's problem solving states. In task structures, a state object can describe what problem-solving stage the task is at (stage of completion), as well as dynamic relationships among multiple objects (constraints satisfaction). State objects are essential for specifying the functionality of the system's tasks. By defining these terms and refining them as needed, we can describe the specification in each level at an appropriate level of abstraction. Furthermore, reusing terms defined in the state model significantly reduces the complexity of process specification and, hence, improves its clarity. A detailed description of model specifications can be found in [23].

The following example, which is adopted from R1/

SOAR [23], illustrates various components in task-based specifications.

R1/SOAR focuses on the unibus configuration portion of R1's configuration task. Two major tasks of concern in this example are configure modules and configure a module.

The functionality of the task configure modules is to configure as many modules as possible into the current backplane while maintaining the optimal ordering in which modules are configured. This is achieved by iterating between two subtasks: 1) configure a module, which attempts to configure the current module into the current backplane, and 2) obtain the next module, which gets an ordered module that follows the current module in the optimal ordering. A correct specification should indicate that obtain the next module should be skipped under the situation that the current module fails to be configured into the current backplane, since we have not finished configuring the current module yet. It is also desirable to indicate that if the current module can not be configured into the current backplane, the system should later find a backplane suitable for the current module before configuring the next module. The specifications for the tasks and methods relevant to this example are shown in Figs. 3, 4, and 5.

3.5 Constraints Network

A state object in the state model describes the system's problem solving states. In task structures, a state is reached by performing a task through constraints satisfaction. State changes of a task can be viewed as satisfying a set of constraints, thus, the state model of a task can be specified

Fig. 2. Dynamic behaviors in a task structure.

by a constraints network. A constraints network is composed of a set of constraints which must be simulta- neously satisfied [19], [27]. In task structures, constraints can be further classified as hard and soft: the former must be satisfied, while the latter are desirable to be satisfied. A constraints hierarchy can be established based on the strength associated with each constraint [3]. The constraints network can, thus, be built level-by-level from constraints at the top level of the hierarchy down to the lower one.

Integrating the constraints hierarchy and the constraints

network is useful for reasoning about constraints through constraint satisfaction and relaxation techniques [12].

3.6 Verification of Task Structures

In TBSM, the proposed framework provides two levels of inconsistency checking in a single layer: strong and weak inconsistency. A system specification is weakly inconsistent if its consistency cannot be proven. On the other hand, a system specification is strongly inconsistent if its consis- tency can be disproven. TBSM also checks for if a

Fig. 3. The task configure-modules.

Fig. 4. A method of the task configure-modules.

Fig. 5. The task configure-a-module.

refinement is consistent by comparing the specificity of conditions at the high layer to that of the low layer. Types of faults that could result in an inconsistent process specifica- tion include protection violation, precondition violation, postcondition violation, and incorrect TSEs. Missing meth- ods will result in incompleteness in the specification.

A specification of a task or a method of a system is inconsistent if 1) the precondition of a task in the TSE of a task or a method can be deduced from the state description before performing the task, 2) the postcondition of the task can be deduced from the description of the state after performing the task, and 3) the protection of a task can be deduced from state descriptions before, after, and during performing the task.

Thus, a method specification of a task is weakly inconsistent if 1) the precondition of a task in the TSE of the method cannot always be deduced be true from the state description before the task, 2) the postcondition of the task cannot always be deduced to be true from the state description after the task, and 3) the protection of the task cannot always be deduced to be true from the state description before, after, or during the task. In contrast, a method specification of a task is strongly inconsistent if 1) the precondition of a task in the TSE of the method can sometimes be proven to be false from the state description before the task, 2) the postcondition of the task can sometimes be proven to be false from the state description after the task, and 3) the protection of the task can sometimes be proven to be false from the state description before, after, or during the task.

The consistent refinement checking is performed be- tween adjacent levels of a task and its methods. The mechanism for verifying the consistency is to check for if a refinement is consistent by comparing the specificity of conditions at the high level to that of the low one. In the meantime, the refinement of a task is complete with its specification if and only if the collection of the before states of its method specifications is equivalent to the collection of the before states of the task. For further details and proofs of the proposed verification technique, please refer to [20].

4 M

ODELING

T

ASK

S

TRUCTURES

U

SING

H

IGH

-L

EVEL

P

ETRI

N

ETS

High-level Petri nets [16], [17], [29] is a directed graph with two kinds of nodes, places and transitions, interconnected by arcs which are either from a place to a transition or from

a transition to a place. The places (drawn as circles) with their tokens reflects states of a system, while the firings of transitions (drawn as rectangles) reflects notions of state changes. Each place may contain several tokens and each of these carries a data value called token color. A token color can be of arbitrarily complex type. A transition table of the firing rule definition dictates how many and which kinds of token colors will be removed from each input place of the transition and added to each output place of the transition.

The lefthand side of a transition table specifies what would be removed from input places, while the righthand side describes what would be added to output places. A transition is said to be enabled if there are enough tokens of the correct colors in each input place of this transition. An enabled transition may or may not fire (depending on whether or not the event actually takes place). The firing of a transition will remove those enabling token colors in its input places and add correct token colors to its output places. A distribution of tokens (on the places) is called a marking. The initial marking M₀represents the initial state.

The firing of an enabled transition will change the token distribution (marking) in a net. A sequence of firings will result in a sequence of markings. A marking M_nis said to be reachable if there exists a sequence of firings that transforms M0 to Mn. A reachability graph contains all possible reachable markings.

Fig. 6 shows an example of high-level Petri nets, where 1. P1, P2, and P3are places,

2. < b; a > , < b; c > , and < a; c > are token colors in P1, 3. t1and t2are transitions,

4. the lefthand side of t10s transition table specifies what would be removed from P₁, while the right- hand side describes what would be added to P2, 5. t20s transition table specifies what would be removed

from P2and what would be added to P3, and 6. t2has a delay time associated with it.

The initial marking M₀ is ‰P₁…< b; a >; < b; c >; < a; c >†Š.

Through a consistent substitution fbjx; ajy; cjzg, the transi- tion t1 is enabled since P1 contains enough tokens of the correct colors (i.e., < b; a > and < b; c > ).

Hierarchical colored Petri nets [16], [17] provide five hierarchy constructs: substitution of transitions, substitu- tion of places, invocation of transitions, fusion of places, and fusion of transitions. Substitution of transitions allows the user to replace a transition with its surrounding arcs by a more complex colored Petri net which gives a more

Fig. 6. An Example of high-level Petri nets.

detailed description of the activity represented by the substituted transition. Analogous to the substituted transi- tion, a substituted place is a short hand for a more detailed subnet. The invocation of transitions allows circular dependencies (i.e., a substituted transition is invoked by its detailed subnet). The fusion of places allows the user to specify that a set of places are considered to be identical (i.e., they all represent a single place even though they are drawn as individual places). Similarly, the fusion of transitions allows the user to specify identical transitions.

Timed Petri nets allow time delays associated with transitions and places in their net models. Time delays specify how fast each transition can initiate firing in a periodically operated timed Petri net, where a period (a cycle time) is defined as the time to complete a firing sequence leading back to the starting marking after firing each transition at least once.

4.1 Issues in Expressing Task Structures in High-Level Petri Nets

High-level Petri nets have several useful features that can facilitate the mapping from task structures to their counter- part nets. For examples, the firing of an enabled transition can express the state transition of performing a task in task structures, and a sequence of firings of transitions corre- sponds to a task sequence in TSEs. However, several important issues remain to be addressed in using high-level Petri nets for representing task structures:

. The metalevel information, such as tasks, methods, and task decomposition, must be represented by high-level Petri nets. The notion of the meta-level information is a key element of task structures.

Without such a notion, we can not refine a complex task, let alone to completely specify task structures.

. A state model is a model about problem solving states. The state of a task can be changed through constraints satisfaction. The high-level Petri nets representation of a state model will be adopted to capture the semantics of constraints network satis- faction and relaxation.

. Methods in task structures are specified by TSEs which are essential for describing the dynamic behavior of a system. To represent TSEs using high-level Petri nets, several problems are required to be solved: the distinction between the follow and immediately follow operator, the notion of mutual exclusion in selectional and conditional operator, and the implementation of iteration operator.

. It is hard to map the TSEs composition operator to high-level Petri nets since high-level Petri nets do not provide the mechanism for combining two nets.

The implementation of the TSEs composition opera- tor in high-level Petri nets is an important issue needed to be addressed.

4.1.1 Mapping Task Decomposition to High-Level Petri Nets

In task structures, a task is treated as a state transition and characterized by precondition, protection, and postcondi- tion. To capture the notion of state transitions of tasks, a task is represented by a transition (called a task transition) in which input places and output places specify pre- and postconditions of the task, respectively. Note that the protection of a task must hold in both an input place and an output place because the protection is an invariant. A task transition (drawn ash

‰ Ši

) may be refined either by its methods to describe the behavior of its subtasks or by its state model to describe constraints satisfaction.

We adopt the substitution of transitions in hierarchical colored Petri nets [16], [17] to represent the notion of the task decomposition in task structures. The decomposition of a task transition is shown in Fig. 7. Consider the task transition t1in Fig. 7a, this transition has two input places (i.e., P1and P₂) and two output places (i.e., P₃ and P₄). The task transition t1 can be decomposed by substituting a subnet for it, in which we use the transition t2 as an input port to connect with all input places of t₁and the transition t₃as an output port to connect with all output places of t1. Input and output places with their arcs to each refinement must remain the same. The concept of balancing ensures that the substituted task transition and its subnet are consistent.

The substituted task transition can be viewed as a black box, while the subnet is a white box which describes how to accomplish its parent task.

To model the example in Fig. 2 using high-level Petri nets, we first use a task transition to represent the task A (see Fig. 8a). As task A can be refined by its method M1, the corresponding task transition will be decomposed into a subnet containing A⁰s two subtasks B and C (see Fig. 8b).

Again, the task transition C will be refined by M2 and substituted by a subnet which contains D and E (see Fig. 8c).

Finally, the task transition D will be decomposed into a subnet with F, G, and B (see Fig. 8d).

Fig. 7. The task decomposition.

4.1.2 Mapping TSEs to High-Level Petri Nets

TSE is an extension of regular expressions and, hence, can be represented using state transitions. To transform TSEs into high-level Petri nets, we treat a task sequence in TSEs as a sequence of firings of transitions in which each firing of a transition corresponds to the performing of a task. The mapping of TSEs operators to high-level Petri nets is summarized in Table 1. The distinction between the follow and immediately follow operator is noted by using a delay time associated with the task transition after the follow operator, whereas no delay time is assigned for the immediately follow operator. For a task transition which attaches a delay time, the firing of the transition will last for a period of time. In a conflict structure in Petri nets, a token can't be used to enable the other transitions as soon as one of the enabled transition begin to fire. The selectional operator is mapped to a conflict structure which captures the semantics of mutual exclusion inherited in selectional operator. In the case of conditional operator, two conditions 1and 2can be represented by different token colors. If the place P holds a token color 1, the transition table of E1will enable the task transition E1. On the other hand, if P holds 2, the transition table of E2 will enable E2. In the case of optional operator, either the task transition E or a dummy transition will be fired. The iteration operator is trans- formed into a self-loop transition which attaches a token color on its input arc to represent the iteration condition. If the place P holds a token color , the task transition E will

be fired and then adds a new token color to the place P;

whereas, if P holds :, the iteration is quit. It should be noted that the iteration won't stop until : is satisfied.

Based on the above discussion (see Table 1 for a summary), the task structure in Fig. 2 can be transformed into Fig. 8d. First, TSE of A⁰s method M₁ is …B; C†, which can be transformed into Fig. 8b based on the mapping of immediately follow operator. Second, C⁰s method M2 (that is, …1D _ 2E†) can be transformed into the subnet of the task transition C according to the conditional operator (see Fig. 8c). Finally, the composition of D⁰s method M3and F⁰s global TSE (that is, …3…F; 4G; B††^† will be transformed into the subnet of the task transition D in Fig. 8d based on iteration, conditional, and follow operator.

4.1.3 Mapping the TSEs Composition Operator to High-Level Petri Nets

Multiple TSEs often need to be combined to obtain a global view of the system's behavior from pieces of local behavior specifications. Since high-level Petri nets do not provide the mechanism for combining two nets, two TSEs cannot be composed by directly combining their high-level Petri nets.

In this paper, we compose two TSEs based on their semantics and temporal relationship. We use two of the general cases described in Section 3 to illustrate the transformation.

Case 1. E T ET ˆ E _ ET; if E does not contain T. Since the two to-be-composed high-level Petri nets do not have

Fig. 8. The task decomposition of the task structure in Fig. 2: (a) A Task Transition. (b) Decomposing A Based on M1. (c) Decomposing C Based on M2. (d) Decomposing D Based on M3.

any task transitions in common (see Fig. 9a), the two TSEs are irrelevant. Therefore, the selectional operator is used to compose the two task transitions based on the semantics of mutual exclusion (see Fig. 9b).

Case 2. …; T; … ₁; ₂†† _T…T; … ₁; !†† ˆ …; T; … ₁; ₂; !††.

The two to-be-composed high-level Petri nets (i.e., E₁and E2) are shown in Fig. 10a. There are two common task transitions T and 1 in the two TSEs. Therefore, we can create a time line (see Fig. 10b) to examine the temporal relationship between E1 and E2. Based on their temporal relationship, the composition of E1 and E2 is obtained (see Fig. 10c).

Consider the example in Fig. 2, D⁰s method M3 (i.e., …₃…F; ₄G††^) and F⁰s global TSE (i.e., …F; B†) can be composed into a complete TSE. After using a time line to examine their temporal relationship, we can obtain a complete TSE …3…F; 4G; B††^ (see Fig. 8d). However, not all TSEs in task structures are eligible for composition. The factor that affects the composability of two TSEs is the conflicting task subsequence. Two TSEs, s1and s2, are said to have a conflicting task subsequence, if 1) there exists a common task T in s₁ and s₂, 2) the predecessor (or successor) of T in s1is different from that in s2, and 3) the sequencing operator between T and the predecessor (or successor) is not the follow operator. Note that condition 3 is necessary since a sequence of unspecified tasks may be

invoked before the follow operator. Obviously, two TSEs that have a conflicting task subsequence are not compo- sable. For example, two TSEs, …; ; T; † and …; T; †, have a conflicting task subsequence since one contains that T immediately follows  and the other contains that T immediately follows . A conflicting task subsequence can be detected by using a time line to examine the temporal relationship between two TSEs.

4.1.4 Mapping Constraints Networks to High-Level Petri Nets

In task structures, a state model of a task is a model about the system's problem solving states. State changes of a task can be viewed as satisfying a set of constraints, thus, the state model of a task can be specified by a constraints network. A constraints network is composed of a set of constraints which must be simultaneously satisfied [12], [19], [27]. Conventionally, a constraints network is formu- lated to consist of a set of variables, each of which must be instantiated in a particular domain and a set of predicates that the values of the variables must simultaneously satisfy.

In our approach, a constraint is transformed into a transition with input and output places where

1. each input place represents a variable,

2. the token color in an input place represents its instantiated value,

3. the transition table of a firing rule definition represents a predicate, and

4. the adding of a token color to the output place represents the satisfaction of the predicate.

Subsequently, a constraints network can also be viewed as a constraint dictating that all specified constraints must be simultaneously satisfied. Therefore, a constraints network is represented by a transition whose input places are the output places of all constraint transitions. A state (marking) M is said to satisfy a constraints network (transition) CN if and only if M can fire CN and won't add FALSE value (denoted as a token color ªFº) into any CN⁰s output place.

That is, a constraints network is satisfied only when all its input places (i.e., the output places of previously specified constraints) hold correct token colors simultaneously.

The mapping of a constraints network into high-level Petri nets is shown in Fig. 11. A unary constraint is represented by transition t1, where the firing of t1expresses the semantics of constraint satisfaction. Only when the input place P₁ holds a correct token color, the constraint is satisfied and then adding a token color to the output place P7. Similarly, transitions t2and t3 represent a binary TABLE 1

Mapping TSEs Operators to High-Level Petri Nets

Fig. 9. TSEs composition in Case 1.

and ternary constraint, respectively. The transition t₄ expresses a constraints network with three constraints: t1, t2, and t3. If P7, P8, and P9have correct token colors (that is, three constraints simultaneously satisfy), t4will be fired and adding a token color to P10. Therefore, we can check the place P10 to examine the satisfaction of the constraints network.

Consider the example in R1/SOAR (see Figs. 3, 4, and 5), the task Configure-Modules can be transformed into Fig. 12, where

1. the task Configure-Modules is represented as a task transition t1,

2. preconditions are specified by input places P1and P3, 3. the postcondition is specified by an output place P₄,

and

4. the protection is specified by P2 which is both an input and output place of t₁.

The method of the task Configure-Modules is …T₁; …₁^ ₂† T2_ :…1^ 2†Texit†^, while the TSE of task T1(i.e., the task Configure-A-Module) is …T1; :1T3†. After composing the two TSEs on T₁, a complete TSE is obtained: ……T₁; …₁^ ₂† T2_ :…1^ 2†Texit†^; :1T3†. Therefore, the task transition Configure-Modules can be decomposed into Fig. 13 based on the complete TSE of its method. The task transition Configure-A-Module in Fig. 13 (i.e., t₅) can be further decomposed according to the constraints network in its state model (see Fig. 14). Constraints 1, 2, 3, and 4 in the state model of T1(see Fig. 5) are transformed into transitions t11, t12, t13, and t14, respectively.

5 V

ERIFICATION OF

S

PECIFICATIONS

Verifying task structures in the requirements specification level helps detect errors early in the software life cycle, thus helping to eliminate design failures and reduce product cost. The verification of task structures in high-level Petri nets is performed on 1) model specifications of a task by checking the consistency of constraint networks [19], [27]

through the constraint satisfaction algorithm [12] and by repairing constraint violation using the constraint relaxation method [3] and 2) process specifications of a task by checking the interlevel and intralevel consistency based on the reachability property of high-level Petri nets [29] and the notion of specificity [20]. The following algorithm will verify task structures in high-level Petri nets one task at a time from the highest level task until all the tasks are considered.

Fig. 10. TSEs composition in Case 2.

Fig. 11. The constraints network in high-level Petri nets.

Fig. 12. The task configure-modules in high-level Petri nets.

Fig. 13. Decomposing the task configure-modules using its method.

Algorithm 1. To verify a task specification T in its conceptual graphs:

1. Verifying the model specification of T by:

a. Establishing a constraint hierarchy for all constraints in T.

b. Building the constraint network level-by-level based on the strength of constraints.

c. Checking the consistency of constraint networks by the constraint satisfaction algorithm and repairing constraint violation by the constraint relaxation method.

2. Verifying the process specification of T by:

a. Comparing the process specification of a task T with the method that contains T (called T⁰s parent method) and other subtasks in the method to prove or disprove T's precondition using the reachability property of high-level Petri nets.

b. Comparing the process specification of a task T with those methods that accomplish T (called T⁰s child method) and their subtasks for consistency checking.

i. The before state description of a T⁰s child method must be semantically more specific than T⁰s precondition.

ii. The protection of T is not violated by any subtasks of T.

iii. The after state description of a T⁰s child method must be semantically more specific than T⁰s rigid postcondition.

5.1 Verifying Model Specifications

A constraint hierarchy can be established based on the strength (denoted as C0; ::; Cn) associated with each con- straint [3]. The constraint hierarchy is useful for reasoning about constraints using constraint satisfaction and relaxa- tion techniques [12]. A constraint network can be built level- by-level from constraints at the top level of the hierarchy down to the lower one. The constraint network [19], [27], which is useful for checking the consistency among constraints, can be established for all the constraints in a task by

1. transforming each constraint into a transition, 2. viewing the constraints network as a constraint

dictating that all specified constraints must be simultaneously satisfied, and

3. transforming the constraints network into a transi- tion whose input places are the output places of all specified constraint transitions.

Constraints with the strongest (denoted as C0) strength are first added to form an initial constraints network. If all Ci

constraints are checked to be consistent, the C_i‡1 (weaker than Ci) constraints will be added into the constraints network and then the consistency of the constraints network will be checked again. If any inconsistency occurs, relaxation will be applied and constraints with the weakest strength will be removed. In the case that there exists more than one constraint with a same strength, the relaxation method may lead to multiple solutions [3]. In our proposed

Fig. 14. Decomposing the task configure-a-module using its state model.

approach, the solution that removes the least number of unsatisfied constraints would be selected. Note that each constraint with strength C₀cannot be violated (that is, each of them cannot be removed from the constraints network), while weak constraints (i.e., strength Cn, n > 0) can be violated and removed. After all constraints are applied, the constraints network would be complete.

Verifying the state model of a task in high-level Petri nets can be formulated as a constraint satisfaction problem by treating a constraint as a transition with input and output places where

1. each input place represents a variable,

2. the token color in an input place represents its instantiated value,

3. the transition table of a firing rule definition represents a predicate, and

4. the adding of a token color to the output place represents the satisfaction of the predicate.

Therefore, a constraints network can be represented by a transition whose input places are the output places of all constraint transitions. A state (marking) M is said to satisfy a constraints network (transition) CN if and only if M can fire CN and won't add FALSE value (denoted as a token color ªFº) into any CN⁰s output place. That is, a constraints network is satisfied only when all its input places (i.e., the output places of previously specified constraints) hold correct token colors simultaneously. We can say that a constraints network CN is consistent if and only if there exists at least one reachable before state which can satisfy CN.

Consider the example in R1/SOAR (see Fig. 14), its reachability graph is shown in Fig. 15. To verify the state model of the task Configure-A-Module (t5), we check to see if at least one of t100s before states can satisfy the constraints

Fig. 15. The reachability graph of the high-level Petri nets in Fig. 14.

network t15. Examining all markings that may fire t10in the reachability graph, there are five reachable t100s before states: M3, M9, M14, M21, and M28. Each of these markings can fire t15 to reach the marking M6, M12, M17, M24, and M₃₁, respectively. Since M₆and M₁₂ contain no ªFº token color (i.e., FALSE value), the fact that M3and M9can satisfy t15 ensures that the constraint network is consistent.

Fig. 16 shows another example of constraints networks, which describes the state model of the task Choose- Meeting-Room in a meeting scheduler system [43]. Based on the strength of the four constraints, a constraint hierarchy can be established as follows:

. C0: The available date of Current Room is the same as the meeting date of Current Meeting (t19).

. C1: The number of seats offered by Current Room must be greater than or equal to the required number of seats in Current Meeting (t22).

. C2: The number of projectors offered by Current Room must be greater than or equal to the required number of projectors in Current Meeting (t20). The number of microphones offered by Current Room must be greater than or equal to the required number of microphones in Current Meeting (t21).

Assume that there are four reachable t₁₈⁰s before states:

. M14: ‰P27…< KDEX98; 11=4=98; 4; 6; 100 >†; P28…<

R101; 11=4=98; 4; 8; 80 >†Š

. M21: ‰P27…< KDEX98; 11=4=98; 4; 6; 100 >†; P28…<

R102; 11=7=98; 7; 10; 150 >†Š

. M₄₇: ‰P₂₇…< KDEX98; 11=4=98; 4; 6; 100 >†; P₂₈…<

R103; 11=4=98; 5; 4; 120 >†Š

. M62: ‰P27…< KDEX98; 11=4=98; 4; 6; 100 >†; P28…<

R104; 11=4=98; 2; 4; 100 >†Š

As each of the reachable t180s before states cannot satisfy the constraints network t23, the state model of the task Choose-Meeting-Room is inconsistent. To relax the con- straints network, some constraints with weakest strength (i.e., C2) will be removed. There may be multiple solutions that make the constraints network consistent.

We select a solution that removes the least number of unsatisfied constraints. Therefore, the C2 constraint t21

(with P45, P50 and P54) is removed. The state model of t13

after the relaxation is shown in Fig. 17. Since M47 satisfies the constraints network t23, the relaxed state model is consistent.

5.2 Verifying Process Specifications of a Task with Its Parent Method

Process specifications of a task, T, is consistent if the precondition of the task can be deduced from the state description before performing the task. That is, T's precondition must be true in the T's before state descrip- tion. A process specification is inconsistent if the precondi- tion of a task can be proven to be false from its before state description. By examining the reachability graph, each T's

Fig. 16. The state model of the task Choose-Meeting-Room.

reachable before state description can be obtained. There- fore, we can verify the consistency of a task with its parent method by checking if each T's reachable before state description contains its precondition.

In our example (see Fig. 18), T10s before state description (BSD1) is the state before T1 is invoked in its parent method. T20s before state description (BSD2) is the result that BSD1 progressed through the TSE of the parent method before T2 is invoked. To verify the consistency, we need to check to see if the precondition of T1 and T2 is true in BSD₁and BSD₂, respectively. BSD₁is the marking before transition t10 is fired in the reachability graph (see Fig. 15), while BSD2 is the marking before transition t6 is fired.

Examining each marking that may fire t10 in the reachability graph, there are five reachable BSD1s: M3,

M9, M14, M21, and M28. On the other hand, the precondition of task T1is described by the lefthand side of t50s transition table (see Fig. 13). We first check if T10s precondition is true in M3. Through a consistent substitution f12js; ajt; 9ju;

15jv; 3jw; 5jzg for the case

‰P₁⁰…<s; t; u; v>†; P6…<w; t; kmc11; z>†Š…if w  s and z  v†;

T10s precondition is true in M3since M3contains ‰P₁⁰…< 12;

a; 9; 15 >†; P6…< 3; a; kmc11; 5 >†Š. Similarly, T10s precondi- tion is true in M9, M14, M21, and M28through substitutions

f9js; ajt; 9ju; 10jv; 3jw; 5jzg;

f6js; ajt; 9ju; 5jv; 6jw; bjx; rk611jy; 10jzg;

f12js; ajt; 9ju; 15jv; 6jw; bjx; rk611jy; 10jzg; and f9js; ajt; 9ju; 10jv; 6jw; bjx; rk611jy; 10jzg;

Fig. 17. Relaxing the constraints network in Fig. 15.

Fig. 18. The task configure-a-module with its parent method.