Verifying task-based speciﬁcations in conceptual graphs Jonathan Lee*, Lein F. Lai

(1)

Verifying task-based specifications in conceptual graphs

Jonathan Lee*, Lein F. Lai

Software Engineering Lab., Department of Computer Science and Information Engineering, National Central University, Chungli 32054, Taiwan, ROC Received 28 August 1995; revised 3 November 1997; accepted 13 November 1997

Abstract

A conceptual model is a model of real world concepts and application domains as perceived by users and developers. It helps developers investigate and represent the semantics of the problem domain, as well as communicate among themselves and with users. In this paper, we propose the use of task-based specifications in conceptual graphs (TBCG) to construct and verify a conceptual model. Task-based specifica- tion methodology is used to serve as the mechanism to structure the knowledge captured in the conceptual model; whereas conceptual graphs are adopted as the formalism to express task-based specifications and to provide a reasoning capability for the purpose of verification.

Verifying a conceptual model is performed on model specifications of a task through constraints satisfaction and relaxation techniques, and on process specifications of the task based on operators and rules of inference inherited in conceptual graphs.q 1998 Elsevier Science B.V.

Keywords: Verification; Conceptual model; Task-based specifications; Conceptual graphs

1. Introduction

It is widely recognized that conceptual modeling is an important step towards the construction of users’ requirements [1,19,21]. A conceptual model is a model of real world concepts and application domains as perceived by users and developers [9,23]. It helps developers investigate and represent the semantics of the problem domain, as well as communicate among themselves and with users. Further- more, conceptual models specify both the static and the dynamic properties of the problem domain in order to serve as a requirements specification for later stages of software development, that is, these models provide an important basis for the design, prototyping and implementation, and against which the design and implementation can be tested [10,16].

There are several benefits for performing the verification at the level of the conceptual model. First, it is easier for developers and users to inspect and validate problem domain knowledge at the conceptual level, since the meaning of problem domain knowledge is not obscured by issues of implementation. Second, the quality and the reliability of end products depend greatly on the accuracy of their conceptual models, as all products originate from these models [15,20]. Finally, verifying a conceptual model helps detect errors early in the software life cycle, thus

helping to eliminate design failures and reduce product cost [2,25].

As a result, several works related to the construction and verification of conceptual models have been proposed.

X Borgida argued that, in order to express the information in a conceptual model, there is a need for a language [3].

After analyzing several conceptual modeling languages, he has identified six important features that a conceptual modeling language should have: mapping entities in the world to objects, distinguishing an object from its name, performing relations on objects and not on their identifiers, expressing most relationships as properties of objects, grouping objects into classes, and organizing classes into subclass hierarchies.

X Lindland et al. proposed a framework to explore the quality of conceptual models [16]. There are three types of model quality: syntactic quality, semantic quality, and pragmatic quality. The goal for syntactic quality is syntactic correctness, which can be achieved by error prevention, error detection, and error correction. As validity and com- pleteness cannot be achieved totally, the semantic goals are decomposed into several subgoals: correct, minimal, annotated and traceable, consistency, and unambiguity.

These semantic goals are achieved by introducing statements, deleting statements, correcting statements, and detecting inconsistency. The goal for pragmatic quality is to achieve comprehension through visualization, explana- tion, simulation, and filtering.

* Corresponding author. E-mail: [email protected]

(2)

X Kung [9] advocated that a good conceptual modeling approach should (1) be a visual and formal approach which is capable of modeling both the static and dynamic aspects of the problem domain, (2) be able to describe the real world semantics incrementally, (3) have a mathematical basis, and (4) produce an executable specification.

The focus of this paper is on the use of task-based specifi- cations in conceptual graphs (TBCG) [13] to construct and verify conceptual models. To construct a conceptual model, task-based specification methodology [14,27] is used to serve as the mechanism to structure the knowledge captured in conceptual models; whereas, conceptual graphs (CGs) are adopted as the formalism to express task-based specifications and to provide a reasoning capability for the purpose of verification. In addition to the essential features identified by Borgida [3], there are several other features inherited in TBCG that are useful for improving the quality of the conceptual model:

X Conceptual graphs enhance the syntactic quality in which the selectional constraints of conceptual graphs facilitate error prevention, while canonical graphs, type definitions, and the type lattice help to accomplish both error detection and error correction.

