Recently, there has been an increasing interest in improving the relia
bility and quality of Al systems. As a result, a number of approaches
to knowledge-based systems modeling have been proposed. However, these
approaches are limited in formally verifying the intended functionali
ty and behavior of a knowledge-based system. In this article, we propo
sed a formal treatment to task structures to formally specify and veri
fy knowledge-based systems modeled using these structures. The specifi
cation of a knowledge-based system modeled using task structures has t
wo 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 descri
bed by two models: a model about domain objects (domain model), and a
model about the problem-solving states (state model). The dynamic prop
erties of the system are characterized by (1) using the notion of stat
e transition to explicitly describe what the functionality of a task i
s, and (2) specifying the sequence of tasks and interactions between t
asks (i.e., behavior of a system) using task state expressions (TSE).
The task structure extended with the proposed formalism not only provi
des a basis for detailed functional decomposition with procedure abstr
action embedded in, but also facilitates the verification of the inten
ded functionality and behavior of a knowledge-based system. (C) 1997 J
ohn Wiley gr Sons, Inc.