As an input for KnowledgeWare there is the output tape produced by Symbolic Absract Machine,  SAM. For the user it is possible to specify and check whether the selected features of the outputs are as assumed by using hypotheses and theorems.

Because of the computational power, the computer should be used systematically as far as possible in order to make the maintenance systematic and reliable. In addition to improved performance, computer support can improve the communication between persons, because every member of a team can see exactly the same models, sequences, and subsequently discuss the problems and assumptions for solving very complex problems, which almost without an exception require laborious operations in skill, rule, knowledge, and meta levels. FIGURE shows the overall principle for the methodology.

The task is transformed into problem recognition, which gives the focused elements in the model, and into problem formulation that gives a logical notation, which describes the sequences and triples that are critical and need to be checked. Checking is done by using the atomistic model as queries that activate simulating runs. For these runs, the user does model checking either manually or by using the theorem prover that gives a proof.  The actions concerning the model are directed at levels specified by Rasmussen (1983), and the information is classified according to the principles of the information ladder.


With the help of the actions of the information ladder at the different levels the user can communicate with the computer in both directions.