X The semantic quality can be enhanced by TBCG as follows: first, the use of CGs together with task-based specifications in specifying software requirements helps in capturing rich semantics of the static and dynamic properties of the problem domain. Second, task state expressions (TSE) of TBCG make easy the traceability of the conceptual model. Third, TBCG provides two ways, including first- order logic and CG operators and rules of inference, to verify conceptual models. First-order logic helps to automate the consistency checking; whereas CG operators and rules of inference prompt a more powerful reasoning capability for the purpose of verification. Finally, the formal foundation of TBCG ensures the unambiguity of the conceptual model.

X TBCG enhances the pragmatic quality by providing a graph-based notation to support visualization, an explana- tion mechanism to describe task-based specifications in conceptual graphs [12], and task state expressions to achieve the simulation.

The verification of task-based specifications in conceptual graphs is performed on: (1) model specifications of a task by checking the consistency of constraints networks through the constraint satisfaction algorithm, and by repairing constraint violation using the constraint relaxation method; and (2) process specifications of a task by checking the interlevel and intralevel consistency based on operators and rules of inference inherited in conceptual graphs.

In the sequel, we first give an overview of task- based specifications in conceptual graphs, which is illustrated using the problem domain of R1/SOAR [22]. In

Section 3, the verification for both model specifications and process specifications of tasks is proposed. Finally, we summarize the potential benefits of the proposed approach and outline our future research plan.

2. Task-based specifications in conceptual graphs

Task-based specification methodology acquires and organizes domain knowledge, functional requirements, and high-level problem solving methods around the general notion of tasks. A specification can be described at various abstraction levels, and thus pieces of abstract specification can be refined into a more detailed one in a lower abstraction level. The specification 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 the system are described by two models: a model about domain objects, and a model about the problem-solving states which we refer to as a state model. The dynamic properties of the system are characterized by (1) using the notion of state transitions to explicitly describe what the functionality of a task is, and (2) specifying the sequence of subtasks and interactions between subtasks (i.e. behavior of a system) using task state expressions (TSE). A TSE uses the following operators that can be divided into three groups: (1) sequencing (follow operator and immediately follow operator), (2) branching (selection, optional operator and conditional operator), and (3) iteration (iteration operator).

Both the model and the process specifications can be first described in their high-level abstract forms, which can be further refined into more detailed specifications at the next level. The notion of task structure (i.e. task/method/subtask) [4] is adopted for the process refinement. A more detailed description of TBSM can be found in Refs. [11,14,27].

The conceptual graph [24] is a directed, finite, connected graph and consists of concepts, concept instances (referents) and conceptual relations. Concepts and relations represent declarative knowledge. Procedural knowledge can be attached through actors. Actors represent processes that can change the referents of their output concepts, based on their input concepts. Concepts are represented in square brackets, relations in parentheses, and actors in angle brackets. Delugach has extended conceptual graphs to include a new type of node, demons (in double angle brackets), to cause creation and retraction of input and output concepts [5]. A demon’s algorithm causes each of its actual output concepts with referents to be asserted (i.e.

marked), while each of its actual input concepts is to be retracted. If there is more than one input concept, no demon action occurs until all of its input concepts have been asserted. The notion of constraint overlays has also been incorporated into the conceptual graphs, which provides a method to attach constraints to objects and collec- tions of objects that make up world states [6,18]. Constraint

(3)

overlays, represented in angle brackets and linked to concepts with dash lines, can overlay actors (procedures or constraints) on a conceptual graph to describe the changes to a model state.

Conceptual graphs have several useful features that can facilitate the mapping from task-based specifications to their counterpart graphs. For example, terms and relations in the domain model of TBSM can be directly mapped to concepts and conceptual relations, and the notion of partial conceptual graphs corresponds to the notion of partial model in our methodology. An overview of the proposed approach depicting the mapping from task-based specifications to conceptual graphs is shown in Fig. 1. Details of task- based specifications in conceptual graphs can be found in Ref. [13].

The following example, which is adopted from R1/SOAR [27], illustrates various components of task-based specifications in conceptual graphs.

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 cannot 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 in conceptual graphs for the tasks and methods relevant to this example are shown in Figs. 2–4.

2.1. Domain model

