Student: Shen (Victor) Rong-Lin Advisor: Feipei Lai

Evaluating analytically computer systems performance is mostly cheap and quick. However, existing analytical performance evaluation techniques usually have a difficult and time-consuming modeling process because (1) analytical modeling requires strong mathematical background; (2) most modern systems are too large and complex to be modeled directly; (3) modeling for exploring various alternative designs always takes time and patience; and (4) translating models to computer programs and their debugging are non-trivial and pain-taking. Moreover, existing techniques do not support well the capability for finding the bottleneck and its cause of a target system being evaluated.

To address the above problems, in this dissertation we propose a subsystem-oriented approach to analytical performance modeling of computer systems. The whole approach is built on a subsystem-oriented performance evaluation methodology (SOPEM) and tool (SOPETOOL), which are, in turn, based on a formal subsystem-oriented performance evaluation technique (SOPET) and a subsystem specification language (SSL). The proposed approach can effectively solve the above problems for the following reasons: (1) the approach allows a system to be modeled by using SSL to specify only the performance parameters related to the system's architectural features, without caring about most mathematical details; (2) the underlying subsystem-oriented concept supports divide-and-conquer modeling by breaking a large and complex system into several small subsystems, which can be modeled easily and independently; (3) the approach supports reuse of SSL models, which reduces the modeling efforts involved in exploring various design alternatives; (4) SOPETOOL can perform automatic model translation and program execution, thus relieves most of the difficult and time-consuming tasks of conventional analytical performance modeling; and (5) the approach supports refined analysis on subsystem performance metrics and make the process of bottleneck and cause identification intuitive and straightforward.

To illustrate the functions and features of the proposed approach, we have developed the performance models for two real computer systems, namely the XMP multiprocessors system and the XDAC disk array system. First, they are broken into several small subsystems, which are modeled individually to demonstrate the divide-and-conquer feature. Then, the outstanding capability for bottleneck analysis is shown by conducting further analysis on the evaluation results and by exploring possible improvement. Particularly, the SSL models of the two example systems are presented to clearly show the features of easy modeling, isolated mathematical knowledge, and model reuse. Finally, the SSL model of XMP in fed to and processed by SOPETOOL to show the capability of automatically generating performance data from the SSL model. These examples and results lead us to believe that the proposed approach has promise to be developed as a better technique and practical tool for analytical computer performance evaluation.

As expert system technology gains wider acceptance in digital system design, the need to build and maintain a large-scale knowledge base will assume greater importance. However, how to build a correct and efficient rule base is even a hard part in the knowledge-based system development. In this dissertation, we develop FARHDL (Frame-And-Rule-based Hardware Description Language) to form a knowledge base. The FARHDL is simple but powerful to specify the hardware requirements and can be directly simulated by PROLOG. Through the knowledge base transformed from FARHDL, a formal method can be developed to design, implement, and validate the digital hardware systems. Furthermore, behavioral properties, anomaly properties, structural properties, and timing properties are applied to analyze the requirement specification. The purposes of those properties are used to detect explicit/implicit incorrect specification clauses and to capture some desired requirements, such as completeness and consistency. And the analysis results can be a useful tool for finding obscure problems in tricky digital system designs and can also aid in the development of formal specifications. Traditional approaches to knowledge-based systems (KBSs) verification have generally adopted pairwise comparison of rules, making them slow for large scale KBSs. This dissertation introduces the least fixpoint semantics of a predicate/transition (pr/t) net model into the KBS for the purposes of speeding up the computation and saving the design time of KBSs. An efficient fault diagnosis algorithm is presented to locate some fault(s) made in the KBS design. The significances of this work are that FARHDL can form a KBS easily, and the pr/t net model provides a T-invariant technique to verify the correctness of KBS requirements. Thus, the performance of a computer-aided design (CAD) tool for digital systems can be improved to some extent.

The real world is not linearly quadratic and many situations can not be modeled accurately by mathematical equations. Fuzzy information often appears in the system requirements. Fuzzy Petri nets (FPN) are Petri nets in which certain fuzzy truth-values are assigned to its transitions. In this dissertation, we show how the FPN model can be used for formal specification and verification of digital systems. The FPN which models digital systems is analyzed formally by using the fuzzy reduction rules and the consistency checking algorithm, through which we can derive a consistent FPN model. The consistent FPN model is actually a state machine, from which we can obtain a consistent marked Petri net (MPN) model. Based on the consistent MPN model, the hardware prototype at register transfer level can be easily induced by using the optimization rules. Since the derived MPN model is live and safe, certainly, some hardware problems like deadlocks and hazards can be avoided. Finally, main results are presented in the form of some theorems or propositions, and are supported by a set of experiments.