Knowledge-Based Software Development for Real-Time Distributed Systems

The following sections are included:

• Contents

Software engineering is a discipline concerned with developing correct software products. We begin by introducing paradigms relied upon in the software engineering community to model the software development process. These paradigms describe the path from an abstract description of the problem to be solved by a software system (the specification) to its implementation (the program). In this book, we subscribe to a view of the software development process maintaining that the specification is a formal theory and that the program is obtained from this theory by applying correctness-preserving transformations.

This chapter begins with presenting demands that have been placed on languages intended to formulate requirements specifications. After describing classes of requirements specification languages, we present a formal requirements specification language, FROM, (Frame- and Rule-Oriented Requirements specification Language) developed to facilitate specification, analysis and development of software systems. The surface syntax of FRORL is based on the concepts of frames and production rules. The frames and rules of a FRORL specification may bear hierarchical relationships to each other relying on multiple inheritance. However, to provide a thorough semantic foundation, FRORL is based on a nonmonotonic variant of Horn-clause logic. The underlying logic of FRORL is proven sound and complete in Chapter 3.

Informal specification languages raise various problems, such as ambiguities, incompleteness, imprecision, and so on. Whereas some of these are alleviated by formal specification languages, formality alone helps little towards achieving correct systems. In addition, we need to provide a firm semantic foundation to allow the specification to be analyzed for various anomalies. In this chapter, we present the formal foundations of the FRORL requirements specification language; later we will show how these foundations permit verification of the requirements specification.

As it stands, FRORL does not provide sufficient mechanisms to meet the specific demands of real-time distributed software systems development. In this chapter, we augment FRORL with constructs specifically geared to the specification of real-time distributed systems. FRORL, thus enhanced, relies on the surface syntax of frames and production rules plus some additional mechanisms presented here. The semantics of FRORL is defined through nonmonotonic Horn-clause logic. Temporal properties of the specification are described by sentences that are given its meaning through temporal logic. The temporal logic will be presented in more detail in Chapter 5. Using FRORL, timing constraints, temporal properties, and other concurrent distributed features of real-time distributed systems can be specified easily.

The semantics of FRORL, as presented in Chapter 3, does not permit us to express the temporal aspects of a FRORL requirements specification. In this chapter, we present a temporal logic to both describe timing-related information and reason about it. We then show how the timing-related constructs of a FRORL specification can be translated into sentences of this temporal logic.

Standard temporal logic cannot specify absolute time, as in maximum or minimum timing constraints, but only the relative orderings between processes [186]. Message passing systems usually impose timing constraints on send/receive commands (e.g., time-out). The temporal logic presented in this chapter is specifically geared to specifying timing constraints.

Various properties of a specification, like reachability, reversibility, liveness, and consistency, etc., are of interest to the specification designer. Once a specification has been constructed using the FRORL requirements specification language, it may be subject to analysis tools which attempt to determine whether such properties hold for a given specification. In this checking process, the users, with the aid of the system, go through a sequence of iterations of specification modification and verification until the specification is assumed to be correct.

FRORL employs various strategies when analyzing requirements specifications, namely (i) resolution refutation (for reachability, reversibility, liveness, consistency, synchronic distance, and bounded fairness), (ii) model checking in temporal logic, and (iii) graph-theoretical algorithms for the determination of the consistency of timing constraints. Note that analysis is performed at the level of the underlying logic, rather than at the level of the FRORL surface syntax of frames and rules. Throughout this chapter, we assume (unless otherwise noted) we are dealing with the requirements specification as translated into a theory of the underlying logic. We speak, for example, of clauses of a specification, by which we mean "clauses of the theory obtained by translating the requirements specification into the base logic." Also, when considering requirements specifications translated into the language of the underlying logic, we are concerned with the nonmonotonically extended theory.

Knowledge-based systems model human know-how and attempt to solve problems in areas where algorithmic solutions are not readily available. Knowledge-based systems can be developed following the same techniques as when developing conventional systems. Because their execution mechanisms are based on formal foundations, various verification techniques have been proposed to aid in the development of knowledge-based systems.

In this chapter, we argue that static analysis algorithms as well as dynamic techniques proposed so far fall short of satisfying the needs of knowledge engineers. We present a novel dynamic approach, potential-conflict backtracking, to the verification of knowledge bases. Potential-conflict backtracking does not pose unreasonable and limiting assumptions on the rule base and can aid the knowledge engineer in the initial development of the rule base.

In this chapter, we discuss the step-by-step transformation of FRORL, specifications into programs written in a procedural programming language, such as Pascal or Ada. FRORL, like any other logic-based specifications relies on several features not usually present in conventional programming languages. The most apparent are computational multi-directionality, logical variables, and search for solutions through backtracking. Although these features are essential in satisfying the demands on requirements specification languages stated earlier, the amount of nondeterminism and inefficiency introduced by them dictates that they be elliminated from the derived implementation. Any implementation of a logic-based specification must eliminate the use of these features in favor of deterministic constructs of the target language.

This chapter focuses on several aspects of the derivation of target code from FRORL specifications: Data dependency and flow analysis provides the information necessary to elliminate logical variables and determine the execution sequence of the resultant program. The analysis of item sets from the specification yields the information required to elliminate unnecessary nondeterminism. Code generation itself proceeds by program transformation which is illustrated by a set of canonicalizing transformations which necessarily precede flow analysis.

The debugging process is indispensable to producing a good program. As pointed out over and over again, mistakes in the earlier phases of the software life cycle cost more to be fixed in the later phases (Boehm cites cost increases of up to 100 times for errors deriving from the requirements phase, but discovered and fixed in the maintenance phase). Validation and verification of the specification are crucial. Validating a specification by executing it (as discussed earlier) will also involve debugging, albeit at a more abstract level.

This chapter introduces techniques for debugging specifications. We have introduced extensions to algorithmic debugging that support the nondeterministic and nonmonotonic nature of FRORL specifications including inheritance. These debugging techniques will aid the users in pinpointing bugs they encountered when validating the specification.

The following sections are included:

• Appendix A Example Specifications
  • Alternate Bit Protocol
  • Subscriber-Line Controller of a Telephone Exchange

• Appendix B Formal Grammar of FRORL

• Appendix C Some Results about Fix-Points

• Appendix D References

• Appendix E Index