Since models are similar to entity-relationship models, the transformation of terms, attributes and relations to conceptual graphs is straightforward. First, a term becomes a concept of type ENTITY. Second, an attribute associated with a term is represented by a relation (attr), and an attribute name is characterized by a concept type as a data type through a relation (chrc). Finally, a relation becomes a conceptual relation. Consider the task specification of Configure-Modules in Fig. 2, the domain model expresses two terms (i.e. Module and Backplane) with their attributes (i.e. Power, Volume, and Room) and two constraints (i.e.

T ¹ L1and T ¹ L2). The referent of each concept attaches an ‘@’ to indicate the cardinality of the concept.

2.2. State model

A conceptual graph representation for a state model should capture two main semantics in the model: the stages

Fig. 1. Expressing task-based specifications in conceptual graphs.

Fig. 2. The task Configure-Modules.

J. Lee, L.F. Lai/Information and Software Technology 39 (1998) 913–923

(4)

of completion and constraints satisfaction. Our translation rules are summarized as follows: (1) to overlay constraint actors on the conceptual graph of state objects. The constraint overlays are used to show the relationships among state objects. All state objects associated with a constraint actor are required to satisfy the relationship expressed by the actor. (2) To use demons for state transitions whose inputs and outputs are state objects as referents of the type STATE, and input tokens are of the type TASK. No demon action occurs until all input concepts are asserted and all input tokens are enabled. The performance of tasks (in the form

of input tokens) is thus essential for state transitions. For example (see Fig. 2), in the task specification of Configure- Modules, the state model expresses that the state [[Backplane]. [Module].] will be changed into another state [Moduled-Backplane] under the conditions that (1) constraints T ¹ L₁ and T ¹ L₂ are satisfied, and (2) the task Configure-Modules is performed.

2.3. Functional specifications

Preconditions, protections and rigid postconditions are

Fig. 3. A method of the task Configure-Modules.

Fig. 4. The task Configure-a-Module.

(5)

represented by propositions. A soft postcondition can be viewed as a fuzzy proposition with fuzzy concepts and fuzzy conceptual relations. Consider the task Configure- Modules in Fig. 2, the precondition of the task represented by a proposition says that a backplane and a set of unconfigured modules exists.

2.4. Behavioral specifications

TSE is an extension of regular expressions and, therefore, can be represented using state transition diagrams. To transform TSEs into conceptual graphs, we have adopted the notion of demons to represent transitions, which possesses the semantics of an actor node with respect to output concepts’ referents, with the additional semantics that a demon actually asserts its output concepts and then retracts its input concepts [5]. We also assume that there is a mapping J that maps an expression to its state where the postcondition after progressing through the expression is true. The distinction between follow and immediately follow operator is noted by using the demon for the immediately follow operator with the task before and after the operator being marked, whereas the follow operator is transformed into a demon whose inputs are not yet com- pletely marked.

In the cases of selectional, iteration, conditional and optional operators, two conventions are adopted. First, we follow the tradition of demons by using an initiator demon (i.e.hhTii) and a START concept (a subtype of STATE) for the beginning state. Second, the convention of viewing a conditional test as a task (e.g., see Ref. [26]) is also adopted, denoted as b?, where b is a condition. That is, b is a special control flow task that is invoked only when b is tested to be true, whereas¬b is another special control flow task that is invoked only when¬b is tested to be true. A final state is denoted by attaching the monadic relation (final). The difference between selectional and conditional operators is that the expression e₁will not be performed unless the conditional test for b₁? is tested to be true, neither of which are marked. The optional operator is treated as a special case of selectional operator. The iteration operator is implemented using three demons. The first demon is invoked by performing an expression e, while the second demon will be invoked by two input tokens, b? and e, to represent the notion of iteration condition. The third demon is to indicate the exit condition. The mapping of TSE operators to conceptual graphs is summarized in Table 1.

Refer to TSE of the method in Fig. 3,hhTii and [START]

indicate the initiator demon and the beginning state, respec- tively. The task T₁is performed first, and the state is then changed into [J(T₁)]. Next, there exist two possible branches: (1) when the condition [[b₁].[b₂].] is tested to be true, the task T₂will be invoked; and (2) when the condition ¬[[b1].[b₂].] is tested to be true, the final state denoted by attaching (final) will be reached. In the former case, T₁will be invoked and the state will be changed into

previous [J(T₁)] after T₂is performed, which represents the iteration operator.

2.5. Method specifications

One of the methods in TBSM is to accomplish its parent task. Generally, a method consists of a collection of subtasks, a guard condition to invoke the method, and a TSE to specify the temporal relationship among those subtasks.

3. Verification

Verifying a conceptual model helps detect errors early in the software life cycle, thus helping to eliminate design failures and reduce product cost. The verification of task-based specifications in conceptual graphs is performed on: (1) model specifications of a task by checking the consistency of constraint networks [8,17] through the constraint satisfaction algorithm [7], and by repairing constraint violation using the constraint relaxation method; and (2) process specifications of a task by checking the interlevel and intralevel consistency based on operators and rules of inference inherited in conceptual graphs [24]. The following algorithm will verify task specifications in its conceptual graphs one task at a time from the highest level task:

Algorithm 1. To verify a task specification T in its concep- tual graphs:

1. Verifying the model specification of T by:

Table 1

Mapping TSE operators to conceptual paths J. Lee, L.F. Lai/Information and Software Technology 39 (1998) 913–923

(6)

(a) Establishing a constraint hierarchy for all con- straints 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 Beta rules of inference.

(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 post- condition.

3.1. Verifying Model Specifications

A constraint hierarchy can be established based on the strength (denoted as C₀,…,C_n) associated with each constraint. The constraint hierarchy is useful for reasoning about constraints using constraint satisfaction and relaxation techniques [7]. 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 [8,17], which is useful for checking the consistency among constraints, can be established for all the constraints in a task by: (1) examining the dependency relationship between their inputs and outputs; and (2) viewing the relationships among concepts as predicates with TRUE value.

Constraints with the greatest (denoted as C₀) strength are first added to the conceptual graph. These C0 constraints cannot be violated and an initial constraint network can thus be established. If any violation occurs, their fix rules will be used to repair the situations. If all C_iconstraints are consistent, the C_iþ1(weaker than C_i) constraints would be added to the constraint network and then the consistency would be checked in turn. Weak constraints can be violated.

If any inconsistency occurs, relaxation will be applied and constraints with weakest strength will be removed. After all constraints are applied, the constraint network would be complete.

Verifying the task specification in its conceptual graphs can be formulated as a constraint satisfaction problem by first treating concepts as a set of variables, each of which must be instantiated in a particular domain and by consider- ing constraints as predicates and relations as predicates with only TRUE value.

Consider the domain model of the task Configure-a- Module, two C₀constraints are: (1) the module’s pin type is equal to the backplane’s pin type; and (2) the module’s pin type is KMC11. One of the C1 constraints is that the backplane’s pin type is RK611. The conceptual graph of the domain model of Configure-a-Module and its logical form are described below.

[Module]→(attr)→[Pin]→(attr)→[Pin ¹ Type]:

[Backplane]→(attr)→[Pin]→(attr)→[Pin ¹ Type]:

('x1)('x2)('x3)('y1)('y2)('y3)Module(x1)

∧ attr(x1,x₂)∧ Pin(x2)∧ attr(x2,x₃)

∧ Pin ¹ Type(x₃)∧ Backplane(y₁)∧ attr(y₁,y₂)

∧ Pin(y₂)∧ attr(y₂,y₃)∧ Pin ¹ Type(y₃):

The constraint hierarchy can thus be established as follows.

(1) C₀: equal-to(module’s pin type, backplane’s pin type), equal-to-KMC11(module’s pin type). (2) C₁: equal-to- RK611(backplane’s pin type).

To verify if all the constraints are consistent, we first consider those constraints with C₀strength to be added to the conceptual graphs. Dash lines denote the constraints:

The initial constraint network consists of two predicates of constraints:

('x3)('y3)equal ¹ to(x₃,y₃)and equal ¹ to ¹ KMC11(x₃):

In examining the node consistency, we check the unary predicate equal-to-KMC11(x₃). The domain of x₃ would be narrowed down and contains only KMC11. The domain is not a null set, which indicates that the node consistency is not violated. In verifying the arc consistency, we check the binary constraint equal-to(x₃,y₃). The domain that y₃would be restricted to contains only KMC11, thus the arc consis- tency is also ensured. All relations among concepts are viewed as predicates with TRUE value, therefore, we know that the path consistency is not violated. After applying the constraint propagation algorithms (including node, arc and path consistency) on the two predicates, we found that no inconsistency was occurred. That is, no relaxation is required. Subsequently, the constraint network is updated by adding the constraint equal-to-RK611 with the strength of C₁.

(7)

Therefore, its logic form is expressed as:

('x3)('y3)equal ¹ to(x3,y₃)∧ equal ¹ to ¹ KMC11(x3)

∧ equal ¹ to ¹ RK611(y3):

To examine the node consistency, we check the unary pre- dicate equal-to-KMC11(x₃) and equal-to-RK611(y₃). The domain of x₃would contain only KMC11 and the domain of y₃would contain only RK611. In verifying the arc con- sistency, we check the binary constraint equal-to(x₃,y₃).

After trying domains of x₃and y₃, none of the instantiations can satisfy the binary constraint. As a result, we have detected an arc inconsistency in the constraint network.

Therefore, we relax the constraint network by removing the weakest constraint (the C₁ constraint). The final constraint network would be consistent after checking all levels of constraints.

3.2. Verifying process specifications of a task with its parent method

Process specifications of a task, T, is consistent with its parent method if the precondition of the task can be deduced from the state description before performing the task. That is, T’s precondition must be provable from T’s before state description. Sowa’s Beta rules of inference [24], a general- ization of Peirce’s Alpha rules, provide a proper reasoning capability to prove one conceptual graph from another. The Beta rules of inference are described below.

Definition 1. Let the outermost context contain a set S of conceptual graphs. Any graph derived from S by the following first-order rules of inference is said to be provable from S.

• Erasure. In an evenly enclosed context, any graph may be erased, any coreference link from a dominating concept to an evenly enclosed concept may be erased, any referent may be erased, and any type label may be replaced with a supertype.

• Insertion. In an oddly enclosed context, any graph may be inserted, a coreference link may be drawn between any two identical concepts, and restriction may be performed on any concept.

• Iteration. A copy of any graph u may be inserted into the same context in which u occurs or into any context dominated by u. A coreference link may be drawn from any concept of u to the corresponding concept in

the copy of u. If concepts a and b in some context c are both dominated by a concept d on some line of identity, then a coreference link may be drawn from a to b.

• Deiteration. Any graph or coreference link whose occur- rence could be the result of iteration may be erased.

Duplicate conceptual relations may be erased from any graph.

• Double negation. A double negation may be drawn around or removed from any graph in any context.

• Coreference join. Two identical, coreferent concepts in the same context may be joined, and the coreference link between them may then be erased.

• Individuals. If an individual concept a dominates a generic concept b where a and b are coreferent, then referent(a) may be copied to b, and the coreference link may be erased.

Consider the example in R1/SOAR, T1’s before state description (i.e. BSD1) is the conjunction of the guard condition and the before state of its parent method (see Fig. 5). T₂s before state description (i.e. BSD₂) is the result of BSD₁progressing through the TSE of the parent method before T₂ is invoked. To verify the consistency, we need to check if the preconditions of T₁ and T₂ are provable from their BSDs. The precondition of T₁ is described below.

G₁ :[Backplane]:[Module]:[Module : {p }]

→(attr)→[Unconfigured]:

The guard condition of the parent method is ‘True’ (i.e. the universal concept [T] in conceptual graphs), and the TSE of the parent method is:

(T1, (b1∧b2)T2∨ ¬(b1∧ b2)Texit)p

From the TSE, we know that the first task invoked is T₁, therefore, the before state of the parent method is equal to T₁’s precondition (i.e. G₁). The guard condition (i.e. [T]) and the before state of the parent method (i.e. G₁) are com- bined into BSD₁(i.e. G₂).

G₂ :[Backplane]:[Module]:[Module : {p }]

→(attr)→[Unconfigured]:[T]:

To examine whether G₁is provable from G₂, we use Beta

Fig. 5. The task Configure-a-Module with its parent method.

(8)

rules of inference to check if G₁can be derived from G₂. By applying the Erasure rule to erase [T], we can deduce G₁ from G₂. Since T₁’s precondition (i.e. G₁) is provable from its before state description (i.e. G2), the task Configure-a- Module is consistent with its parent method.

Next, consider the task Obtain-the-Next-Module (T₂). In order to obtain BSD₂, we first compute BSD₁and then pro- gress BSD₁through the TSE of the parent method. Based upon the TSE, T₁must be performed before T₂is invoked.

Therefore, BSD₂ can be computed by progressing BSD₁ through the task Configure-a-Module. The postcondition of T₁is:

To progress BSD₁through the task Configure-a-Module, BSD₁(i.e. G₂) and T₁’s postcondition (i.e. G₄) are joined.

Applying Sowa’s join operator on two concepts [Back- plane] and [Module], G4is derived.

As the condition b₁∧ b2should be satisfied before T₂is invoked, BSD₂(i.e. G₆) is obtained by combining G₄and b₁

∧ b2 (see Fig. 6). The conceptual graph of b₁ ∧ b2 is described below.

The precondition of T₂is:

G₇:[Backplane]→(state)→[Moduled ¹ Backplane]:

[Module : {p }]→(attr)→[Unconfigured]:

To examine whether T2is consistent with its parent method, it is required to check if T₂’s precondition (i.e. G₇) is prov- able from BSD₂(i.e. G₆). By applying the Erasure rule to erase [Module], (compatible), and (configured-into), we can derive G₂ from G₆. Therefore, the task Obtain-the-Next- Module is consistent with its parent method.

3.3. Verifying process specifications of a task with its child method

There are three steps involved in verifying if a child method is consistent with its task T: (1) the before state description of a T’s child method must be semantically more specific than T’s precondition; (2) the protection of T is not violated by any subtasks of T; and (3) the after state description of a T’s child method must be semantic- ally more specific than T’s rigid postcondition. Based on

Sowa’s definition [24], we define the notion of specificity below.

Definition 2. A conceptual graph u is more specific than v if and only if u is canonically derivable from v, where u is called a specialization of v, denoted as u# v, and v is called a generalization of u.

Several important implications are derived from this definition: any subgraph is a generalization of the original;

replacing a type label with a supertype generalizes a graph;

and erasing an individual marker generalizes a graph. In

particular, the graph consisting of the single universal concept [T] is a generalization of every other conceptual graph.

Consider the task Configure-Modules (T) with its child

method and two subtasks T₁and T₂(see Fig. 7). BSD and ASD denote the before and after state descriptions of its child method, respectively. Based upon the TSE of its child method, BSD is the conjunction of the guard condition

and the precondition of the first task. ASD is equal to the result that BSD progresses through the child method’s TSE.

We first check if BSD is more specific than the precon- dition of T. Since the first task invoked by the TSE is T1, BSD is equal to the conjunction of T1’s precondition and the guard condition (i.e. G₈).

G₈ :[Backplane]:[Module]:[Module : {p }]

→(attr)→[Unconfigured]:[T]:

The conceptual graph of T’s precondition is:

G₉ :[Backplane]:[Module : {p }]→(attr)

→[Unconfigured]:

The projection operator p of conceptual graphs [24] is applied to check the specificity between two conceptual graphs. For any conceptual graphs u and v, where u# v, there must exist a mapping p: v→ u, where pv is a subgraph of u called a projection of v in u. That is, projections map graphs at higher levels of the generalization into graphs at lower levels. To examine the specificity between G₈and G₉,

(9)

we can project G₉ onto G₈. Since {[Backplane].

[Module:{*}]→ (attr) → [Unconfigured].} is a projection of G₉ in G₈, we can obtain G₈ # G9 (i.e. BSD is more specific than T’s precondition). Hence, we know that the precondition of the task Configure-Modules is consistent with the before state description of its child method.

To ensure that T’s protection is not violated by any sub- tasks of T, all conditions (i.e. precondition, protection, and postcondition) of T₁ and T₂ must be consistent with T’s protection. The consistency checking mechanism of conceptual graphs can be exploited to examine whether two conceptual graphs are consistent. The definition of consis- tent is described below.

Definition 3. A set S of conceptual graphs is said to be consistent if there is no pair of conceptual graphs p and¬[p]

that are both provable from S.

T’s protection and T₁’s precondition are G₁₀ and G₁₁, respectively.

G₁₀ :[Module]→(keep)→[Optimal ¹ Order]:

G₁₁ :[Backplane]:[Module]:[Module : {p }]

→(attr)→[Unconfigured]:

Since G₁₀ and G₁₁ cannot derive any pair of conceptual graphs p and ¬[p], G10 and G₁₁ are consistent. After examining all conditions of T₁and T₂, we can ensure that all the conditions are consistent with G₁₀. Therefore, T’s protection is not violated by any subtasks of T.

Finally, we check if the ASD of T’s child method is more specific than T’s postcondition. To obtain the ASD, we first compute the BSD and then progress the BSD through the TSE of its child method. From the TSE, we know that T₁ must be performed first. To progress the BSD through the task Configure-a-Module (T₁), BSD (i.e.

G₈) and T₁’s postcondition are joined. Applying the join operator on two concepts [Backplane] and [Module], G₁₂ is obtained:

Fig. 6. To derive BSD2: (a) combining G4and b1∧ b2, (b) applying the Iteration rule, (c) applying the Deiteration rule, and (d) applying the Double Negation operator.

Fig. 7. The task Configure-Modules with its child method.

(10)

Subsequently, it depends on the condition b₁ ∧ b2 to decide whether T₂ or T_exit will be performed. The post- condition of the task Obtain-the-Next-Module (T₂) is:

G₁₃:[Backplane]→(state)→[Moduled ¹ Backplane]:

[Module : {p }]→(attr)→[Unconfigured]:

Progressing G₁₂through T₂or T_exit, ASD is obtained:

The postcondition of the task Configure-Modules (T) is:

G₁₅:[Backplane]→(state)→[Moduled ¹ Backplane]:

To examine the specificity between G₁₄ and G₁₅, we can project G₁₅ onto G₁₄. Since [Backplane] → (state) → [Moduled-Backplane] is a projection of G₁₅ in G₁₄, we have G₁₄# G15 (i.e. ASD is more specific than T’s post- condition). Hence, we know that the postcondition of the task Configure-Modules is consistent with the after state description of its child method.

In this section, we have applied the proposed verification algorithm to a part of the R1/SOAR specifications. More specifically, we have demonstrated: (1) the verification on the model specification of the task Configure-a-Module through constraints satisfaction algorithm; (2) the verifica- tion on process specifications of two tasks Configure-a- Module and Obtain-the-Next-Module with their parent method based on Beta rules of inference; and (3) the verifi- cation on the process specification of the task Configure- Modules with its child method based on the projection operator inherited in conceptual graphs.

4. Conclusion

In this paper, we propose the use of task-based specifi- cations in conceptual graphs to construct and verify a con- ceptual model. Task-based specification methodology is used to serve as the mechanism to structure the knowledge captured in the conceptual model; whereas, conceptual graphs are adopted as the formalism to express task-based specifications. The verification of task-based specifications in conceptual graphs is performed on: (1) model specifications of a task by checking the consistency of constraints networks through the constraint satisfaction algorithm, and by repairing constraint violation using the constraint relaxation method; (2) process specifications of a task by checking the interlevel and intralevel consistency based on the projection operator and Beta rules of inference.

Task-based specifications in conceptual graphs offer several benefits that are useful for constructing and verifying conceptual models.

X The use of conceptual graphs together with task-based specifications in specifying software requirements helps in capturing richer semantics than that of task-based specifica- tions or conceptual graphs alone. The expressive power of

conceptual graphs facilitates the capturing of semantics that task-based specifications find difficult to express. For example, the semantics of state transitions (i.e. the notion of retraction and assertion of state objects) can be manifested through demons; whereas the semantics of constraints satisfaction (i.e. the relationships among state objects) can be represented using actor overlays.

X Requirements specifications for different views are represented in their conceptual graphical specifications, and are tightly integrated under the general notion of tasks. In addition, artifacts constructed in each model (i.e.

domain, state, functional, or behavioral) are sharable, for example, constraints in domain models can be used to describe state objects, which in turn are usually used in the description of functional specifications.

X TBCG uses first-order logic, CG operators, and rules of inference to verify conceptual models. First-order logic helps to automate the consistency checking; whereas, CG operators and rules of inference prompt a more powerful reasoning capability for the purpose of verification. For example, CG rules of inference can derive a generic graph from a restricted one, which is absent from first-order logic.

Our future research plan will consider the following tasks: (1) to extend the current framework to fuzzy logic for modeling imprecise requirements, and (2) to utilize task- based specifications in conceptual graphs as design patterns for reusing requirements specifications.

Acknowledgements

This research was sponsored by National Science Council (Taiwan, ROC) under grant NSC86-2213-E-008-006.

References

[1] R. Balzer, M. Goldman, Principles of good software specification and their implications for specification languages, in: Proceedings of IEEE Conference on Specifications of Reliable Software, 1979, pp. 58–67.

(11)

[2] B.W. Boehm, Verifying and validating software requirement and design specification, IEEE Software 1 (1) (1984) 75–88.

[3] A. Borgida, Features of languages for the development of information systems at the conceptual level, IEEE Software 2 (1) (1985) 63–72.

[4] B. Chandrasekaran, Design problem solving: A task analysis, AI Magazine 11 (4) (1990) 59–71.

[5] H.S. Delugach, Dynamic assertion and retraction of conceptual graphs, in: Proceedings of the Sixth Annual Workshop on Conceptual Graphs, 1991, pp. 15–26.

[6] D. Eshner, J. Hendler, D. Nau, Incremental planning using conceptual graphs, J. Exp. Theoretical Artificial Intelligence 4 (2) (1992) 85–92.

[7] B.N. Freeman-Benson, J. Maloney, A. Borning, An incremental constraint solver, Commun. ACM 33 (1) (1990) 54–63.

[8] V. Kumar, Algorithms for constraint-satisfaction problems: A survey, AI Magazine 13 (1) (1992) 32–44.

[9] C.H. Kung, Conceptual modeling in the context of software development, IEEE Trans. Software Eng. 15 (10) (1989) 1176–1187.

[10] D.C. Kung, An executable visual formalism for object-oriented conceptual modeling, J. Systems Software 31 (1995) 33–43.

[11] J. Lee, Task structures as a basis for modeling knowledge-based systems, Int. J. Intelligent Systems 12 (1997) 167–190.

[12] J. Lee, L.F. Lai, Y. Fei, S.J. Yang, W.T. Huang. Contextual retrieval mechanism for reusing task-based specification, in: Proceedings of the 1997 IEEE Knowledge and Data Engineering Exchange Workshop, November 1997.

[13] J. Lee, L.F. Lai, W.T. Huang, Task-based specifications through conceptual graphs, IEEE Expert 11 (4) (1996) 60–70.

[14] J. Lee, J. Yen, J. Passtor, A tool for task-based knowledge and specification acquisition, Int. J. Intelligent Systems 9 (9) (1994) 839–851.

[15] S. Lee, R.M. O’Keefe, Developing a strategy for expert system verification and validation, IEEE Trans. Systems Man Cybernetics 24 (4) (1994) 643–655.

[16] O.I. Lindland, G. Sindre, A. Solvberg, Understanding quality in conceptual modeling, IEEE Software 11 (2) (1994) 42–49.

[17] A.K. Mackworth, Consistency in networks of relations, Artificial Intelligence 8 (1977) 99–118.

[18] H.D. Pfeiffer, R.T. Hartley, The conceptual programming environ- ment, cp, in: T.E. Nagle, J.A. Nagle, L.L. Gerholz, P.W. Eklund (Eds.), Conceptual Structures: Current Research and Practice, Ellis Horwood, UK, 1992, pp. 87–107.

[19] K. Pohl, The three dimensions of requirement engineering: a framework and its application, Information Systems 19 (3) (1994) 243–258.

[20] A.D. Preece, R. Shinghal, Verifying and testing expert system conceptual models, in: Proceedings of the 1992 IEEE International Conference on Systems, Man and Cybernetics, Vol. 1, 1992, pp. 922–927.

[21] G.C. Roman, A taxonomy of current issues in requirements engineering, Computer 18 (4) (1985) 14–21.

[22] P.S. Rosenbloom, J.E. John, J. McDermott, A. Newell, E. Orciuch, R1-soar: An experiment in knowledge-intensive programming in a problem-solving architecture, IEEE Trans. Pattern Analysis Machine Intelligence (PAMI) 7 (5) (1985) 561–569.

[23] I. Shemer, Systems analysis: a systemic analysis of a conceptual model, Commun. ACM 30 (6) (1987) 506–512.

[24] J.F. Sowa, Conceptual Structures: Information Processing in Mind and Machine, Addison-Wesley, Reading, MA, 1984.

[25] D.R. Wallace, R.U. Fujii, Software verification and validation: An Overview, IEEE Software 5 (May) (1989) 10–17.

[26] D.H.D. Warren, Generating conditional plans and programs, in:

Proceedings of Summer Conference on Artificial Intelligence and Simulation of Behavior, July 1976, pp. 344–354.

[27] J. Yen, J. Lee, A task-based methodology for specifying expert systems, IEEE Expert 8 (1) (1993) 8–15.